3
$\begingroup$

Just like the title says, how to prove that equation? The equation basically says that there is only one function a -> M a parametric in both M and a. I am not very familiar with proofs involving parametricity. Only simple ones, like proving that there is only one parametric identity function. Or that church booleans are equivalent to inductively defined booleans. There is one catch though. We can't prove it using initiality of Id in the category of monads, because I want to prove initiality via the sought equation.

Edit: A more vigorous formulation of the goal statement I want to prove:

//Fix the category of types and functions — Type

//Functor is an endofunctor on Type

//Given a functor F and a type a
//we write
F a : 𝕌
//to represent the functorial action of F on object a.

//Given a functor F and a function f : a → b
//we write
F f : F a → F b
//to represent the functorial action of F on morhism f.

//Notation:
M⁰ a = a
M¹⁺ⁿ a = M (Mⁿ a)

//Monad is a Functor M with additional two functions:
pure : ∀a. a → M a
join : ∀a. M² a → M a
//which satisfy the following laws:
(x : a) ⊦ M f (pure x) = pure (f x)            } naturality laws
(t : M² a) ⊦ M f (join t) = join (M² f t)      }

(t : M a) ⊦ join (pure t) = t                  }
(t : M a) ⊦ join (M pure t) = t                } monoid laws
(t : M³ a) ⊦ join (M join t) = join (join t)   }

//Define a category of Monads:
//Objects are monads
//Arrows are functions f : ∀a. M a → N a
//that additionally have the following properties:
(x : a) ⊦ f (pure x) = pure x : N a
(t : M² a) ⊦ f (join t) = join (f (M f t) : N² a) : N a
(α : a → b) (t : M a) ⊦ f (M α t) = N α (f t) : N b

//Isomorphism between types A and B is a pair of both-way functions between A and B that compose to identity in both ways.

//The goal is to prove:
(∀(M : Monad). ∀a. a → M a) ≅ 𝟙
//In english: the space of functions that for arbitrary monad M, arbitrary type a take an element of a to an element of M a is
//isomorphic to one element space (𝟙).

```
$\endgroup$
3
  • 5
    $\begingroup$ Please provide a context in which this question makes sense. The statement in the title looks like something that one migth write in a polymorphic calculus of some sort, but you did not say which one. You should also define what Monad stands for, precisely, and what notion of isomorphism you are using. $\endgroup$ Oct 7, 2023 at 8:52
  • $\begingroup$ You can assume that the statement is formulated against a constructive extensional dependent type theory with quotient types and an open universe. If we ever need to be more concrete, we can fix a theory. $\endgroup$
    – Russoul
    Oct 15, 2023 at 10:47
  • $\begingroup$ Updated the question to reflect the statement more rigorously $\endgroup$
    – Russoul
    Oct 15, 2023 at 10:54

3 Answers 3

0
$\begingroup$

I have a partial solution. But I got stuck.

//Define a quotient inductive type:
data FreeMonad : 𝕌 → 𝕌 where
  Map : (a → b) → FreeMonad a → FreeMonad b
  Pure : a → FreeMonad a
  Join : FreeMonad² a → FreeMonad a
  //Define Bind
  Bind : FreeMonad a → (a → FreeMonad b) → FreeMonad b
  Bind t f = Join (Map f t)

  //Functor laws
  (t : FreeMonad a) ⊦ Map id t = t : FreeMonad a
  (t : FreeMonad a) ⊦ Map (g ∘ f) t = Map g (Map f t) : FreeMonad a

  //Define
  Map² f = Map (Map f)

  //naturality laws
  Map f (Pure x) = Pure (f x) : FreeMonad a
  (t : FreeMonad² a) ⊦ Map f (Join t) = Join (Map² f t) : FreeMonad a

  //Monoid laws
  (t : FreeMonad a) ⊦ Join (Pure t) = t : FreeMonad a
  (t : FreeMonad a) ⊦ Join (Map Pure t) = t : FreeMonad a
  (t : FreeMonad³ a) ⊦ Join (Map Join t) = Join (Join t) : FreeMonad a


//Let's prove that
(t : FreeMonad a) ⊦ Bind t Pure = t : FreeMonad a
                    Join (Map Pure t) = t ✔

//Let's prove that
(x : a) ⊦ Bind (Pure x) f = f x : FreeMonad b
          Join (Map f (Pure x)) = f x
          Join (Pure (f x)) = f x
          f x = f x ✔

//Let's prove that
(t : FreeMonad a) ⊦ (do y ← (do x ← t; f); g) = (do x ← t; y ← f; g) : FreeMonad a
                    Join (Map (y ↦ g) (do x ← t; f)) = Join (Map (x ↦ do y ← f; g) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (x ↦ Join (Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map (Join . (x ↦ Map (y ↦ g) f)) t)
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Map Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Map (y ↦ g) (Join (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Join (Join (Map² (y ↦ g) (Map (x ↦ f) t))) = Join (Join (Map (x ↦ Map (y ↦ g) f) t))
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g) . (x ↦ f)) t
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map (Map (y ↦ g)) (Map (x ↦ f) t)
                    Map² (y ↦ g) (Map (x ↦ f) t) = Map² (y ↦ g) (Map (x ↦ f) t) ✔


//FreeMonad satisfies functor laws and monad laws. 

//define
interp : ∀(M : Monad). FreeMonad a → M a 
interp M (Pure x) = pure x
interp M (Map f t) = M f (interp M t)
interp M (Join t) = join (M (interp M) (interp M t))

interp M (Map id t) = interp M t 
M id (interp M t) = interp M t
interp M t = interp M t ✔

interp M (Map (g ∘ f) t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = interp M (Map g (Map f t)) 
M (g ∘ f) (interp M t) = M g (interp M (Map f t)) 
M (g ∘ f) (interp M t) = M g (M f (interp M t)) 
M g (M f (interp M t)) = M g (M f (interp M t)) ✔ 

interp M (Map f (Pure x)) = interp M (Pure (f x))
M f (interp M (Pure x)) = pure (f x)
M f (pure x) = pure (f x)
pure (f x) = pure (f x) ✔

interp M (Map f (Join t)) = interp M (Join (Map² f t))
M f (join (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
join (M² f (M (interp M) (interp M t))) = join (M (interp M) (interp M (Map² f t)))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map² f t))
M² f (M (interp M) (interp M t)) = M (interp M) (interp M (Map (Map f) t))
M² f (M (interp M) (interp M t)) = M (interp M) (M (Map f) (interp M t))
M² f (M (interp M) (interp M t)) = M (interp M . Map f) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f . interp M) (interp M t)
M² f (M (interp M) (interp M t)) = M (M f) (M (interp M) (interp M t))
M² f (M (interp M) (interp M t)) = M² f (M (interp M) (interp M t)) ✔

(t : FreeMonad a) ⊦ interp (Join (Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Pure t))) = interp M t
                    join (M (interp M) (pure t)) = interp M t
                    join (pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad a) ⊦ interp M (Join (Map Pure t)) = interp M t : M a
                    join (M (interp M) (interp M (Map Pure t))) = interp M t
                    join (M (interp M) (M Pure (interp M t))) = interp M t
                    join (M (interp M . Pure) (interp M t)) = interp M t
                    join (M pure (interp M t)) = interp M t
                    interp M t = interp M t ✔
                    
(t : FreeMonad³ a) ⊦ interp (Join (Map Join t)) = interp (Join (Join t)) : M a
                     join (M (interp M) (interp M (Map Join t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M) (M Join (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (M (interp M . Join) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M (join . M (interp M) . interp M) (interp M t)) = join (M (interp M) (interp M (Join t)))
                     join (M join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (interp M (Join t)))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (M (interp M) (join (M (interp M) (interp M t))))
                     join (join (M (M (interp M) . interp M) (interp M t))) = join (join (M² (interp M) (M (interp M) (interp M t))))
                     M (M (interp M) . interp M) (interp M t) = M² (interp M) (M (interp M) (interp M t))
                     M (M (interp M) . interp M) (interp M t) = M (M (interp M)) (M (interp M) (interp M t))
                     M (M (interp M)) (M (interp M) (interp M t)) = M (M (interp M)) (M (interp M) (interp M t)) ✔


//Note that interp is automatically a natural transformation (preserves map) and
//a monad morphism (moreover preserves pure and join).

//Let's show that interp is a unique monad morphism 
(M : Monad) (μ : FreeMonad ⇝ M) ⊦ μ = interp M : ∀a. FreeMonad a → M a  
//By function extensionality
(M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad a) ⊦ μ t = interp M t : M a  
//By induction on t
* (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (x : a) ⊦ μ (Pure x) = interp M (Pure x)  
  //by definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (x : a) ⊦ μ (Pure x) = pure x
  //by properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (x : a) ⊦ pure x = pure x ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = interp M (Map f t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad a) (f : a → b) ⊦ μ (Map f t) = Map f (interp M t)
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad a) (f : a → b) ⊦ M f (μ t) = M f (interp M t)
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad a) (f : a → b) ⊦ μ t = interp M t 
  //By induction hypothesis
  ✔
  
* (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad² a) ⊦ μ (Join t) = interp M (Join t) : M b  
  //By definition of interp
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad² a) ⊦ μ (Join t) = join (M (interp M) (interp M t))
  //By properties of a monad morphism
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad² a) ⊦ join (M μ (μ t)) = join (M (interp M) (interp M t))
  //congruence
  (M : Monad) (μ : FreeMonad ⇝ M) (a : 𝕌) (t : FreeMonad² a) ⊦ M μ (μ t) = M (interp M) (interp M t)
  //By induction hypothesis
  ✔

//Hence FreeMonad is the initial object in the category of monads.

//Let's show that FreeMonad and Id are isomorphic objects of the category of monads.

//There is a monad morphism:
pure : ∀a. Id a → FreeMonad a

//interp gives us a morphism in other direction:
interp Id : ∀a. FreeMonad a → Id a

interp Id . pure = pure = id //follows immediately from definition of interp

pure . interp Id = id
//By function extensionality
(t : FreeMonad a) ⊦ pure (interp Id t) = t
//By induction on t
* (x : a) ⊦ pure (interp Id (Pure x)) = Pure x
            pure (pure x) = Pure x
            pure (id x) = Pure x
            pure x = Pure x
            Pure x = Pure x ✔
* (t : FreeMonad a) (f : a → b) ⊦ pure (interp Id (Map f t)) = Map f t
                                  pure (Id f (interp Id t)) = Map f t
                                  //pure is a natural transformation
                                  Map f (pure (interp Id t)) = Map f t
                                  //By induction hypothesis
                                  Map f t = Map f t ✔
* (t : FreeMonad² a) ⊦ Pure (interp Id (Join t)) = Join t
                       Pure (join (Id (interp Id) (interp Id t))) = Join t
                       //pure preserves join
                       Join (pure (Id pure (Id (interp Id) (interp Id t)))) = Join t
                       Join (pure (Id pure (interp Id (interp Id t)))) = Join t
                       Join (interp Id (interp Id t)) = Join t
                       Join (interp Id t) = Join t
                       Join t = Join t ✔

//Hence Id and FreeMonad are isomorphic objects of the monad category.

∀M. ((∀a. a → M a) ≅ 𝟙)
≅
∀M. ((∀a. Id a → M a) ≅ 𝟙)
≅
∀M. ((∀a. FreeMonad a → M a) ≅ 𝟙)
//I am stuck
//We know that the set of monad morphisms (Free ⇝ M) is isomorphic to singleton set but we can't say the same about
//merely functions (∀a. FreeMonad a → M a)

```
$\endgroup$
21
  • 1
    $\begingroup$ Your goal seems to be to avoid proving directly (via monad laws) that Id is an initial object in the category of monads. But I don't see how your proof is different. You defined FreeMonad and then you need to prove that there is a unique monad morphism from FreeMonad to M. You showed one such monad morphism. How are you going to prove that it is unique; that any other monad morphism FreeMonad -> M is equal to that one? If you have a proof of that, you can just as easily prove that there is a unique monad morphism Id -> M. $\endgroup$
    – winitzki
    Oct 4, 2023 at 12:11
  • 1
    $\begingroup$ I do not know enough about the theory that proves how your FreeMonad code is actually constructing an initial object. Your FreeMonad is not the same as the usual free monad construction (which takes an arbitrary given functor F and wraps it into some structure in order to obtain a free monad on F). Could you give a reference? Also, it's not clear to me how you prove that pure . interp = id. (The other direction is easy, interp . pure = id.) $\endgroup$
    – winitzki
    Oct 4, 2023 at 17:23
  • 1
    $\begingroup$ I do not understand the definition of FreeMonad. How are a and b quantified? Please write explicitly for every variable appearing what it ranges over and where it's introduced (and how it's quantified). Furthermore, in order to have a monad there has to be an underlying functor. What is it? $\endgroup$ Oct 5, 2023 at 18:07
  • 1
    $\begingroup$ Slight abuse? If you want to be understood, you should change both the notation and the title. Or at the very least put up a very, very big warning that you're abusing accepted terminology. $\endgroup$ Oct 7, 2023 at 8:49
  • 1
    $\begingroup$ I know of two uses of "monad", in category theory and in functional programming, both of which presume an underlying functor. Indeed, it is beginning to look like your question is misleading because of strange terminology. $\endgroup$ Oct 8, 2023 at 8:01
0
$\begingroup$

I think I found a better proof.

Simplify $(\forall a. a \to M\, a) \cong M\, \mathbb 1$

This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:

Yoneda lemma: For any fixed object $X$ of a category $C$, define the hom-functor $\textrm{Hom}(X, \_)$ as a functor from $C$ to the category of sets; it maps an object $A$ to the set $\textrm{Hom}(X, A)$ of all morphisms between $X$ and $A$. So, $\textrm{Hom}(X, \_)$ is a set-valued functor. For any other set-valued functor $M$ from CT to the category of sets, the set of all natural transformations of type $\textrm{Hom}(X, \_) \to M$ is equivalent to the set $M(X)$.

If we use the Yoneda lemma for the category CT, we interpret a covariant type constructor $M$ as a set-valued functor from CT to the category of sets (since all types are sets). The hom functor for a type $X$ is the type constructor $H\,A = X\to A$. The set of natural transformations from $H$ to $M$ is the type $\forall a.\,H\,a\to M\, a$ under assumptions of full parametricity.

Then the Yoneda lemma gives the following type equivalence:

$$ \forall a. (x \to a) \to M\,a \cong M\,x $$

To obtain $\forall a. a \to M\, a \cong M\, \mathbb 1$, we use the Yoneda lemma with $x = \mathbb 1$.

So, it remains to prove that $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

Use a theorem by Jaskelioff and O'Connor

The paper https://arxiv.org/pdf/1402.1699.pdf proves the following identity:

(Equation 6.1 in section 6)

$$\forall (M: \mathrm{Monad}). \forall (a, b, x: \mathrm{Type}). (a \to M\, b) \to M\, x \cong \mathrm{Free} \,(R \,a\, b) \,x $$

where $R \, a \, b$ is defined by $R \, a \, b \, x = a \times (b \to x)$ (it is a covariant endofunctor in $x$) and "Free F" is the free monad on a covariant endofunctor $F$. The free monad construction is a covariant endofunctor $\mathrm{Free}\, F$ defined as a recursive type by:

$$ \mathrm{Free}\, F\, a = a + F\, (\mathrm{Free}\, F\, a) $$

or using the $\mu$ (least fixpoint) notation:

$$ \mathrm{Free}\, F\, a = \mu \,r.\, (a + F\, r) $$

So, we can rewrite the identity as:

$$\forall (a, b, x: \mathrm{Type}). \forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \mu\,r.\, (x + a \times (b\to r)) $$

Now we will substitute some suitable types for $a$, $b$, $x$ so that the left-hand side of the identity gives what we want: $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

We set $a = \mathbb0$, $x = \mathbb1$ and we find:

$$ (a \to M\, b) \to M\, x \cong (\mathbb0 \to M\, b) \to M\, \mathbb1 \cong \mathbb1 \to M\, \mathbb1 \cong M\,\mathbb1 $$

so:

$$\forall (M: \mathrm{Monad}). (a \to M\, b) \to M\, x \cong \forall (M: \mathrm{Monad}). M\, \mathbb1 $$

Then we substitute $a = \mathbb0$, $x = \mathbb1$ into the right-hand side of the identity and get:

$$ \mu\,r.\, (x + a \times (b\to r)) = \mu\,r.\, (\mathbb1 + \mathbb0 \times (b\to r)) = \mu\,r.\,\mathbb1=\mathbb1 $$

This completes the proof.

$\endgroup$
-1
$\begingroup$

This proof is most likely incorrect and is left here only for reference!

Here is a derivation of $\forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1$ based on parametricity.

Preliminaries

The type $\forall (M:\textrm{Monad}). \forall a. a \to M\, a$ is a type of functions with type parameters $M$ and $a$. In addition, there is a typeclass constraint on the type parameter $M$: the type constructor $M$ must be a monad.

We require that the code of those functions must be purely functional and "fully parametric": the type parameters $M$ and $a$ are used as opaque unknown arbitrary types about which no information may be used. (For example, the code may not try to discover the actual types of $a$ and $M$ using run-time type reflection that some programming languages support. We should imagine that all code is written purely in System F$\omega$ or something similar.) This means the code may use only the monad $M$'s methods, without using any other information about the type $M$. (There is no information at all about the type parameter $a$.)

The assumptions of "full parametricity" about the code allow us to use the parametricity theorems. One consequence of the parametricity theorems is that any fully parametric code with type signature $\forall x.\, F\, x \to G\,x$ (where $F$ and $G$ are covariant type constructors) will automatically satisfy the law of a natural transformation. The natural transformation is between functors $F$ and $G$ that will arise when we translate that code into the language of category theory.

We will use two categories here:

  1. The category of types: objects are all System F$\omega$'s ground types (i.e. types of kind $*$) and morphisms are all functions implementable as terms in System F$\omega$. We will denote this category by CT.

  2. The category of endofunctors in the category of types. Endofunctors correspond to type constructors in the programming language (types of kind $*\to*$). We will denote this category by Endo(CT).

So, the programming language notation $\forall a.\, F\, a \to G\,a$ under assumptions of full parametricity means the type of natural transformations between $F$ and $G$ where $F$ and $G$ are endofunctors in CT.

Similarly, the programming language notation $\forall (M:\textrm{Monad}). F\,M \to G\,M$ means the type of natural transformations between some functors $F$, $G$. For our usage, those functors will be between Endo(CT) and CT.

Finally, the programming language will have to implement all types as sets (actually, as countable sets because the byte size of any value in memory must be finite). So, the category of types CT is in some way embedded into the category of sets.

Simplify $(\forall a. a \to M\, a) \cong M\, \mathbb 1$

This can be shown quickly (without directly dealing with relational parametricity) via the Yoneda lemma:

Yoneda lemma: For any fixed object $X$ of a category $C$, define the hom-functor $\textrm{Hom}(X, \_)$ as a functor from $C$ to the category of sets; it maps an object $A$ to the set $\textrm{Hom}(X, A)$ of all morphisms between $X$ and $A$. So, $\textrm{Hom}(X, \_)$ is a set-valued functor. For any other set-valued functor $M$ from CT to the category of sets, the set of all natural transformations of type $\textrm{Hom}(X, \_) \to M$ is equivalent to the set $M(X)$.

If we use the Yoneda lemma for the category CT, we interpret a covariant type constructor $M$ as a set-valued functor from CT to the category of sets (since all types are sets). The hom functor for a type $X$ is the type constructor $H\,A = X\to A$. The set of natural transformations from $H$ to $M$ is the type $\forall a.\,H\,a\to M\, a$ under assumptions of full parametricity.

Then the Yoneda lemma gives the following type equivalence:

$$ \forall a. (x \to a) \to M\,a \cong M\,x $$

To obtain $\forall a. a \to M\, a \cong M\, \mathbb 1$, we use the Yoneda lemma with $x = \mathbb 1$.

So, it remains to prove that $\forall (M:\textrm{Monad}). M\,\mathbb 1 \cong \mathbb 1$.

From monads to pointed endofunctors

It is easier to prove a stronger statement: instead of the Monad typeclass, we require only a Pointed typeclass. An endofunctor $F$ is pointed if there exists a natural transformation of type $\textrm{Id} \to F$. In a programming language, this means there exists a value of type $\forall a. a\to F\,a$. This is equivalent to a value of type $F \, \mathbb 1$. There are no laws required for this value.

So, the requirement of having a pointed endofunctor ($F:\textrm{Pointed}$) is the same as assuming an existing value of type $F\,\mathbb 1$.

Then we will obtain the statement

$$ \forall (M:\textrm{Monad}). \forall a. a \to M\, a \cong \mathbb 1 $$

as a consequence of a stronger statement:

$$ \forall (F:\textrm{Pointed}).\, F\, \mathbb 1 \cong \mathbb 1$$

or equivalently:

$$ \forall (F:\textrm{Functor}). F\,\mathbb1\to F\,\mathbb1\cong\mathbb1$$

Now we have a simpler problem that can be solved by Yoneda lemma in the category Endo(CT).

The meaning of $\forall (F:\textrm{Functor})$

In order to use the Yoneda lemma, we need to formulate the last statement more clearly in terms of category theory.

In the programming language notation, a function of type $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$ is simply a function that is parameterized by a type constructor $F$ that is assumed to have a law-abiding fmap method (i.e., a covariant type constructor). Also, it is assumed that any function of type $\forall (F:\textrm{Functor}). (...)$ does not use any information about $F$ other than its fmap method.

The parametricity theorem says that such functions will satisfy a naturality law with respect to the type parameter $F$. This corresponds in the language of category theory to a natural transformation between functors from Endo(CT) to CT.

So, the programming language notation $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1)$ means the type of natural transformations $S\, F\to S\, F$ where we defined a functor $S$:Endo(CT)$\to$CT by $S\,F = F\,\mathbb 1$.

Shortcut for the proof

A shortcut is the following identity: for fixed types $b$ and $c$:

$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$

The paper https://arxiv.org/abs/1402.1699 has a more general result that also covers what we need:

$$ \forall (F:\textrm{Functor}). (a\to F\,b)\to F\,c \cong a\times(b\to c)$$

Setting $a=b=c=\mathbb1$, we obtain $\forall (F:\textrm{Functor}). (F\,\mathbb1\to F\,\mathbb1) \cong\mathbb1 \to\mathbb1 \cong \mathbb1$.

Yoneda lemma for endofunctors

Let's look at the identity:

$$ \forall (F:\textrm{Functor}). F\,b\to F\,c \cong b\to c$$

We can prove this using Yoneda lemma twice.

First, we want to reformulate this from the programming language notation into the category theory language. We want to rewrite the type of functions shown above as a type of some natural transformations like this:

$$ \forall F. P\,F \to Q\,F $$

In the language of category theory, this is the set $P \to Q$ of natural transformations between functors $P$, $Q$.

Between which functors $P$, $Q$ will those natural transformations work? In our case, we must have $P\,F = F\,b$ and $Q\,F = F\,c$. Clearly $P$ maps $F$ to a type from CT. So, we need to work with $P$, $Q$ that are functors from Endo(CT) to CT.

If we want to use the Yoneda lemma, we need a natural transformation between a hom-functor and some other functor. So, $P$ must be a hom-functor (but right now our $P$ is not of that form). The type $ \forall F. P\,F \to Q\,F $ must be of the form that Yoneda lemma requires, which looks like this:

$$ \forall F.\, \textrm{Hom}(X, F) \to Q\,F \cong Q\,X$$

Here $\textrm{Hom}(X, F)$ is the set of all morphisms between $X$ and $F$ in the category Endo(CT). Those morphisms are natural transformations between $X$ and $F$.

In the category theory notation, the Yoneda lemma in the category Endo(CT) is:

$$ \textrm{Hom}(X, \_) \to Q \cong Q\,X$$

Here we interpret $Q$ as a set-valued functor from Endo(CT) to the category of sets.

How can we rewrite $P\,F$ as $\textrm{Hom}(X, F)$? What is the endofunctor $X$ from Endo(CT) that fits here? To figure that out, write the types in the programming language notation:

$$ P\,F = F\,b \quad \textrm{but}\quad \textrm{Hom}(X, F) = \forall a.\,X\,a\to F\,a $$

We need to find $X$ such that $\forall a.\,X\,a\to F\,a \cong F\,b$.

We use the Yoneda lemma for the category CT to find:

$$\forall a.\,(b\to a)\to F\,a \cong F\,b$$

So, a suitable $X$ is the functor defined by the code $X\,a = b \to a$, or in the category theory notation, $X = \textrm{Hom}(b,\_)$.

With this $X$, we obtain $Q\,X =X\,c=\textrm{Hom}(b,c)$. In the programming language notation, this is just the type $b\to c$.

So, we have proved that the type of natural transformations $P\to Q$ is equivalent to the set $\textrm{Hom}(b,c)$ or, in the programming language notation, to the type $b\to c$.

$\endgroup$
17
  • 1
    $\begingroup$ Please specify the category on which you're using the Yoneda lemma, explain what universal quantification over "functors" is supposed to be, etc. $\endgroup$ Oct 7, 2023 at 8:51
  • $\begingroup$ @AndrejBauer I updated my answer. $\endgroup$
    – winitzki
    Oct 7, 2023 at 19:38
  • 1
    $\begingroup$ In "Preliminaries" you state that $M$ is a type parameter, but by the end of the paragraph you call it a "monad". Which is it? And if $M$ is indeed a type parameter, then why "$M : \mathrm{Monad}$"? Is $\mathrm{Monad}$ a synonym for $\mathrm{Type}$? $\endgroup$ Oct 8, 2023 at 8:04
  • 1
    $\begingroup$ In the category CT, do you mean only closed terms to be morphisms, and only closed types to be objects? What does it mean for two terms to be equal, precisely (whatever the answer, you must check that composition is associative)? $\endgroup$ Oct 8, 2023 at 8:07
  • $\begingroup$ @AndrejBauer I edited the answer to clarify the "Monad" $M$. As for the category CT, I do not know how to define everything completely rigorously down to axioms and first principles. I think both types and terms must be closed. But I don't know how to define equality and how to prove associativity. This probably needs some model and not just definitions about terms of System F$\omega$. This is a basic assumption underlying all reasoning in functional programming. Can you suggest papers or books where the category similar to CT is defined completely rigorously? $\endgroup$
    – winitzki
    Oct 8, 2023 at 15:08

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.