## Positive Subtyping

**Martin Hofmann and Benjamin Pierce**
*Abstract:* The statement *S leq T* in a
lambda-calculus with subtyping is traditionally interpreted as a
semantic coercion function of type *[[S]] -> [[T]]* that
extracts the *``[[T]]* part'' of an element *S*. If the
subtyping relation is restricted to covariant positions, this
interpretation may be enriched to include both the coercion and an
overwriting function *put[S,T] in [[S]] -> [[T]] ->
[[S]]* that updates the *T* part of an element of *S*.
We give a realizability model and a sound equational theory.

Though weaker than familiar calculi of bounded quantification,
the restricted system retains sufficient power to model objects,
encapsulation, and message passing. Moreover, inheritance may be
implemented very straightforwardly in this setting, using the
*put* function arising from ordinary subtyping of records in
place of the sophisticated systems of record extension and update
often used for this purpose. The equational laws relating the
behaviour of coercions and *put* functions can be used to
prove simple properties of the resulting classes in such a way that
proofs for superclasses are ``inherited'' by subclasses.

*LFCS report ECS-LFCS-94-303,
September 1994.*

Previous |

Index |

Next