Lambda the Ultimate

Semantic types: a fresh look at the ideal model for types, Jerome Vouillon and Paul-André Melliès. POPL 2004.

We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types (computed by fixpoint of a typing operator) does not rely on metric properties, but on the fact that the identity is the limit of a sequence of projection terms. This establishes a connection with the work of Pitts on relational properties of domains. This also suggests that ideals are better understood as closed sets of terms defined by orthogonality with respect to a set of contexts.

A couple of days ago, we had a post about game models of linear logic, which led to a discussion of Girard's ludics. One of the key ingredients of ludics is the idea of biorthogonality, which is the idea that the semantics of types should be stable under biorthogonality. Now, the idea of biorthogonality is that for every term in a language has an orthogonal -- the set of client programs with which our term will run safely together. A set of terms is a biorthogonal when it is equal to the orthogonal of its orthogonal. The reason this idea is interesting is that it offers a way to sensibly pass back and forth between a local, proof-theoretic notion of "type as intro and elim rule" and a global, semantic notion of type as "predicate on terms".

This paper offers a relatively accessible entry point to those ideas, assuming you're familiar with the basic ideas behind either solving domain equations or doing logical relations proofs.