PS

Continuation monad

圏論 Kan-extension Monad Adjunction Haskell

Association between monads and adjunctions

について

  • T = RL
  • \mu = R \epsilon L

を満たすとき、互いに associated というのであった。

Identity monad

  • identity functor: I := 1 _ { \mathcal{C} } : \mathcal{C} \to \mathcal{C}
  • identity natural transformation: \eta ^ I := \mu ^ I := 1 _ { 1 _ {\mathcal{C}} } : 1 _ {\mathcal{C}} \Rightarrow 1 _ {\mathcal{C}}

は monad (I, \eta ^ I, \mu ^ I) になる。

Trivial adjunction

さらに

  • \epsilon ^ I := 1 _ { 1 _ {\mathcal{C}} } : 1 _ {\mathcal{C}} \Rightarrow 1 _ {\mathcal{C}}

とすると (I \dashv I, \eta ^ I, \epsilon ^ I) は adjunction になる

Codensity monads for free

Free theorem のもと、functor:

  • R : \mathcal{Hask} \to \mathcal{Hask}

および、right kan extension of R along R:

  • (\mathrm{Ran} _ R R)(c) \cong \underset{m}{\forall} \big( (c \to Rm) \to Rm)

から作った Codensity monad - PS (T, \eta, \mu) は

  • T(c) := \underset{m}{\forall} \big( (c \to Rm) \to Rm)
  • \eta _ c := (x : c) \mapsto \big( (h : c \to Rn) \to h(x) \big) _ n
  • \mu _ c := (x : T ^ 2 c) \mapsto \big( (h : c \to Rn) \mapsto x _ n( (k : Tc) \mapsto k _ n (h) ) \big) _ n

となる。

Continuation monad

Identity monad と trivial adjunction は互いに associated なので、特に

  • \mathcal{C} := \mathcal{Hask}
  • R := I

とすると CPS monad - PS より

  • (T, \eta, \mu) \cong (I, \eta ^ I, \mu ^ I)

参考文献