[Prev][Next][Index][Thread]

bounded quantification and record-update problems

Date: Wed, 19 Oct 88 13:50:20 EDT
To: epr@qucis.lcs.mit.edu, gunter@linc.cis.upenn.edu, ohearn@qucis.lcs.mit.edu,
        types@theory.LCS.MIT.EDU

Cardelli and Wegner [1985] introduced a concept of "bounded"
quantification in polymorphic lambda calculi with subtyping.
The type expression  ALL[t <= A] ...t...,  where A is a type
expression, is intended to denote the type of generic values
which yield values of type ...B... when applied to any
type B which is a sub-type of A.  The class of applications they
suggest to motivate this feature are record-updating problems
such as the following.  Let type POINT = {x: real, y: real}
and consider the "function"

    moveX = ALL[t <= POINT] fun(dx:real,p:t) (p.x := p.x+dx; p)

This is intended to be applicable to all record types with (at least)
x and y fields of type real, preserving other fields unchanged.

While Carl Gunter was on a visit here recently, he pointed out that
it was not possible to express this function in the "pure" (functional)
subset of the Cardelli-Wegner language and asked whether such functions
even existed in the Bruce and Longo [1988] model.  This led us to look
more closely at the intended application for bounded quantification.

Suppose int <= real, either as a built-in coercion on primitive types,
or because int is a boundedly-quantified type variable in the context.
Then moveX must be applicable to a record type with (at least) fields
x:int and y:int.  But this is clearly wrong since one cannot expect
that moveX will produce a result with a field x:int for arbitrary
integers x and reals dx.  In short, it seems that bounded quantification
is inadequate to solve record-updating problems.

Further evidence for this is the following result about the Bruce-Longo
model, which answers Carl's question.

Lemma: For any per C, the interpretation of the type

    FOR[a <= C] a -> a

is trivial (i.e., contains only the polymorphic identity).

Proof: Recall that for a per A, A <= C iff nAm implies nCm.
Therefore the domain of A is contained in the domain of C.
Let e be of type (FOR[a <= C] a -> a), and n be in the domain
of C. Let A be the per mAm' iff m=m'=n. Then e maps A to itself.
Hence {e}n = n. Thus e acts as the identity for all n in the
domain of C, and hence acts as the identity on any per A <= C. QED

As an immediate corollary of this semantic result, we obtain a
simple proof of Carl's original observation that moveX is not
definable in Bounded Fun: moveX fairly clearly satisfies an equation
not satisfied by the polymorphic identity. We also see that Bounded Fun is
incapable of expressing any other polymorphic record update either.

This leads to two questions.

1.  Are there any (other) applications of bounded quantification?

2.  Are there (other) ways of solving the record-update problem?

A possible answer to the second question is to add the following
structural coercion:

    a -> b <= a /\ c -> b /\ c

where a, b and c are record types with the labels of c disjoint
>from those of a and b, and /\ denotes the obvious merge of fields.
The interpretation should be clear:  the resulting function
transforms the a-fields using the given function and the c-fields
are preserved.  Then

    moveX = fun(dx:real, p:{x:real}) {x=p.x+dx}
      : real -> {x:real} -> {x:real}

will be applicable to values of any type coercible to {x:real}
and additional fields will be preserved, if necessary.
It remains to be seen whether the proposed coercion is syntactically
and semantically compatible with the other desired coercions.
If so, this approach would work in a system without bounded quantification,
and it results in a "type" for moveX which is not expressible in
the system with bounded quantification.

Edmund Robinson
Bob Tennent