[TYPES] completeness of subtype judgments

[Alain Frisch]

Sophia Drossopoulou wrote:
> Dave Clarke and I have been wondering whether there is any work
> on the completeness of type systems, in the presence of subtyping
> and rather intricate types.

You might be interested in our paper at LICS 2002 (_Semantic subtyping_,
A. Frisch, G. Castagna, and V. Benzaken). An informal introduction
can be found in _A Gentle Introduction to Semantic Subtyping_ and the
full development is in my PhD thesis (in French); a journal version is
in preparation. ---> http://www.cduce.org/papers.html

The system in these papers includes type constructors (products,
records, arrows), Boolean connectives (finite union and intersection,
negation) and recursive types. Types are interpreted as sets of values
and Boolean connectives are interpreted purely set-theoretically,
so e.g. the negation of a type t contains all the (well-typed) values
which don't have type t. The calculus is a CBV lambda-calculus,
with overloaded first-class functions (whose explicit signature
can mention several arrow types) and dynamic type-dispatch.

The subtyping relation is defined such that it corresponds exactly
to set inclusion. If we write [[t]] for the set of values of type t
[[t]] = { v | |- v : t }, then:

(*) t <: t'  iff  [[t]] \subset [[t']]

Clearly, because of the subsumption rule in the type system
and because values are expressions, we also have:

t <: t'  iff \forall \Gamma, e.  \Gamma |- e : t  ==>  \Gamma |- e : t'

where e stands for expressions. We have another completeness result
which relates the subtyping of arrow types and the dynamic semantics.

The trick to obtain (*) was to actually start from (*)
as a definition for <:, and then derive an axiomatic formulation and an
algorithm (we did this work for a concrete programming language).  In
order to avoid the circularity between the subtyping relation, the type
system and the type-directed semantics, we developed a bootstrapping
approach.


Cheers,

 Alain Frisch