2010-06-27

ProofCafe #3

Coq

第三回ProofCafeが開催されました。CPDTの Inductive Types の前半を読みました。

個人的には injective タクティックを使ったことがなかったので次から積極的に使おうと思いました。

2010-06-27

限定継続モナドと再帰

Haskell

この記事の続きはこちら

三次会では 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

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

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

2010-06-27

限定継続でmap関数をひっくり返す

Haskell

前回の例はちょっと意味不明だった。単にshiftをmap関数に渡してみたかったのだけど…

もっとわかりやすく、shift/reset を使って map 関数をひっくり返したものを作ってみた。
が、やっぱりモナドなので普通のSchemeの例より読みにくいような気もする。

まあしかし、shift/reset の型付けを理解するのに良い例のような気もするので、そのまま載せちゃいます

-- 再帰的な限定継続を保持する型
data Iter = 
    Iter (Int -> C [Int] [Int] Iter, Int) -- 限定継続と，何か整数を保持 
  | End [Int] -- おわり

-- ひっくり返されたmap関数
pam []     = ret []
pam (x:xs) = shift (\k -> ret $ Iter (k, x)) >== \y -> pam xs >== \ys -> ret (y:ys)

使ってみる。

expr = reset (pam [1,2,3] >== \xs -> ret (End xs))

ここで reset の前にリストの結果を End に格納しているのに注目。
shiftのanswer type ( \k -> e の e の型) とresetの型は一致させる必要がある。 Iter 型は限定継続を格納する型だが、shiftが消費され尽くした後は、計算結果がほしい。 End はそんな「計算結果」を格納するのに使う。

expr の結果を取り出すには、run expr とする。 run expr した結果、型 Iter が返ってくる。 Iter型に格納されている継続を呼び出して、返ってきたIter型の継続を更に呼び出す… 関数 iter を次の通り定義する。

iter :: (Int -> Int) -> Iter -> [Int]
iter f (Iter (k,x))  = run (k (f x) >== \it -> ret (iter f it))
iter _ (End xs)      = xs

run expr した結果返ってくるIter型(限定継続)を iter でぶん回せば、ひっくり返されたmap関数が実行できる．

main = mapM_ print [iter id $ run expr, iter (*10) $ run expr]

ideoneに貼付けてみた。

[1,2,3]
[10,20,30]

あえて型シグネチャを書かなかったけど、 expr :: C a a Iter, pam :: [Int] -> C Iter Iter [Int] である。 C a a b の型 a に、shiftに渡す式のアンサータイプを書く感じだろうか??

2010-06-27

multi-promptな限定継続 in Haskell (失敗編＆成功編)

Haskell OCaml

multi-promptな限定継続の方が型がわかりやすい件について。

なんだかshift/resetの型付けはむつかしいなーと思っていた。
限定継続のOCaml実装を見てみたくて、Olegさんのdelimccライブラリとその論文を眺めていた。
こちらはmulti-promptな限定継続といい、複数の限定継続を同時に扱える体系の実装なのだけど、こちらの方が型が分かりやすかった。

理論的基礎はDybvig, Peyton Jones, Sabryの論文で、cc-delcontというHaskell版の実装がHackageにある。この実装も indexed monad ではなく普通のモナドなので型は理解しやすいはず。

これらのライブラリでは、 newPrompt, pushPrompt, withSubCont, pushSubCont の 4つのプリミティブを使う。また扱うデータ型も、「プロンプト(Prompt)」「部分継続(SubCont)」の2種類がある。

mutil-prompt 限定継続に関する私の理解

ざっくりとした説明

Prompt
- 複数の限定継続を区別するための識別子
SubCont
- 限定継続そのもの。呼び出すには pushSubCont を使う

newPrompt
- 新しいpromptを作る
pushPrompt p
- resetのようなもの。限定継続の開始地点をpでマークする。pushSubCont するとこのマークは消えちゃう。
withSubCont p f
- shiftのようなもの(ちょっと違うけど)。 pushPrompt pでマークした箇所まで大域脱出しつつ、そこまでの限定継続(SubCont)に f を適用する。
- 大域脱出したら pushPrompt pのマークは消えちゃう。マークがない状態で withSubCont すると実行時エラー。
pushSubCont k
- 限定継続kを表す関数を返す。

shiftと同じような挙動を得たい場合はpushSubCont k e のすぐ外でもういちど pushPrompt する。すると、呼び出した限定継続の中で次のwithSubContが使われて大域脱出した場合にもそこに戻ってきてくれる。

使ってみた

先の例(mapをひっくり返す)を CC-delim を使って焼き直してみた。
Promptを持って回るためにちょっとややこしくなってしまった。

{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Monad.CC
import Control.Monad.Identity (Identity)

-- 再帰的な限定継続を保持する型
data Iter a = 
    Iter (SubCont a Identity Int (Iter a), Int) -- 限定継続と，何か整数を保持 
  | End [Int] -- おわり

pam :: Prompt ans (Iter ans) -> [Int] -> CC ans [Int]
pam _  []     = return []
pam p0 (x:xs) = do
  y <- withSubCont p0 (\k -> return $ Iter (k, x))
  ys <- pam p0 xs
  return (y:ys)

expr :: CC ans (Prompt ans (Iter ans), Iter ans)
expr = do 
  p0 <- newPrompt
  it <- pushPrompt p0 $ do
    xs <- pam p0 [1,2,3]
    return (End xs)
  return (p0, it)
    
iter :: (Int -> Int) -> (Prompt ans (Iter ans), Iter ans) -> CC ans [Int]
iter _ (_,End xs)      = return xs
iter f (p0,Iter (k,x))  = do 
  it <- pushPrompt p0 (pushSubCont k (return $ f x))
  iter f (p0,it)

main = mapM_ print [runCC $ iter id =<< expr, runCC $ iter (*10) =<< expr]

Haskellなので promptを渡して回らないといけないのが面倒(implicit parameterを使えばいいけど…)。また pushPrompt を忘れると実行時エラーになるので、少し扱いに気を遣う。

うまくいかなかった版

こちらはNG. expr と iter を別の runCC に入れてしまった．

{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Monad.CC
import Control.Monad.Identity (Identity)

-- 再帰的な限定継続を保持する型
data Iter a = 
    Iter (SubCont a Identity Int (Iter a), Int) -- 限定継続と，何か整数を保持 
  | End [Int] -- おわり

pam :: Prompt ans (Iter ans) -> [Int] -> CC ans [Int]
pam _  []     = return []
pam p0 (x:xs) = do
  y <- withSubCont p0 (\k -> return $ Iter (k, x))
  ys <- pam p0 xs
  return (y:ys)

expr :: CC ans (Iter ans)
expr = do 
  p0 <- newPrompt
  pushPrompt p0 $ do
    xs <- pam p0 [1,2,3]
    return (End xs)
    
iter :: (Int -> Int) -> Iter a -> [Int]
iter _ (End xs)      = xs
iter f (Iter (k,x))  = runCC $ do 
  it <- pushSubCont k (return $ f x); -- (*) ここで 外からもってきた subcont を使ってるのが駄目
  return (iter f it)

CC-delcont の継続モナドは CC ans a という型をもち、 runCC :: (forall ans. CC ans a) -> a によって実行できるが、だがちょっと待って欲しい。いわゆるContモナドと違うのは、 answer type (Cont r a の r) がforall束縛されている点だ。この束縛おかげで CC ans a から aが取り出せている…ともいえるのだけど、今回のように runCC から帰ってきた部分継続(限定継続)を別の runCC の中から呼び出せないのだ！ (型変数の動く範囲が runCC で限定されているため, (*) の k の SubCont ans ...) の ans と unify できない)

~~shift/reset の感覚で使ったのがまずかった。ちゃんと multi-prompt っぽく複数の promptを使えば似たようなことはできるはずだ。。。~~