[Prev][Next][Index][Thread]
Re: Parametricity Theorem, relational interpretation of constant types

To: Janis Voigtlaender <voigt@orchid.inf.tudresden.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

InReplyTo: Your message of "Mon, 17 Dec 2001 13:32:50 +0100." <200112171321.fBHDL4Q17436@saul.cis.upenn.edu>

UserAgent: EMH/1.10.0 SEMI/1.13.7 (Awazu) CLIME/1.13.6 (=?ISO2022JP?B?GyRCQ2YlTj4xGyhC?=) MULE XEmacs/21.1 (patch 14) (Cuyahoga Valley) (i386redhatlinux)
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 "definednesspreorder", 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