[Haskell-beginners] Are functors in Haskell always injective?

[Brent Yorgey]

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 <byorgey at seas.upenn.edu>
> 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