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

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 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.p... 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