Unary parametricity vs. binary parametricity 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)
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.