PS

Codensity monad

圏論定義 Monad Haskell

Codensity monad

Functor:

$G : \mathcal{C} \rightarrow \mathcal{D}$

について、right Kan extension of $G$ along $G$ :

$\omega : MG \rightarrow G$

が存在するならば、

$M : \mathcal{D} \rightarrow \mathcal{D}$
$\langle 1 _ {G} \rangle : 1 _ {\mathcal{D}} \rightarrow M$ *1
$\langle \omega \circ M \omega \rangle : M ^ 2 \rightarrow M$

は、monadを成す。このmonadをcodensity monad of $G$ という。

Adjunctionからのcodensity monad

特に、 $G$ がleft adjoint:

$F \dashv G$
$\epsilon : FG \rightarrow 1 _{\mathcal{C}}$

を持つとき、Adjunction lifting - PSによるright Kan extension of $G$ along $G$ :

$G \epsilon : GFG \rightarrow G$

から作ったcodensity monadは、Adjunctionからのmonad - PSそのものである。

Haskellのcodensity monad

Endからのright Kan extension - PSと(Co)Ends for free - PSにより、

$(\text{Ran}_ G G)(a) \cong \forall _ b \left( (a \rightarrow Gb) \rightarrow Gb \right)$

なので、codensity monadが作れる。

参考文献

*1: $\omega$ とのmediator