Relationally-parametric polymorphic contracts

ABSTRACT

The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic types in languages like Standard ML.

We present a contract counterpart to parametricity. We explore multiple designs for such a system and present one that is simple and incurs minimal execution overhead. We show how to extend the notion of contract blame to our definition. We present a form of inference that can often save programmers from having to explicitly instantiate many parametric contracts. Finally, we present several examples that illustrate how this system mimics the feel and properties of parametric polymorphism in typed languages.

REFERENCES

• 1: Carrillo-Castellon, M., J. Garcia-Molina, E. Pimentel and I. Repiso. Design by contract in Smalltalk. Journal of Object-Oriented Programming, 7(9):23--28, 1996.
• 2: Conway, D. and C. G. Goebel. Class::Contract -- design-bycontract OO in Perl. search.cpan.org/?ggoebel/Class-Contract-1.14.
• 3: ECMA. ECMAScript language specification.
• 4: Conal Elliott , Paul Hudak, Functional reactive animation, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.263-273, June 09-11, 1997, Amsterdam, The Netherlands
• 5: Findler, Barzilay, Blume, Codik, Felleisen, Flatt, Huang, Matthews, McCarthy, Scott, Press, Rainey, Reppy, Riehl, Spiro, Tucker and Wick. The eighth annual ICFP programming contest. icfpc.plt-scheme.org/.
• 6: 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
• 7: Findler, R. B. and M. Blume. Contracts as pairs of projections. In International Symposium on Functional and Logic Programming, pages 226--241, 2006.
• 8: Robert Bruce Findler , Mario Latendresse , Matthias Felleisen, Behavioral contracts and behavioral subtyping, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 9: Flapjax Team. Flapjax programming language. www.flapjax-lang.org.
• 10: Matthew Flatt, Composable and compilable macros:: you want it when?, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.72-83, October 04-06, 2002, Pittsburgh, PA, USA
• 11: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 12: Hinze, R., J. Jeuring and A. Löh. Typed contracts for functional programming. In International Symposium on Functional and Logic Programming, pages 208--225, 2006.
• 13: Ignatoff, D., G. H. Cooper and S. Krishnamurthi. Crossing state lines: Adapting object-oriented frameworks to functional reactive languages. In International Symposium on Functional and Logic Programming, pages 259--276, 2006.
• 14: Murat Karaorman , Urs Hölzle , John L. Bruno, jContractor: A Reflective Java Library to Support Design by Contract, Proceedings of the Second International Conference on Meta-Level Architectures and Reflection, p.175-196, July 19-21, 1999
• 15: Jacob Matthews , Robert Bruce Findler, Operational semantics for multi-language programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 16: McFarlane, K. Design by contract framework. www.codeproject.com/csharp/designbycontract.asp.
• 17: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 18: Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, August 1978.
• 19: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 20: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 21: Pierce, B. and E. Sumii. Relating cryptography and polymorphism, 2000. Unpublished manuscript.
• 22: Reinhold Ploesch, Design by Contract for Python, Proceedings of the Fourth Asia-Pacific Software Engineering and International Computer Science Conference, p.213, December 02-05, 1997
• 23: Reinhold Ploesch , Josef Pichler, Contracts: From Analysis to C++ Implementation, Proceedings of the Technology of Object-Oriented Languages and Systems, p.248, August 01-05, 1999
• 24: PLT. PLT MzLib: Libraries manual. Technical Report PLTTR05-4-v300, PLT Scheme Inc., 2005. www.plt-scheme.org/techreports/.
• 25: Reynolds, J. C. Types, absraction, and parametric polymorphism. In Information Processing 83, pages 513--523, 1983.
• 26: David S. Rosenblum, A Practical Approach to Programming With Assertions, IEEE Transactions on Software Engineering, v.21 n.1, p.19-31, January 1995 [doi>10.1109/32.341844]
• 27: Sam Tobin-Hochstadt , Matthias Felleisen, Interlanguage migration: from scripts to programs, Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1176617.1176755]
• 28: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]
• 29: Steve Zdancewic , Dan Grossman , Greg Morrisett, Principals in programming languages: a syntactic proof technique, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.197-207, September 27-29, 1999, Paris, France

INDEX TERMS

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

General Terms:
Languages, Reliability

Keywords:
contracts, parametricity, polymorphism