Re: Parametricity Theorem, relational interpretation of constant types

• To: Janis Voigtlaender <voigt@orchid.inf.tu-dresden.de>
• Subject: Re: Parametricity Theorem, relational interpretation of constant types
• From: Andrew Pitts <Andrew.Pitts@cl.cam.ac.uk>
• Date: Mon, 17 Dec 2001 14:00:39 +0000
• cc: types@cis.upenn.edu
• In-Reply-To: Your message of "Mon, 17 Dec 2001 13:32:50 +0100." <200112171321.fBHDL4Q17436@saul.cis.upenn.edu>
• User-Agent: EMH/1.10.0 SEMI/1.13.7 (Awazu) CLIME/1.13.6 (=?ISO-2022-JP?B?GyRCQ2YlTj4xGyhC?=) MULE XEmacs/21.1 (patch 14) (Cuyahoga Valley) (i386-redhat-linux)

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