限定継続モナドと再帰

この記事の続きはこちら

三次会では Olegさんによる限定継続モナド を触っていた。
これまで皆が使っているのを指をくわえて見ていたけど、自分でもやっと使いこなせるようになってきた気がする。うれしくなったのでこの記事を書く。

説明では疑似Haskellっぽい構文を使う。実際にOlegの限定継続モナドを使う場合はそれっぽく型を合わせる必要がある。

私の限定継続の理解

私の shift と reset はこういう理解:

  • reset e
    • 内側(引き数)にshiftが無ければ、中身(e)をそのまま返す
    • shiftがあれば、shiftによる大域脱出の効果をそこまでに限定する (つまりこの時点での継続を「捕まえておく」)
  • shift f
    • 限定継続kを取り出して、f k を計算し、その値で reset まで大域脱出する (つまりresetで捕まえていた継続を呼ぶ)
    • このkは、引き数を渡すと shift から reset までの計算結果を返す関数(継続)

つまり、継続を2重に扱っているイメージ。あってるかな。ただshiftによる大域脱出はレキシカルではなくダイナミックなスコープ(直前に実行されたresetまで大域脱出)

一方 callcc f は 単に 継続kを取り出して f k を計算するだけ。ここで k を呼ぶと大域脱出される(callcc時点の継続だから、当たり前か)

簡単な例

reset しか使わない例はつまらないし、かといってshiftで捕まえた限定継続をその場で使う(reset (1:2:shift (\k->k [1])) みたいな)はちょっと難しくないかと思う。私もよくわかってなかった。

まず一番簡単な例として、限定継続をそのまま戻してしまう shift (\k -> k) 例を考える。

-- 疑似Haskell
f = reset (1 : 2 : shift (\k -> k))

shift で取り出したkはshift から reset までの限定継続、つまり

\x -> 1 : 2 : x

という関数だ。
この継続は、shiftの続きから始まって、resetまで実行して、戻ってくる。非常にわかりやすい。
しかも、 shift の中身で k をそのまま返して大域脱出するので、結局 f の値も \x -> 1 : 2 : x となる。

f 3

と適用すれば

[1,2,3]

が返ってくるはずだ(疑似コードだけど)。

何が嬉しいの?

あまりに簡単な例なので、何が嬉しいのか分かりづらいが、最も端的な例は sprintf だ。

-- 疑似Haskell
str = shift (\k -> k)
sprintf = reset
hello = sprintf ("Hello, "++str++". Today is "++str++".")

などとすれば、

-- 疑似Haskell
helloKeigo = hello "Keigo" "Sunday"
-- "Hello, Keigo. Today is Sunday."

となる。

shift (\k->k) と「穴」

これは、 shift (\k -> k) が 一種の「穴」を作っていると考えるとわかりやすい。

reset ("Hello, "++穴++".")
reset ("Hello, "++穴++". Today is "++穴++".")

という式は

\s1 -> \s2 -> ("Hello, "++s1++".")
\s1 -> \s2 -> ("Hello, "++s1++". Today is "++s2++".")

という、「穴を埋めて中身を返す関数」という風にみることができる。

少し複雑な例

少し複雑な例をみる。といっても、上のsprintfと全くかわらない。

-- 疑似Haskell
appnd [] = shift (\k -> k)
appnd (a:rest) = (a:appnd rest)

reset (appnd [1,2,3]) は reset (1:2:3:穴) となり、結局 \xs -> 1:2:3:xs が返ってくる。

何度もshift

Scheme:部分継続:イテレータの反転 で示されている例は、3つの意味でちょっと難しかった:

  • shift の位置が reset のレキシカルスコープの外にある
  • 何度も shift している
  • 破壊的代入がある

似たようなコードをHaskellで書いた.
http://ideone.com/DYaRO
map関数に、shift を渡している. 穴が無数にあるのでそのままでは型がつかない.なので 型X を定義してそこに限定継続をぶちこんでいる.
自分でもちょっと難しいコードだと思う.三日後くらいには読めない気さえする.

どうやって書いたかというと

Occurs check: cannot construct the infinite type: b = a -> C t t b

と怒られたのでそういう再帰型を作っただけなんだけど


次回(あれば)、これをうまく説明したい。