Hostname: page-component-8448b6f56d-wq2xx Total loading time: 0 Render date: 2024-04-16T19:21:52.093Z Has data issue: false hasContentIssue false
  • English
  • Français

Contracts made manifest*

Part of: JFP Research Articles

Published online by Cambridge University Press:  29 May 2012

MICHAEL GREENBERG ,
BENJAMIN C. PIERCE  and
STEPHANIE WEIRICH
MICHAEL GREENBERG
Affiliation:
University of Pennsylvania, Philadelphia, PA 19104, USA (e-mail: mgree@seas.upenn.edu)
BENJAMIN C. PIERCE
Affiliation:
University of Pennsylvania, Philadelphia, PA 19104, USA (e-mail: mgree@seas.upenn.edu)
STEPHANIE WEIRICH
Affiliation:
University of Pennsylvania, Philadelphia, PA 19104, USA (e-mail: mgree@seas.upenn.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Since Findler and Felleisen (Findler, R. B. & Felleisen, M. 2002) introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen (2002) 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 (Gronski, J. & Flanagan, C. 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, 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.

Type
Articles
Information
Journal of Functional Programming , Volume 22 , Issue 3 , May 2012 , pp. 225 - 274
Copyright
Copyright © Cambridge University Press 2012

References

Ahmed, A. (2006) Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the European Symposium on Programming (ESOP), Lecture Notes in Computer Science, vol. 3924. Berlin, Germany: Springer-Verlag, pp. 69–83.Google Scholar
Aydemir, B. & Weirich, S. (June 2010) LNgen: Tool support for locally nameless representations. Tech. Report MS-CIS-10-24. Department of Computer and Information Science, University of Pennsylvania.Google Scholar
Belo, J. F., Greenberg, M., Igarashi, A. & Pierce, B. C. (2011) Polymorphic contracts. In Proceedings of the European Symposium on Programming (ESOP), Saarbrücken, Germany, pp. 18–37.Google Scholar
Blume, M. & McAllester, D. A. (2006) Sound and complete models of contracts. J. Funct. Program. (JFP) 16, 375–414.Google Scholar
Cardelli, L., Martini, S., Mitchell, J. C. & Scedrov, A. (1994) An extension of system F with sub-typing. Inf. Comput. 9, 4–56.CrossRefGoogle Scholar
Chitil, O. & Huch, F. (2007) Monadic, prompt lazy assertions in Haskell. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), LNCS vol. 4807. New York, NY: Springer, pp. 38–53.Google Scholar
Dimoulas, C., Findler, R. B., Flanagan, C. & Felleisen, M. (2011) Correct blame for contracts: No more scapegoating. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Austin, TX, USA, pp. 215–226.Google Scholar
Findler, R. B. & Blume, M. (2006) Contracts as pairs of projections. In Proceedings of the Functional and Logic Programming (FLOPS), Fuji Susono, Japan, LNCS vol. 3945, pp. 226–241.Google Scholar
Findler, R. B. & Felleisen, M. (2002) Contracts for higher-order functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on International Conference on Functional Programming (ICFP), Pittsburgh, PA, USA, pp. 48–59.Google Scholar
Flanagan, C. (2006) Hybrid type checking. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (POPL), Charleston, SC, USA, pp. 245–256.Google Scholar
Greenberg, M., Pierce, B. C. & Weirich, S. (2010) Contracts made manifest. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on the Principles of Programming Languages (POPL), Madrid, Spain, pp. 353–364.Google Scholar
Gronski, J. & Flanagan, C. (2007). Unifying hybrid types and contracts. In Proceedings of the 8th Symposium on Trends in Functional Programming (TFP), New York, NY, USA, pp. 54–70.Google Scholar
Guha, A., Matthews, J., Findler, R. B. & Krishnamurthi, S. (2007) Relationally-parametric polymorphic contracts. In Proceedings of the Dynamic Languages Symposium (DLS), Montreal, Quebec, Canada, October 22, pp. 29–40.Google Scholar
Hinze, R., Jeuring, J. & Löh, A. (2006) Typed contracts for functional programming. In Proceedings of the Functional and Logic Programming (FLOPS), Fuji Susono, Japan, LNCS vol. 3945, pp. 208–225.Google Scholar
Knowles, K. & Flanagan, C. (January 2010) Hybrid type checking. ACM Trans. Program. Lang. Syst. (TOPLAS) 32 (2), Article 6, 34 pp.Google Scholar
Knowles, K., Tomb, A., Gronski, J., Freund, S. N. & Flanagan, C. (2006) Sage: Hybrid checking for flexible specifications. In Proceedings of the Scheme and Functional Programming Workshop, University of Chicago, pp. 93–104.Google Scholar
Meyer, B. (1992) Eiffel: The Language. Upper Saddle River, NJ: Prentice-Hall.Google Scholar
Ou, X., Tan, G., Mandelbaum, Y. & Walker, D. (2004) Dynamic typing with dependent types. In Proceedings of the IFIP Conference on Theoretical Computer Science (TCS), Toulouse, France, pp. 437–450.Google Scholar
Pitts, A. M. (2005) Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Chap. 7. Pierce, B. C. (ed). Cambridge, MA: MIT Press, pp. 245–289.Google Scholar
Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnisa, R. (2007) Ott: Effective tool support for the working semanticist. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP), Freiburg, Germany, October 1–3, pp. 1–12.Google Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2008) The design and implementation of typed scheme. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, USA, pp. 395–406.Google Scholar
Wadler, P. & Findler, R. B. (2007) Well-typed programs can't be blamed. Proceedings of the Scheme and Functional Programming Workshop, Freiburg, Germany, September 30.Google Scholar
Wadler, P. & Findler, R. B. (2009) Well-typed programs can't be blamed. In Proceedings of the 18th European Symposium on Programming (ESOP), York, UK, March 25–27, pp. 1–16.Google Scholar
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Inf. Comput. 115, 38–94.Google Scholar
Xu, D. N., Peyton Jones, S. & Claessen, K. (2009) Static contract checking for Haskell. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (POPL), Savannah, Georgia, January 21–23, pp. 41–52.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.