In this memo I outline how iterating parametricity generates hypercubes; each iteration adding another dimension.

The problem

Previously Patrik, Ross and I ¹ have shown that Reynold’s abstraction theorem is neatly expressed as a transformation of terms and judgements in type theory:

Γ ⊢ A : B ⇒ Γ! ⊢ A! : B! A

That is, if A has type B, then A satisfies the relational interpretation of the type B (written B! here). The proof of that fact is given by A!. Cherry on the cake: the proof is just the relational interpretation of A. In other words A! and B! are given by the same transformation of terms, written as a postfix !. The context Γ! is obtained by adding a witness of parametricity for each variable in Γ.

Usually, the abstraction theorem is presented in its binary version (two copies of A are related by the interpretation of B), but here we study the unary version.

In the above theorem, the judgement on the right of the implication arrow is in the same system as the judgement on the left. So, it seems natural to try and apply the theorem on that judgement again (effectively composing the theorem with itself). We obtain:

Γ ⊢ A : B ⇒ Γ!! ⊢ A!! : B!! A A! A!

To see that the above is indeed the iterated version, you should know that (B! A)! is convertible to B!! A A!.

We can go on and apply the basic theorem three times:

Γ ⊢ A : B ⇒ Γ!!! ⊢ A!!! : B!!! A A! A! A!! A! A!! A!!

(exercise: apply it four times! ☺)

The questions I want to address are:

1. what is the type of B!!!?
2. why are A! and A!! repeated, and how many times?
3. and in general: what is the pattern?

Iterated relational interpretatons

Let us examine a lemma related to the abstraction theorem, which essentially states that a type is interpreted as a (in our case) unary predicate. If A is a type, and x has type A, then A! x is a type as well (or, under Curry-Howard, a proposition). Hence A! is really a predicate.

Γ ⊢ A : ⋆ ⇒ Γ!, x : A ⊢ A! x : ⋆

Iterating that lemma yields the following statement, which says that A!! is a relation of arity 3, between an object x of type A, and two objects y₁ and y₂ of type A! x. (To see that the following is indeed the iterated version, note that the binding (x:A)! expands to the double binding x : A, y₁ : A! x and that y₂ in the below plays the role of x in the above lemma.)

Γ ⊢ A : ⋆ ⇒ Γ!!, x : A, y₁ : A! x, y₂ : A! x  ⊢ A!! x y₁ y₂ : ⋆

Another iteration yields (indented to align similar types):

Γ ⊢ A : ⋆ ⇒ Γ!!!, x : A, y₁ : A! x, 
                         y₂ : A! x, z₁ : A!! x y₁ y₂,
                         y₃ : A! x, z₂ : A!! x y₁ y₃,
                                    z₃ : A!! z y₂ y₃ 
           ⊢ A!!! x y₁ y₂ z₁ y₃ z₂ z₃ : ⋆

Quite a mouthful! To make sense of all this, let’s draw a graph where the variables are nodes and there is an arc between variables if the type of one depends on another.

The graph of the 1st level is trivial:

A single vertex

The 2nd one barely more interesting:

Two arcs

But the 3rd level gives more insight towards the general case:

A cube structure appears

In general, the structure of the arguments to a $n$-level relation forms an hypercube of dimension $n$ minus a vertex. A full $n$-cube has $2n$ faces; and the effect of removing this single vertex is to halve the number of faces, such that the graph of level $n$ has exactly $n$ faces. (For fun, try $n=4$.)

Conclusion

To sum it up, by iterating unary parametricity, one gets $n$-ary parametricity “for free”, with the catch that relations are between objects whose types have the structure of the faces of an $n$-cube.

Loose ends

As often, the devil is in the details, and I am guilty of leaving out most of them here. In fact, this memo is just an appetizer; in particular it is left to the reader to find out why cubic structures are consistently generated, and why a vertex is missing from cubes.