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.
me (mel@mailinator.com)
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.