Polymorphic manifest contracts, revised and resolved

Abstract

Manifest contracts track precise program properties by refining types with predicates-for example, {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 instance, an abstract type of stacks might specify that the pop operation has input type {x:αStack | not (empty x)}. This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts, but existing calculi are not very satisfactory. Gronski et al. developed the SAGE language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this article have produced two separate works: Belo et al. [2011] and Greenberg [2013] studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations. Indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures-it resolves the issues in prior calculi with delayed substitution on casts.