Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Are functors in Haskell always injective? (Brent Yorgey)
----------------------------------------------------------------------
Message: 1
Date: Sun, 6 Jul 2014 14:10:14 -0400
From: Brent Yorgey <[email protected]>
To: [email protected]
Subject: Re: [Haskell-beginners] Are functors in Haskell always
injective?
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
On Sun, Jul 06, 2014 at 06:38:57AM +0700, Kim-Ee Yeoh wrote:
> On Sun, Jul 6, 2014 at 12:27 AM, Brent Yorgey <[email protected]>
> wrote:
>
> > On Sat, Jul 05, 2014 at 02:51:07AM -0300, Dimitri DeFigueiredo wrote:
> > >
> > > However, I don't think there is any way this mapping of types cannot
> > > be injective in Haskell. It seems that a type constructor, when
> > > called with two distinct type will always yield another two
> > > *distinct* types. (E.g. Int and Double yield Maybe Int and Maybe
> > > Double) So, it seems that Functors in Haskell are actually more
> > > restrictive than functors can be in general. Is this observation
> > > correct or did I misunderstand something?
> >
> > Yes, that's correct.
>
>
> Why is that correct? How would you show that?
The fact that type constructors are injective is encoded directly into
the equality rules for the type system. In the original paper on
System FC, the formal system underlying GHC's core language,
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-tldi.pdf
this is the rule labeled "Right" in Figure 2 on page 5. It says that
if we have a proof that s1 s2 ~ t1 t2, then it is also the case that
s2 ~ t2. (In fact, it is also the case that s1 ~ t1---this is the
"Left" rule and could be referred to as "generativity" of type
constructors; different type constructors always construct distinct
types.) Things have changed a bit since that paper (in fact, I don't
recommend reading it), but there is still a similar "right" rule used
in GHC's constraint solver.
-Brent
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 73, Issue 5
****************************************
