fundeps help

[Jan-Willem Maessen]

On Dec 3, 2007, at 4:02 AM, Simon Peyton-Jones wrote:

> GHC's new intermediate language, System FC, is specifically designed  
> to do this.  Currently we're in transition: equality constraints are  
> starting to work, but fundeps are implemented as they always were.   
> I hope we can eventually switch over to implementing fundeps using  
> equality constraints, and then the above program will work.
>
> Meanwhile, in the HEAD you can write
>        conv :: (a~b) => a -> b
>        conv = id
>
> Which, IHMO, is a much clearer way to say it!

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!

Hoping this will give me a bit of insight into SystemFC,

-Jan-Willem Maessen

> You may also like to try the paper that Martin and I and others  
> wrote about fundeps:
>        http://research.microsoft.com/%7Esimonpj/papers/fd-chr
>
> Simon
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users