読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

Codensity Monad

Agda Haskell

Codensity という型がある. 定義は以下.

newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }

instance Functor (Codensity k) where
  fmap f (Codensity m) = Codensity (\k -> m (k . f))

instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ.

instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
  wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Codensityはnewtypeで実装されているから, 実行時には CodensityrunCodensity によるオーバーヘッドは考えなくて良い. だから, m のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のmが「重い」モナドなら, Codensity をかぶせるだけで劇的に速くなることがある.

Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.

以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.

RanとCodensity

functor p : C → Dに対し, functor  p^{-1} \colon \mathcal{E}^\mathcal{D} → \mathcal{E}^\mathcal{C}を,  p^{-1}(F) = F \circ p によって定める. ただしここで  \mathcal{E}^\mathcal{D} とはDからEへの関手のなす関手圏のこと.

functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張  p \ddagger f を考える.
 p \ddagger が存在すれば, これは  p^{-1} の右随伴である.

D
↑ ↘ p‡f
| ⇓ ↘
C ――→ E

随伴の定義から,

 \hom(p^{-1}(-),f) \cong \hom(-,p \ddagger f)

ここで,  \mathcal{C} の対象aを一つ固定し, 米田関手yを用いて

 \hom(p^{-1}(ya),f) \cong \hom(ya,p \ddagger f)

 p^{-1} の定義に戻れば,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f)

さらに右辺で(共変)米田の補題を用いて,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f) \cong (p \ddagger f)(a)

なる同型を得る. ゆえに (p \ddagger f)(a) が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である.  \hom(ya \circ p,f) とは, 自然変換の集合であるが, これを ya \circ p \rightarrow fなる自然変換からなる型と同一視する.

このような仕方で (p \ddagger f)(a)を最左辺で定義すると,
自然変換 ya . p ~> fRankNTypes を用いて, forall b. (a -> p b) -> f b なる型を持つ.

よって,

newtype Ran p f a = Ran (forall b. (a -> p b) -> f b)

を得る. これは http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Kan-Ran.html で定義されている.

最後に, pもfもmで固定してしまうと,

newtype Ran     m m a = Ran       (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity (forall b. (a -> m b) -> m b)

により, Codensityが得られた.

HaskellでのFunctor, Monad

上のような操作でCodensityは得られるが, 上の操作では pやfは関手 であった.
しかしCodensityはFunctorのinstanceで(Functor m) =>を要求しない (つまり, mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる).

最初の実装で確かにCodensityがFunctorやMonadになることは確認が必要なので, Agdaで証明を書いてみた.

確かに,

instance Functor (Ran p f)
instance Functor (Codensity k)
instance Monad (Codensity f)

なるインスタンスが正しく実装されていることが分かる.

参考文献