Codensity Monad in Agda

Codensity.agda

module Codensity where

open import Level
open import Function

data Codensity {l} (M : Set l → Set l) (A : Set l) : Set (suc l) where
  codensity : ({B : Set l} → (A → M B) → M B) → Codensity M A

runCodensity : ∀ {l} {A : Set l} {M : Set l → Set l}
             → Codensity M A
             → ({B : Set l} → (A → M B) → M B)
runCodensity (codensity c) = c

record Functor {l₁ l₂} (F : Set l₁ → Set l₂) : Set (suc (l₁ ⊔ l₂)) where
  field
    map : {A B : Set l₁} → (A → B) → F A → F B
open Functor ⦃...⦄

instance
  codensity-Functor : ∀ {l} {M : Set l → Set l} →  Functor (Codensity {l} M)
  codensity-Functor {l} {M} = record { map = codensity-map }
    where
      codensity-map : {A B : Set l} → (A → B) → Codensity M A → Codensity M B
      codensity-map f (codensity c) = codensity λ k → c (k ∘ f)

record Applicative {l₁ l₂} (F : Set l₁ → Set l₂) : Set (suc (l₁ ⊔ l₂)) where
  field
    pure : {A : Set l₁} → A → F A
    _⊛_  : {A B : Set l₁} → F (A → B) → F A → F B
open Applicative ⦃...⦄

instance
  codensity-Applicative : ∀ {l} {M : Set l → Set l} → Applicative (Codensity M)
  codensity-Applicative {l} {M} = record { pure = codensity-pure
                                         ; _⊛_ = codensity-⊛
                                         } 
    where
      codensity-pure : {A : Set l} → A → Codensity M A
      codensity-pure x = codensity λ k → k x

      codensity-⊛ : {A B : Set l} → Codensity M (A → B) → Codensity M A → Codensity M B
      codensity-⊛ (codensity f) (codensity x) = codensity λ k → x (λ x' → f (λ f' → k (f' x')))

record Monad {l₁ l₂} (M : Set l₁ → Set l₂) : Set (suc (l₁ ⊔ l₂)) where
  field
    unit : {A : Set l₁} → A → M A
    _⟫=_ : {A B : Set l₁} → M A → (A → M B) → M B
open Monad ⦃...⦄

instance
  codensity-Monad : ∀ {l} {M : Set l → Set l} → ⦃ F : Applicative M ⦄ → Monad (Codensity M)
  codensity-Monad {l} {M} = record { unit = pure
                                   ; _⟫=_ = codensity-⟫=
                                   }
    where
      codensity-⟫= : {A B : Set l} → Codensity M A → (A → Codensity M B) → Codensity M B
      codensity-⟫= (codensity x) f = codensity (λ k → x (λ x' → runCodensity (f x') k))