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