<p>This should be a comment to Neel's answer, but it's a bit long. Prompted by a hint from Rasmus Petersen, I found the following in Møgelberg's thesis (emphasize mine):</p>

<blockquote>
  <p>Ivar Rummelhoff [36] has studied the encoding of natural numbers in
  per-models over different PCA’s, and showed that in some of these
  models, the encoding contains more than natural numbers. So these
  models cannot be parametric. <em>Even though he does not mention it, this
  shows that unary parametricity is different from binary (relational)
  parametricity, since one can easily show that the encoding of the
  natural numbers in any per-model is unary parametric.</em></p>
</blockquote>

<p>The cited paper is <a href="http://scholar.google.co.uk/scholar?q=polynat%20in%20per%20models" rel="noreferrer">Polynat in PER-models</a>.</p>

CC BY-SA 3.0
2012-05-30T10:40:09.430Z
2012-05-30T10:40:09.430Z
Radu GRIGore
<p>Let me a bit more abstract in answering this.  At each arity $n$, you have the following situation: $n$-ary relations $R$ can be embedded into $(n+1)$-ary relations by defining $R'(\vec{x},y) \iff R(\vec{x}) \land y = x_i$ (for some fixed $i \in [1..n]$). In words, you can use some $n$ arguments out of the $n+1$ arguments for simulating the smaller relation and make the new argument equal to some old one.  (Note that <em>equality</em> is key to doing this.)  So, you have "more" relations at arity $n+1$ than you had at arity $n$, and this goes on <em>ad infinitum</em>.  Since more relations means stronger parametricity and fewer function families would be regarded "parametric", we understand that "true parametricity" is what we obtain in the limit, and each finitary parametricity is an approximation to it.</p>

<p>These infinitary relations have been formalized as "Kripke logical relations of varying arity", also called Jung-Tiuryn relations.  <a href="http://www.cs.bham.ac.uk/~axj/pub/papers/log-rel.ps.gz" rel="nofollow">Jung and Tiuryn have shown</a> that such infinitary parametricity is enough to characterize lambda-definability, and <a href="http://www.dcs.qmw.ac.uk/~ohearn/papers/pcf.ps.Z" rel="nofollow">O'Hearn and Riecke have shown</a> that it is enough to characterize fully abstract models for programming languages, including sequential PCF.  These are fundamental and beautiful results!</p>

<p>Thus, unary parametricity is the simplest, and least expressive, approximation of true parametricity, and binary parametricity gets a little better.  Your question is "how much better"?  My impression is that it is a <em>lot</em> better.  The reason is that, at the unary level, the "identity relation" is the every-true relation, which doesn't mean very much.  At the binary level, the "identity relation" is equality.  So, you get a sudden jump in the power of parametricity in going from the unary to binary level.  After that, it gets increasingly refined.</p>

<p>Kurt Sieber has studied these issues in some depth: for <a href="http://books.google.com/books?hl=en&amp;lr=&amp;id=7g5WU-D8RkIC&amp;oi=fnd&amp;pg=PA258&amp;dq=kurt+sieber&amp;ots=ZggRFB5YN7&amp;sig=WZZ21OVzuEi3ivZOnrOZaJ4zoEo" rel="nofollow">sequentiality</a> and for <a href="http://www.springerlink.com/index/p635542k74t2mg77.pdf" rel="nofollow">Algol-like languages</a>.</p>

CC BY-SA 3.0
2012-06-04T07:37:21.557Z
2012-06-04T07:37:21.557Z
Uday Reddy
<p>Probably the easiest paper to read for the applications of binary parametricity is Wadler's <a href="http://dl.acm.org/citation.cfm?id=99404" rel="nofollow">Theorems for Free!</a>.</p>

<p>Actually, I am a bit surprised by the question because binary parametricity is what is most often mentioned in parametricity papers.  Even the original Reynolds paper "Types, abstraction and parametric polymorphism" mentions it everywhere.  It is rather the unary parametricity that is not widely known.</p>

CC BY-SA 3.0
2012-05-25T12:30:29.013Z
That's a great paper, but I'm familiar with binary parametricity--what I wanted was a clear explanation of why binary parametricity is more powerful than unary parametricity.
Christopher Monsanto
CC BY-SA 3.0
2012-06-02T08:48:04.813Z
I have now added some elaboration, which I thought might have been obvious, but it isn't widely known.  So, it seems good to document it here.
Uday Reddy
CC BY-SA 3.0
2012-05-25T09:17:33.200Z
2012-06-04T07:38:12.960Z
2012-06-04T07:38:12.960Z
Uday Reddy
<p>Typically, you use binary parametricity to prove program equivalences. It's unnatural to do this with a unary model, since it only talks about one program at a time. </p>

<p>Normally, you use a unary model if all you are interested in is a unary property. For example, see our recent draft, <em><a href="http://www.mpi-sws.org/~neelk/icfp12-superficial-krishnaswami-turon-dreyer-garg.pdf">Superficially Substructural Types</a></em>, in which we prove a type soundness result using a unary model. Since soundness talks about the behavior of one program (if $e : A$  then it either diverges or reduces to a value $v : A$), a unary model is sufficient. If we wanted to prove program equivalences in addition, we would need a binary model. </p>

<p>EDIT: I just realized that if you look at our paper, it just looks like a plain old logical relations/realizability model. I should say a little bit more about what makes it (and other models) parametric. Basically, a model is parametric when you can prove the identity extension lemma for it: that is, for any type expression, if all of the free type variables are bound to identity relations, then the type expression is the identity relation. We don't explicitly prove it as a lemma (I don't know why, but you rarely need to when doing operational models), but this property is essential for our language's soundness.</p>

<p>The definition of "relation" and "identity relation" in parametricity is actually a bit up for grabs, and this freedom is actually essential if you want to support fancy types like higher kinds or dependent types, or wish to work with fancier semantic structures. The most accessible account of this I know is in Bob Atkey's draft paper <a href="https://personal.cis.strath.ac.uk/robert.atkey/fomega-parametricity.html"><em>Relational Parametricity for Higher Kinds</em></a>. </p>

<p>If you have a good appetite for category theory, this was first formulated in an abstract way by Rosolini in his paper <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.9972"><em>Reflexive Graphs and Parametric Polymorphism</em></a>. It has since been developed further by Dunphy and Reddy in their paper <a href="http://www.cs.bham.ac.uk/~udr/papers/parametric.pdf"><em>Parametric Limits</em></a>, and also by Birkedal, Møgelberg, and Petersen in <a href="http://dl.acm.org/citation.cfm?id=1316367"><em>Domain-theoretical Models of Parametric Polymorphism</em></a>. </p>

CC BY-SA 3.0
2012-05-25T05:39:39.297Z
2012-05-25T08:54:14.863Z
2012-05-25T08:54:14.863Z
Neel Krishnaswami
<p>I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( <a href="https://dl.acm.org/citation.cfm?id=2359499" rel="noreferrer">https://dl.acm.org/citation.cfm?id=2359499</a>). In this paper, they internalize unary parametricity in a pure type system with dependent types and hint at how you can extend the construction to arbitrary arities. </p>

<p>I've only seen binary parametricity defined before. My question is: what is an example of an interesting theorem that can be proved using binary parametricity, but not with unary parametricity? It would also be interesting to see an example of a theorem provable with tertiary parametricity, but not with binary (although I've seen evidence that n-parametricity is equivalent for n >= 2: see <a href="http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/art/par-tlca.ps.gz" rel="noreferrer">http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/art/par-tlca.ps.gz</a>)</p>

CC BY-SA 4.0
2023-11-08T16:57:24.837Z
The second link appears to be broken; is it https://doi.org/10.1007/3-540-62688-3_46?
Mike Shulman
<lo.logic><pl.programming-languages><type-systems><logical-relations><parametricity>
Unary parametricity vs. binary parametricity
Christopher Monsanto
# Unary parametricity vs. binary parametricity

(Asked by: username_0 on 2012-05-25)

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( <https://dl.acm.org/citation.cfm?id=2359499>). In this paper, they internalize unary parametricity in a pure type system with dependent types and hint at how you can extend the construction to arbitrary arities.

I've only seen binary parametricity defined before. My question is: what is an example of an interesting theorem that can be proved using binary parametricity, but not with unary parametricity? It would also be interesting to see an example of a theorem provable with tertiary parametricity, but not with binary (although I've seen evidence that n-parametricity is equivalent for n >= 2: see <http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/art/par-tlca.ps.gz>)

**Tags:** lo.logic, pl.programming-languages, type-systems, logical-relations, parametricity

> **Comments:**
> **username_1**: The second link appears to be broken; is it https://doi.org/10.1007/3-540-62688-3_46?  

---

## 4 answers

### Answer by username_4 on 2012-05-25. Score: 12 | Accepted answer

Typically, you use binary parametricity to prove program equivalences. It's unnatural to do this with a unary model, since it only talks about one program at a time.

Normally, you use a unary model if all you are interested in is a unary property. For example, see our recent draft, *[Superficially Substructural Types](http://www.mpi-sws.org/~neelk/icfp12-superficial-krishnaswami-turon-dreyer-garg.pdf)*, in which we prove a type soundness result using a unary model. Since soundness talks about the behavior of one program (if $e : A$ then it either diverges or reduces to a value $v : A$), a unary model is sufficient. If we wanted to prove program equivalences in addition, we would need a binary model.

EDIT: I just realized that if you look at our paper, it just looks like a plain old logical relations/realizability model. I should say a little bit more about what makes it (and other models) parametric. Basically, a model is parametric when you can prove the identity extension lemma for it: that is, for any type expression, if all of the free type variables are bound to identity relations, then the type expression is the identity relation. We don't explicitly prove it as a lemma (I don't know why, but you rarely need to when doing operational models), but this property is essential for our language's soundness.

The definition of "relation" and "identity relation" in parametricity is actually a bit up for grabs, and this freedom is actually essential if you want to support fancy types like higher kinds or dependent types, or wish to work with fancier semantic structures. The most accessible account of this I know is in Bob Atkey's draft paper [*Relational Parametricity for Higher Kinds*](https://personal.cis.strath.ac.uk/robert.atkey/fomega-parametricity.html).

If you have a good appetite for category theory, this was first formulated in an abstract way by Rosolini in his paper [*Reflexive Graphs and Parametric Polymorphism*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.9972). It has since been developed further by Dunphy and Reddy in their paper [*Parametric Limits*](http://www.cs.bham.ac.uk/~udr/papers/parametric.pdf), and also by Birkedal, Møgelberg, and Petersen in [*Domain-theoretical Models of Parametric Polymorphism*](http://dl.acm.org/citation.cfm?id=1316367).


---

### Answer by username_2 on 2012-05-30. Score: 5

This should be a comment to Neel's answer, but it's a bit long. Prompted by a hint from Rasmus Petersen, I found the following in Møgelberg's thesis (emphasize mine):

> Ivar Rummelhoff [36] has studied the encoding of natural numbers in
> per-models over different PCA’s, and showed that in some of these
> models, the encoding contains more than natural numbers. So these
> models cannot be parametric. *Even though he does not mention it, this
> shows that unary parametricity is different from binary (relational)
> parametricity, since one can easily show that the encoding of the
> natural numbers in any per-model is unary parametric.*

The cited paper is [Polynat in PER-models](http://scholar.google.co.uk/scholar?q=polynat%20in%20per%20models).


---

### Answer by username_3 on 2012-06-04. Score: 4

Let me a bit more abstract in answering this. At each arity $n$, you have the following situation: $n$-ary relations $R$ can be embedded into $(n+1)$-ary relations by defining $R'(\vec{x},y) \iff R(\vec{x}) \land y = x\_i$ (for some fixed $i \in [1..n]$). In words, you can use some $n$ arguments out of the $n+1$ arguments for simulating the smaller relation and make the new argument equal to some old one. (Note that *equality* is key to doing this.) So, you have "more" relations at arity $n+1$ than you had at arity $n$, and this goes on *ad infinitum*. Since more relations means stronger parametricity and fewer function families would be regarded "parametric", we understand that "true parametricity" is what we obtain in the limit, and each finitary parametricity is an approximation to it.

These infinitary relations have been formalized as "Kripke logical relations of varying arity", also called Jung-Tiuryn relations. [Jung and Tiuryn have shown](http://www.cs.bham.ac.uk/~axj/pub/papers/log-rel.ps.gz) that such infinitary parametricity is enough to characterize lambda-definability, and [O'Hearn and Riecke have shown](http://www.dcs.qmw.ac.uk/~ohearn/papers/pcf.ps.Z) that it is enough to characterize fully abstract models for programming languages, including sequential PCF. These are fundamental and beautiful results!

Thus, unary parametricity is the simplest, and least expressive, approximation of true parametricity, and binary parametricity gets a little better. Your question is "how much better"? My impression is that it is a *lot* better. The reason is that, at the unary level, the "identity relation" is the every-true relation, which doesn't mean very much. At the binary level, the "identity relation" is equality. So, you get a sudden jump in the power of parametricity in going from the unary to binary level. After that, it gets increasingly refined.

Kurt Sieber has studied these issues in some depth: for [sequentiality](http://books.google.com/books?hl=en&lr=&id=7g5WU-D8RkIC&oi=fnd&pg=PA258&dq=kurt+sieber&ots=ZggRFB5YN7&sig=WZZ21OVzuEi3ivZOnrOZaJ4zoEo) and for [Algol-like languages](http://www.springerlink.com/index/p635542k74t2mg77.pdf).


---

### Answer by username_3 on 2012-05-25. Score: 2

Probably the easiest paper to read for the applications of binary parametricity is Wadler's [Theorems for Free!](http://dl.acm.org/citation.cfm?id=99404).

Actually, I am a bit surprised by the question because binary parametricity is what is most often mentioned in parametricity papers. Even the original Reynolds paper "Types, abstraction and parametric polymorphism" mentions it everywhere. It is rather the unary parametricity that is not widely known.

> **Comments:**
> **username_0**: That's a great paper, but I'm familiar with binary parametricity--what I wanted was a clear explanation of why binary parametricity is more powerful than unary parametricity.  
> **username_3**: I have now added some elaboration, which I thought might have been obvious, but it isn't widely known.  So, it seems good to document it here.  

---

