Are fundeps the right model at all?
Mark P Jones
mpj@cse.ogi.edu
Mon, 15 Jan 2001 02:01:18 -0800
| 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
|=20
| 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.
|=20
| 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 =3D> 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 =3D> 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) =3D TV(t), but also =
can
accommodate things like AV(Has_field r a) =3D 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 =3D> 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 =3D> 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 =3D> 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) =3D> e -> f -> c -> c =
to
(Collects c e) =3D> 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 =3D 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 =3D> C t1 ... tn where ...
you treat it, in the notation of (2) above, as if they'd written:
instance P =3D> C t1 ... tn=20
improves C t11 ... t1n, ..., C tm1 ... tmn where ...
Here, m is the number of keys, and: tij =3D ti, if parameter i is =
in key j
=3D 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 ...