Injective type families?

Simon Peyton-Jones simonpj at
Tue Feb 15 11:15:20 CET 2011

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!

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list