Codensity Monad
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で実装されているから, 実行時には Codensity
や runCodensity
によるオーバーヘッドは考えなくて良い. だから, m
のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のm
が「重い」モナドなら, Codensity
をかぶせるだけで劇的に速くなることがある.
Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.
以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.
RanとCodensity
functor p : C → Dに対し, functor を, によって定める. ただしここで とはDからEへの関手のなす関手圏のこと.
functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張 を考える.
が存在すれば, これは の右随伴である.
D ↑ ↘ p‡f | ⇓ ↘ C ――→ E
随伴の定義から,
ここで, の対象aを一つ固定し, 米田関手yを用いて
の定義に戻れば,
さらに右辺で(共変)米田の補題を用いて,
なる同型を得る. ゆえに が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である. とは, 自然変換の集合であるが, これをなる自然変換からなる型と同一視する.
このような仕方でを最左辺で定義すると,
自然変換 ya . p ~> f
は RankNTypes
を用いて, 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)
なるインスタンスが正しく実装されていることが分かる.
参考文献
- http://alg-d.com/math/category/ 日本語で読める圏論pdfで, Kan拡張についても記述があるサイト.
- http://hackage.haskell.org/package/kan-extensions-4.1.0.1 package kan-extensions (by ekmett)
- http://comonad.com/reader/2011/free-monads-for-less/ Codensityについての解説.