This message is an attempt to comment on the relationship between the
various treatments of extensible records that have been referred to in
the past couple of days.
While the proposal on records for Haskell 2 that I just posted is
intended for a fairly wide Haskell audience, this one will probably be
of interest only to a smaller group of people. If you're not
interested in technical discussion about record type systems, now is a
good time to stop reading!
The final section of the Haskell 2 proposal corresponds to the system I
described in my thesis (which is where you should look for formal
details). The system presented there uses two forms of predicates (or
type classes, if you prefer):
r has l:t the record r has an l field of type t. Another way
to write this is to use a subtyping notation:
r <= { l : t }
r lacks l the record r has no l field. In the proposal below,
I have used an alternative syntax -- r\l -- for the
same thing.
These two forms of predicates express what I would call positive and
negative information, respectively, about the fields of a record (i.e.
the first asserts that a field is present, the second that it is
absent). In this sense, the approach has some relationship with the
work of R'emy on natural extensions of ML type inference with records.
You will see that the proposal below uses only the negative form. An
observation which goes back at least as far as the work of Harper and
Pierce is that we can replace positive information with negative. For
example, (r has x:Int) => r -> Int becomes (r\x) => (r|x:Int) -> Int.
I have also found that the negative form of constraint is better than
the positive form because it avoids coherence problems, ambiguities,
and generally leads to more concise principal types.
Extending Haskell with a system of records like this requires a kind
system with two kinds; * (representing all types) and () (representing
all record types) where () is a subkind of *. This may sound complex
but it actually works out very easily in practice. Extending the
system to deal with constructor classes requires the addition of
function kinds, and a new rule for subkinding; I believe this can all
work out quite nicely, but the added complexity is one of the main
reasons that I haven't got around to implementing the whole thing in
Gofer.
Ohori also used kinds in his work; he has a kind U corresponding to *
but he uses a whole family of record kinds to record the fields that
are present in a particular record. With my approach, the additional
information about fields is captured instead by predicates, so a single
() kind suffices. Apart from this technical difference, I believe that
the two type systems are actually very close to one another, at least
from a programmer's perspective. There are, however, a couple of
advantages of my work over Ohori's:
o Support for polymorphic extension and restriction of records
(i.e. adding new fields, or removing existing fields). Ohori's
system provides only selection (r.l) , update (r|x:=x+1) and
construction (x=2, y=True).
o By describing records and type classes as applications of the same
framework (qualified types), it is clear that the two ideas can be
used side by side in an attractive manner. It also allows us to
apply the large body of work on the theory of type classes to study
systems of record types.
>From his description, Martin's approach sounds like the combination of
a new approach to type classes together with a restricted version of
the treatment of records that I proposed in my thesis. I will have to
read the paper in some detail before I can be sure that my analysis is
correct.
I would like to see some more information about Giuliano Procida's system
to see where that fits in to the picture.
All the best,
Mark
