functional dependencies not satisfactory?
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? Best wishes, Wolfgang
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
Am Dienstag, 4. September 2007 22:00 schrieben Sie:
[…]
It should be emphasized that this program worked the very first time I typed it in.
Which version of GHC are you using? I’m a bit confused since the latest successful nightly build for i386-unknown-linux seems to be from August 20. Are type families already implemented in this version? Was there any change in type family support since then? Best wishes, Wolfgang
On Tue, Sep 04, 2007 at 11:11:00PM +0200, Wolfgang Jeltsch wrote:
Am Dienstag, 4. September 2007 22:00 schrieben Sie:
[…]
It should be emphasized that this program worked the very first time I typed it in.
Which version of GHC are you using? I’m a bit confused since the latest successful nightly build for i386-unknown-linux seems to be from August 20. Are type families already implemented in this version? Was there any change in type family support since then?
Type synonym families were only merged on the 28th IIRC. stefan@stefans:~$ ghci -V The Glorious Glasgow Haskell Compilation System, version 6.7.20070829 Stefan
Wolfgang Jeltsch wrote,
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?
You may want to have a look at Section 2.3 of "System F with Type Equality Coercions" <http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html>, which explains why GHC rejects the program. The mentioned paper also outlines an alternative translation of FDs using System FC that does not suffer from this problem. Unfortunately, it is not quite clear how to extend type checking for FDs in such a way that the required System FC coercion-evidence types are produced by the type checker. This is one of the reasons why I believe that we should use the type families mentioned by Stefan instead of functional dependencies. Type checker support for type synonym families (the flavour needed for your example) has been merged into GHC's development version a week ago. For more details, see http://haskell.org/haskellwiki/GHC/Type_families Manuel
participants (3)
-
Manuel M T Chakravarty -
Stefan O'Rear -
Wolfgang Jeltsch