<p>Here's an Agda formalization of the non-linear version of your argument, and my comment above:</p>
<pre><code>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 -&gt; B) × A -&gt; B
ev (f , x) = f x

Rel : Set -&gt; Set -&gt; Set₁
Rel A B = A -&gt; B -&gt; Set

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

[_×_] : Rel A B -&gt; Rel C D -&gt; 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 -&gt; B) (g : ⊤ -&gt; B) (x : A)
         → [ R ⇒ _≡_ ] φ g
         → ev (φ , x) ≡ g tt
  lemma₀ φ g x p = pev R _≡_ (φ , x) (g , tt) (p , tt) 

  lemma₁ : ∀(φ : A -&gt; B) (g : ⊤ -&gt; B) → [ R ⇒ _≡_ ] φ g → ∀ x → φ x ≡ g tt
  lemma₁ φ y p x = p x tt tt
</code></pre>
<p>The only real difference is that there isn't a unique function <span class="math-container">$⊤ → A$</span>. But, nevertheless, if we assume that all functions <span class="math-container">$A → B$</span> are related to a function <span class="math-container">$g : ⊤ → B$</span> via <span class="math-container">$R → B$</span>, then we get that <span class="math-container">$\mathsf{ev}(f, x) = g\ \mathsf{tt}$</span> for arbitrary <span class="math-container">$x$</span>. Similarly, every function related by <span class="math-container">$R → B$</span> to <span class="math-container">$g$</span> is constant.</p>
<p>Just because <span class="math-container">$R$</span> relates all values of <span class="math-container">$A$</span> to the single value of <span class="math-container">$⊤$</span> does not mean that <span class="math-container">$R → B$</span> relates all functions with type <span class="math-container">$A → B$</span> to a given function with type <span class="math-container">$⊤ → B$</span>. Only the constant functions with matching output are related. In the linear case, this is reduced down to the <span class="math-container">$0$</span> function.</p>

CC BY-SA 4.0
2023-07-08T19:59:27.733Z
2023-07-08T19:59:27.733Z
Dan Doel
<p>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 <a href="https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf" rel="nofollow noreferrer">Logical relations and parametricty: A Reynolds programme for Category Theory and Programming Languages</a>.</p>
<p>In a linear type system, I believe the evaluation function <span class="math-container">$ev_{AB} : (A \multimap B) \otimes A \to B$</span> should be parametric because it is defined independently of <span class="math-container">$A$</span> and <span class="math-container">$B$</span>. Indeed, the paper states:</p>
<blockquote>
<p>The “<span class="math-container">$evaluation$</span>” map <span class="math-container">$ev_{AB} : [A \to B] \times A \to B$</span> given by
<span class="math-container">$ev(f, x) = f (x)$</span> is similarly parametric in both <span class="math-container">$A$</span> and <span class="math-container">$B$</span> (as
opposed to just <span class="math-container">$B$</span>).</p>
<p>The reader will be able to construct similar examples for the internal
homs in other closed categories.</p>
</blockquote>
<p>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 <span class="math-container">$V$</span> and consider the evaluation map <span class="math-container">$ev_A : (A \multimap V) \otimes A \to V$</span>.</p>
<p>Let <span class="math-container">$k$</span> be the base field and consider how <span class="math-container">$ev_k$</span> and <span class="math-container">$ev_0$</span> must be related. In particular, consider the linear relation <span class="math-container">$R : k \leftrightarrow 0$</span> which relates every <span class="math-container">$x \in k$</span> with <span class="math-container">$0$</span>. Then I believe any <span class="math-container">$\varphi \otimes l \in (k \multimap V) \otimes k$</span> is related by <span class="math-container">$(R \multimap V) \otimes R$</span> to <span class="math-container">$0 \in (0 \multimap V) \otimes 0$</span>. Then by parametricity, <span class="math-container">$ev$</span> sends related things to equal things in <span class="math-container">$V$</span>. It must send <span class="math-container">$\varphi \otimes l$</span> to <span class="math-container">$0$</span>, so it is not evaluation.</p>
<p>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?</p>

CC BY-SA 4.0
2023-07-08T16:53:08.107Z
$(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$?
Dan Doel
<type-theory><pl.programming-languages><ct.category-theory><parametricity><logical-relations>
Is Linear Evaluation Parametric?
vigenary
# Is Linear Evaluation Parametric?

(Asked by: username_0 on 2023-07-08)

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](https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf).

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?

**Tags:** type-theory, pl.programming-languages, ct.category-theory, parametricity, logical-relations

> **Comments:**
> **username_1**: $(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$?  

---

## 1 answers

### Answer by username_1 on 2023-07-08. Score: 4 | Accepted answer

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.


---

