Relationally-parametric polymorphic contracts

10 years 3 months ago
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
Arjun Guha, Jacob Matthews, Robert Bruce Findler,
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where DLS
Authors Arjun Guha, Jacob Matthews, Robert Bruce Findler, Shriram Krishnamurthi
Comments (0)