[Prev][Next][Index][Thread]

Re: Parametricity Theorem, relational interpretation of constant types

Janis,

> 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

<www.cl.cam.ac.uk/users/amp12/papers/index.html#parpoe>
<www.cl.cam.ac.uk/users/amp12/papers/index.html#exitlr>

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
mind.

Andrew Pitts