3
$\begingroup$

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?

$\endgroup$
1
  • 1
    $\begingroup$ $(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$? $\endgroup$
    – Dan Doel
    Commented Jul 8, 2023 at 16:53

1 Answer 1

4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.