[Haskell-cafe] Equality constraints in type families
claus.reinke at talk21.com
Mon Mar 24 07:55:30 EDT 2008
>>>>> type family F a :: * -> *
>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>> 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.
sorry, i don't understand how that could be meant by 'F x ~ F u';
that equality doesn't even refer to any specific point on which these
two need to be equal, so it can only be a point-free higher-order
equality, can't it?
the right-to-left implication is obvious, but the left-to-right
implication seems to say that, for 'F x' and 'F u' to be equal on
any concrete pair of types 'y' and 'u', they have to be equal on
all possible types and 'y' and 'u' themselves have to be equal.
again, i gave a concrete example of how ghc behaves as i
would expect, not as that decomposition rule would suggest.
i'll try to re-read the other paper you suggested, but it would
help me if you could discuss the two concrete examples i
gave in this thread.
More information about the Haskell-Cafe