Parametricity of Linear Logic

Question

Are we able to prove a free parametricity theorems about functions like $f : \forall A . [A] ⊸ [A]$? It is supposed to state that $f$ takes a list and always returns a permutation of it.

Another example: prove that function $f : \forall A . (A ⊸ (A, A)) ⊸ [A] ⊸ [A]$ will always return a permuted list with exactly one element copied.

Answer 1

Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem here. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For example, if you have $A, x : [A], y : [A] \vdash e : [A]$, then in an ordered type system, $e$ must append the lists $x$ and $y$.

The short answer is that yes, we can prove your first example. In the context of lambda calculi, a logical relations-based approach is described in this paper. They would prove your theorem in two steps:

1. Define a relational interpretation of types and use it to prove a conventional free theorem completely ignoring linearity i.e. essentially using the same reasoning you see in, for example, “Theorems for Free!”. Given $\vdash f : \forall A . [A] \multimap [A]$, the usual free theorem tells us that $f$ returns a list which contains only elements that were present in the list it was given. Given a list of distinct free linear variables $x_1 \ldots x_n$, we deduce that $f [x_1, ..., x_n]$ evaluates to some list $[y_1, ..., y_m]$ where $\{y_1, \ldots, y_m\} \subseteq \{x_1, ..., x_n\}$.
2. Notice that free linear variables must be preserved under evaluation. This lets us take advantage of linearity. If $[y_1, \ldots, y_m]$ were not a permutation of $[x_1, ..., x_n]$, then it would imply that some $x_i$ were lost or duplicated during evaluation, which cannot happen.

But, these sorts of theorems get more interesting when we look at a language with effects and our ability to prove them for such languages is sadly limited. For example, consider the isomorphism $\tau \cong \forall A . (\tau \to A) \to A$ from System F. In a call-by-value setting, this isomorphism breaks when we add non-termination. We should be able to recover a similar isomorphism, though, with linear types: $\tau \cong \forall A . (\tau \to A) \multimap A$. Unfortunately, we do not have operational logical relations that can prove this.

That said, there are also syntactic methods that can prove both this isomorphism and your theorem. This seems to be a particularly useful approach in a linear setting, and is much less of a burden than setting up a logical relation for proving simple theorems.

Edit: Since you asked, here’s an example of a syntactic proof of a free theorem for the type $\forall A . (A \otimes A) \multimap A$ in a setting with a term $\bot$ that loops forever and is well-typed under any context at any type. The idea is to find a set of canonical terms of a type and use that to determine what the possible return values for a function are. We start with a soundness theorem for well-typed terms.

Theorem (Canonicity). If $\Delta; \Gamma \vdash e : \tau$ then either

• $e \approx v$, which is a value such that $\Delta; \Gamma \vdash v : \tau$.
• $e \approx n$, a term which is stuck because it is trying to use a free variable in $\Gamma$, and $\Delta; \Gamma \vdash n : \tau$ OR
• $e \approx \bot$

Here, $\approx$ is your favorite notion of equivalence for the language and $\Delta$ is an environment containing free type variables. I will consider free variables $x$ to be values. For simple languages, a straightforward progress & preservation argument can be made to justify this theorem.

Now, given a value $\vdash f : \forall A . (A \otimes A) \multimap A$, we know that $f \approx \lambda x . e$ where $A; x : (A \otimes A) \vdash e : A$. From the type of e, we have a couple possible cases:

• $e$ is equivalent to a pair $A; x : (A \otimes A) \vdash (v_1, v_2) : A$. This case is impossible since $v_1$ and $v_2$ must be values of type $A$, which is a free type variable. There are no such values because there are no variables in the context of type $A$.
• $e$ is equivalent to a term which tries to use the free variable $x$.
• $e$ diverges. This case gives us one possible value for $f$: $\lambda x . \bot$.

Since the second case is the only one left, we assume $e \approx\ \mathrm{let} (x_1, x_2) = x\ \mathrm{in}\ e’$ where $A; x_1 : A, x_2 : A \vdash e’ : A$. Thus far in the proof, we have established that $f \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ e’$. Finally, we apply our canonicity theorem one more time and find that $e’$ must diverge: the only values of type $A$ are variables but we have two variables in the context, so it cannot be the case that $e’ \approx x_i$.

Therefore, we have that the only inhabitant of $\forall A . (A \otimes A) \multimap A$ is $\lambda x . \bot \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ \bot$.

You asked for a reference for this sort of proof, but I’m not sure of a good one. This kind of reasoning is well-known in certain circles and goes back perhaps as far as Gentzen. I'm told that it is reminiscent of focused proof search for sequent calculus, but I don't know exactly what the connection is.

That said, I’m not aware of any modern published work that explains this relatively simple method well. Admittedly, it is a bit limited in its applicability to simpler languages. On the other hand, I think it has been overshadowed by “Theorems for Free!” et al and as a result even many senior researchers immediately think of logical relations when they hear the phrase “free theorem”, unaware that techniques like this can be a simpler alternative approach to such proofs (especially in the context of linear type systems).

As for your second example, I don’t think the free theorem you want actually holds. I could for example, instantiate $A$ with the integer type and then pass in a function that returns integers which are not in the list I give to $f$. Perhaps $\forall A. (\forall B. B \multimap (B, B)) \multimap [A] \multimap [A]$ is closer to the type you had in mind. But even then, no function of type $\forall B. B \multimap (B, B)$ exists since it would have to duplicate its input.