Talk:Parametricity
 | This article has not yet been rated on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
| ||||||||||||||||||
Abstraction Theorem
[edit]I just finished a presentation of Reynolds' theorem for school (John C. Reynolds - Types, Abstraction and Parametric Polymorphism).
It states that relations on sets (type interpretations), appropriately extended to things such as ordinary functions, functions on the class of sets (polymorphic functions), pairs and environments (assignments of values to lambda-variables), carry over from the above-mentioned environments to semantic values. That is, if two environments are related, then the values of any lambda-term according to these environments are also related. A corollary to the abstraction theorem [actually I am not quite sure that this cannot be proven, without invoking the abstraction theorem, by a simple induction on the semantic functions] is that: the semantic value of any lambda-term with a polymorphic type, is a parametric function.
Would you like me to write something along these lines (without my own comment of course) - PanayiotisK (talk) 08:25, 1 November 2012 (UTC)
What you are saying, these details on how Reynolds explains his theorem, it's very important to add to the article.
So far, I may be wrong, but in my view his theorem consists of this: take a well-pointed cartesian-closed category, map its objects to Set so that points, limits and exponentials are preserved - and you get a functor. The proof relies on representing functions in Set binary relations, so it's kind of pretty transparent.
But what I do not see is how this can be applied to any type theory, without an attached semantics in Sets.