Injective type families?
simonpj at microsoft.com
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...
More information about the Glasgow-haskell-users