[PRL] the denotation of contracts

[Matthias Felleisen]

As you may recall, a couple of weeks ago I presented a denotational 
model of contracts. The model suggested that contracts should be error 
projections. From that we could work out a number of properties of 
software contracts, but we couldn't verify in the end that contracts 
(with blame) are the proper way of understanding "types as retracts".

Well, we just discovered how to solve this last piece of the puzzle. 
Instead of abstracting the error projection over the kind of error it 
should produce (consumer or producer), we compose the error projection 
from two projections: one for the producer and one for the consumer:

   proj = proj_producer o proj_consumer

Low and behold, once we have introduced this separation, we almost get 
the rest for free. It's literally just a calculation. So we now have a 
full Scott-style understanding of types in a denotational world:

  types are retracts (projections), if we use a blame assignment for 
mistaken uses

We thank Matthias Blume for suggestion this approach. -- Matthias

P.S. In case you're wondering: yes carrying out this program in a 
Universal domain is still an open problem.