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

Parametricity Theorem, relational interpretation of constant types



Hello,

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, ...?

I don't see a reason why this should not be done, provided that the constants 
and functions that come with constant types map related arguments to related 
results, which would clearly be the case if the relation is the 
"definedness"-preorder $\sqsubseteq$. But then, I'm not an expert in this, so 
maybe someone can point out whether this is possible or not?
Any hints would be helpful.

Thanks and regards, 
Janis Voigtlaender.


[1] J.C Reynolds. Types, Abstraction, and Parametric Polymorphism. Information 
Processing, 1983.

[2] P. Wadler. Theorems for free! Functional Programming Languages and Computer 
Architecture, 1989. 


--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de