Injective type families?

[Simon Peyton-Jones]

shouldn't the check go the other way?  (i.e., if the RHSs unify, then the LHS must be the same).  Here is an example:

-- This function is not injective.
type instance F a = Int
type instance F b = Int

Yes, you’re right.

Still, Conal's example would not work if we just added support for injective type functions because + is not injective (e.g., 2 + 3 = 1 + 4).  Instead, what we'd need to say is that it is injective in each argument separately, which would basically amount to adding functional dependencies to type functions.  Perhaps something like this:

type family (a :+: b) ~ c | c b -> a, c a -> b

Interesting!  Injectivity is more complicated than one might think!

Simon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110215/4f8d8698/attachment.htm>