Re: Parametricity Theorem, relational interpretation of constant types


> I've got a question regarding Reynold's abstraction (or parametricity) theorem 
> for polymorphic lambda calculus [1].

> Wadler's paper on Free Theorems [2], and other related papers using 
> parametricity for functional programming languages, all seem to choose identity 
> as relational interpretation for types that are taken as constant (like Int, 
> Bool, whatever). The question is:

> Is this really a forced choice? I.e., could one also choose some other 
> relational interpretation (extending the identity relation) for constant types, 
> e.g., the "definedness"-preorder $\sqsubseteq$ of a lazy functional language 
> (assuming it has free theorems in the first place), without violating the free 
> theorems obtained from parametricity by applying the usual relational 
> interpretations for type constructors (->), \forall, ...?

Yes, different choices can be made. What you choose depends on what
use one is intending to make of the relationally parametric logical
relation. For example my papers


develop such logical relations as a tool for proving operationally
defined contextual _equivalences_ of programs in various polymorphic
languages; but if one wanted to characterise a contextual _preorder_
(what I guess you mean by "definedness-preorder", roughly) that would
be straightforward and would involve changing the definition of the
logical relation at the base types in the way I think you have in

Andrew Pitts