Relationally-parametric polymorphic contracts

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. Categories and Subject Descriptors D.2.4 [Software / Program Verification]: Programming by contract General Terms Languages, Reliability Keywords Contracts, polymorphism, parametricity

• Type: Conference
• Year: 2007
• Where: DLS
• Authors: Arjun Guha, Jacob Matthews, Robert Bruce Findler, Shriram Krishnamurthi
• Keywords: Contracts, DLS 2007, Dynamic Contracts, Languages, Reliability Keywords Contracts