Home

Semantic types: a fresh look at the ideal model for types

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.

By neelk at 2009-12-22 17:01 | Theory | other blogs | 10239 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Just a terminological quibble

It's a shame that ‘biorthogonality’ (which I read several times, despite its ludicrousness in this context, as ‘bio-orthogonality’) was used, when we already have the perfectly good term ‘reflexive’. Does the latter term lead to confusion with some other meaning in logic? (‘Closed’, which is how one recognises this property in subspaces of a Hilbert space, is clearly highly ambiguous, so I don't suggest it.)

By L Spice at Fri, 2009-12-25 01:57 | login or register to post comments

In domain theory, I've seen

In domain theory, I've seen the term "reflexive" used to refer to domains which are the solution to a recursive domain equation, or sometimes to a section-retraction pair. The analogy you suggest is a really nice one, so it's bit of a shame the terminology is already in use.

By neelk at Sat, 2009-12-26 11:54 | login or register to post comments