# Is Linear Evaluation Parametric?

Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of Logical relations and parametricty: A Reynolds programme for Category Theory and Programming Languages.

In a linear type system, I believe the evaluation function $$ev_{AB} : (A \multimap B) \otimes A \to B$$ should be parametric because it is defined independently of $$A$$ and $$B$$. Indeed, the paper states:

The “$$evaluation$$” map $$ev_{AB} : [A \to B] \times A \to B$$ given by $$ev(f, x) = f (x)$$ is similarly parametric in both $$A$$ and $$B$$ (as opposed to just $$B$$).

The reader will be able to construct similar examples for the internal homs in other closed categories.

However, I wasn't able to see how this result applies to general closed categories. In particular, it seems to fail for vector spaces. Fix some vector space $$V$$ and consider the evaluation map $$ev_A : (A \multimap V) \otimes A \to V$$.

Let $$k$$ be the base field and consider how $$ev_k$$ and $$ev_0$$ must be related. In particular, consider the linear relation $$R : k \leftrightarrow 0$$ which relates every $$x \in k$$ with $$0$$. Then I believe any $$\varphi \otimes l \in (k \multimap V) \otimes k$$ is related by $$(R \multimap V) \otimes R$$ to $$0 \in (0 \multimap V) \otimes 0$$. Then by parametricity, $$ev$$ sends related things to equal things in $$V$$. It must send $$\varphi \otimes l$$ to $$0$$, so it is not evaluation.

It seems like evaluation should still be parametric even when using linear types. Is there good explanation for why the expected free theorem fails to hold?

• $(R ⊸ V)[φ, ψ] = ∀ s\ t. R(s,t) → φ(s) = ψ(t)$, no? So, $(R ⊸ V)[φ,0] = ∀ s\ t. φ(s) = 0$? I.E. only the $0$ function $k → V$ is related to $0$, and evaluation of the $0$ function gives $0$? Jul 8 at 16:53

Here's an Agda formalization of the non-linear version of your argument, and my comment above:

open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

variable
A B C D : Set

ev : (A -> B) × A -> B
ev (f , x) = f x

Rel : Set -> Set -> Set₁
Rel A B = A -> B -> Set

[_⇒_] : Rel A B -> Rel C D -> Rel (A -> C) (B -> D)
[ R ⇒ S ] f g = ∀ a b → R a b -> S (f a) (g b)

[_×_] : Rel A B -> Rel C D -> Rel (A × C) (B × D)
[ R × S ] (w , x) (y , z) = R w y × S x z

module Parametricity
(pev : ∀{A B C D}
→ (R : Rel A B) (S : Rel C D)
→ [ [ [ R ⇒ S ] × R ] ⇒ S ] ev ev)
where

R : Rel A ⊤
R _ _ = ⊤

lemma₀ : (φ : A -> B) (g : ⊤ -> B) (x : A)
→ [ R ⇒ _≡_ ] φ g
→ ev (φ , x) ≡ g tt
lemma₀ φ g x p = pev R _≡_ (φ , x) (g , tt) (p , tt)

lemma₁ : ∀(φ : A -> B) (g : ⊤ -> B) → [ R ⇒ _≡_ ] φ g → ∀ x → φ x ≡ g tt
lemma₁ φ y p x = p x tt tt


The only real difference is that there isn't a unique function $$⊤ → A$$. But, nevertheless, if we assume that all functions $$A → B$$ are related to a function $$g : ⊤ → B$$ via $$R → B$$, then we get that $$\mathsf{ev}(f, x) = g\ \mathsf{tt}$$ for arbitrary $$x$$. Similarly, every function related by $$R → B$$ to $$g$$ is constant.

Just because $$R$$ relates all values of $$A$$ to the single value of $$⊤$$ does not mean that $$R → B$$ relates all functions with type $$A → B$$ to a given function with type $$⊤ → B$$. Only the constant functions with matching output are related. In the linear case, this is reduced down to the $$0$$ function.