[Haskell] functional dependencies not satisfactory?
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Sep 4 22:03:19 EDT 2007
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
More information about the Haskell
mailing list