Checking that the State Monad is a Monad.

Question

$ T(X) = (S \to X\times S)$ $\mbox{fmap}:=\lambda f:A\to B. \lambda q\in T(A). \lambda s\in S. \langle(f\circ pr_1 \circ q)(s),(pr_2 \circ q)(s)\rangle$

I defined the following functions:

$\eta_a := \lambda a\in A. \lambda s\in S. \langle a,s\rangle$

$\mu_X := \lambda F:T^2X\to TX. \lambda s\in S. ((pr_1 \circ F)(s)) ((pr_2 \circ F)(s)))$

And successfully proved the this diagram's identities:

But on this one I got stuck:

https://en.wikipedia.org/wiki/Monad_(category_theory)

I have a $p \in T^3X$, and I think I need to prove that $\mu_X (\mbox{fmap}(\mu_X)(p))=\mu_X (\mu_{TX} (p))$.

But I but i feel like I don't know how to prove this equality even after unfolding the definitions.

Answer 1

Perhaps a simpler way to prove that the state monad is a monad is to derive the adjunction that gives rise to the monad.

In this case, the adjoint functors are $F(X) = X \times S$ and $U(X) = S \to X$. $\DeclareMathOperator{Hom}{Hom}$

We see that there is a clear natural isomorphism $curry_{X, Y} : \Hom(X \times S, Y) \cong \Hom(X, S \to Y)$, which is natural in both $X$ and $Y$. This natural isomorphism is known as "currying" (which is hopefully familiar to you, since I'm guessing you're coming to this material from functional programming). The explicit form of $curry_{X, Y}$ is $\lambda f : X \times S \to Y . \lambda x : X . \lambda s : S . f(\langle x, y \rangle)$, and the explcit form of its inverse is $uncurry_{X, Y} := \lambda f : X \to (S \to Y) . \lambda pair : X \times Y . f(pr_1(pair))(pr_2(pair))$. $\DeclareMathOperator{id}{id}$

From here, we see that the unit $\eta : 1 \to UF$ of the adjunction is given by $\eta_X = curry_{X, X \times S}(\id_{X \times S})$ as usual. The explicit form of $\eta_X$ is $\lambda x : X . \lambda s : S . \langle x, s \rangle$

The counit $\epsilon : FU \to 1$ of the adjunction is $\epsilon_Y = uncurry_{S \to Y, Y}(\id_{S \to Y})$, which is also known as "the evaluation map". The explicit form is $\epsilon_Y = \lambda pair . (pr_1(pair))(pr_2(pair))$.

One now defines $\mu = U \epsilon F : UFUF \to UF$. This agrees with your definition of $\mu$ (exercise).

Therefore, $(UF, \eta, \mu)$ forms a monad. This is always true whenever $\eta$ is the unit of the adjuction $U \dashv F$, $\eta$ is the counit, and $\mu = U\epsilon F$.

For more on this, I would recommend reading through a category theory textbook on the construction of monads from adjunctions.

Answer 2

Here's a proof that State is a monad, in agda:

module State where

open import Function
open import Data.Product

open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

record MathMon (M : Set → Set) : Set₁ where
  field
    fmap : {A B : Set} → (A → B) → M A → M B
    unit : {A : Set} → A → M A
    mult : {A : Set} → M (M A) → M A
    -- functoriality
    fun-idty : ∀ {A : Set} → fmap {A} id ≡ id
    fun-comp : ∀ {A B C : Set} {f : B → C} {g : A → B} → fmap (f ∘ g) ≡ (fmap f) ∘ (fmap g)
    -- naturality
    nat-unit : ∀ {A B : Set} {f : A → B} → (fmap f) ∘ unit ≡ unit ∘ f
    nat-mult : ∀ {A B : Set} {f : A → B} → (fmap f) ∘ mult ≡ mult ∘ fmap (fmap f)
    -- monadicity
    unitˡ : ∀ {A : Set} → mult {A} ∘ unit ≡ id
    unitʳ : ∀ {A : Set} → mult {A} ∘ fmap unit ≡ id
    assoc : ∀ {A : Set} → mult {A} ∘ fmap mult ≡ mult ∘ mult

stateM : ∀ {S : Set} → Set → Set
stateM {S} X = S → S × X

isMonad : ∀ {B : Set} → MathMon (stateM {B})
isMonad {B} =
  record
    { fmap     = fmap
    ; unit     = unit
    ; mult     = mult
    ; fun-idty = refl
    ; fun-comp = refl
    ; nat-unit = refl
    ; nat-mult = refl
    ; unitˡ    = refl
    ; unitʳ    = refl
    ; assoc    = refl
    }
  where
    fmap : {A B S : Set} → (A → B) → stateM {S} A → stateM {S} B
    fmap {A} {B} {S} u x = λ t → (proj₁ (x t) , u (proj₂ (x t)))
    unit : {A S : Set} → A → stateM {S} A
    unit {A} {S} = λ x t → (t , x)
    ev : {A B : Set} → (A → B) → A → B
    ev f b = f b
    --
    mult : {A S : Set} → stateM {S} (stateM {S} A) → stateM {S} A
    mult {A} {S} f = λ s → ev {S} {S × A} (proj₂ (f s)) (proj₁ (f s))

For agda, it's all pretty trivial from the definitions :=)...