論文メモ：Abstract machines for programming language implementation
Abstract machines for programming language implementationを読んだのでメモ。
どのようなAbstract Machineがどのようなプログラミング言語の実装に使われてきたのか、というサーベイ。2000年に書かれており筆頭著者はHaskell界隈ではそれなりに知られている（多分）Stephen Diehl。Write You a HaskellやGHC Internalsなど、Haskellの言語実装について調べている場合参考になる記事が多い。最近は仮想通貨やNFTに対する批判でも有名。
@sin_clavさんにもおすすめされた：
あっ知ってる論文！ この論文わりとサクッと読めてよいですよ。最高にナイスなサーベイです。
— t-sin (@sin_clav) March 30, 2022
この論文ではAbstract Machineの定義をかなり広くとっており：
Abstract machines are machines because they permit step-by-step execution of programs; they are abstract because they omit the many details of real (hardware) machines.
The extremes of this spectrum are characterized as follows:
• An abstract machine is an intermediate language with a small-step operational semantics.
• An abstract machine is a design for a real machine yet to be built.
と非常に抽象的なものからハードウェアとして実装可能なものまで全てAbstract Machineの範疇だと定義している。
結果かなり広範囲かつ多数のAbstract Machineを扱うことになり、あまり個々のAbstract Machineの内容には立ち入らず、以下の９つの分類の中で代表的なAbstract Machineを列挙しつつ多少コメントする、という形をとっている：
- imperative programming languages
- object-oriented programming languages
- string processing languages
- functional programming languages
- logic programming languages
- hybrid programming languages
- parallel programming languages
- Special-purpose abstract machines
- Concrete abstract machines
有名どころではJVMやPython Bytecode Interpreter、SECDやZinc Abstract Machine、Krivine's MachineやG Machine、Warren's Abstract Machine、Symbolics Lisp MachineやScheme-81 Chipあたりがカバーされている。FelleisenのCEK Machineは言及されていない。
他に面白そうだなと思ったのはPascalのP4 Machine、SASLのSK Machine、並列処理のPCKS Machine、項書き換えのabstract rewriting machine、WAMベースの第五世代コンピュータ計画やBerkeley Abstract Machineのハードウェアなど。
謝辞にK＆RのBrian Kernighan、Tcl作者（＆ A Philosophy of Software Design著者）John OusterhoutそしてPythonのGuido van Rossumがいるのも興味深い。
参考文献を追っていくだけでも相当長い間楽しめそうな論文である。ちなみにSECD、G Machine、WAMについてより詳細を知りたい場合はThe Architecture of Symbolic Computersという本がおすすめ。
Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む（前編）
型推論のためのAlgorithm Wを実装するため、DamasとMilnerのPrincipal Type Schemes for Functional Programsを読んでいる。
重要そうな概念としては
- expression
- type/type-scheme
- substitution
- instance/generic instance
- assumption
- assertion
- closure
- type inference
- Robinson's unification algorithm
- algorithm W
あたり。それらの定義や周辺のポイントを整理するためにメモっていく。長かったので今回はexpressionからclosureまで。
Expression
型付けをする言語の式：
e::= x | e e′ | λx.e | let x = e in e′
ラムダ計算にletが加えられている。Hindley-Milner-Damasだとletを使ってのみ多相を扱えるので、STLCのように「letは関数適用の糖衣構文」というスタンスを取れない。
Vが値だとして
Env = Id → V be the domain of environments η semantic function ε : Exp → Env → V
という関数も重要。Envは変数環境、εは式の評価関数。
以下のように使う：
η[x] : 変数xに対応する値を環境ηからとる ε[e]η : 変数環境ηで式eを評価した結果の値を得る
Type and Type Scheme
Type τとType Scheme σが分けられている。
定義は：
τ ::= α | ι | τ → τ σ ::= τ | ∀α σ
typeは型変数α、何らかのbase type ι（intとかunitとか）、そして二つのtypeをとるbinary type constructor →で作る関数型で再帰的に定義。
type schemeはただのtypeか、何らかのtype schemeの前に何らかの型変数の全称量化∀αがついたもの。
この定義だとtypeには全称量化子がでて来ないので、typeに含まれる型変数は必ずfree variableで、さらに関数型の中のどちら側にも全称量化子はでてくることができない。例えば多相的な型を引数にとるような関数の型は定義できない。
全称量化はtype schemeの先頭にズラーっと並んで、そのあとに必ずtypeがくる、という形になる。
いくつか関連用語：
A type-scheme ∀α_1 . . . ∀α_n τ (which we may write ∀α_1 . . . α_n τ) has generic type variables α_1 . . . α_n .
A monotype μ is a type containing no type variables.
Substitution
S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i]
Substitutionとは型変数をtypeにマップするもの。注意点としては、任意の型ではなく型変数から、type schemeではなくtypeへのマッピングだということ。
Instantiation
If S is a substitution ... and σ is a type-scheme, then Sσ is the type-scheme obtained by replacing each free occurrence of α_i in σ by τ_i , renaming the generic variables of σ if necessary. Then Sσ is called an instance of σ; the notions of substitution and instance extend naturally to larger syntactic constructs containing type-schemes.
Substitution同士を組み合わせることもできる。後述のunificationの部分で：
If S unifies τ and τ′ then U(τ,τ′) returns some (substitution) V and there is another substitution R such that S = RV
と出てくる。この組み合わせ方がよくわからない。RVというのはVに出てくる型変数をRのマッピングで変換したものなのか、それともRとVに含まれるマッピングをすべて合わせた新しいマッピングなのか（その場合、同じ型変数が出てくる場合どうするのか）
さらに後ほどalgorithm Wの説明でS = V S_2 S_1のようにSubstitutionを３つ組み合わせるものも出てくるのだが、これは右結合でいいのだろうか？
Generic instantiation
By contrast a type-scheme σ = ∀α_1 ...α_m τ has a generic instance σ′ = ∀β_1 ...β_n τ′ if τ′ = [τ_i/α_i]τ for some types τ_1,...,τ_m and the β_j are not free in σ. In this case we shall write σ > σ′.
generic instanceというのは「よりgenericになったinstance」ではなく「generic variableをinstantiateしたもの」で、結果としては元のtype schemeよりnon-genericになっている。元のtype schemeの全称量化を一つ以上外して型変数をtypeで入れ替えたもの。全称量化をすべて外す必要はない。
（ちなみに型変数もtypeなのでα_1は∀α_1 α_1のgeneric instanceなんだな・・・）
Assumption
A is a set of assumptions of the form x :σ
Assumptionというのは式における変数（型変数ではなく）とtype schemeのマッピング。
... we shall assume that A contains at most one assumption about each identifier x.
A_x stands for removing any assumption about x from A.
というのも注意点。
AssumptionsはSubstitutionを適用できる。基本的には単体のassumptionではなく、set of assumptionsにsubstitutionを適用して自由型変数をtypeに入れ替えるようだ。
Assertion
Assertionというのは「あるset of assumptions（式変数からtype schemeへのマッピング）Aを前提とすると、式eの型はtype scheme σ」という意味を持つ文で、以下のように表される：
A |= e:σ
（ちなみに「式eの型はtype scheme σ」でいいのだろうか？それとも「式eの型はtype scheme σの何らかのgeneric instance」とした方が正しい？）
「Assertionが成立する」という意味：
(An) assertion is closed ... if A and σ contain no free type variables
(T)he sentence is said to hold iff, for every environment η, whenever η[x] :σ′ for each member x :σ′ of A, it follows that ε[e]η:σ
Closed assertionが成り立つには、Assumptionsと合致するいかなる変数環境においても式を評価した結果の値が正しいtype schemeである必要がある。
(A)n assertion holds iff all its closed instances hold
all its closed instancesと書いていることからも、assertionにもsubstitutionが適用できることがわかる。Assertionを構成するAssumptionsとType Schemeをcloseさせるような（自由変数をすべて束縛するような）いかなるsubstitutionを適用しても、その結果得られるclosed assertionが成り立つ必要がある。すでにclosedなassertionは自身を唯一のclosed instanceとして持つ、という認識でいいのだろうか。
Closure
We also need to define the closure of a type τ with respect to assumptions A;
A(τ)=∀α_1,...,α_n τ
where α_1,...,α_n are the type variables occurring free in τ but not in A.
Type τに出てきてAssumptionsに出てこない自由型変数を全称量化する。type schemeではなくtypeなのは何か理由があるのだろうか。
実例で考えるとAがx:α_1; y:∀α_2 (α_2 -> α_1)でτがα_1 -> α_2 -> α_3だった場合、A(τ)は∀α_2 ∀α_3 (α_1 -> α_2 -> α_3)になる。
次回
今回の用語の整理を踏まえて、次は以下の三点を見ていく：
- type inference
- Robinson's unification algorithm
- algorithm W
これらの詳細を読んでいくことでsubstitutionについての不明点なども解決されることを期待・・・
1byte = 8bitsにしたのは「人月の神話」のフレッド・ブルックス？
少し前にTwitterで「面接で『なんで1byteって8bitsになっているのか？』と聞くといい」というツイートが話題になっていた。
それを見た時は「まあ8bitsだとは限らないよね、現在主流のアーキテクチャがそうなってるだけで」と思っただけで終わったのだが。
最近Edsger W. Dijkstra: a Commemorationという文章を読んでいて、IBM System/360について触れられていた。（ダイクストラは「360が発表されたのは私の職業人生で最悪の日だった」「360によって計算科学の進歩は10年遅れた」と言っていたらしい）
その関係で少し調べていたら、どうやら1964年に発表されたSystem/360が1byte = 8bitsを主流にした決定的なプロダクトラインであったことがわかった。そしてSystem/360の開発マネージャをしていたのは、「人月の神話」という著作で有名なフレッド・ブルックスだった。
開発マネージャだから「1byte = 8bitsにした」というのは言い過ぎ、と考える向きもあるかと思う。しかし、この決定に関してフレッド・ブルックスはかなり積極的に関与していたようだ。
2015年のCommunications of the ACMでフレッド・ブルックスのインタビューがあった：
その「Designing the System/360」の部分で
There was one very big difference. Gene's machine was based on the existing 6-bit byte and multiples of that: 24-bit instructions and a 48-bit instruction or floating point. Jerry's machine was based on an 8-bit byte and 32-bit instructions, so 64-bit and 32-bit floating point. This is not a real happy choice. There are strong arguments each way, but you want your architecture to be consistent. You are not going to have an 8-bit byte and 48-bit instruction floating point word.
It was our biggest internal fight. Gene and I each quit the company once that week, but Mannie Piore, the senior scientist in the company and a person of great wisdom, got us back together. I had made the decision for the 8-bit byte. Gene appealed to Bob; but Bob affirmed it.
とある。Geneというのはジーン・アムダールのことで、彼がSystem/360のチーフ・アーキテクトだった。（ちなみに並列実行によるプログラム高速化において並列化できない部分がボトルネックとなって高速化を制限する、という「アムダールの法則」の提唱者）
System/360というIBMの今後の統一的なアーキテクチャを決定するためのプロジェクトで、「IBMの過去のアーキテクチャで採用されていた6bitか新しい8bitか」という点でチーフ・アーキテクトとプロジェクトのマネージャがお互い進退をかけてぶつかって、その結果ブルックスの主張が勝った。（ちなみにBobというのはSystem/360プロジェクトを始めることを決定したData Systems部門長のBob Evans）
その後System/360のプロダクトラインは売れに売れて、すでにコンピュータ界の巨人だったIBMの覇権の持続に大きく寄与した。（七人の小人と言われた競争相手に対して、シェア７割を維持し続けたらしい）
現代のコンピュータアーキテクチャに多大な（ダイクストラによれば進歩を10年遅らせるほどの・・・）影響を与えたSystem/360。そのプロジェクトでの「1byte = 8bits」という選択が60年近く経った今も主流のままでいる、というのが真相のようだ。まさにその点で争って勝った、という意味でフレッド・ブルックスの「功績」であると言えるのではないか。（ただし8bitが主流になった後の本人によるインタビューがソースなので、その分信憑性は差し引く必要があるが・・・）
A正規化されたIRをCPSに変換する
A正規化について非常に参考にさせてもらっているMatt Mightのブログ記事で
A later transformation to continuation-passing style (like that in Appel's book) is also simplified if transforming from A-Normal Form.
とあるので、これまでのA正規化されたIRに関してCPS変換がどのようになるのかを試してみた。
ちなみに（A正規形からではない）CPS変換についてもMatt Mightの記事を非常に参考にしている：
CPS形
<vexp> ::= <int> | <bool> | <var> | (Fn <var>* <cexp>) <aexp> ::= <vexp> | (Add <vexp> <vexp>) | (Lt <vexp> <vexp>) <cexp> ::= <aexp> | (Call <aexp> <aexp>*) | (If <aexp> <cexp> <cexp>)
Fnの中の式が
一つ重要なポイントとしてはLet式がなくなっていること。CPS変換の過程でLetは継続関数の呼び出しに変換されるのでCallとFnだけでLetが表現される。
また、継続自体も独自の式を持つのではなく、単に関数として表される。（このやり方に関してはいろいろ議論のあるところだが、今回は一番簡単なアプローチでやってみた）
let rec is_value = function | Int _ | Bool _ | Var _ -> true | Fn(_,e) -> is_cps e | _ -> false and is_atomic = function | Add(e1,e2) | Lt(e1,e2) -> is_value e1 && is_value e2 | e -> is_value e and is_cps = function | Call(f,es) -> List.fold_left (fun a b -> a && is_atomic b) (is_atomic f) es | If(e1,e2,e3) -> is_atomic e1 && is_cps e2 && is_cps e3 | e -> is_atomic e
実はこの記事を書くにあたって（コードを書いた後で）BNFで文法をちゃんと定義してみたら、OCamlのコードがバグっていることを発見した。さらにBNFに従って書くことでアドホック性が減ってかなりスッキリした。というわけで文法を定義するのは大事だと再認識。
CPS変換
それではCPS変換を行うコードを見ていく。
まずは新しい変数を作成するヘルパ関数：
let n = ref (-1) let gensym s = incr n; "k" ^ s ^ string_of_int !n
今回は「継続そのもの」と「継続に渡す値」の二つの異なる概念を表す変数を作成する必要があり、変換後のコードの理解しやすさのためにそれらを変数名で区別できるようにしたい。そのためgensymに文字列引数を渡せるようにした。
それでは変換の根本である二つの相互再帰的な関数を見ていく。
まずはアトミックな値を変換するためのtransform_m：
let rec transform_m = function | Fn(ss,e) -> let k = gensym "" in Fn(ss@[k],(transform_t e (Var k))) | e -> e
アトミックな式に関しては、関数式だけ「中身の式」にさらにCPS変換を加える必要があり、それ以外は変化なし。すでにA正規化されているためAddやLtの中の式を変換する必要はない（実はこれらの中にFn式が入っている場合は本当は変換が必要だが、それはそもそも型エラーなので今回の実装では無視）
そして一般的な式とその継続を受け取り、CPS形の式を返すtransform_t関数。ケースごとに見ていく：
and transform_t e k = match e with
まずアトミックな式：
| Fn _ | Var _ | Int _ | Bool _ | Add _ | Lt _ -> Call(k,[transform_m e])
これらはtransform_mした上で継続kの実引数として関数適用している。
関数適用：
| Call(f,es) -> let f = transform_m f in let es = List.map transform_m es in Call(f,es@[k])
関数・引数すベてにtransform_mし、引数の最後に継続を追加した形の関数適用式に修正している。A正規化されているおかげで関数・引数がすでにアトミックな式であることが保証されているので変換が楽になっている。
Let式：
| Let(s,e1,e2) -> transform_t e1 (Fn([s], transform_t e2 k))
Letはすでにかなり継続っぽい。本体の式を継続とみなして、変数束縛する対象の式を再帰的にtransform_tする。
最後にIf式：
| If(e1,e2,e3) -> If(e1, transform_t e2 k, transform_t e3 k)
すでにA正規化されているので条件式e1の部分は変更の必要がない。分岐先の二つの式をどちらも継続kとともにtransform_tしておく。
最後にプログラム全体の式をtransform_tと終端継続で変換するf関数：
let f e = transform_t e (let kv = gensym "v" in Fn([kv],Var(kv)))
やってみると実際A正規化してあることの恩恵は大きいように感じる。現在すべてが同じAst.t型の中での変換なので、変換の正しさの型システムによる保証がまったくないのが怖い点だが・・・
使ってみる
こんな感じのmain.mlモジュールを定義して使ってみる：
let f s = Lexing.from_string s |> Parser.f Lexer.f |> Alpha.f |> Anormal.f let () = let e = read_line () |> f in e |> Ast.to_string |> print_endline; e |> Anftocps.f |> Ast.to_string |> print_endline; e |> Anftocps.f |> Anftocps.is_cps |> string_of_bool |> print_endline;
まずはA正規形を出力、その後CPS形を出力し、ちゃんとCPS形の定義に沿っているかをチェックしている。
試しに以下の式を入力：
((if (< (+ 1 2) 3) (fn [x] (+ x 1)) (fn [x] (+ x 2))) (+ 1 2))
A正規形：
(let [g0 (+ 1 2)] (let [g1 (< g0 3)] (let [g2 (if g1 (fn [x.1] (+ x.1 1)) (fn [x.0] (+ x.0 2)))] (let [g3 (+ 1 2)] (g2 g3)))))
CPS形：
((fn [g0] ((fn [g1] (if g1 ((fn [g2] ((fn [g3] (g2 g3 (fn [kv0] kv0))) (+ 1 2))) (fn [x.1 k2] (k2 (+ x.1 1)))) ((fn [g2] ((fn [g3] (g2 g3 (fn [kv0] kv0))) (+ 1 2))) (fn [x.0 k1] (k1 (+ x.0 2)))))) (< g0 3))) (+ 1 2))
とりあえずうまくいっているようだ。目で追うのは大変だが・・・
今回のコード
C++のiostreamの<<を導入したのはストラウストラップ
最近@karino2さんのポッドキャスト「プログラム雑談」のバックナンバーをいろいろ聴いている：
二週間ほど前に書いた聴いてるポッドキャストの記事ではまだ「気になっている」という分類だったのだけど、聴き始めたらいい感じにゆるいのと技術的な内容が面白いのと（そして本人の技術や生活に関する哲学が見えるのも）で、続けて聴いている。
2020年あたりの「ストラウストラップ本のエピソード」で：
「iostreamの<<構文を導入した人は何十年かに渡って『やっちまった』と思っているはず」という話があった。
ここら辺の：
のoperator<<メソッドをオーバーロードしてIO出力に使う構文の話だ。確かにあの構文はC++の見た目のユニークさの最たるもので、それはつまり後続言語にまったく模倣されなかったということだ。自作言語勢でも「IOはあの構文で行こう」と考えている人は見たことがない。
ただ、「途中結果として不必要な文字列を作成することなく複数の文字列をバッファに書き込む」ということをうまく表そうと考えると、それなりに理に適った構文なような気もする。<<をオーバーロードしている、というのはかなり怪しげではあるが・・・
で「導入した人」って誰なの？と自分も気になったので調べたところ、記事のタイトルにもあるとおりストラウストラップ本人だった。まあ意外性のない無難な結果である。
ストラウストラップのウェブサイトに載ってる、彼が2001年に中国のC++ View誌でインタビューされた記事をみると：
C++ View: Jerry Schwarz reviewed the history of IOStream in the preface of the book Standard C++ IOStream and Locales. I guess that there must be many interesting stories in the process of transiting from classic stream into the standard IOStream. Can you tell us some?
Bjarne Stroustrup: I do not want to try to add to Jerry's description of the transition from my streams to the current iostreams. Instead, I'd like to emphasize that the original streams library was a very simple and very efficient library. I designed and built it in a couple of months.
The key decisions was to separate formatting from buffering, and to use the type-safe expression syntax (relying on operators << and >>). I made these decisions after discussions with my colleague Doug McIlroy at AT&T Bell Labs. I chose << and >> after experiments showed alternatives, such as < and >, comma, and = not to work well. The type safety allowed compile-time resolution of some things that C-style libraries resolve at run-time, thus giving excellent performance.
iostreams自体はStroustrupが実装したわけではないけど<<を使うスタイルは彼が作ったstreamsから継承されたもの、とのこと。StroustrupのA History of C++によるとstreamsは1984年に実装されたようだ。
他のオペレータのオーバーロードも試したけど<<が一番うまくいった、ということのようだが、そもそも標準出力でオペレータを使う必要はあったのだろうか？普通のメソッドではダメなのか？というのは気になるところだ。少なくともストラウストラップは2001年の時点では（公式には）このデザインに不満を持っていたわけではなかったようだ。前述のA History of C++によると：
The idea of providing an output operator rather than a named output function was suggested by Doug McIlroy. This requires operators that return their left−hand operand for use by further operations.
というわけでオペレータを使ったら？というアイデアはこのDoug McIlroyの提案らしい。彼が「やっちまった」と思い続けているかは定かでない。
CEK抽象機械をCESK抽象機械に拡張する
前回のCEK抽象機械を拡張して、ミュータブルな状態のある言語も自然に実行できるようにする。
CESK抽象機械
CEK抽象機械はControl（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つの要素を持つ。
CESK抽象機械はそこにStore（格納）を追加する。Storeは可変なメモリ領域を表す。
前回に続いて詳細についてはMatt Mightのブログ：
あるいはFelleisen他の著作：
を参照してほしい。
ちなみに今回のCESK拡張部分の実装に関してはMatt Mightのブログに厳密に準拠していない。コードやデザインに微妙なところがある責は私個人のものであることは断っておきたい。
型の変更
CEKをCESKに拡張するにあたってまず各種の型がどう定義されるかを見ていく。
値と環境：
type env = (string * int) list type val_ = | Int of int | Bool of bool | Closure of Ast.t * env
val_型には変更はないのだが、envが直接値を持つのではなく、変数の文字列とstoreのアドレスを指す整数のペアを持つようになる。ということでval_型と相互再帰する必要がなくなっている。
次にstore：
module Store = struct type t = {x:val_ array; mutable i:int} let n = 10000 let init () = {x=Array.make n (Int 0); i=0} let get s = Array.get s.x let set s i v = Array.set s.x i v let add s v = Array.set s.x s.i v; s.i <- (s.i + 1); s.i-1 end
storeは「メモリ領域全体」を表すval_ arrayと「未使用のメモリ領域の先頭」を表す整数を持つレコードで表現される。
また、関連する関数がいくつかあるのでモジュール化。コンストラクタinit、特定アドレスの値を取得するget、特定アドレスに値を書き込むset、未使用のメモリ領域先頭に値を書き込むaddが定義されている。
getとsetはunitを、addは書き込み先のアドレスを返している。
最後に抽象機械の状態を表すcesk型：
type cesk = | Running of Ast.t * env * Store.t * kont | Done of val_
cek型のRunning of Ast.t * env * kontにStore.tが追加されている。
アトミックな式の評価
アトミックな式を評価する際、CEKでは直接評価結果の値を返していた。CESKではまずstoreに書き込んでから、そのアドレスを返すかそのアドレスに入っている値を返すか使い分ける必要がある。
なのでeval_atomicとeval_store_atomicを分ける（前者は後者を呼び出している）：
let eval_store_atomic e env s = match e with | A.Int n -> Store.add s (Int n) | A.Bool b -> Store.add s (Bool b) | A.Fn _ -> Store.add s (Closure(e,env)) | A.Var v -> List.assoc v env | _ -> failwith "Evaluating non-atomic expression as atomic" let eval_atomic e env s = Store.get s (eval_store_atomic e env s)
eval_store_atomicでは変数以外のアトミックな式は値をstoreに書き込んでからそのアドレスを返している。変数に関しては単に変数環境で対応するアドレスを探して返すだけ。この関数名は微妙だがあまりうまい名前が思いつかない・・・
eval_atomicではeval_store_atomicから返ってくるアドレスに入っている値をStore.getで取得して返す。
継続の実行
control部分の評価が終わって値を次の継続に渡すためのapply_kont関数：
let apply_kont k s i = match k with | Halt -> Done (Store.get s i) | Letkont(var,e,c,k) -> Running(c,(var,i)::e,s,k)
以前は値を直接次の継続に渡していたのだが、それを値が入っているstoreのアドレスを渡すように変更。
終端継続の場合はStore.get s iでそのアドレスから直接値を取り出す。（この記事を書いていて気づいたが、この部分に関してはDoneをDone of Store.t * iにして「最終状態の記憶領域と結果の値が入っているアドレス」にするべきだった。現在のデザインだと他のアドレスを参照しているような複雑な値を正しく返せない。）
Letkontの場合は変数環境に変数とアドレスのペアを追加した上で継続に格納されていた式を新しいcontrolとして実行。
状態遷移
状態遷移を表すstep関数については、前回の記事と同じように各パターンを個別に見ていく。
まずはcontrolにアトミックな式が来ている場合：
let step c e s k = match c with | A.Int _ | A.Bool _ | A.Fn _ | A.Var _ -> apply_kont k s (eval_store_atomic c e s)
apply_kontに渡すのが値そのものではなく、store上のアドレスになっているのでeval_store_atomicしている。
和や比較：
| A.Add(e1,e2) -> (match eval_atomic e1 e s, eval_atomic e2 e s with | Int n, Int m -> apply_kont k s (Store.add s @@ Int(n+m)) | _ -> failwith "Adding non-integer values") | A.Lt(e1,e2) -> (match eval_atomic e1 e s, eval_atomic e2 e s with | Int n, Int m -> apply_kont k s (Store.add s @@ Bool(n<m)) | _ -> failwith "Comparing non-integer values")
これらは保持しているアトミック（なはず）なサブ式を評価し、整数値であることを確認してから新しい値（整数値か真偽値）を継続に渡す、という処理の流れになっている。まずサブ式をeval_atomicで評価（内部でeval_store_atomicとStore.getを使っているので「store上のアドレスに格納されている値」を返すことがことが保証されている）、その値のタプルに対してパターンマッチして結果をStore.addでstoreに書き込み、そのアドレスをapply_kontに渡している。
条件分岐とlet式：
| A.If(cond,e1,e2) -> (match eval_atomic cond e s with | Bool b -> Running((if b then e1 else e2), e, s, k) | _ -> failwith "Conditional on non-boolean") | A.Let(var,e1,e2) -> Running(e1,e,s,Letkont(var,e,e2,k))
ほぼ変更なし。各種関数やコンストラクタの引数にstoreが増えたくらい。
関数適用：
| A.Call(f,es) -> (match eval_atomic f e s with | Closure(A.Fn(ss,body),e') -> let vs = List.map (fun v -> eval_store_atomic v e s) es in Running(body, (List.combine ss vs)@e', s, k) | _ -> failwith "Non-function in operator position")
変数環境が(変数の文字列, 値)ではなく(変数の文字列, アドレス)になっているので、仮引数と実引数のタプルも同じく実引数はアドレスで表現する必要がある。なのでeval_atomicではなくeval_store_atomicをList.mapに渡している。
しかし、よく見たらlet vs = List.map (fun v -> eval_store_atomic v e s) esってOCamlコードの変数名がめちゃくちゃだな・・・ 1文字変数はやめよう・・・
使ってみる
前回と同じ例：
(+ 1 2) (+ 1 2) 3
(if (< 1 2) (+ 1 (+ 3 4)) 5) (let [g0 (< 1 2)] (if g0 (let [g1 (+ 3 4)] (+ 1 g1)) 5)) 8
前回と同じく、とりあえずこれらの入力ではうまくいっているようだ。
今後
今回は抽象機械は拡張したけど言語機能は変更しなかったのでありがたみが感じにくい。これからstoreが加わったことを利用しrefなどの機能を追加していく。
今回のコード
A正規化されたIRをCEK抽象機械で実行
前回で定義した言語とそのA正規化されたIRをインタプリタで実行したい。
というわけでまたしてもMatt Mightのブログを参考にする：
こちらのブログはCESKマシンの話だが、今のところ破壊的変更を言語機能として実装してないので、まずはCESKのステートSを抜いてCEK抽象機械での実行を目指す。
CEK抽象機械
CEK抽象機械というのは大雑把にいうとSECD抽象機械の仲間で、抽象機械の状態とその変遷関数を厳密に定義することで「プログラムの実行」をモデル化するもの。CEKという名前はこの抽象機械の状態を構成する三つの要素の頭文字（？）からきている。Control（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つである。
(control, environment, kontinuation)という状態を変遷関数stepに渡すとcontrolの形を元に条件分岐する。
controlが簡単な式であるなら直ちに評価する。結果が値ならkontinuationの先頭の継続をとってきて新しいcontrolに変換し、environmentに評価した値を追加した上で新しい状態(control', environment', kontinuation')を返す。結果が関数適用による新しい式と環境ならそのままそれを現在の継続と合わせて新しい状態(control', environment', kontinuation)として返す。結果が条件分岐による新しい式なら新しい状態(control', environment, kontinuation)として返す。などなど。
controlが複雑な式なら分解して、次に「実行するべき」式を新しいcontrolに、それ以外はkontinuationに追加する形で退避させておくことで新しい状態(control', environment', kontinuation')を返す。
余談だが以前作ったS式言語のインタプリタも、作った後にCEK機械の再実装であることがわかった：
ある意味自然に導出されるようなインタプリタ形態なのかもしれない。
CEK抽象機械の詳細に関しては上記のMatt MightのブログやFelleisen他のSemantics Engineering with PLT Redexに詳しく載っている：
特に後者ではラムダ計算を愚直に実行するインタプリタから効率・機能を求めてCEK、CESK抽象機械に段階的に発展していく経緯やSECD抽象機械との比較なども載っていて面白い。
CEKマシンの実装
cek.mlモジュールでCEK抽象機械を実装する。
まずは式を評価した結果となる値と、その値に変数を束縛する変数環境の二つを型として定義：
type val_ = | Int of int | Bool of bool | Closure of Ast.t * env and env = (string * val_) list
クロージャも値の一つで、クロージャは変数環境も持つ。なので値と変数環境は相互再帰的な型になる。
次は継続の型：
type kont = | Letkont of string * env * Ast.t * kont | Halt
A正規化したIRに特化したCEK抽象機械の特徴として、継続が非常に簡単になっている。「そのまま評価できない複雑な式」というのが必ずlet v = simple_exp in ...という形になっている、というA正規化形の性質を利用してLetkontという継続と、終端継続であるHaltのみを定義。
CEK抽象機械の状態は「実行中」の(control, environment, kontinuation)のタプルか、「評価結果」の値：
type cek = | Running of Ast.t * env * kont | Done of val_
値を直接返す「アトミックな式」の評価関数：
let eval_atomic e env = match e with | Ast.Int n -> Int n | Ast.Bool b -> Bool b | Ast.Fn _ -> Closure(e,env) | Ast.Var v -> List.assoc v env | _ -> failwith "Evaluating non-atomic expression as atomic"
値を継続に渡すためのヘルパ関数：
let apply_kont k v = match k with | Halt -> Done v | Letkont(s,e,c,k) -> Running(c,(s,v)::e,k)
継続と値を受け取り、新たなCEK状態を返す。継続がHaltの場合は抽象機械が停止し、評価結果を返す。Letkontの場合には継続の仮引数s、継続の変数環境e、継続の式cそして残りの継続kが保持されている。受け取った値vをsと合わせて変数環境eを拡張し、その変数環境で式cを評価した結果の値を継続kに渡す、という新しいCEK状態を返す。
stepが抽象機械の動的な振る舞いの根本である変遷関数。
ASTノードに対してパターンマッチしているので各項目を個別に見ていく。
まずはアトミックな式から：
let step c e k = match c with | Ast.Int _ | Ast.Bool _ | Ast.Fn _ | Ast.Var _ -> apply_kont k (eval_atomic c e)
整数、真偽、関数、変数は直接eval_atomicで値に変換してからapply_kontで継続に渡している。
整数の和・比較：
| Ast.Add(e1,e2) -> (match eval_atomic e1 e, eval_atomic e2 e with | Int n, Int m -> apply_kont k (Int(n+m)) | _ -> failwith "Adding non-integer values") | Ast.Lt(e1,e2) -> (match eval_atomic e1 e, eval_atomic e2 e with | Int n, Int m -> apply_kont k (Bool(n<m)) | _ -> failwith "Comparing non-integer values")
+と<に関してはまず引数部分をアトミックな式として評価（もしアトミックでなければここでエラーになる）、引数が整数値であることを確認して（整数でなければまたしてもエラー）、和や比較結果を値として継続に渡している。
条件分岐：
| Ast.If(cond,e1,e2) -> (match eval_atomic cond e with | Bool b -> Running((if b then e1 else e2), e, k) | _ -> failwith "Conditional on non-boolean")
条件分岐に関しては（厳密なA正規化かどうかは置いておいて）条件部分のみアトミックな式になっているはずなのでeval_atomicして結果がBoolであることを確かめ、その値によって次のcontrol式を選択して新しいCEK状態を返す。
let式：
| Ast.Let(s,e1,e2) -> Running(e1,e,Letkont(s,e,e2,k))
すでに述べたとおり、A正規化したIRだと継続を拡張する唯一のケースがlet式の評価。実際には何も評価せず、新しい継続を作った上で新しいCEK状態を返している。
関数適用：
| Ast.Call(f,es) -> (match eval_atomic f e with | Closure(Ast.Fn(ss,body),e') -> let vs = List.map (fun v -> eval_atomic v e) es in Running(body,(List.combine ss vs)@e', k) | _ -> failwith "Non-function in operator position")
関数部分、実引数部分すべてがアトミックな式であるはず。なのですべてに対してeval_atomicして、関数がクロージャ値であることを確認した上で(関数本体の式、仮引数・実引数で拡張されたクロージャの変数環境、元の継続)という新しいCEK状態を返す。
注意すべき点としてはすべてのeval_atomicが終わった時点で現在の変数環境は破棄されること。関数の本体部分の式はクロージャの変数環境で実行されるし、それ以降の評価ための環境は継続に保存されている。
これでstep関数は終わり。基本的に実行時エラーが多い。本来A正規化されたIRであれば通らないはずの条件分岐の部分なわけだが、IRの型がソース言語のASTと同一なのでこういった実行時チェックが必要になる。GADTなどで型としてA正規化を表現できればここら辺はスッキリしそう。
式を受け取り値を返すeval関数：
let eval c = let rec f = function | Running(c,e,k) -> f(step c e k) | Done v -> v in f (Running(c,[],Halt))
(実引数の式、空の環境、空の継続)というCEK状態を作成してstepを繰り返し適用し、状態が「停止」した時点で評価結果として値を返している。
val_型を文字列化するヘルパ関数も定義しておく：
let string_of_val = function | Int n -> string_of_int n | Bool b -> string_of_bool b | Closure _ -> "closure"
使ってみる
main.mlを以下のように変更して使う：
let f s = Lexing.from_string s |> Parser.f Lexer.f |> Alpha.f |> Anormal.f let () = let e = read_line() |> f in e |> L.Ast.to_string |> print_endline; e |> L.Cek.eval |> L.Cek.string_of_val |> print_endline;
これで受け取った式をまずA正規化してその式を出力、その後CEK抽象機械上でA正規化された式を実行してその結果を出力する。
試してみる：
(+ 1 2) (+ 1 2) 3
(if (< 1 2) (+ 1 (+ 3 4)) 5) (let [g0 (< 1 2)] (if g0 (let [g1 (+ 3 4)] (+ 1 g1)) 5)) 8
とりあえずこれらの入力ではうまくいっているようだ。
今回のコード
（cek.mlとmain.ml以外は前回の記事のものを完全に流用）
