[Prev][Next][Index][Thread]
bounded quantification and record-update problems
Date: Thu, 20 Oct 88 09:53:04 EDT
To: rdt%QUCIS.BITNET@mitvma.mit.edu
Cc: types@theory.LCS.MIT.EDU
In-Reply-To: rdt%QUCIS.BITNET@mitvma.mit.edu's message of Wed, 19 Oct 88 20:09:22 EDT <8810200009.AA08967@theory.LCS.MIT.EDU>
In the 1987 I proposed a type system which handles at least the functional
analogue of record updating. In this system, the basic operation on records
is "M with a = N", which returns a record just like M except that it has an
a-field with value N. If M had no a-field, one is added. This is like the
usual notion of extending a partial function at one point. Then we can write
things like
\x. x with a = (x.a)+1
which returns a record just like x, but with the a-field incremented.
The type system relies on "rows" to express the polymorphism. The details in
the 87 paper were buggy, but this was fixed by an observation of Didier Remy.
If we add a new kind, called Field, with type constructors
absent : Field
present : Type => Field
then Field becomes Type+{absent}, and we can make the type of a record be a
record of fields. Then the type of the term above becomes
[a:pres(int)]r -> [a:pres(int)]r
where [a:pres(int)]r is read as the type of all records whose a-field is
present with type integer, and with other fields called r. (Think of r as a
named ellipsis).
Then we can write the type of extension as
(_) with a=(_) : [a:f]r -> t -> [a:pres(t)]r
that is, the first argument is a record whose a-field may either be present
or absent (this is indicated by the FIELD variable f), and whose other fields
are described by the row r; the second argument is of type t; and the result
is a record whose a-field is present with type t and whose other fields are
the same types as they were in the input.
The neat thing about this model is that the type expressions constitute a free
algebra, so all the ordinary results about unification, principal types, etc,
carry over for free.
The language is mine; the solution to getting principal types is due to Remy.
I've worked out the proof of why this works even when the set of fields is
potentially infinite, and also some connections with object-oriented
programming.
I have a paper describing this in more detail, which I can send to anyone who
would like it.
Mitchell Wand
College of Computer Science
Northeastern University
360 Huntington Avenue #161CN
Boston, MA 02115
CSNet: wand@corwin.ccs.northeastern.edu