Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

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.

REFERENCES

• 1: Matthias Blume , David McAllester, Sound and complete models of contracts, Journal of Functional Programming, v.16 n.4-5, p.375-414, July 2006 [doi>10.1017/S0956796806005971]
• 2: Olaf Chitil and Frank Huch. Monadic, prompt lazy assertions in haskell. In APLAS, pages 38--53, 2007.
• 3: Robert Bruce Findler. Contracts as pairs of projections. In Symposium on Logic Programming, pages 226--241, 2006.
• 4: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA [doi>10.1145/581478.581484]
• 5: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA [doi>10.1145/1111037.1111059]
• 6: Jessica Gronski and Cormac Flanagan. Unifying hybrid types and contracts. In Trends in Functional Programming (TFP), 2007.
• 7: Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93--104, 2006.
• 8: Arjun Guha , Jacob Matthews , Robert Bruce Findler , Shriram Krishnamurthi, Relationally-parametric polymorphic contracts, Proceedings of the 2007 symposium on Dynamic languages, October 22-22, 2007, Montreal, Quebec, Canada [doi>10.1145/1297081.1297089]
• 9: Ralf Hinze, Johan Jeuring, and Andres L¨oh. Typed contracts for functional programming. In Functional and Logic Programming (FLOPS), pages 208--225, 2006.
• 10: Kenneth Knowles and Cormac Flanagan. Hybrid type checking. To appear in TOPLAS., 2009.
• 11: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 12: Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and DavidWalker. Dynamic typing with dependent types. In IFIP TCS, pages 437--450, 2004.
• 13: Sam Tobin-Hochstadt , Matthias Felleisen, The design and implementation of typed scheme, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA [doi>10.1145/1328438.1328486]
• 14: Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Workshop on Scheme and Functional Programming, 2007.
• 15: Philip Wadler , Robert Bruce Findler, Well-Typed Programs Can't Be Blamed, Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00590-9_1]
• 16: Dana N. Xu , Simon Peyton Jones , Koen Claessen, Static contract checking for Haskell, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA [doi>10.1145/1480881.1480889]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract

General Terms:
Languages, Theory

Keywords:
blame, contract, dynamic checking, postcondition, precondition, refinement type, translation