[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Mon Mar 24 00:18:25 EDT 2008
Claus Reinke:
>>>> type family F a :: * -> *
>> ..
>>> We made the design choice that type functions with a higher-kinded
>>> result type must be injective with respect to the additional
>>> paramters. I.e. in your case:
>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>
> actually, i don't even understand the first part of that:-(
>
> why would F x and F u have to be the same functions?
> shouldn't it be sufficient for them to have the same result,
> when applied to y and v, respectively?
Oh, yes, that is sufficient and exactly what is meant by F x ~ F u.
It means, the two can be unified modulo any type instances and local
given equalities.
Manuel
More information about the Haskell-Cafe
mailing list