Continuationモナドに関するメモ
HaskellっぽくてHaskellぽくない記法がたくさんでてくるが，これは，モナドはHaskellのみのものではなく，また，Haskellの記法はきれいであり，しかし，Haskellの無名関数の表記は，どうせWebで外字参照が使用できるから……ということなので見逃してほしい．
そのうちcallCCについてもメモするかも
たとえば，なんでも継続などが詳しい．今回は，継続そのものについては，何も述べない．
簡単にいうと，関数の返った先に実行される関数を，引数として一緒に渡してあげるやりかたである．つまり，
f :: a -> b
という関数fに対して，
f♠ x = λ k. k (f x)
のようなものを考える．ここでとりあえずkの返り値の型を固定して，
f♠ :: a -> (b -> r) -> r
という型であると考える．
このようなものを考えて何のメリットがあるだろうか．ひとつは末尾再帰でない再帰関数を末尾再帰に直すことができる点である．
fact n = if n == 0 then 1 else n * fact (n-1)
というコードを考えると，これは明らかに末尾再帰ではないが，継続渡し形式で記述すると，
fact♠ n = λk. if n == 0 then k 1 else fact♠ (n-1) (k.(n *))
となる．末尾再帰である．O'Camlのように末尾再帰を見てくるコンパイラだと，この2つの差は明らかである．入力がある数を越えたところで前者がスタックオーバフローを起こすのを確認できるはずだ．Haskellだとあんまり効果はない．
同様に
foldr f e xs = (foldl (λx♠y.λz.λk. x♠ (f y z) k) id♠ xs) e id
が確認できるだろう．
他にも，callCCを用いることで処理の途中で外側に抜けだすような関数を書いたりできるらしいが，今回は触れない．
モナドとは，"関数合成の意味の変化"であった．ならば継続渡し形式で記述された関数同士の関数合成を考えることで，Continuationモナドの定義が見えてくるであろう．
f :: a -> b, g :: b -> c
に対し，
f♠ :: a -> (b -> r) -> r, g♠ :: b -> (c -> r) -> r
の合成
g♠ @ f♠ :: a -> (c -> r) -> r
を考えよう．ここで重要なのは，もはや，f♠ってものがどう定義されているかは考えないということだ．つまり，fとかgとかは忘れる．他にもこのような型の関数が定義できる方法があるfact♠とか．それを除くのはまずい．さらに重要なのはもし，f♠ x k = k (f x)であった場合は期待通りに動くということである．
意味から考えると，f♠の返る部分として，g♠を，g♠の返る部分として，c -> rな何かを設定しなればならないということがわかる．これらのことから，
g♠ @ f♠ = λa.λk. f♠ a (λb. g♠ b k)
ということが推測されるだろう．こいつが関数合成のようにふるまえば万々歳である．
(h♠ @ g♠) @ f♠ = (λb.λk. g♠ b (λc. h♠ c k)) @ f♠ = λa.λk′. f♠ a (λb′. (λb.λk. g♠ b (λc. h♠ c k)) b k′) = λa.λk′.f♠ a (λb′. g♠ b′(λc. h♠ c k′))
であり，
h♠ @ (g♠ @ f♠) = h♠ @ (λa.λk. f♠ a (λb. g♠ b k) ) = λa′.λk′. (λa.λk. f♠ a (λb. g♠ b k) ) a′ (λc. h♠ c k′) = λa′.λk′. f♠ a (λb. g♠ b (λc. h♠ c k′)
となり結合性を満たす．
まぁきっと
id♠ x k = k (id x) = k x
が単位元だろう．
左から
id♠ @ f♠ = λa.λk. f♠ a (λx. id♠ x k) = λa.λk. f♠ a (λx. k x) = λa.λk. f♠ a k = f♠
右から
f♠ @ id♠ = λx.λk. id♠ x (λa. f♠ a k) = λx.λk. (λa. f♠ a k) x = λx.λk. f♠ x k = f♠
これだと，外延性を利用しているから厳密でないかもしれない．f♠が⊥だとこれがなりたたない．
あとは自然に導出できて(Kleisli TripleとKleisli圏の関係から)
M a :: (a -> r) -> r unit a = λk. k a m `bind` f = λk. m (λa. f a k)
となる．