GADTs and functional dependencies
claus.reinke at talk21.com
Fri Sep 26 12:58:33 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,
while both GHC and Hugs accept this variation:
class FD a b | a -> b
f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
f x y = undefined
and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'.
So they use the FD globally (when checking use of 'f'), but not locally
(when checking the definition of 'f'). Is that interpretation correct, or is
there another bug involved?
> The problem is that the implementation technique for FDs used by GHC and Hugs (global unification)
> isn't up to the job.
Interesting. When the FD-via-CHR discussion started, I toyed with the
idea of writing an instance inference engine based on CHR (since CHR
happen to be a variant of CPN - Coloured Petri Nets -, I happened to
have an implementation at hand;-). But once I noticed the difficulties of
managing local constraint stores (and exchanging some, but not all inferred
information with the global constraint store), I abandoned the idea.
Ever since then I've been wondering how GHC handles that!-)
>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.
Since FDs constrain the set of valid instances, I had been wondering
whether one could apply the FD-based refinements/substitutions to the
code obtained (just as they are applied to the class constraints) while
keeping a typed intermediate language.
More information about the Glasgow-haskell-users