TY - GEN
T1 - Contracts made manifest
AU - Greenberg, Michael
AU - Pierce, Benjamin C.
AU - Weirich, Stephanie
PY - 2010
Y1 - 2010
N2 - Since Findler and Felleisen 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, 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.
AB - Since Findler and Felleisen 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, 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.
KW - Blame
KW - Contract
KW - Dynamic checking
KW - Postcondition
KW - Precondition
KW - Refinement type
KW - Translation
UR - http://www.scopus.com/inward/record.url?scp=77950893656&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77950893656&partnerID=8YFLogxK
U2 - 10.1145/1706299.1706341
DO - 10.1145/1706299.1706341
M3 - Conference contribution
AN - SCOPUS:77950893656
SN - 9781605584799
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 353
EP - 364
BT - POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
Y2 - 17 January 2010 through 23 January 2010
ER -