Search

International audience; Coercive subtyping is a useful and powerful framework of subtyping for type theories. The key idea of coercive subtyping is subtyping as abbreviation. In this paper, we give a new and adequate formulation of T[C], the system that extends a type theory T with coercive subtyping based on a set C of basic subtyping judgements, and show that coercive subtyping is a conservative extension and, in a more general sense, a definitional extension. We introduce an intermediate system, the star-calculus T[C]^@?, in which the positions that require coercion insertions are marked, and show that T[C]^@? is a conservative extension of T and that T[C]^@? is equivalent to T[C]. This makes clear what we mean by coercive subtyping being a conservative extension, on the one hand, and amends a technical problem that has led to a gap in the earlier conservativity proof, on the other. We also compare coercive subtyping with the 'ordinary' notion of subtyping - subsumptive subtyping, and show that the former is adequate for type theories with canonical objects while the latter is not. An improved implementation of coercive subtyping is done in the proof assistant Plastic.

The statement S≤T in a λ-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[[T]] that extracts the “T part” of an element of S. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to include both the implicit coercion and an overwriting function put[S,T] ∈ [[S]]→[[T]]→[[S]] that updates the T part of an element of S. We give a realizability model and a sound equational theory for a second-order calculus of positive subtyping.Though weaker than familiar calculi of bounded quantification, positive subtyping retains sufficient power to model objects, encapsulation, and message passing. Moreover, inheritance may be implemented very straightforwardly in this setting, using the put functions 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 behavior 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.

Structured data are generally composed from constituent parts by constructors and decomposed by selectors . We show that the usual many-sorted algebra approach to abstract data types cannot capture this simple intuition in a satisfactory way. We also show that order-sorted algebra does solve this problem, and many others concerning partially defined, ill-defined, and erroneous expressions, in a simple and natural way. In particular, we show how order-sorted algebra supports and elegant solution to the problems of multiple representations and coercions. The essence of order-sorted algebra is that sorts have subsorts , whose semantic interpretation is the subset relation on the carriers of algebras.