Cont.agda

module Categories.Agda.Cont where

open import Categories.Category
open import Categories.Agda
open import Categories.Functor
open import Categories.Monad
open import Categories.Adjunction

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≣_)

-- The direct version of the monad.
ContM : ∀ {ℓ} (R : Set ℓ) → Monad (Sets ℓ)
ContM R = record
  { F = record
    -- newtype Cont r a = Cont { runCont :: (a -> r) -> r }
    { F₀ = λ A → (A → R) → R           

    -- just the Functor fmap on Cont
    ; F₁ = λ f g h → g (λ z → h (f z))  

    -- The proofs of functor laws are trivial because the terms just reduce to the same thing
    ; identity     = refl -- fmap id = id
    ; homomorphism = refl -- fmap f . fmap g = fmap (f . g)
    }

  -- The return method of Monad. The natural transformation square commutes trivially
  ; η = record { η = λ _ x f → f x; commute = λ _ → refl }

  -- The join method of Monad. Again, the square is trivial
  ; μ = record { η = λ _ f h → f (λ z → z h); commute = λ _ → refl }

  -- The laws are all trivial, just for a change
  ; assoc     = refl -- join . join = join . fmap join
  ; identityˡ = refl -- join . return = id
  ; identityʳ = refl -- join . fmap return = id
  }

-- Our contravariant "negation" functor.
Not : ∀ {ℓ} (R : Set ℓ) → Functor (Sets ℓ) (Category.op (Sets ℓ))
Not R = record
  -- newtype Not r a = Not { runNot :: a -> r }
  { F₀ = λ A → A → R

  -- the contramap method on Contravariant is just pre-composition (opposite side from Reader)
  ; F₁ = λ f g h → g (f h)

  -- Functor laws are trivial
  ; identity = refl
  ; homomorphism = refl
  }

-- The adjunction between Not R and itself (flipped around: Functor.op takes Functor C D and gives you Functor C^op D^op in the trivial way)
Adj : ∀ {ℓ} (R : Set ℓ) → Adjunction (Not R) (Functor.op (Not R))
Adj R = record
  { unit = record { η = λ _ x f → f x; commute = λ _ → refl }
  ; counit = record { η = λ _ x f → f x; commute = λ _ → refl }
  ; zig = refl
  ; zag = refl
  }

-- You can construct a monad by composing a pair of adjoint functors. The proofs behind this are actually fairly involved but it's not ground-breaking stuff
ContM′ : ∀ {ℓ} (R : Set ℓ) → Monad (Sets ℓ)
ContM′ R = Adjunction.monad (Adj R)

-- Our two continuation monads are identical!
proof : ∀ {ℓ} (R : Set ℓ) → ContM R ≣ ContM′ R
proof R = refl