Functional dependencies interfere with generalization

[Brandon Michael Moore]

On Wed, 26 Nov 2003, Ken Shan wrote:

> Hello,
>
> Consider the following code, which uses type classes with functional
> dependencies:
>
>     {-# OPTIONS -fglasgow-exts #-}
>     module Foo where
>     class R a b | a -> b where r :: a -> b
>
>     -- 1
>     rr :: (R a b1, R a b2) => a -> (b1, b2)
>     rr a = (r a, r a)
>
>     -- 2
>     data RAB a = RAB (forall b. (R a b) => (a, b))
>     mkRAB :: (R a b) => a -> b -> RAB a
>     mkRAB a b = RAB (a, b)
>
> Neither 1 nor 2 passes the type-checker (GHC 6.0.1).  The error messages
> are similar:

I agree that the typechecker could handle this better, but I don't see why
you should need types like this. You should be able to use

rr :: (R a b) =>  a -> (b,b)

and

data RAB a = forall b. (R a b) => RAB (a,b)

equally well, and these typecheck.

I think the root of the problem is the foralls. The typechecker doesn't
realize that there is only one possible choice for thse universally
quantified values based on the functional dependencies. For rr it
complains because you can't allow every b2, just b2 = b1, not realizing
that that is already implied by the class constraints. Similarly for RAB
it complains because the pair you give it is obviously not unviersally
polymorphic in b, not realizing that there is only one choice for b
consistent with the class constraints. Compare this code:

class R a b where r :: a -> b

rr :: (R a b1, R a b2) => a -> (b1, b2)
rr x = let rx = r x in (rx, rx)

and

data P a = P (forall b. (a,b))

Off the top of a my head, the solution to this problem would probably be
something like ignoring foralls on a type variable that is determined by
fundeps, but I think the type system would need some sort of new
quantifier or binding construct to introduce a new type variable that is
completely determined by its class constraints. Something like forall a .
constrained b. (R a b) => a -> (b, b). A forall binding a variable
determined by fundeps could be reduced to a constrained binding, which
would be allowed to do things like unify with other type variables.

I'm not sure anything really needs to be done. I think you can always
type these examples by unifying the reduntant type variables in a
signature by hand, and by using existentially quantified data types
rather than universally quantified ones. Do you have examples that
can't be fixed like this?

Brandon


>
>     Inferred type is less polymorphic than expected
>         Quantified type variable `b2' is unified with another quantified type variable `b1'
>     When trying to generalise the type inferred for `rr'
>         Signature type:     forall a b1 b2.
>                             (R a b1, R a b2) =>
>                             a -> (b1, b2)
>         Type to generalise: a -> (b1, b1)
>     When checking the type signature for `rr'
>     When generalising the type(s) for `rr'
>
>     Inferred type is less polymorphic than expected
>         Quantified type variable `b' escapes
>         It is mentioned in the environment:
>           b :: b (bound at Foo.hs:17)
>     In the first argument of `RAB', namely `(a, b)'
>     In the definition of `mkRAB': mkRAB a b = RAB (a, b)
>
> In both cases, the compiler is failing to make use of functional
> dependencies information that it has at its disposal.  Specifically,
> it seems to me that, if two type variables b1 and b2 have been unified
> due to functional dependencies, making two constraints in the context
> identical, then the inner constraint ("inner" with respect to the scope
> of quantified type variables) should be ignored.
>
> Is there a technical reason why the type checker should reject the code
> above?  Would it be possible to at least automatically define a function
> like
>
>     equal :: forall f a b1 b1. (R a b1, R a b2) => f b1 -> f b2
>
> for every functional dependency, with which I would be able to persuade
> the type checker to generalize (Baars and Swierstra, ICFP 2002)?  I
> suppose I can use unsafeCoerce to manually define such a function... is
> that a bad idea for some reason I don't see?
>
> Thank you,
> 	Ken
>
> --
> Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
> Tax the rich!
> new journal Physical Biology: http://physbio.iop.org/
> What if All Chemists Went on Strike? (science fiction):
> http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html
>