On Tue, Sep 04, 2007 at 06:20:26PM +0200, Wolfgang Jeltsch wrote:
Hello,
I came across the following problem:
I define a class with a functional dependency like so:
class C a b | a -> b
Then I want to define a datatype using the fact that the second argument of C is dependent on the first:
data C a b => T a = MkT a b
But unfortunately, this doesn’t work, at least not in GHC.
I can try this:
data T a = forall b. C a b => MkT a b
But if I do pattern matching on a value of T a, GHC doesn’t recognize that the type of MkT’s second argument is determined by the type of the first. For example, the following function definition is not accepted:
useB :: C a b => T a -> (b -> ()) -> () useB (MkT a b) f = f b
In my opinion, the problem is that GHC doesn’t see that because of the functional dependency the type exists b. C a b => b is at least as general as the type forall b. C a b => b. Is there a solution to this problem?
And so yet another person discovers why functional dependancies are Bad(tm) - the semantics generated by their typing derivations do not correspond to the naïve model. In particular, functional dependencies serve *only* to avoid ambiguity; they cannot be used to satisfy equality constraints. Type synonym families, the proposed alternative to functional dependencies, can handle this well: {-# LANGUAGE TypeFamilies #-} class C a where type B a :: * data C a => T a = MkT a (B a) useB :: C a => T a -> (B a -> ()) -> () useB (MkT a b) f = f b It should be emphasized that this program worked the very first time I typed it in. No back-and-forth arguing with the checker! Stefan