PS

CPS monad

圏論 命題 Monad Kan-extension

任意のmonad:

  • (T, \eta, \mu)

について･･･

Monadからのadjunction

Adjunctionからのmonad - PSの対応:

  • (L \dashv R) \mapsto RL

は、surjectiveであったので

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

なるcounit-adjunction:

  • L \overset{\epsilon}{\dashv} R

が存在する。

Adjunction liftingによるright Kan extension

Adjunction lifting - PSにより、

  • (F \epsilon : FLR \rightarrow F) _ F

は、right Kan extension along R の族であったので、特に

  • R \epsilon : RLR \rightarrow R

は、right Kan extension of R along R となる。

Endによるright Kan extension

特に R のcodomainが \mathcal{Set} の場合、Endからのright Kan extension - PSにより、もう一つのright Kan extension of R along R:

  • \sigma : \displaystyle\int _ z \mathcal{Set}( \mathcal{Set}(\unicode{x2013}, Rz), Rz) \circ R \rightarrow R

が存在したが、Kan extensionはunique up to isomorphismなので

  • \sigma \cong R \epsilon

Monadからのcodensity monad

R \epsilon から作ったCodensity monad - PS:

  • (RL, ...)

は、 (T, \eta, \mu) に等しかったので、 \sigma から作ったcodensity monad:

  • (\displaystyle\int _ z \mathcal{Set}( \mathcal{Set}(\unicode{x2013}, Rz), Rz), ...)

は、 (T, \eta, \mu) にisomorphic。*1

これで、monadをcontinuation-passing styleに変換できた。

参考文献

*1:codensity monad化の操作はcategory of monadsに対してfunctorial