Are fundeps the right model at all?

[Mark P Jones]

| 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 ...