OchaCamlで限定継続/answer type modificationを勉強する
限定継続は面白いのですが、型がつくとイマイチ自分にはよくわからなくなってしまいます…。 何度目かの正直で、 去年の Continuation Workshop 2011 Tutorialで紹介された OchaCaml を使って勉強してみます。 何となくしか限定継続を分かってない自分用メモ。
難しいと感じる理由：型が変わる
自分が限定継続の型をムズカシイと思ってしまうのは
# reset (fun () -> 1);; - : int = 1
のように、resetの中にshiftが無い場合にはそのままresetは恒等関数になるのに、ひとたび shift を使うと
# reset (fun () -> shift (fun k -> 1) ^ "abc");; - : int = 1
reset の中が string なのに、 resetの外が int になってしまい、一貫した型がないように感じられてしまうから、のような気がします。 これがいわゆる answer type modification なのですが、shift/resetには具体的にどういう型が付いているのか、調べてみます。
準備
まず、OchaCamlを起動して、answer typeを全て表示するように設定します。
$ ochacaml #answer "all";;
answer type modificationと reset
answer typeとは何でしょう？ 理論は知らないのですが、 継続渡し計算の型 ('a -> 'r) -> 'r の 'r が answer typeと呼ばれます。(この型 'r の値を便宜的に answer と呼ぶことにします。)
では answer type modificationとは。 簡単な例として reset の型を見てみましょう
# reset;; - : (unit / 'a -> 'a / 'b) -> 'b = <fun>
この型 (unit / 'a -> 'a / 'b) は、「 unit -> 'a なんだけど、実行したらanswer typeが 'a から 'b に変わる」という読むらしいです。 この「実行したら型が変わる」というのは分かりにくいですが、最後に answer を'aから'bに変換する関数が走る、と思えばよさそうです。
shiftの型
# shift;; - : (('a -> 'b) / 'c -> 'c / 'd) / 'b -> 'a / 'd = <fun>
ほとんどワケわからないので、引数の中でanswer type mod.が起こらないと仮定しましょう。
さらに '/' も取っ払ってみます。
- : (('a -> 'b) -> 'c) / 'b -> 'a / 'c = <fun>
- (('a -> 'b) -> 'c) という(pureな)継続渡し計算を引数に取る
- shift (...) そのものは型'aを持っている (継続のスタート地点/文脈の穴の型は'a)
- shift全体としては、answer typeを 'b から 'c に変える
つまり、引数は shift がある位置から reset までの、型'a -> 'bの限定継続 をもらって、 それを 'c の値に変換するってことですね。 これがそのまま answer type mod. の /'b -> .. / 'c に現れています。おおっ。
全体として
# reset;; - : (unit / 'a -> 'a / 'b) -> 'b = <fun>
つきつめると、resetとは限定継続付き計算を実行し、answerを返す計算のようです。
reset の中の計算がpureなら、answer typeは変わらないので、型 unit / 'a -> 'a / 'a を持ちます (pureなunit->'a型の関数 (unit / 'c -> 'a / 'c) と (unit / 'a -> 'a / 'b) を単一化)。
- : (('a -> 'b) -> 'c) / 'b -> 'a / 'c = <fun>
一方、shift は、『限定継続 : 'a -> 'bをもらい、answer : 'cそのものを返す』という計算を使って、実際にanswerを変換する（と同時にresetまで脱出する） という感じでしょうか。
実験
ここまでの話とあまり関連しませんが少し例を書いてみます。
関数
let mydelim = fun f -> reset (fun () -> f () ^ "100") + 1;;
を定義します。 fの中から取れる継続は最終的に ^"100" と文字列を結合するところまでで「限定」されているわけですね。
ところでreset の中と 外で型が変わってますね。 型は
mydelim : (unit / string -> string / int) -> int = <fun>
で、 mydelim に渡す関数は必ずanswer typeをstringからintに変えなければならないようです。 つまりfの中で必ずshift呼べってことですね。
mydelim はどんな値に適用できるでしょうか。
shiftを呼ばないのでanswer typeが変わらない→型エラー
shiftを呼ばないと
Toplevel input: > mydelim (fun () -> "200");; > ^^^^^^^^^^^^^^^ This expression has type unit / string -> string / string, but is used with type unit / string -> string / int.
などと怒られます。 (fun () -> "200") の型はこの出現位置だと上記の型ですが 本来の型は unit / 'a -> string / 'a という「answer typeを変えない関数」ですね。 mydelim には answer type を変える関数を渡さなければならないので型エラーというわけ。
型付けできる例
# mydelim (fun () -> shift (fun k -> int_of_string (k "1234")));; - : int = 1234101
shiftで resetまでの継続 ( ? ^ "100" ) をkに束縛し(?は穴)、それを "1234"で呼ぶと "1234100" が得られます。 shift は中身が完了するとresetまで大域脱出する(といっていいのか何なのか)ので、あとは int_of_string で 整数にすれば、 reset の続き +1 とも型が整合する、と。
まとめ
限定継続のanswer type modificationの基本的なところを調べてみました。
次回以降(あれば)では、限定継続が制御を逆転するさまを調べてみたり、callerとcalleeがより複雑に相互作用する様子が型で表現されるとか、そういう方向の例を作ってみたいと思います。
実務で使うOCaml - 泥臭い仕事をサクっとこなす方法
プログラマが実務で出会うのは、問題が整理されたキレイな仕事ばかりじゃない。プロダクトに本質的じゃない部分でもプログラムを書く必要に迫られる。いわゆる開発方法論では抽象化されてしまう、今ここにいるソフトウェア開発者の悩みだ。
今日は、私が仕事で書いたOCamlのコードを晒して、如何にOCamlがプログラマの仕事の道具として優れているかを主張したい。泥臭く、関数的でない、エレガントさのかけらもない、生活臭のあるコードだ。勤務先はOCamlをメイン言語として使っている。研究所とかではなく普通に受託開発を生業としている会社だ。OCamlは理論一辺倒で、マニア向けで、現実のソフトウェア開発には使えない、という誤解が万が一あるかもしれないが、全くそんなことはない。 (Haskellもそうだけど、それはまたの機会に)
いかにOCamlが優れているかについての概論めいた話は、OCamlを数十人体制で10年使っているJane Street Capitalの Yaron Minskyによる なぜ次に学ぶ言語は関数型であるべきか をナナメ読みすればいいと思う。特に「なぜOCamlなのか?」のあたり。これはACM Queueという立派な雑誌の記事だし、もちろん熟読するに越したことはないと思う。
追記：キャミバ様 (@camloeba)にコードを改善していただけました! ↓のコードはザックリすぎてイマイチでしたが、面白い批評付きで読み易くなっています。
状況: 金融業のメッセージ通信プロトコル on TCP/IP
今回のコードを書くに至った状況について書きます。
指定した銘柄の株価を時系列で取得するソフトウェアを書くお仕事だった(*ちょっとぼかしてある*)。ここで問題になったのは、通信処理の実装だ。
プロトコルは上流側により定義されたTCP/IP上に作られた独自のもの。繋ぎっぱなしのストリームに、メッセージと呼ばれる単位のかたまりが、いくつも連番が振られて流れてくるようになっている。この基本プロトコルの上で、株価の銘柄コードと、ある日付範囲を指定してリクエストすると、レスポンスとして株価の系列が複数のメッセージに載って返送されてくる。あまりインターネット時代を感じさせるプロトコルではないけれど、これがリアルな金融業界の通信プロトコルのひとつなのだ。
説明のため、A社の1日から4日までの株価を取得するリクエストを
要求： ("A",1,4)と書き、レスポンス(メッセージの列)は
応答：[1100; 1098; 1081; 1120]
のように書くようにする。
泥臭い問題
調べていくうちに、プロトコルのアプリ層で欲しい機能が欠けていることがわかった。 というのは、レスポンスとリクエストを対応づけるIDがなかったのだ。
これは大きな問題だった。受け取ったメッセージがどのリクエストに対応するレスポンスのものか、すぐにはわからないのだ。 複数のリクエストを同時に投げると、複数のレスポンスの系列がストリーム中でインターリーブ(混ざりながら)しながら返送されてしまう。
要求の列：[("A",1,4); ("B",2,3)]応答の列：[1100; 1098; 910; 1081; 940; 1120] (* 1100, 1098, 1081, 1120 は A社の株価, 910, 940 は B社の株価 *)
なんということだ…
幸い、レスポンスのヘッダにはリクエストされた銘柄コードと日付範囲が入っている。
具体的には、上の応答の列は、ヘッダを含めると、次のような感じになる。 (ここでa=("A",1,4), b=("B",2,3)と略記します)
応答の列：[(a,1100); (a,1098); (b,910); (a,1081); (b,940); (a,1120)]
しかし、依然として、同じリクエストを2回投げた場合にはキーがかぶってしまう。
こんなプログラムを書きました
次の OCaml の関数 receive_quote は、金曜の昼間に一息で書いたコードだけど、それなりにまともに動いている。
ポイントは、
- コードが比較的短い。
- バッファがやや複雑な構造をしているにも関わらず、実行時エラーになるようなヘマをやらかしていない
- 引数の型をほとんど書いていない (実際、無くてもよい)
ざっくり書いただけのコードだし、RubyやPythonならこれよりちょっとだけ少ない分量で書けるかもしれないけど、実行時エラーに悩まされることになるかもしれない。私ならたぶんそうなる。しかしOCamlなら、コンパイル時にほとんどのエラーが検出されるし、実際、コンパイル成功後は意図通り動作しているので、週末は仕事を忘れて遊んで暮らせる。
コードに入る前にもっと詳細なことを書くと、各メッセージには「連番」と「リクエスト全体のメッセージ数」が振られている。
応答の列：[(a,1100,0,4); (a,1098,1,4); (b,910,0,2); (a,1081,2,4); (b,940,1,2); (a,1120,3,4)]
といった感じだ。
OCamlをよく知らない人のためにたくさんコメントを書いたけれど、普段はこんなに詳細に書いたりしない。コメントを外したバージョンは http://ideone.com/aWBKX にある。あれ？ 結構くどく書いてあるな…
type request = string * string * string (* リクエスト. 銘柄id,期間from,期間toの三つ組 *) ;; let code (c,_,_) = c type quote = { price:int; } (* 銘柄の値段．実際には、他にも多くの情報が含まれている *) ;; type response = { req: request; (* どのリクエストに対するレスポンスか *) body: quote; (* レスポンスの内容 *) seq:int; (* レスポンス中、何番目のメッセージか *) total:int; (* 応答メッセージの総数 *) } ;; (* 受信途中のレスポンスのバッファを次の連想テーブル(Map)で構成する。 OCamlのMapは、キーの型と比較関数をMap.Makeに渡せば得られる *) module M = Map.Make ( struct type t = request (* リクエスト型をキーとして *) let compare = Pervasives.compare (* 何か適当に比較してもらう *) end) ;; (* レスポンスを保持するバッファ。 一息で書いたのでやたら複雑な型だが、 リクエストをキー(上記)として、受信途中のレスポンスをペア (int * quote option array) で保持する。 このペアは (受信済みメッセージ数, 銘柄データの配列) という意味だ。 - 未受信のメッセージをNoneで埋めておきたいがため option 型の配列になっている。 - 同じキーをもつ複数のレスポンスを同時に扱う格納するため、リストにしてある。 - グローバル変数なのは醜いけれど、クロージャに入れればすぐになんとかなる *) let buf : (int * quote option array) list M.t ref = ref M.empty ;; (* 株価のリストをデータベースに保存する. ダミー *) let save (code:string) (quotes:quote option list) : unit = () ;; (* メッセージrをバッファに格納する。 レスポンス全体が得られたら、saveで保存する。 *) let receive_quote (r:response) : unit = if r.total=1 then save (code r.req) [Some r.body] (* 総レコードが1件のみであればすぐに保存 *) else begin let map = !buf in (* このリクエストに対するレスポンスのリスト(更新前) *) let all = try M.find r.req map with Not_found -> [] in (* バッファに新しいレスポンスを追加 *) let newentry () = let arr = Array.make r.total None in (* レスポンス全体をNoneで初期化 *) arr.(r.seq) <- Some r.body; buf := M.add r.req ((1, arr)::all) map (* 1つ受信しましたよとバッファを更新 *) in (* レスポンスのリストを走査し適切な位置に格納 / レスポンス全体が満たされたら保存 *) let rec addentry rest = function | [] -> newentry () (* 受信ずみレスポンスなし. 新しいレスポンスを追加する *) | (cnt, arr) as y::ys -> (* 受信ずみレスポンスあり *) match arr.(r.seq) with (* 当該の連番は受信済みか *) | None -> arr.(r.seq) <- Some r.body; (* レスポンスの該当する連番を満たす *) if cnt+1=r.total then begin (* レスポンス全体が満たされた. 保存後、この配列をバッファから除く *) save (code r.req) (Array.to_list arr) (* 保存 *); buf := M.add r.req (List.rev_append rest ys) map (* yの削除によりバッファを更新 *) end else (* また足りない．受信済み数をインクリメントしバッファを更新 *) buf := M.add r.req (List.rev_append rest ((cnt+1, arr)::ys)) map | Some q -> (* このレスポンスでは格納済み. 次のレスポンスを見る *) addentry (y::rest) ys in addentry [] all end ;;
簡単な動作確認
プログラム全体は http://ideone.com/6tUYa にある。
次のように入力を与えることができる。 Aのが2つ,Bのが1つ、レスポンスが来た状況だ。
let _ = let a="A","1","4" and b = "B","1","2" in let resps = [ {req=a; body={price=1100}; total=4; seq=0}; {req=a; body={price=1098}; total=4; seq=1}; {req=a; body={price=1100}; total=4; seq=0}; {req=b; body={price=910}; total=2; seq=0}; {req=a; body={price=1098}; total=4; seq=1}; {req=a; body={price=1081}; total=4; seq=2}; {req=a; body={price=1081}; total=4; seq=2}; {req=a; body={price=1120}; total=4; seq=3}; {req=b; body={price=940}; total=2; seq=1}; {req=a; body={price=1120}; total=4; seq=3}; ] in List.iter receive_quote resps
save関数を、画面にプリントするようにしてあるので、次のような出力が得られる：
A 1100;1098;1081;1120; B 910;940; A 1100;1098;1081;1120;
結論
同じコードをJavaで書こうと思っていたけれど、ちょっと大変そうでそんな気が起きないのでそれは誰か物好きに任せたい。
十中八九、OCamlのほうがJavaより保守性が高く見やすいコードになるはずで、それは上のコードをもっとエンタープライズ的に(log4j的なものににログを出すとか、アサーションを埋め込むとか、例外的状況に対処するコードを入れるとかで)書き加えても変わらないだろう。
ここまで書いておいて何だけれど、OCamlでうまくプログラムを書く方法とかはよくわからない。 ただ、上の場合は、
- データ構造を先に決めた。レスポンスのキーで引くためにMapが必要だな、で、ランダムアクセスなので配列をここに、キーが被るのでリストにして…破壊的に更新されるバッファだからrefに、という風に。
- そして関数本体を、上で決めたデータ構造をなめるように書いた。
という手順だったように思う。 いつでも使えるわけではないけれど、とりあえず型を決めて、あとはガリガリコードを書いて、型エラーをつぶしていけば、いつのまにか問題は解けている。
OCamlは、何も概念的に難しいわけではない。関数プログラミングで実行効率を高めるためのちょっとしたイディオムはあるかもしれない(上のコードでいうrestとList.rev_appendとか)けど、基本的にはスッキリとした簡潔な言語だし、なんといっても多相性と完全な型推論が嬉しい。
また上の副作用バリバリの例を見ればわかるが、実のところ、OCaml で関数型プログラミングにこだわる必要はないのである。というか、caml.inria.fr/ocaml には関数型なんて言葉は一つもでてこない。
Haskellの純粋関数的なフレーバーとモナドの話は知的好奇心をくすぐるし、FRPのように根本的な解決策は夢を与えるし、見た目もエレガントだ。一方、OCamlはあくまでもC++,Java,RubyやPythonのような既存のプログラミング言語の延長線上にあるものだ。手続き的・オブジェクト指向なプログラムの書き方もできる。しかしそれに加えて、型によるバグの発見が非常にパワフルで、また関数的(immutableなデータ構造や高階関数を使った)プログラミングを基礎に設計されているため何かとスッキリしている言語なのだ。
「すごいHaskellたのしく学ぼう！」は気配りと楽しさがすごい
本書はHaskellの入門書です。とっても親しみやすい内容と文体で、構成についても、順序を踏んで丁寧に書かれているようです。また日本語(マルチバイト文字)の扱いを付録で解説しているのもポイント高いですね。
以下、ざっくり目を通して、これは！と思った点をまとめました。
イントロはHaskellの概要をやさしい文体で、でもしっかり説明しています。 Haskellがもつ純粋さと参照透明性の重要さ、必要最小限の計算を行う遅延評価であること。型付けが重要なのは当然として、型推論がすばらしいこと。さいごに「Haskellはエレガントで簡潔です」。
全体として：気配り
翻訳が読みやすいです！親しみやすさが日本語になってグッと増した感があります。翻訳文であることを全く感じさせません。
また随所で、著者の気配りを感じさせられます。 文中の補足説明やNOTEが親切です。たとえば、初見ではワケわからない型の周りエラーの読み方 (No instance for (Num [Char])とか) が1章の最初にあることからしてもそう。 5(数値リテラル)は実はすごいやつで、整数にも浮動小数にもなれるとか。項や型の読み方をその時点で必要な分だけ丁寧に説明して、残りは後ろの章に送っているのも良いですね。
前半の構成はなるほど王道！ Haskellで最も重要な「型」は2章で読み方とともに基本が丁寧に解説されます。続けて、2.4節で型クラスの基本が分かってしまうのはお得感があるね。
「すごいHaskell」な所
普段はまったく内容を説明しない挿絵ですが、ヤマ場ではちゃんと内容を説明しています。最初のヤマ場はfoldとか再帰とか二分探索とか。どちらも関数型の肝といえる部分で、7.7の解説は熱が入ってます！
挿し絵が本文の内容をちゃんと説明をしていたら、その内容が「すごいHaskell！」な所じゃないかなと思ったりしている:)
型クラスを「たのしく」
二つ目のヤマ場は前半のゴールともいえる「7.8 型クラス 中級講座」。その直後で型クラスを応用する方法が面白い。JavaScriptを引き合いに出して、YesNoという型クラスを作って遊んでみる。 それほど長くない節だけれども、型クラスのオープンさと、プログラミング的楽しさがよく出ていると思う。
実用もちゃんと意識してます
IOは、当初は8章でモナド無しで(do構文で)導入されます。モナドはもっと後。しかし ByteStringが9章で紹介され、文字列処理は高速にチューニングできるんだよ、と語られる。 Haskellを実用するうえで避けて通れない問題です。(付録も含めて。)
10章「関数型問題解決法」これは気になるよね！ 関数型プログラミングのエッセンスです。たぶん中盤のヤマ場です。 なぜなら挿し絵がちゃんと仕事してるから! 逆ポーランド電卓と、単純化した最短路問題を解きます。これも「たのしく」て、かつ手ごろで良いと思う。
本書のユニークな点：Applicativeの次にモナド
本書の最もユニークな点はモナドの説明にApplicativeを使っているところ。いきなりモナドを説明するのでなく、Applicativeという中間ステップを踏めば、たしかに概念的なジャンプが少なくなる気がする。
とくに注目したいところは、IOアクション同士をつなぐ方法としてApplicativeを最初に使っているところだ。 pure (++) <*> getLine <*> getLine *1 と書けば、文字列を連結する (++) を、IOアクション getLine の戻り値に適用していることがわかる。 (++) str1 str2 の 関数適用の空白を <*> に置き換えればこの形になるので、IOアクションを合成する最初の方法として良い感じ。
うゎぁあああああ落ちるぅぅうううああああ
13.4「綱渡り」。モナドを説明するヤマ場です。ついに発狂したと思ったよ。でもマジです。Applicativeではダメで、モナドが必要な理由がここで明らかになります。
まず「普通の値を取り、モナド値を返す関数」の必要性が語られます。
landLeft :: Birds -> Pole -> Maybe Pole landLeft n (left, right) | abs((left+n)-right)<4 = Just (left+n,right) | otherwise = Nothing
leftとrightの差が4以上になったら、バランス崩れたのでしっぱーい。ナッシングというわけ。
そして、こういう関数を合成しようと思ったら、Applicativeではむり。モナドの出番というわけだ！Hooray!
すごいリストモナド
後半戦の最初のヤマ場、すごいHaskellな所はリストモナドだ。納得。それにp.303の絵をみればちゃんと仕事してるし:) 威力はチェス盤の上で示されます。ナイトの動きを非決定的計算で全て列挙してみよう！
（続いて14章では各種モナド＆モナディック関数(mapMとか)の紹介があり、これで普通にHaskellを使えるようになりましたね！という構成。無いのはContモナドくらいのものだけど、あれ私はあんまり使わないし本書には要らないと思う）
さいごにpureなzipper
最後にzipperが来て、モナドなくてもHaskellすごい！ となるわけです。（挿し絵調べ）ここはまたちゃんと読みたいです。
そして15.5節、感動のフィナーレが君を待つ。
私に関して言えば
ApplicativeやZipperの章はあまり真面目にやってなかったので役に立ちました/立ちそうです。また後半でも普通に役に立つ訳注があり読み応えがあります。（そういうピックアップが目的なら、PDF版がサクサク読めるのでいいですね）。付録、マルチバイト文字とViewPatternとの組み合わせも面白い！訳語表があるのも信頼できます
気になった(些細な)こと
- バッククォートの書体が文中とコードでかなり異なりますね。仕方ないのかな
- p.26右下の空白はなに？
- p.61の右にも何か空白がある。絵が抜けてるのかな。
- p.288の右
何かPDF版の挿し絵が一部抜けているような気がしますねー。 ビューアの問題かな。→ オーム社開発部ブログにアナウンスがありました
- 私の環境(MacOSX 10.7.3) で Preview.app を使って閲覧すると絵が欠けるのですが…ううむ
- Adobe Readerなら正しく表示されるようです(私も確認ずみ)
- どうも10.5系のPreview.app だと正常に表示され、10.7系だと挿し絵が欠けるようです。10.6は手元にないので不明。 これは発覚しづらいですね。。
weak pointとか
*1:原文では (++) <$> getLine <*> getLineだけど、<$>の意味はちゃんと説明されている
ConduitとPersistentを使って高パフォーマンスなDB処理を目指す
Iteratee/Enumerator系の話題がHaskell界隈で騒がれて久しい (日本語の紹介記事)。これらはHaskellで細粒度のリソース制御ができるストリーム処理の方法で、例外処理もやりやすい、という触れ込みだった。曰く、ストリーム処理はリソースの消費量の点で（オンメモリに全てを置くよりも）優れているが、hGetContents::IO Handle->Stringのような遅延IOはファイルのクローズなどリソースの制御が難しい。それを改良したのがIteratee/Enumerator系のライブラリだそうだ。
Conduit
iteratee/enumeratorの改良を試みているのが Conduit （コンディット？）だ（日本語の紹介記事）。 最近でもずっと改良がつづいているようで(参考：tanakhさんの発表資料)、例えばSource/Conduit/Sinkの型がPipeに統一されたりと、概念的に整理されてきている段階なのかな、という印象を受ける。ConduitはWebフレームワークYesod （おそらく主流の一つ） で使われており、きっと今後も期待できるライブラリだ。
Persistent
Persistentは、Yesodアプリのバックエンド部分で使うライブラリだ。 オブジェクト指向言語におけるO/Rマッパー（…よりもシンプルで頑健かつ安全だと期待している…）のように、HaskellにおいてDBアクセスをシームレスに行うライブラリだ。
Persistentには selectSource という関数が用意されており、Conduitを用いたストリーム処理でDBの読み出しが書ける。
ごく簡単な例
ほぼPersistentの最初の例からの写しだけど、こんな感じに：
{-# LANGUAGE QuasiQuotes, TemplateHaskell, TypeFamilies, OverloadedStrings #-} {-# LANGUAGE GADTs, FlexibleContexts #-} import Database.Persist import Database.Persist.Sqlite import Database.Persist.TH import Control.Monad.IO.Class (liftIO) import System.IO (stdout) import Data.ByteString.Char8 (pack) import Data.Text.Internal (Text) import Data.Conduit import qualified Data.Conduit.Binary as CB share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persist| Person name String age Int Maybe deriving Show |] type SqlSource v = Source (ResourceT (SqlPersist IO)) v conduit_test :: IO () conduit_test = withSqliteConn ":memory:" $ runSqlConn $ do runMigration migrateAll johnId <- insert $ Person "John Doe" $ Just 35 janeId <- insert $ Person "Jane Doe" Nothing runResourceT $ mapOutput (pack . (++"\n") . show) (selectSource [] [] :: SqlSource (Entity Person)) $$ CB.sinkHandle stdout return () main = conduit_test
[persist| … |]で囲まれた部分がDBのスキーマ記述にあたるDSLで、Haskellのデータ型に展開されると同時にsqliteのテーブルが作られる。 Template HaskellやQuasi-Quotation を使って実現されている。シンプルでDRYな感じに好感が持てる。
runResourceT から始まる行が Conduit部分だ。 $$ は Source と Sink を接続する演算子であり、接続された物体がResourceT型を持つモナドを、runResourceTで実行する．
Souceは、selectSource で Entity Person型のデータを無条件にselectしたものだ。
さらに、mapOutputで、Entity Person型のsourceからの出力を、ByteString型に変換している。
Sinkは、CB.sinkHandle という関数で、 ByteString型の入力を全てstdoutに流し込む。
いわゆるリストを使った遅延IOより少しだけ複雑だが、さらにモナド変換子を重ねるための抽象化のため、最初はとっつきにくい印象だ。しかし Source, Conduit, Sink の型がすべて Pipe i o m r 型 の型シノニムになっているため、じつのところ非常にすっきりしているように思う。
Pipe i -- 入力の型 o -- 出力の型 m -- 下にあるモナド (IOや ReaderT r IO など。上記では SqlPersist IOというモナド) r -- モナドの計算結果の型
Pipeはモナドになっているので、お馴染みのdo構文でsourceやsinkを合成できるのも良い感じだ。
例外処理の扱いなども興味深いがまたの機会に。
型エラーの怪
ところで、上の例を作ったとき、型エラーを解消するのにちょっと時間がかかってしまった。
pack . (++"\n") . show :: Show a => a -> ByteString
で、データベースから取り出したデータをshowしByteString型に変換しているが、最初に書いたときはここで、
(++"\n") . show
と、packを忘れてしまっていた。 もちろんこの型エラーはGHCによって報告された：
persisttest.hs:32:14:
Couldn't match expected type `[Char]'
with actual type `Data.ByteString.Internal.ByteString'
(略)しかし、この上の行には、何やら別の型エラー2つが出ていた。
persisttest.hs:23:16:
No instance for (Control.Monad.Trans.Control.MonadBaseControl
IO m0)
arising from a use of `withSqliteConn'
(略)
persisttest.hs:27:15:
No instance for (Control.Monad.Trans.Control.MonadBaseControl
IO m1)
arising from a use of `insert'
(略)通常、こういった型変数がらみの"No instance for ..."というエラーは，型注釈が足りていないために起こる。 (show . read) が良い例で、どの型クラスのインスタンスを選んでよいかわからないとコンパイラ様がお怒りになる。
しかし 上の ByteString と Char の型ミスマッチを解消すれば、この型エラーは消える。順番に withSqliteConn や insert に型注釈を加えていた私は釈然としない。
原因はたぶん、 型エラーのせいで 型が分からなくなった runResourceT の呼び出し部分に (fresh な) 型変数 m a を割り当てるためだ。
runSqlConn の引数もまた SqlPersist m a 型なので結局 型変数 mを具体化できず、インスタンスを特定できないのだ。
上の例では、型推論による型mの伝播方向が単方向である(Entity型が決まると、associated type ([persist|...|]の部分から生成される) によりモナドの型SqlPersist IOが決まり、それが全体に伝播する)。
このため、型を具体化している源流で型エラーが起こると、連鎖的に別の"No instance for"エラーが引き起こされるのだった。
結局、モナド変換子をあまり型変数で抽象化しまくるのも問題だということか。
しかしこの場合なら、ただ
runSqlConn :: SqlPersist IO a -> Connection -> IO a
としておくだけで余計な型エラーを抑制できる。場合によっては使えそうなテクニックかもしれない
型クラスで tagless DSL メタプログラミング
これは Haskell Advent Calendar 2011 の5日目の記事です。 去年も書きましたが、その記事はこちら → Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記
先日の記事 Haskell＋タグレスな型付きDSLで楽々！C言語コード生成 - keigoiの日記 をちょっとブラッシュアップした。前回はコードについては全く説明しなかったので、改めて解説する。
おさらい
HaskellやOCamlなどの関数型言語は、プログラミング言語の処理 ― 構文解析とコード生成 ― がとても得意だ。 大手のソフトウェア企業として知られる NTTデータも既存コードの処理 (構文解析〜リバースエンジニアリング) のために Haskell を使っているそうだ。 (函数プログラミングの集い2011より。インドに外注する部分もあるそう togetter 1, 2, 3)
ソフトウェア設計でホットな話題の一つは、ドメイン特化言語 (DSL) による抽象化である。 ある問題領域（ドメイン）の語彙をDSLにうまくまとめて、そのDSLからコードを生成するコンパイラを書けば、より迅速に、かつスケールする形で（例えば多人数で）効率的にソフトウェアを開発できる。
特にプログラマにとって面白いのは、 EDSL (Embeded DSL) という、ライブラリの形で言語に「埋め込んで」提供する形のDSLだ。利用者側にとってはホスト言語 (Haskellなど) の型や関数定義などの抽象化機能を利用できる点で便利であり、また実装者にとっては、かかる手間がより少なく済む(構文解析や型チェッカが不要)。
今回のソース
今回の記事で使ったHaskellのソースコードを http://proofcafe.org/~keigoi/Advent2011.hsに置いた。長さは180行弱。
純粋関数的（簡易）EDSLの設計
今回は、ごく簡単な四則演算とループのみを備えた、純粋関数的なEDSLを実装する。 このEDSLでプログラムを記述し、実行すると、記述内容をC言語にコンパイルしたソースコードが出力される。そのコードをgccなどのコンパイラに与えれば、実行形式が得られる。
別の見方をすると、 C言語の「マクロ」をHaskellで書くと思えばいい。 HaskellはCの標準のプリプロセッサと違って、強力な型システムを備えている。 例としては非常に小さいが、それでも Haskellの高階関数を効果的に利用すれば、C言語では不可能な抽象化も簡単にできる。
タグレスDSL
前回書いた通り、実装はタグレスにする。 これはつまり、中間データ表現を介さないということだ。 ただ中間表現を廃止してまうと、その中間表現から得られたであろう様々な柔軟性が失われ、一つの用途にしか使えなくなる。これを回避するために、変換先の型を型クラスで抽象化する（今回の記事ではC言語コード生成しかしないのだが）。
まず、対象言語の「式」を表す型構築子Expを与える。
newtype Exp l a = Exp {unExp::l a}
ここでaは式の型、lは変換先の型を抽象化した型構築子だ。
次に、対象言語の関数プリミティブを導入する。
data FunName = Op String | Name String newtype Func1 a b = Func1 (FunName, a -> b) newtype Func2 a b c = Func2 (FunName, a -> b -> c)
FunNameは、その関数のC言語における名前（または演算子）を表す。 Func1は１引数関数、Func2は2引数関数だ。それぞれ中身は関数名と関数のペアになっている。前者はC言語のコード生成に使われる。後者はHaskellの式を評価するときに使い、Cのコード生成には関係ない。
構文は、次の型クラスで与える。Langという名前は、このEDSLがC言語ソースを生成するだけでなく、Haskellの式としても評価でき、他さまざまなプログラミング言語を出力できる可能性を表しているつもりだ。*1
-- 'tagless' representation of the language class Lang (l :: * -> *) where -- | true constant true :: Exp l Bool -- | false constant false :: Exp l Bool -- | constant of type Int int :: Int -> Exp l Int -- | func e1 func1 :: Func1 a b -> Exp l a -> Exp l b -- | func e1 e2 func2 :: Func2 a b c -> Exp l a -> Exp l b -> Exp l c -- | if-then-else ifThenElse :: Exp l Bool -> Exp l Int -> Exp l Int -> Exp l Int -- | loop loop :: Exp l Int -> Exp l Int -> Exp l Int -> (Exp l Int -> Exp l Int -> Exp l Int) -> Exp l Int -- | let-binding in the target language let_ :: Exp l Int -> (Exp l Int -> Exp l Int) -> Exp l Int
true,false,intは言語の定数だ。 func1, func2 は関数の呼び出しである。 ifThenElseは文字通りif文だ。loopはややわかりにくいが、 loop from to acc f でfromからtoまでaccにfを繰り返し適用する高階関数である。 let_ は、ターゲット言語におけるletである。Haskellのletだと式が複製されてしまうので、こちらのlet_を使うようにする（このように、式の共有を自然には扱えないのがEDSLの欠点のひとつだが、解決策もある(observable sharing)）。
C言語ソースコード生成部
型クラスLangのインスタンスとして、C言語のソースコードを生成する部分を与える。 つまり、型 Exp l a の l に相当する部分を与え、それへの変換をここで実装する。
名前生成モナド
まず、自動生成するコードに現れる変数どうしが衝突しないように工夫する必要がある。この名前管理をStateモナドで与える。
class Monad q => MonadQ q where newName :: String -> q String instance MonadQ (State [(String,Int)]) where newName str = do varmap <- get let cnt = fromMaybe 0 $ lookup str varmap put $ (str,cnt+1):deleteBy (\(a,_)(b,_)->a==b) (str,0) varmap return $ str ++ show cnt instance (Monoid w, MonadQ m) => MonadQ (WriterT w m) where newName = lift . newName
要するにnewNameは文字列fooからfoo0,foo1,..という名前を生成するだけだ(アホなバグがあったので直した)。 後で使うために、WriterTでリフトした場合にもMonadQのインスタンスになるようにしてある。
C言語ステートメントを運ぶWriterモナド
C言語は残念ながらHaskellのような式を中心とした言語ではなく、ifやforなど一部の制御構造は文（ステートメント）である (gcc拡張でブロックを式として扱えたりするが)。 そこで、コード生成モナドには「その式を計算する前に実行しなければならない文のリスト」を持たせるようにする。コード生成計算毎に副作用として文のリストが生成されてゆくことになる。 このような場合に適したモナドは何か？ そう、Writerモナドだ。 既にStateモナドを使っているので、それを WriterT で持ち上げるようにする。このモナドにWという名前をつける。
type W a = WriterT [C.BlockItem] (State [(String,Int)]) a
C.BlockItemはC言語の文を表すlanguage-c-quoteの型だ（Language.C.SyntaxをCと略している）。一方、C言語の式は C.Exp という型を持つ。
結局、EDSLの式に相当するC言語コードを表す型は、 W C.Exp という型になる。
ソースコード生成器
ここまでに見てきたように、コード生成結果の型は、Wモナドの型をもつ。 結局、型Exp l aのlに置く型 (CGenと名付ける) は次のようになる：
newtype CGen a = CGen {unCGen :: W C.Exp}
型 CGen a は、型aの値を計算するC言語の式(と文)であるが、 型aは コード生成に使わない幽霊型である*2。
いろいろな型を変換する便利関数も準備しておく。
unExp_ :: Exp CGen a -> W C.Exp unExp_ (Exp (CGen m)) = m cgen :: C.Exp -> Exp CGen a cgen = E. CG . return cgenW :: W C.Exp -> Exp CGen a cgenW = E . CG
実際にC言語のコードを生成する部分は、次のLangのインスタンス宣言だ。 CGen型がWモナドになっているので、コード生成器に必要な様々な副作用を入れられるようになっている。
-- generate C code!! instance Lang CGen where true = cgen $ [cexp| TRUE |] false = cgen $ [cexp| FALSE |] int i = cgen $ [cexp| $int:i |] func1 fun e1 = cgenW $ do x <- unExp_ e1 return $ case fun of Func1(Name funname,_) -> [cexp| $id:funname( $x ) |] Func1(Op opname,_) -> (C.UnOp (toCUnOp opname) x noSrcLoc) func2 fun e1 e2 = cgenW $ do x <- unExp_ e1; y <- unExp_ e2; return $ case fun of Func2(Name funname,_) -> [cexp| $id:funname( $x, $y ) |] Func2(Op opname,_) -> (C.BinOp (toCBinOp opname) x y noSrcLoc) ifThenElse cond then_ else_ = cgenW $ do tmp <- newName "tmp" cond' <- unExp_ cond (thenExp, thenStmts) <- lift $ runWriterT $ unExp_ then_ (elseExp, elseStmts) <- lift $ runWriterT $ unExp_ else_ -- 変数宣言を生成し、if文の内部で代入する tell [C.BlockDecl [cdecl| int $id:tmp; |], C.BlockStm [cstm| if($cond') { $items:thenStmts $id:tmp = $thenExp; } else { $items:thenStmts $id:tmp = $elseExp; } |] ] return [cexp| $id:tmp |]
let_, loop については読者に委ねる（ifを参考にすればそう難しくないはずだ）。 toCUnOp, toCBinOpはFunc1,Func2からC言語の演算子に変換する関数である。
実行
次のようにモナドを走らせればよい：
toString :: Exp CGen Int -> String toString exp = case flip evalState [] $ runWriterT $ unExp_ exp of (exp, blocks) -> unlines (map show blocks) ++ "return " ++ show exp ++ ";"
時間がなくなってきたので非常につまらない例で恐縮だが、例えば ifThenElse (1 >. 0) 1 2 という式からC言語の式を生成すると
Main> putStrLn $ toString (ifThenElse (1 >. 0) (1*2) (3+4-5)) int tmp0; if (1 > 0) { tmp0 = 1 * 2; } else { tmp0 = 3 + 4 - 5; } return tmp0;
のようになる。ここで、 E CGen Int を Num のインスタンスにすることで、よりHaskellっぽい構文で書けるようになっている。
まとめ
この記事では、以前に引き続き、Oleg Kiselyov氏のtagless interpreterを応用して、C言語のソースコードを生成する例を示した。 ソースコードは http://proofcafe.org/~keigoi/Advent2011.hsにある。 以前よりはソースコード生成の具体的な方法に踏み込めたと思う。実装にモナド変換子を使ったりと、初心者にも面白い用例になっているかもしれない。
この言語を使って書ける計算は限られているが、Langクラスのメソッドを追加すればどんどん拡張できる。純粋関数に限定しなければ、もっと複雑で実用的なプログラムの生成も簡単だろう（その場合、EDSLの見た目が純粋関数的なHaskellの意味と乖離していくことになるが、モナドの記法などを流用してそれらしく見せることもできる）。
タグレスDSLを入り口として、Haskellを使ったプログラム生成でソフトウェア開発をより効率よく開発できるようになることを期待したい。
*1:私の手元にある実装では、これに加え タプル型や配列、構造体の一部を扱えるのだが、簡潔さのため割愛した。特にタプルの扱いはちょっと工夫したので、機会あればお披露目したい
*2:幽霊型なので、型はコード生成時に「捨てられる」ことになる。型を捨てているせいで、let_やifにおいてC言語の変数宣言における型がint一種類に決め打ちせざるを得なくなっている。後の拡張として、ifやletがint以外の型を返せるようにするには、型aの情報を使って変数宣言を生成することになる。これを実現するためには、実行時型情報を持ち運べるData.TypeableかGADTを使う。今はint型のみを相手にしているので、勝手にint型の宣言を生成している
OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完)
VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。
仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。
検証にはCFMLというツールを勉強しながら使った。 これを使えば OCaml のソースコードを Coq で検証できる。 それも ref型による破壊的代入つきの手続き的なOCamlを含む。 そして Coqと違い、プログラムは停止しなくてもいい。 つまり、CFMLを使えば、 手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って検証できる。 他の検証器を使えば似たようなことができるだろうけど、OCamlのコードを読んでくれるのは手ごろでよい。パターンマッチも、高階関数も使える。 （最近ではICFP 2011でも発表があった。 @esumii さんのツイートを目にしたときにちょっと興味をもったのだけど、例も多く興味深いツールだと思った）
ただ、時間が足りずまともな証明はひとつも書けなかった。残念。
CFML のパワー
CFMLは、既にかなりの量のプログラムの検証に成功している。
- 一例として、かの有名な Chris Okasaki による Purely functional data structures (純粋関数的データ構造) のアルゴリズムの証明が CFML で書かれている。
- 手続き的なプログラムも検証できる。 Dijkstra の最短路アルゴリズムなど
非常に強力なパワーを持っており、あとは使いこなせれば幸せな世界が待っているに違いない！
CFML の理論
CFMLはホーア論理によく似た方法で仕様を記述する。
ホーアの三つ組みは
{P} t {Q}という形をした式で、 「事前条件P(というメモリの内容)のもとで プログラムtを実行し、停止したとき結果はQ(というメモリの内容)である」、と読む。
CFMLにおけるそれは、特性論理式 *1 (characteristic formula / formulae) という。CFMLのCFだ。 とりあえず特性論理式はホーアの三つ組みのようなものだと思っておいてよさそうだ。ホーアの3つ組と非常に良く似た形をしており、
[t] P Q
のように書く。tはプログラムで、[t]はtの特性論理式だ。P,Qは事前・事後条件を表す。 P,Qが右に来ているのはCoq（というか関数型言語）の記法で、高階な論理式 [t] に 命題 P, Qを適用しているという操作を表しているが、 単にそういう書き方だから、と思っていい。 特性論理式は高階論理式になっており、ホーアの3つ組の P(事前), Q(事後) の部分に穴があいたテンプレートとして扱える。 特性論理式に事前条件・事後条件を適用した論理式を証明できれば、その性質は証明完了というわけだ。
また特性論理式は元のプログラムの構造を保存しており、ちょうどホーア論理の推論規則を適用するかのような証明ができる。
(考え方自体は、並行理論の様相論理式と並行プロセスの関係によく似ており、特性論理式という名前もそれに由来する（論文中でも言及されている）。 あるプロセスp に対し、それを特徴づける様相論理式の集合 L(p) が存在する、という、 HennessyとMilnerによる characterization theorem という定理が知られている。 論文 Algebraic Laws for Nondeterminism and Concurrency の Theorem 2.2 だ。 曰く、プロセスpとqが振舞い等価(bisimilar) iff 特性論理式の集合L(p)とL(q)は一致する。同様に、プログラムt1,t2の振る舞いが同じとき、 高階論理式 [t1] と [t2] が論理的同値である、ということもあるかもしれない(が、ぱっと見た感じではそういう定理はなかった)。)
CFML のツール、ライブラリ、サンプル
CFMLは、OCamlのソースをCoqの特性論理式に変換するツールと、Coqのライブラリからなる。
ドキュメントにかなり詳しく書かれているので、とても参考になる。
ツールの使い方は簡単だ。foobar.ml を コマンドラインツール main.byte に与えれば、 特性論理式が書かれた foobar_ml.v が出てくる。 ただ実際に特性論理式を直接使うわけではないようだ。 ドキュメントや色んなサンプルを眺めてみると、Spec という謎の記法を使って仕様を書いている。
たとえばλ式の評価器 LambdaEval.ml は 代入の関数 subst と β簡約の関数 eval がある。 これの仕様は、
Lemma subst_spec : Spec subst x v t |R>> R [] \[= Subst x v t].
と書いてある (LambdaEval_proof.v)。 ここで subst は OCamlの関数名だ。 Spec _ _ … _ |_>> _ は特殊な記法で、 最初の x,v,t,R は右に出現するx,v,t,Rをそれぞれ束縛している。 >> の右に出現する R が特性論理式になっている。 [ ] は 分離論理の 空ヒープを表す論理式だ。 (subst関数はグローバルな参照セルを使わないので 事前条件は [ ] になる。) \[= Subst x v t] は、 実行結果の値が Subst x v t と等しいことを表す。 ここで Subst は人間が手動で定義したCoqの関数でMLの substに相当する。
全体で、 「MLの式 subst x v t を評価すると Subst x v t と等しい値になる」と読む。
もちろん subst は停止する関数なので、 わざわざ CFML を使わなくても、 Coqで定義した Subst を Extract すればいい。
eval は事情がことなる。停止しないのだ。そこで、(LambdaEval_proof.v) では λ式 t が vに(big stepで)β簡約される、という関係 Reds を定義して、
Lemma eval_spec : Spec eval t |R>> forall v, Reds t v -> R [] (\= v).
と書いている。 「t のβ簡約が 止まってvになるならば、 evalも停止してvを返す」と読む。
これらは純粋関数的に書かれた証明だが、他の手続き的なアルゴリズムの証明もまたぜひ読んでみたいと思う。
CFMLを使った証明
ホーア論理の一定の推論規則に相当するタクティックが用意されている。 (後で書くかも)
VSTTE 2011 competition 問2
問題は手続き型アルゴリズムの問題がいくつかあったので、CFML向きといえたかもしれない。
ただ自分はとりあえず純粋関数的な問2に当たってみた。 停止しない関数なのでCoqでは扱えないが、CFMLではどうなるか見てみたかったのだ。
SKコンビネータという超簡単なプログラミング言語の評価器を書いて検証する問題だった。 問題じたいは(ぱっと見)そう難しそうに見えない。 しかしこの評価器は停止しないため、Coqの関数として直接Fixpointで書くことはできない。
OCamlで評価器を書くとこんな感じになる(検証してないのでバグがあるかも！)：
type cmb = S0 | K0 | Ap of cmb * cmb;; let rec reduction : cmb -> cmb = function | S0 -> S0 | K0 -> K0 | Ap(K0,t1) -> Ap(K0, reduction t1) | Ap(S0,t1) -> Ap(S0, reduction t1) | Ap(Ap(S0,t1),t2) -> let v1 = reduction t1 and v2 = reduction t2 in Ap(Ap(S0,v1),v2) | Ap(Ap(K0,t1),t2) -> let v1 = reduction t1 and v2 = reduction t2 in v2 | Ap(Ap(Ap(S0,t1),t2),t3) -> let v1 = reduction t1 and v2 = reduction t2 and v3 = reduction t3 in reduction (Ap (Ap (v1,v3), Ap (v2,v3))) | Ap(t1,t2) -> reduction (Ap (reduction t1,t2)) ;;
(S,K,適用を それぞれ S0, K0, Ap としている)
証明（途中）
*1:とりあえずこう呼ぶ． 特性論理式という訳は誰が思いついたんだろう. ググってもひとつも出てこない． 私が適当に考えた訳をそのまま使っているだけかもしれない．ただ characteristic function=特性関数なので、そんなに変ではないはずだ
最近の話
論文でました
EPTCSというオンライン論文集に私の論文が掲載されました。 指導教員の先生との共著になっています。 Session Type Inference in Haskell
WOCS9で発表します
第９回クリティカルソフトウェアワークショップ (WOCS9) @ パシフィコ横浜 (11/17木-18金) で発表します。 17(木)の午前です。 主著はわたしですが id:yoshihiro503 の代理のようなもので、内容は彼が PPL2009/TPP'10 で発表した ミドルウェア検証の話をより詳しく、といったところです。
いつか自分のネタでCoqを使って発表したいなあ。
ICFP 2011に行きました/CUFP 2011で発表しました
もう1ヶ月以上前になりますが、 はじめてICFPに参加しました。またCUFP 2011で発表させていただきました。 発表資料はこちら(えらく重いですorz)。 id:camlspotter さんには大変お世話になりましたm(__)m
