On 2003-11-27T07:51:37-0800, Brandon Michael Moore wrote:

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'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?

Thanks for indicating that I am not out of my mind! Unfortunately, when I try to use an existential type for RAB as you do above, I run into problems later when unpacking the value. Essentially, I need the type system to be smart at either universal introduction or existential elimination. For example, I can't write: useRAB :: (Eq b, R a b) => RAB a -> b -> Bool useRAB (RAB (a, b1)) b2 = b1 == b2 The compiler makes two complaints: Could not deduce (Eq b) from the context (R a b) arising from use of `==' Probable fix: Add (Eq b) to the existential context of a data constructor In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2 Inferred type is less polymorphic than expected Quantified type variable `b' escapes When checking an existential match that binds b1 :: b and whose type is RAB a -> b1 -> Bool In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2 The first complaint is that it doesn't know that the "b" from within the RAB is an instance of "Eq". The second complaint is that it doesn't know that the "b" from within the RAB is the same as the one from outside. The first complaint seems to be due to failing to infer "Eq b1" from Eq b, R a b, R a b1. This seems to me like a matter of simply unifying b with b1, but perhaps I am missing something. As for the second complaint:

I think the root of the problem is the foralls. [...]

Right...

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.

Looking at section 6.4 ("generalizing inferred types") of Mark Jones's ESOP 2000 paper (http://www.cse.ogi.edu/~mpj/pubs/fundeps.html), I have another possible solution that doesn't involve a new kind of quantifier or binding construct. Jones says that In a standard Hindley-Milner type system, principal types are computed using a process of generalization. Given an inferred but unquantified type P=>t, we would normally just calculate the set of type variables T = TV(P=>t), over which we might want to quantify, and the set of variables V = TV(A) that are fixed in the current assumptions A, and then quantify over any variables in the difference, T\V. In the presence of functional dependencies, however, we must be a little more careful: a variable a that appears in T but not in V may still need to be treated as a fixed variable if it is determined by V. To account for this, we should only quantify over the variables in T\V+. (Here V+ is the set of all type variables uniquely determined by the type variables in V via functional dependencies.) Contrary to this paragraph, I think we can actually be -less- careful in the presence of functional dependencies: we can quantify over any variable v in T, even if v also appears in V, as long as v is determined by V\{v} via functional dependencies, by renaming v to some fresh v'. Unfortunately, this procedure must be guided by type annotations if it is to work deterministically (i.e., giving rise to principal types). For example: class Q a c | a -> c class R b c | b -> c data QAC a = QAC (forall c. (Q a c) => (a, c)) data RBC b = RBC (forall c. (R b c) => (b, c)) mk2 :: (Q a c, R b c) => a -> b -> c -> (QAC a, RBC b) mk2 a b c = (QAC (a, c), RBC (b, c)) -- or equivalently -- mk2 a b c = let c' = c in (QAC (a, c'), RBC (b, c')) Here the type of c aka c' needs to be generalized to forall c'. (Q a c') => c' on one hand, and forall c'. (R b c') => c' on the other. Both type-schemes are valid semantically, but they are not comparable -- neither subsumes the other. I would be quite content with a type-checker that uses local type inference (in this case, the definition of QAC and RBC) to decide how to generalize. I've also just discovered "Simplifying and Improving Qualified Types" (http://www.cse.ogi.edu/~mpj/pubs/improve.html). Maybe the details in it would help... Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig 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