Polymorphic Contracts

By João Filipe Belo and Michael Greenberg and Atsushi Igarashi and Benjamin C. Pierce. In Proceedings of European Symposium on Programming (ESOP2011), volume 6602 of Springer LNCS, pages 18-37, Saarbrücken, Germany, March, 2011.


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 strong contracts to abstract types, precisely stating pre- and post-conditions while hiding implementation details--for example, an abstract type of stacks might specify that the pop operation has in- put type {x : α Stack | not (empty x )}. We formalize this combination by defining FH , a polymorphic calculus with manifest contracts, and estab- lishing fundamental properties including type soundness and relational parametricity. Our development relies on a significant technical improve- ment 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.