チュートリアル復習

ハンドアウトとプレゼン資料と使用したソースコードなどは http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/

OchaCaml

手元の AMD64 FreeBSD 8-STABLE だと Ocha版以前になんか Caml Lite の make world の途中でなんだかコケている
Mac (Snow Leopard) では特に問題起きず
OchaCaml のココロは OchaCaml.diff 。C ソースにも手を入れている
入力が readline になってなくてうれしくないが rlwrap を使えば幸せ
継続とは: 注目している簡約基(リデックス)の外側にある式(計算)が「継続」(call by nameの時は?)
限定継続: 外側にある式(継続)では、プログラムなどだと、ある部分以外の全部、ということになって大変。それを「ここまで」と区切るのが限定継続
reset: reset (fun () -> 《式》) のようにして使う。「《式》の中からの継続」(後述)は reset までに限定される。reset は引数の (fun () -> 《式》) に () “unit” を apply し、何もなければ(後述)それから返された値を返す

# reset (fun () -> 1 + 2) ;;
- : int = 3

shift: shift (fun k -> 《式》) のようにして使う。reset に渡す引数内の式で、このように shift を使うと、shift から reset までの継続が k に束縛され、一方 shift の継続すなわち reset の継続になるような短絡がされ、《式》を評価し、その値が返される
( k は、継続 Continuation の C を換字した K で、よく使われている)

# reset (fun () -> "a" ^ shift (fun k -> "b" ^ k (k "c"))) ;;
- : string = "baac"

(↑ k の値は fun s -> "a" ^ s となる。文字列の先頭が "a" ではなく "b" である点に注意)
call/cc と グローバル変数を使った超々手抜きの reset & shift を Scheme で実装してみる(これは、チュートリアルにはなかった内容)

(define *the-outer-continuation* ())
(define *the-inner-continuation* ())

(define (reset closure)
  (call/cc (lambda (k)
    (set! *the-outer-continuation* k)
    (set! *the-inner-continuation* #f)
    (let ((result (closure)))
      (if (not *the-inner-continuation*)
        result
        (let ((k *the-inner-continuation*))
          (set! *the-inner-continuation* #f)
          (k result) ))))))

(define (shift closure)
  (call/cc (lambda (middle-continuation)
    (*the-outer-continuation*
      (closure
        (lambda (arg)
          (call/cc (lambda (k)
            (set! *the-inner-continuation* k)
            (middle-continuation arg) ))))))))
> (reset (lambda () (cons 1 2)))
(1 . 2)

> (reset (lambda () (cons 1 (shift (lambda (k) (cons 2 (k (k ()))))))))
(2 1 1)

(追記: Scheme では reset と shift は、明示的に引数を手続きにしなくてもよいマクロとして実装するのが一般的なようです)
(さらに追記: 当然ながら↑の実装はダメダメです。ちゃんとした実装例は http://dl.acm.org/citation.cfm?id=581504 ← この論文( Final shift for call/cc:: direct implementation of shift and reset )中にサーベイとして(§ 2 )示されています)
ここまで、チュートリアルにはなかった内容
(限定)継続を取り出す: shift (fun k -> k) によって限定継続を取り出すことができる

# reset (fun () -> 1 + shift (fun k -> k)) 2 ;;
- : int = 3

↑「1 を足して返す」という継続を取り出し、2 を apply
(ツリーを辿る例)
(一種の非決定性計算をストレイトフォワードなコードだけでおこなう例)

Haskell

ContExample の Cont を cont にしないと動かなかったりするのは、自分の Haskell 環境の mtl がバージョン 1 系かバージョン 2 系かによる。1 は Cont で 2 は cont 。手元の環境の MacPortshaskell-platform を入れたものは 1 (配布してる ContExample の想定環境)、FreeBSD 環境は hs-mtl-2.0.1.0_1 が入っていたので 2 。FreeBSD portsGHC のソースを展開したものを見てみると ghc-7.0.3/libraries/mtl/Control/Monad/Cont.hs というファイルがあって内容は 1 系だが、hs-mtl-2.0.1.0_1 をアンインストールすると「Could not find module `Control.Monad.Cont':」になる
まず ContTutorial から。ContTutorial は Control.Monad を利用した限定継続の実装、その利用例、実装の正しさのチェック、といった内容である Control.Monad は 2010 標準( http://www.haskell.org/onlinereport/haskell2010/haskellch13.html#x21-19300013
演算子 +! とか定義してるのは、型を合わせるために liftM2 とかを付けてまわらなくてもいいようにするため( Scheme 使いでも、最初のカッコの山はこれはひどいと思うだろう)
t2 の中にある return (k 5*2) は return (k (5*2)) のミス。結果の値は 15 でなく 12 が正しい
newtype Cont の定義中の型変数の変数名 w は ω を暗示

*ContTutorial> runC $ reset $ (liftM2 (:)) (return 1) $ shift $ \k -> (liftM2 (:)) (return 2) $ return $ k $ k []
[2,1,1]

チュートリアルでは(ML にない演算子のためか)使われなかったが、$ を駆使するとこんな感じ)
(衝撃の「泡」が出てくる証明。ソースコード中のは UTF-8 で変数名として使われている)
ソースコード中の証明は、コメントアウトされていない。つまりコンパイルが通るということは型が正しいということ。ghci で :t proof1 とかやると型が表示される)
続いて ContExample 。こちらは Control.Monad.Cont を使っている( ContTutorial では、自分で定義している)。mtl パッケージ( http://hackage.haskell.org/package/mtl )に入っており Haskell Platform をインストールすれば入る
( runCT & resetT & shiftT と、それを利用した same_fringe のデモ( OchaCaml の same_fringe に相当))
(以下雑感)
たぶん普通に一日がかりの内容
限定されない継続によってもたらされる副作用の問題はどんなか( WiLiKi:Scheme:call/ccと副作用 http://d.hatena.ne.jp/sumii/20061121/p1
ML や Haskell では関数は 1 引数なので、タプルの中で shift してみる
OchaCaml の場合

# reset (fun () -> (shift (fun k -> 1), (shift (fun k -> 2)))) ;;
- : int = 2

一方 Haskell では型が合わなくなるのでこのようなことはできない(ようだ)