What is the relation of parametricity and function extensionality?

Question

In Agda function extensionality can be defined like this:
funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2
One may note a similarity in the definition of a (binary) logical relation
f1 [A -> B] f2 being:
∀ x1 x2 → x1 [A] x2 -> f1 x1 [B] f2 x2.

What is the relation of logical relations to function extensionality? Is there perhaps a relation to eta-equality?

• Joey Eremondi: Might be relevant, since Univalence implies extensionality: arxiv.org/abs/1909.05027

Answer 1

Indeed there is a similarity in these two definitions.

Function extensionality that you showed is just a condition that specifies when two functions are equal.

If we talk about logical relations then a relation between two functions of types $A \to B$ does not necessarily have to express equality between two functions. But the equality relation is a possible binary relation between functions. Let us see how we can formulate a logical relation that specifies that two functions (both of type $A \to B$) are equal.

Denote by $A \leftrightarrow B$ the type of relations between values of types $A$ and $B$. The identity relation for the type $A$ is denoted by $[\textrm{id}^A]: A \leftrightarrow A$.

The logical relation for the extensional equality is formulated like this: Two functions are equal when they are in the identity relation for the type $A \to B$. That identity relation is denoted by $[\textrm{id}^{A \to B}]$. Then we can rewrite the Agda definition of the extensional equality in the language of relations like this:

$f_1,円 [\textrm{id}^{A \to B}],円 f_2$ means $\forall x_1,,円 x_2$ if $ x_1 ,円[\textrm{id}^{A}],円 x_2$ then $f_1 (x_1) ,円[\textrm{id}^{B}],円 f_2 (x_2)$

Now we can further rewrite this definition via the function-type construction for relations. The function-type construction is defined like this: Given any two relations $[r] : A \leftrightarrow B$ and $[s]:C\leftrightarrow D $, we can define the relation $[r\to s]: (A \to C) \leftrightarrow (B \to D)$ by the formula similar to what you wrote: for any two functions $f: A\to C$ and $g: B\to D$, we have:

$f,円 [r\to s],円 g$ means $\forall x:A,,円 y:B$, if $ x ,円[r],円 y$ then $f(x) ,円[s],円 g(y)$

Now if we set $A=B$, $C = D$, $[r] = [\textrm{id}^A]$, and $[s] = [\textrm{id}^C]$, then we will get: $[r \to s] = [\textrm{id}^{A\to C}]$. So, the identity relation on functions is obtained by the function-type construction from identity relations on types A and B. That's all it seems to be.

• Neel Krishnaswami: This answer is totally correct, but let me add one additional comment. Parametric models satisfy the identity extension property: if $A[a]$ is a type with a free variable $a,ドル and $\mathsf{Id}_X$ is the identity relation for $X,ドル then $[\![ A[a] ]\!] (\mathsf{Id}_X/a) = \mathsf{Id}_{A[X]}$. This forces all parametric models to satisfy the condition above.
• winitzki: @NeelKrishnaswami It is hard for me to follow the notation in your comment. I will revise my answer a bit. I think the main point is that we must show a proof that [A -> B] = id follows from [A] = id and [B] = id, it does not follow automatically.
• Neel Krishnaswami: Sorry! I didn't think my commented warranted a whole new answer, but comments make it hard to use rich notation...
• winitzki: @NeelKrishnaswami I have rewritten my answer and introduced new notation. I showed the derivation now. I'm not an expert in programming language theory, and I don't really understand the notation or the substance of what's going on in Reynolds's papers. For example, you said that "parametric models" will satisfy the "identity extension lemma". I think a practical programmer will not need to worry about the details of the models of the programming language. A programmer would never expect the programming language to implement a model that doesn't satisfy the identity extension lemma.