Are fundeps the right model at all?

Mark P Jones
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
| 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 =
|     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 =
   uses, but also tends to lead to ambiguity problems.  It doesn't =
   Marcin's needs.

1) "A weaker notion of ambiguity" (title of Section 5.8.3 in my =
   which is where I think the following idea originated):  We can modify =
   definition of ambiguity for certain kinds of class constraint by =
   (for example) only certain subsets of parameters.  In this setting, a =
   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 =
   accommodate things like AV(Has_field r a) =3D TV(r).  A semantic =
   for the definition of AV(...) is needed in cases where only some =
   are used; this is straightforward in the case of Has_field-like =
   Note that, in this setting, the only thing that changes is the =
   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 =
   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 =
   For his example, a partial dependency might ensure that the type t in =
   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 =
   at each use.  My old work on improvement provides a theoretical =
   for this.  And, in fact, an unimplemented proposal for supporting =
this kind
   of extension is included in the source code for Hugs (subst.c), =
   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 =
   whereas functional dependencies use improvement at the level of whole
   classes.  Given a declaration  instance P =3D> p where ...  we expect =
   instance to be used for any constraint that matches p.  If an =
   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, ..., =
   and we expect the instance to apply to any constraint that matches =
   (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 =
   the values of certain parameters in a constraint are *uniquely* =
   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 =
   particular instance must actually be Bool (say).  I don't know =
   anyone has seriously explored this point in the design space, in =
   to determine conditions under which we can be sure that missing =
   can be inferred, or to come up with a good, clean syntax.  The whole =
   may seem a bit odd, but it is in line with proposals circulating a =
   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 =
   manual, and the HTML note on my web page, don't tell the whole =
   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 =
   dependencies, inferred constraint sets can be improved in ways that =
   (a) important in practice, and (b) not possible in any of the options
   mentioned previously.  For example, given class Collects c e | c -> =
   we can simplify (Collects c e, Collects c f) =3D> e -> f -> c -> c  =
   (Collects c e) =3D> e -> e -> c -> c.

   [Aside: Marcin's specific problem with Has_parens could be dealt with =
   this framework also, but that would probably require the introduction =
   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 =
   an appropriately defined inverse) in expressions, which would =
   be too messy and awkward in practice; a record system designed to =
   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 =
previous postings; at different times it has seemed as though keys could =
any of options 1, 2, 3, 4, or 5 in the above.  But I hope that my =
of the design space above is helping us to reach a better shared =
of exactly what you are proposing.  In terms of what I've written above, =
current guess at interpreting your proposal goes something like this:

- You want to allow each class declaration to be annotated with zero or =
  subsets of the parameters, each of which you refer to as a "key" for =

- 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 =
  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 =
  applies uniformly to all instances of a class.  It's hard to know what =
  tradeoffs will be in practice, but I'm inclined to believe that keys =
  too limited, and the more general mechanism will not be too cumbersome =
  many practical cases.

- Keys will not give you the full functionality of functional =
  and that missing functionality is important in some cases.

All the best,

PS. If we're going to continue this discussion any further, let's take =
over into the haskell-cafe ...