GADTs and functional dependencies
simonpj at microsoft.com
Fri Sep 26 12:08:24 EDT 2008
By "global" I really meant "throughout the scope of the type variable concerned.
Nevertheless, the program you give is rejected, even though the scope is global:
class FD a b | a -> b
f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
f x y = y
Both GHC and Hugs erroneously reject the program, just as they do this one
instance FD Int Bool
g :: FD Int b => ...
The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job. That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to.
| -----Original Message-----
| From: Claus Reinke [mailto:claus.reinke at talk21.com]
| Sent: 24 September 2008 19:27
| To: Simon Peyton-Jones; glasgow-haskell-users at haskell.org
| Subject: Re: GADTs and functional dependencies
| >> This has never worked with fundeps, because it involves a *local* type
| equality (one that holds
| >> in some places and not others) and my implementation of fundeps is
| fundamentally based on
| >> *global* equality. Prior to GADTs that was fine!
| Actually, how does that relate to reasoning under assumptions?
| class FD a b | a -> b
| f :: (FD t1 t2, FD t1 t3) => ..
| f = ..
| There is no instance of 'FD', so no equalities can be derived from there
| outside of 'f', and no equalities should be derived globally from instances
| that are only local hypotheses in 'f' . But inside 'f', we assume that those
| two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of
| the implication.
| Isn't that decidedly local?
More information about the Glasgow-haskell-users