実務で使う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なデータ構造や高階関数を使った)プログラミングを基礎に設計されているため何かとスッキリしている言語なのだ。

バグ、余談

上の例には、Mapに空リストが残ったままになるというバグがある。ヘビーに使っているとメモリリークが顕在化するかも。
余談だけれど、実のところ ベースのプロトコルはもっと複雑で、大半はC++で書かれている。 我々のアプリはOCamlで書かれており、上記のようなglue codeを書いたというわけ。

「すごい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とか

• Hackageの紹介を8章の訳注扱いにとどめるのではなく、付録とかでHaskellの有用なライブラリを紹介できたらいいかなと思う(欲張り)。DB, Web, コンパイラ, 並列など, 面白いトピックは多いと思う。(でも、それ特有の難しさはあると思う(枯れやすいとか))

*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の読み出しが書ける。

インストール

Haskell Platformが入った状態で

cabal install persistent
cabal install persistent-sqlite

でインストールできる。

ごく簡単な例

ほぼ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

函数プログラミングの集い

行ってきました。 togetter ← 発表資料へのリンクあり。
色んな方の発表が聞けて、また色んな人と再会できてよかったです。

ProofSummit 2011

発表しました (separation logicについてざっくり調べたことをお話しました。) 資料はこちら togetter

Haskell＋タグレスな型付きDSLで楽々！C言語コード生成

関数型プログラミング言語とコード生成

HaskellやOCamlなどはコンパイラなどの言語処理系の実装を得意としている。さすがに日常的にコンパイラを実装している人はそう多くないと思うけど、例えばコード自動生成はすぐ試せる割に効き目が大きく、仕事を効率化する方法としてぜひ試してみたい選択肢だ。

今回は、Haskellの言語内DSLからC言語のコードを生成する方法（の一つ）を簡単に紹介する。 この方法で、Haskell上のEDSLを使って (1) C言語のソースコードを生成でき、 (2) Haskellの式として評価できる。 このように、わざわざパーサを書かなくても、コンビネータを適当に作ればすぐにDSLを作ってしまえるのも、関数型言語の魅力かもしれない。

taglessな方法

ただし、ちょっと他と違う方法を試す。 OlegさんのサイトにTyped Tagless Interpretations という記事があり、そこで紹介されている方法を追いかける。 バリアント型/代数的データ型を使わず(=tagless)に、型付きのDSLのインタプリタを実装しよう、という内容だ。 そもそも、言語を実装するには、抽象構文木を表現するバリアント型を作るのが普通なのだが、この方法ではバリアントのような具体的な中間表現を使わないという点に特徴がある。

このエントリ末尾のコードを見てほしい。 対象言語の抽象構文木が型クラスで表現されており、 GADTやバリアント型を使っていないことに注目。 同様のコードはOCamlでも書ける。 シグネチャで構文を定義し、モジュールで変換方法を、 ファンクタでDSLの項を書くことになる。

特に「型付きの」DSLをGADT抜きで実装できている点が面白い。GADTにより、対象言語の型情報をうまくHaskell （ないしOCaml）の型システムと結びつけて扱うことができ、型安全なインタプリタないしコンパイラを作ることができるが、taglessな方法では中間表現を経由しないためにそもそもGADTが必要ない。

C言語の構文解析ライブラリ language-c-quote

C言語のコード生成にはlanguage-c-quoteというライブラリを使っている (cabal install language-c-quoteでインストールできる)。 以前紹介したLanguage.Cとは別もので、こちらは[cexp| … |] という構文でC言語のコード片を書くことができる QuasiQuotationの機能を備えており、コード生成が多少やりやすくなっている。

議論

中間表現を経由しないのはメリットだと思う。

• 処理速度の向上（？） パターンマッチのオーバーヘッドがない。
  • 中間表現を排した分、空間効率は良いのだろうと思う。
  • しかしHaskellの場合、最適化がないと辞書渡しのオーバーヘッドが別に加わることになる。OCamlも同様。時間効率が具体的にどうなのかよくわからない…
• HOASのexotic termの問題がない。 言語内のbinderの表現に Higher Order Abstract Syntax (HOAS) を使っているが、 型表現がパラメトリックなので、exotic termがそもそも作れないようになっている。

一方デメリットは…あるのかよくわからない。一見、中間表現を排しているので、項の構造を調べるのが困難な気がしないでもないけれど、例えばOlegさんの論文には項の大きさを計る方法が載っていたり、特に難しいことはないような感じもする。

• 部分評価器 (partial evaluator) の例では、インタプリタとコンパイラの結果の両方を保持しているのが非効率といえなくもない、かな…（わからない）

コード

(ワンライナーを駆使しているのは見逃してほしい…)

{-# LANGUAGE QuasiQuotes, UndecidableInstances, GADTs, RankNTypes, TypeSynonymInstances, FlexibleInstances, 
KindSignatures, TypeFamilies, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, 
NoMonomorphismRestriction #-}

-- requires GHC>7 (Haskell platform of the current version will suffice)
-- cabal install language-c-quote hashtables

import Prelude hiding (sum)
import Data.Maybe
import Control.Monad
import Control.Monad.ST
import qualified Data.HashTable.ST.Basic as HT
import Language.C.Syntax
import Language.C.Syntax as C
import Language.C.Quote.GCC {- quasiquote! -}
import Data.Loc
import Data.Symbol

type D = Double

--------------------
-- our purely-functional DSL
--------------------

-- unary and binary operators in our DSL
data Op1 = Neg deriving Show
data Op2 = Plus | Minus | Mult | Divi deriving Show

-- 'tagless' representation of the language
class Lang (e :: * -> *) (array :: * -> *) | e -> array, array -> e where
  -- | e1 `op` e2
  binOp :: Op2 -> e D -> e D -> e D
  -- | op e1
  unOp :: Op1 -> e D -> e D
  -- | iter from to init body -- evaluate the 'body', and accumulate it for (to-from+1) times
  iter :: e Int -> e Int -> e D -> (e Int -> e D -> e D) -> e D
  -- | constant of type Int
  int :: Integer -> e Int
  -- | constant of type double
  double :: D -> e D
  -- | let-binding in the target language
  let_ :: String -> e a -> (e a -> e b) -> e b
  -- | index-based array access (yet not be implemented) 
  at :: e Int -> e (array x) -> e x

{-
Above tagless representation is much similar to the type declaration in GADT, 
which should be like following:
data Lang t where
  BinOp :: Op2 -> Lang D -> Lang D -> Lang D
  UnOp :: Op1 -> Lang D -> Lang D
  Iter :: Lang Int -> Lang Int -> Lang D -> (Lang Int -> Lang D -> Lang D) -> Lang D
  Int :: Integer -> Lang Int
  Double :: D -> Lang D
  Let :: String -> Lang a -> (Lang a -> Lang b) -> Lang b
  At :: Lang Int -> Lang (Array x) -> Lang x
-}

--------------------
-- SYNOPSIS
--------------------

-- add x for ten times
tenTimes x = 
  iter (int 1) (int 10) (double 0.0) (\_ acc-> binOp Plus acc x)
  -- literally, this can be read as 
  -- 'foldl (+) 0.0 $ take 10 $ repeat x' in Haskell,
  -- or 'double accum=0.0; for(int i=0; i<=10; i++) { accum += x; } return accum;' in C

-- 
ex1 = tenTimes (tenTimes (double 1.0))

-- Try this:

-- Evaluate it in Haskell:
---- runHaskell ex1
---- ===> 100.0

-- Generate C Code:
---- genCCode (tenTimes (tenTimes (double 1.0)))
---- ===> (evaluated into the code below)
{-
{
    double accum0 = 0.0;
    
    for (int i0 = 1; i <= 10; i0++) {
        double accum1 = 0.0;
        
        for (int i1 = 1; i <= 10; i1++) {
            ;
            accum1 = accum1 + 1.0;
        }
        ;
        accum0 = accum0 + accum1;
    }
    accum0;
}
-}

--------------------
-- Lesson 1. Evaluate everything in Haskell
--------------------

newtype H x = H x
liftH f (H x) = H (f x)
liftH2 f (H x) (H y) = H (f x y)

toHBinOp :: Op2 -> H D -> H D -> H D
toHBinOp Plus = liftH2 (+)
toHBinOp Minus = liftH2 (-)
toHBinOp Mult = liftH2 (*)
toHBinOp Divi = liftH2 (/)

toHUnOp :: Op1 -> H D -> H D
toHUnOp Neg = liftH pred

instance Lang H [] where
  binOp = toHBinOp
  unOp = toHUnOp
  iter (H from) (H to) (H init) f = 
    if from>to then H (init) 
    else let acc = f (H from) (H init) in iter (H (from+1)) (H to) acc f
  int = H . fromInteger
  double = H
  let_ _ x f = f x
  at = liftH2 (flip (!!))

runHaskell :: H a -> a
runHaskell (H x) = x




--------------------
-- Lesson 2. C code generation
--------------------

-- preparation for embedding typed terms into untyped world
class UntypedLang e where
  binOpU :: Op2 -> e -> e -> e
  unOpU :: Op1 -> e -> e
  iterU :: e -> e -> e -> (e -> e -> e) -> e
  atU :: e -> e -> e
  intU :: Integer -> e
  doubleU :: Double -> e
  letU :: String -> e -> (e -> e) -> e

newtype Untyped t z = U {unU::t}
data Dummy a

instance UntypedLang t => Lang (Untyped t) Dummy where
  binOp op (U e1) (U e2) = U $ binOpU op e1 e2
  unOp op (U e) = U $ unOpU op e
  iter (U e1) (U e2) (U e3) f = U $ iterU e1 e2 e3 (\x y -> unU $ f (U x) (U y))
  at (U e1) (U e2) = U $ atU e1 e2
  int i = U $ intU i
  double d = U $ doubleU d
  let_ s (U e) f = U $ letU s e (\x -> unU $ f (U x))


-- my own Q monad for generating fresh names
newtype Q a = Q (forall s. HT.HashTable s String Int -> ST s a)

instance Monad Q where
  Q f >>= g = Q (\ht -> f ht >>= (\x -> case g x of Q g' -> g' ht))
  return a = Q (\_ -> return a)

runQ :: Q a -> a
runQ (Q m) = runST $ do ht <- HT.new; m ht

newName :: String -> Q String
newName str = Q (\ht -> do
    cnt <- liftM (fromMaybe 0) $ HT.lookup ht str
    HT.insert ht str (cnt+1)
    return $ str ++ show cnt
  )

makeVar :: String -> Exp
makeVar str = Var (Id str noSrcLoc) noSrcLoc



-- mapping operators in our DSL into ones in C
toCBinOp :: Op2 -> BinOp
toCBinOp Plus = C.Add
toCBinOp Minus = C.Sub
toCBinOp Mult = C.Mul
toCBinOp Divi = C.Div

toCUnOp :: Op1 -> UnOp
toCUnOp Neg = C.Negate

-- generate C code!!
instance UntypedLang (Q ([BlockItem],Exp)) where
  -- The pair (stmts, exp) :: ([BlockItem], Exp) is the code that first execute C statements 'stmts' then evaluate 'exp'
  -- Although things are provided as 'UntypedLang', the translation should be type-safe.
  -- since terms are firstly typed using typeful constructor functions of 'Lang', then are embedded into untyped world.
  binOpU op e1 e2 = do (s1,x1) <- e1; (s2,x2) <- e2; return (s1++s2,BinOp (toCBinOp op) x1 x2 noSrcLoc)
  unOpU op e1 = do (s1,x1) <- e1; return (s1,UnOp (toCUnOp op) x1 noSrcLoc)
  iterU from to init body = do
    (sf,f) <- from;
    (st,t) <- to;
    (si,i) <- init;
    cntvar <- newName "i";
    accumvar <- newName "accum";
    let (cntvar_, accumvar_) = (makeVar cntvar, makeVar accumvar)
    (sb,body') <- body (return ([],cntvar_)) (return ([],accumvar_))
    return (sf++st++si++ [
      BlockDecl [cdecl|
        double $id:accumvar = $(i);
      |], BlockStm [cstm|
      for(int $id:cntvar = $(f) ; i <= $(t) ; $(cntvar_)++) {
        $items:sb;
        $accumvar_ = $(body');
      }
      |] ], accumvar_)
  intU i = return ([], [cexp| $int:i |])
  doubleU d = return ([], [cexp| $double:(toRational d) |])
  atU idx_ arr_ = do (sidx,idx) <- idx_; (sarr,arr) <- arr_; return (sidx++sarr, [cexp| $arr[$idx] |])
  letU varname exp_ body_ = do
    var <- newName varname;
    (se,exp) <- exp_;
    let assign = BlockDecl [cdecl| double $id:var = $exp; |]
    (sb,body) <- body_ (return ([],makeVar var));
    return (se++[assign]++sb,body)

genCCode :: Untyped (Q ([BlockItem],Exp)) a -> Stm
genCCode (U expr) = runQ block
  where
    block :: Q Stm
    block = do (items,exp) <- expr; return (Block (items++[BlockStm (Exp (Just exp) noSrcLoc)]) noSrcLoc)