[Haskell] functional dependencies not satisfactory?

[Stefan O'Rear]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell/attachments/20070904/a85a7b2e/attachment.bin