Unary parametricity vs. binary parametricity

Question

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)

Answer 1

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

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. It has since been developed further by Dunphy and Reddy in their paper Parametric Limits, and also by Birkedal, Møgelberg, and Petersen in Domain-theoretical Models of Parametric Polymorphism.

Answer 2

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.

Answer 3

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 that such infinitary parametricity is enough to characterize lambda-definability, and O'Hearn and Riecke have shown 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 and for Algol-like languages.

Answer 4

Probably the easiest paper to read for the applications of binary parametricity is Wadler's Theorems for Free!.

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.