<p>I'm quite fond of Wadler's paper <a href="http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html" rel="nofollow">The Girard-Reynolds Isomorphism</a> which shows that there is a translation from system $\mathrm{F}$ to and from <a href="http://en.wikipedia.org/wiki/Higher-order_logic" rel="nofollow">Second Order Predicate Logic</a> (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type.</p>

<p>Wadler shows that in some conditions, these transformations are inverses of each other.</p>

<p>So to answer your question: the theorems-for-free can be expressed in a form of second-order logic, which is described in the aforementioned paper.</p>

CC BY-SA 3.0
2013-01-11T20:09:06.397Z
2013-03-21T14:23:26.840Z
2013-03-21T14:23:26.840Z
cody
<p>The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper <a href="http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf"><em>A Logic for Parametric Polymorphism</em></a>. </p>

<p>The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper <a href="http://www.sciencedirect.com/science/article/pii/0304397590901517"><em>Functorial Polymorphism</em></a>. </p>

CC BY-SA 3.0
2013-01-08T17:07:06.430Z
Thanks, the first paper seems to answer my first question.
When one says "by parametricity if I : /\X.X->X, then a . I{A} = I{A'} . a for a : A -> A'", isn't one saying "if |- I : /\X.X->X and "|- a : A -> A' then a . I{A} is beta-eta-something-equivalent to I{A'} . a"? Where does this relationship with operational semantics happen? What would be a non-parametric model of System F, and wouldn't it be inconsistent w.r.t. its operational semantics?
user13264
CC BY-SA 3.0
2014-03-22T02:23:50.407Z
This talk shows an example of a non-parametric function (which can't be expressed in System F).
http://www.mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf
For the rest, you need to learn about the correspondence between denotational and operational semantics, and the relation of *soundness*.

A model *can* contain functions which don't correspond to programs. This violates full abstracion, but not soundness.
Blaisorblade
CC BY-SA 3.0
2013-01-08T13:39:52.430Z
2013-01-08T13:39:52.430Z
Neel Krishnaswami
<p>I've found this <a href="https://www-ps.informatik.uni-kiel.de/%7Esad/FreeTheorems/cgi-bin/free-theorems-webui.cgi" rel="nofollow noreferrer">webapp</a> which lets you generate a free theorem for a given type.</p>
<p>The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which theory/logical system? How does this system relate to the equational theory of the language?</p>

CC BY-SA 3.0
2013-01-08T13:06:24.453Z
This seems to be a repost of [the same question on Stack Overflow](http://stackoverflow.com/q/14207218/157360), where it was considered off-topic, and garnered only a cursory answer linking to the "Theorems for Free" paper. Again, [this link](http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html) is relevant.
C. A. McCann
CC BY-SA 3.0
2013-01-08T13:16:28.373Z
Thanks for the reference. I've seen Wadler's paper, but I don't really understand it. He's working with frame semantics, then the relations seem to be between elements in these frames. How does the relations between these elements relate to the equational logic of the language (in Wadler's case, System F)? He instantiates relations with functions, do these functions need to be computable in System F?
user13264
CC BY-SA 4.0
2018-06-21T18:07:45.117Z
the web app is down, are there mirrors anywhere?
user833970
<lo.logic><functional-programming><type-systems><parametricity><logical-relations>
Free theorems, where?
user13264
# Free theorems, where?

(Asked by: username_0 on 2013-01-08)

I've found this [webapp](https://www-ps.informatik.uni-kiel.de/%7Esad/FreeTheorems/cgi-bin/free-theorems-webui.cgi) which lets you generate a free theorem for a given type.

The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which theory/logical system? How does this system relate to the equational theory of the language?

**Tags:** lo.logic, functional-programming, type-systems, parametricity, logical-relations
> **Comments:**
> **username_1**: This seems to be a repost of [the same question on Stack Overflow](http://stackoverflow.com/q/14207218/157360), where it was considered off-topic, and garnered only a cursory answer linking to the "Theorems for Free" paper. Again, [this link](http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html) is relevant.  
> **username_0**: Thanks for the reference. I've seen Wadler's paper, but I don't really understand it. He's working with frame semantics, then the relations seem to be between elements in these frames. How does the relations between these elements relate to the equational logic of the language (in Wadler's case, System F)? He instantiates relations with functions, do these functions need to be computable in System F?  
> **username_2**: the web app is down, are there mirrors anywhere?  

---

## 2 answers

### Answer by username_4 on 2013-01-08. Score: 14 | Accepted answer

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper [*A Logic for Parametric Polymorphism*](http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf).

The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper [*Functorial Polymorphism*](http://www.sciencedirect.com/science/article/pii/0304397590901517).

> **Comments:**
> **username_0**: Thanks, the first paper seems to answer my first question. When one says "by parametricity if I : /\X.X->X, then a . I{A} = I{A'} . a for a : A -> A'", isn't one saying "if |- I : /\X.X->X and "|- a : A -> A' then a . I{A} is beta-eta-something-equivalent to I{A'} . a"? Where does this relationship with operational semantics happen? What would be a non-parametric model of System F, and wouldn't it be inconsistent w.r.t. its operational semantics?  
> **username_5**: This talk shows an example of a non-parametric function (which can't be expressed in System F). http://www.mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf For the rest, you need to learn about the correspondence between denotational and operational semantics, and the relation of *soundness*.  A model *can* contain functions which don't correspond to programs. This violates full abstracion, but not soundness.  

---

### Answer by username_3 on 2013-01-11. Score: 7

I'm quite fond of Wadler's paper [The Girard-Reynolds Isomorphism](http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html) which shows that there is a translation from system $\mathrm{F}$ to and from [Second Order Predicate Logic](http://en.wikipedia.org/wiki/Higher-order_logic) (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type.

Wadler shows that in some conditions, these transformations are inverses of each other.

So to answer your question: the theorems-for-free can be expressed in a form of second-order logic, which is described in the aforementioned paper.


---

