Polymorphic Contracts

João Belo, Atsushi Igarashi, Benjamin Pierce, and I submitted a paper, Polymorphic Contracts, to ESOP’11. Here’s the abstract:

Manifest contracts track precise properties by refining types with predicates—e.g., {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give abstract types strong contracts, precisely stating pre- and post-conditions while hiding implementation details—for example, an abstract type of stacks might specify that the pop operation has input type {x:α Stack | not (empty x)}. We formalize this combination by defining FH, a polymorphic calculus with manifest contracts, and establishing its fundamental properties, including type soundness and relational parametricity. Our development relies on a significant technical improvement over earlier presentations of contracts: instead of introducing a denotational model to break a problematic circularity between typing, subtyping, and evaluation, we develop the metatheory of contracts in a completely syntactic fashion, omitting subtyping from the core system and recovering it post facto as a derived property.

1 Comment

  1. At the risk of sounding inane; Wooo :) I love contracts; They have the same joy as never forgetting your keys because you can’t lock your door without them. Its an amusing coincidence that people consistently use a stack abstract datatype to introduce postconditions. I’ll post again once I’ve finished the paper.

Leave a Reply

Your email address will not be published. Required fields are marked *