| Now I have a practical example where fundeps don't work and keys | would work - but the type variable is later instantiated. | ... | Each record field in my proposal induces a class: | class Has_field r a | r -> a where | get_field :: r -> a | | The fundep, or something which allows to find the instance from the | type of the record only, is required to make this practical. A type | which includes Has_field r a in its context, and includes r but not a | in its body, is legal. | | For non-polymorphic fields it works great. But parens cause trouble: | instance Has_parens TokenParser (Parser a -> Parser a) | This instance is illegal because of the fundep. What it should mean is: | instance Has_parens TokenParser (forall a. Parser a -> Parser a) | but this is not possible either. Let's explore the design space a little more carefully. There's a wide spectrum of options, and it's not yet entirely clear which one Marcin is referring to by "keys". Perhaps it will be one of the entries on the following list: 0) "Standard multiple parameter classes": A class constraint Has_parens r a does not imply any connection between the different parameters, and a type like Has_parens r a => r is ambiguous. This kind of class has its uses, but also tends to lead to ambiguity problems. It doesn't address Marcin's needs. 1) "A weaker notion of ambiguity" (title of Section 5.8.3 in my dissertation, which is where I think the following idea originated): We can modify the definition of ambiguity for certain kinds of class constraint by considering (for example) only certain subsets of parameters. In this setting, a type P => t is ambiguous if and only if there is a variable in AV(P) that is not in t. The AV function returns the set of potentially ambiguous variables in the predicates P. It is defined so that AV(Eq t) = TV(t), but also can accommodate things like AV(Has_field r a) = TV(r). A semantic justification for the definition of AV(...) is needed in cases where only some parameters are used; this is straightforward in the case of Has_field-like classes. Note that, in this setting, the only thing that changes is the definition of an ambiguous type. A similar weakening of the notion of ambiguity is permitted by each of the following points in the design space. 2) "Partial dependencies": At this point in the spectrum, we allow the values of one or more class parameters to specify something about the shape of the values of the other parameters, without uniquely determining them. This is perhaps closest to what Marcin is asking for in the text included above. For his example, a partial dependency might ensure that the type t in any constraint of the form Has_parens TokenParser t is of the form Parser a -> Parser a for *some* a, which may be chosen in different ways at each use. My old work on improvement provides a theoretical foundation for this. And, in fact, an unimplemented proposal for supporting this kind of extension is included in the source code for Hugs (subst.c), predating functional dependencies by several years. With the syntax used there, the improvement would be specified as follows: instance Has_parens TokenParser (Parser a -> Parser a) improves Has_parens TokenParser b where ... The idea here is to use improvement at the level of individual instances, whereas functional dependencies use improvement at the level of whole classes. Given a declaration instance P => p where ... we expect the instance to be used for any constraint that matches p. If an improves clause is specified, possibly with multiple predicates, as in: instance P => p improves p1, ..., pn where ... then we expect p to be a substitution instance of each of p1, ..., pn, and we expect the instance to apply to any constraint that matches one (or more) of p1, ..., pn, with an appropriate improving substitution applied to bring it into line with p. 3) "Underspecified/Inferred Functional Dependencies": Here, we insist that the values of certain parameters in a constraint are *uniquely* determined by the values of other parameters ... but we allow the values of the determined types to be inferred rather than declared explicitly. For example, one might write: instance C Int b where ... and then leave type inference to figure out that the value for b in this particular instance must actually be Bool (say). I don't know whether anyone has seriously explored this point in the design space, in particular to determine conditions under which we can be sure that missing parameters can be inferred, or to come up with a good, clean syntax. The whole idea may seem a bit odd, but it is in line with proposals circulating a couple of weeks ago by folks who want to allow declared types like forall b. C Int b => b -> Bool in situations where they knew that the only possible instantiation for b was some fixed type like Int (say). 4) "Functional Dependencies": As described in my ESOP 00 paper (the Hugs manual, and the HTML note on my web page, don't tell the whole story). This allows a programmer to indicate that, like (3), some of the parameters in a constraint will be *uniquely* determined by other parameters. Unlike (3), the assumption in the ESOP paper, and in current implementations, is that these uniquely determined types will be mentioned explicitly in each instance declaration. With functional dependencies, inferred constraint sets can be improved in ways that are (a) important in practice, and (b) not possible in any of the options mentioned previously. For example, given class Collects c e | c -> e, we can simplify (Collects c e, Collects c f) => e -> f -> c -> c to (Collects c e) => e -> e -> c -> c. [Aside: Marcin's specific problem with Has_parens could be dealt with in this framework also, but that would probably require the introduction of a newtype like: newtype PP = forall a. PP (Parser a -> Parser a) instance Has_parens TokenParser PP where ... This, of course, would require extra games with the PP constructor (and an appropriately defined inverse) in expressions, which would probably be too messy and awkward in practice; a record system designed to support polymorphic fields from the outset would be a better solution here.] 5) And so on. There are other alternatives ... | I want keys instead of fundeps! :-) I've found it hard to assess or make sense of your descriptions of keys in previous postings; at different times it has seemed as though keys could be any of options 1, 2, 3, 4, or 5 in the above. But I hope that my analysis of the design space above is helping us to reach a better shared understanding of exactly what you are proposing. In terms of what I've written above, my current guess at interpreting your proposal goes something like this: - You want to allow each class declaration to be annotated with zero or more subsets of the parameters, each of which you refer to as a "key" for the class. - When a user writes an instance declaration: instance P => C t1 ... tn where ... you treat it, in the notation of (2) above, as if they'd written: instance P => C t1 ... tn improves C t11 ... t1n, ..., C tm1 ... tmn where ... Here, m is the number of keys, and: tij = ti, if parameter i is in key j = ai, otherwise where a1, ..., an are distinct new variables. If this is correct, then it seems to me that: - Keys will provide a more concise, but less expressive notation than (2). The notation of (2) is considerably more expressive because it isn't limited to the form used in the translation above, and because it can be used on an instance by instance basis rather than a specification that applies uniformly to all instances of a class. It's hard to know what the tradeoffs will be in practice, but I'm inclined to believe that keys are too limited, and the more general mechanism will not be too cumbersome in many practical cases. - Keys will not give you the full functionality of functional dependencies, and that missing functionality is important in some cases. All the best, Mark PS. If we're going to continue this discussion any further, let's take it over into the haskell-cafe ...