Contracts made manifest

Since Findler and Felleisen [2002] introduced higher-order contracts, many variants 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 to each value. These two approaches are commonly 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 [2007], who defined a latent calculus λ C and a manifest calculus λ H, gave a translation Ø from λ C to λ H, and proved that, if a λ C term reduces to a constant, then so does its Ø -image.We enrich their account with a translation ψ from λ H to λ C and prove an analogous theorem. We then generalize the whole framework to dependent contracts, whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of λ H and two dialects ("lax" and "picky") of λ C, establish type soundness-a substantial result in itself, for λ H- and extend Ø and ψ accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: The extended translations preserve behavior in one direction but, in the other, sometimes yield terms that blame more.