http://myuon-myon.hatenablog.com/entry/2014/11/03/183032

Codensity.agda

module Codensity where

open import Level
open import Function
open import Category.Functor
open import Category.Monad
open import Relation.Binary.PropositionalEquality

record Functor {a b} (F : Set a → Set b) : Set (suc (a ⊔ b)) where
  field
    fmap : ∀{A B} → (A → B) → F A → F B

  infixl 4 _<$>_ _<$_

  _<$>_ : ∀{A B} → (A → B) → F A → F B
  _<$>_ = fmap

  _<$_ : ∀ {A B} → A → F B → F A
  _<$_ x y = const x <$> y

  field
    preserve-id : ∀{A} (Fa : F A) → fmap id Fa ≡ id Fa
    covariant : ∀{A B C} (f : A → B) → (g : B → C) → (Fa : F A)
      → fmap (g ∘ f) Fa ≡ fmap g (fmap f Fa)
open Functor public

record Monad {a b} (M : Set a → Set b) : Set (suc (a ⊔ b)) where
  infixl 1 _>>=_

  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A B} → M A → (A → M B) → M B

  field
    return-apply : ∀{A B} → (a : A) → (k : A → M B) → (return a >>= k) ≡ k a
    return-id-right : ∀{A} → (m : M A) → (m >>= return) ≡ m
    bind-assoc : ∀{A B C} → (m : M A) → (k : A → M B) → (h : B → M C) →
      (m >>= (λ x → k x >>= h)) ≡ ((m >>= k) >>= h)

data Ran {ℓ} (g h : Set ℓ → Set ℓ) (a : Set ℓ) : Set (suc ℓ) where
  kan : (∀{b : Set ℓ} → (a → g b) → h b) → Ran g h a

runRan : ∀ {ℓ g h a} → Ran {ℓ} g h a → ∀ {b} → (a -> g b) -> h b
runRan (kan f) = f

data Codensity {ℓ} (m : Set ℓ → Set ℓ) (a : Set ℓ) : Set (suc ℓ) where
  codensity : (∀{b : Set ℓ} → (a → m b) → m b) → Codensity m a

runCodensity : ∀ {ℓ m a} → Codensity {ℓ} m a → ∀ {b} → (a -> m b) -> m b
runCodensity (codensity f) = f

Codensity-Monad : ∀ {ℓ m} → Monad (Codensity {ℓ} m)
Codensity-Monad {ℓ} {m} = record
  { return = return'
  ; _>>=_ = _>>='_
  ; return-apply = \a k →
    begin
      return' a >>=' k                                        ≡⟨ refl ⟩
      (codensity $ \k → k a) >>=' k                           ≡⟨ refl ⟩
      codensity (\c → (\k → k a) $ \a → runCodensity (k a) c) ≡⟨ refl ⟩
      codensity (\c → runCodensity (k a) c)                   ≡⟨ refl ⟩
      codensity (runCodensity (k a))                          ≡⟨ codensity-runCodensity-id (k a) ⟩
      k a                                                     ∎
  ; return-id-right = \ma →
    begin
      ma >>=' return'                                                    ≡⟨ refl ⟩
      codensity (\c → runCodensity ma $ \a → runCodensity (return' a) c) ≡⟨ refl ⟩
      codensity (\c → runCodensity ma $ \a → (\k → k a) c)               ≡⟨ refl ⟩
      codensity (\c → runCodensity ma $ \a → c a)                        ≡⟨ refl ⟩
      codensity (runCodensity ma)                                        ≡⟨ codensity-runCodensity-id ma ⟩
      ma                                                                 ∎
  ; bind-assoc = \ma k h →
    begin
      (ma >>=' (\x → k x >>=' h))
    ≡⟨ refl ⟩
      (codensity $ \c → runCodensity ma $ \a → runCodensity (k a >>=' h) c)
    ≡⟨ refl ⟩
      (codensity $ \c → runCodensity ma $ \a → (\d → runCodensity (k a) $ \b → runCodensity (h b) d) c)
    ≡⟨ refl ⟩
      (codensity $ \c → (\d → runCodensity ma $ \a → runCodensity (k a) d) $ \a → runCodensity (h a) c)
    ≡⟨ refl ⟩
      (codensity $ \c → runCodensity (ma >>=' k) $ \a → runCodensity (h a) c)
    ≡⟨ refl ⟩
      (ma >>=' k) >>=' h ∎
  }
  where
    open ≡-Reasoning

    return' : ∀ {A} (a : A) → Codensity m A
    return' a = codensity $ \k → k a

    _>>='_  : ∀ {A B} → (Codensity m A) → (A → Codensity m B) → Codensity m B
    ma >>=' k = codensity $ \c → runCodensity ma $ \a → runCodensity (k a) c

    codensity-runCodensity-id : ∀{A} → (ma : Codensity {ℓ} m A) →
      codensity (runCodensity ma) ≡ ma
    codensity-runCodensity-id (codensity _) = refl