We’ve sent off the final version of Contracts Made Manifest. There have been quite a few improvements since submission, the most important of which is captured by Figure 1 from our paper:
Our submission only addressed lax λC, where we had an inexact translation φ into λH and an exact translation ψ out of λH. We show a dual situation for picky λC, where φ is exact and ψ is inexact. Intuitively, languages farther to the right on the “axis of blame” are pickier. Translating from right to left preserves behavior exactly, but left-to-right translations generate terms that can blame more than their pre-images. (There are examples in the paper.) I should note that lax and picky λC seem to be the extremes of the axis of blame: I don’t see a natural way to be laxer than lax λC or pickier than picky λC.
We also show that restricting these calculi to first-order dependency leaves them exactly equivalent; before, we could only show an exact equivalence by eliminating all dependency.
I am immensely pleased to report that our paper on Flapjax was accepted to OOPSLA 2009.
This paper presents Flapjax, a language designed for contemporary Web applications. These applications communicate with servers and have rich, interactive interfaces. Flapjax provides two key features that simplify writing these applications. First, it provides event streams, a uniform abstraction for communication within a program as well as with external Web services. Second, the language itself is reactive: it automatically tracks data dependencies and propagates updates along those data?ows. This allows developers to write reactive interfaces in a declarative and compositional style.
The real heroes of this story are my co-authors. Leo, Arjun, and Greg were there for the initial, heroic-effort-based implementation. Jacob and Aleks wrote incredible applications with our dog food. Shriram, of course, saw the whole thing through. Very few of my contributions remain: the original compiler is gone (thank goodness); my thesis work is discussed briefly in How many DOMs? on page 15. Here’s to a great team and a great experience (and a great language)!
Benjamin Pierce, Stephanie Weirich, and I submitted a paper to POPL 2010; it’s about contracts. Here’s the abstract:
Since Findler and Felleisen introduced higher-order contracts, many variants of their system have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied. These two approaches are generally assumed to be equivalent—different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding.
Our work extends that of Gronski and Flanagan, who defined a latent calculus \lambda_C and a manifest calculus \lambda_H, gave a translation \phi from \lambda_C to \lambda_H, and proved that if a \lambda_C term reduces to a constant, then so does its \phi-image. We enrich their account with a translation \psi in the opposite direction and prove an analogous theorem for \psi.
More importantly, we generalize the whole framework to dependent contracts, where the predicates in contracts can mention variables from the local context. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of \lambda_C (following Findler and Felleisen’s semantics) and \lambda_H, establish type soundness—a challenging result in itself, for \lambda_H—and extend \phi and \psi accordingly. Interestingly, the intuition that the two systems are equivalent appears to break down here: we show that \psi preserves behavior exactly, but that a natural extension of \phi to the dependent case will sometimes yield terms that blame more because of a subtle difference in the treatment of dependent function contracts when the codomain contract itself abuses the argument.
Edit on 2009-11-03: there’s a newer version, as will appear in POPL 2010.
Edit on 2010-01-22: I have removed the link to the submission, since it is properly subsumed by our published paper.