Lambda the Ultimate

Relationally-Parametric Polymorphic Contracts, Arjun Guha, Jacob Matthews, Robert Bruce Findler, Shriram Krishnamurthi. 2007

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.

There's a really simple and elegant idea here: you can test at runtime whether a function uses a particular argument parametrically (ie, doesn't examine it) by wrapping it in a value that raises an error if you try to use it before sending it to the function.