Is Linear Evaluation Parametric?

Question

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?

Answer 1

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.