The State monad

State.agda

module Categories.Agda.State where

open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction

open import Data.Product
open import Relation.Binary.PropositionalEquality

-- The traditional form of the monad
StateM : ∀ {ℓ} (S : Set ℓ) → Monad (Sets ℓ)
StateM S = record
  { F = record
    { F₀ = λ A → S → (A × S)
    ; F₁ = λ f g → λ s → map f (λ x → x) (g s)
    ; identity     = refl
    ; homomorphism = refl
    }
  ; η = record { η = λ _ → _,_; commute = λ _ → refl }
  ; μ = record { η = λ _ → λ f → λ s → uncurry (λ f → f) (f s); commute = λ _ → refl }
  ; assoc     = refl
  ; identityˡ = refl
  ; identityʳ = refl
  }

module FromAdjunction ℓ where
  -- Our (,a) functor
  [-×_] : Set ℓ → Functor (Sets ℓ) (Sets ℓ)
  [-× S ] = Sets ℓ [ binaryProducts ℓ ][-× S ]

  -- We get our (a ->) functor from here, as Hom[ a ,-]
  open Hom (Sets ℓ)

  -- Exponential would work here instead of Hom, too, but I don't the machinery for that yet
  Adj : (S : Set ℓ) → Adjunction [-× S ] Hom[ S ,-]
  Adj S = record
    { unit   = record { η = λ _ → _,_; commute = λ _ → refl }
    ; counit = record { η = λ _ → uncurry (λ f → f); commute = λ _ → refl }
    ; zig = refl
    ; zag = refl
    }

  -- Make a monad from the adjunction
  StateM′ : (S : Set ℓ) → Monad (Sets ℓ)
  StateM′ S = Adjunction.monad (Adj S)

  -- The monads are equal!
  proof : StateM ≡ StateM′
  proof = refl