Jan-Willem Maessen:
Is it really a good idea to permit a type signature to include
equality constraints among unifiable types? Does the above type
signature mean something different from a ->a? Does the type
signature:
foo :: (a~Bar b) => a -> Bar b
mean something different from:
foo :: Bar b -> Bar b
? I know that System FC is designed to let us write stuff like:
foo :: (Bar a ~ Baz b) => Bar a -> Baz b
Which is of course what we need for relating type functions. But
I'm wondering if there's a subtlety of using an equality constraint
vs just substitution that I've missed---and if not why there are so
many ways of writing the same type, many of them arguably unreadable!
Simon answered most of your question, but let me make a remark
regarding "why there are so many ways of writing the same type, many
of them arguably unreadable!" Equalities of the form "a ~ someType"
are essentially a form of let-bindings for types - you can give a type
a name and then use the name in place of the type. Just like with
value-level let bindings, you can abuse the notation and write
unreadable terms. However, this is no reason to remove let-bindings
from the value level, so why should it be different at the type level?
Manuel
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
