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