2008-03-02

まずは元論文にもあるリストの appendを限定継続で書く例。この時点でついて行けてなかった。

実はOlegさんのソースにもあるのだけど自分で書き直してみる。

-- -fno-implicit-prelude を指定すること (GHC 6.6)
import ShiftResetGenuine
import Prelude hiding ((>>=),(>>),return)
m >>= f =  m `bind` f
m >> n = m >>= (\_ -> n)
return x = ret x

appendCont (x:xs) = appendCont xs >>= \xs' -> return (x:xs') -- doを使わない理由は後述
appendCont [] = shift (\k -> return k)

append123 ys = do
  k <- reset $ appendCont [1,2,3]
  k ys

-- *Main> run (append123 [3,4,5])
-- [1,2,3,3,4,5]

shiftは大域脱出のための演算子のようなもの。shift (\k -> e) でresetまで大域脱出が起こり結果がeになる。ここで k には reset-shift間で切り出した限定継続が入る。この限定継続 kというのは、引数を食わせると、その引数がちょうどshiftの位置に登場してresetまでの残りの計算が実行されて戻るという関数。つまり reset ( .... (shift (\k -> e)) ...) ==> let k x = (.... x ....) in e という感じなのだけどこれは他の解説でもよく目にする。

上の例では、モナドがあってややこしいけど、reset-shiftで切り出した限定継続を、そのまま返している (\k->return k)。

reset 内の項 appendCont [1,2,3] は do xs <- shift (ほげほげ); return (1:2:3:xs) のように簡約され(るというのはたぶん嘘で単にこういう項と等価になる;めんどいので以下略)、ここで shiftで切り出された限定継続kは (\xs -> return (1:2:3:xs)) という感じになる。 (\k->return k) でこの限定継続がそのまま reset の戻り値になる。

なんとなくわかってきた気がするけど、型のことを考えると、より一層混乱するのは言うまでもない。

do-notation bug?

GHC6.6で、-fno-implicit-prelude を加えて以下をコンパイル。

import ShiftResetGenuine
import Prelude hiding ((>>=),(>>),return)
m >>= f =  m `bind` f
m >> n = m >>= (\_ -> n)
return x = ret x

appendCont (x:xs) = do 
  xs' <- appendCont xs
  return (x:xs')

これの型が appendCont_ :: (Monadish m) => [t] -> m a a [t] となってしまう。 do記法が定義どおり展開されているならば (Monadish m) => [t] -> m a g [t] となるはず。式全体の型がreturn (x:xs')の型に縛られている? 普通のMonadならそれでも大丈夫なんだけど…。

keigoiの日記

限定継続その2

do-notation bug?