[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