HaxeのGADT (一般化代数的データ型) を使って言語処理系を実装する

HaxeにはGADT(generalized algebraic data type; 一般化代数的データ型)という機能がある。この機能を使って、型付きのインタープリターとコンパイラーをつくろう。参考文献[CPDT]の2.2 Typed Expressionsでやっていることを部分的にやる。

# 概要

```
ソース言語 →[denote]→ 式の値
↓
[compile]
↓
ターゲット言語 →[denote]→ スタックを受け取ってスタックを返す関数
```

# 二項演算

二項演算をGADTを使って定義する。`enum BinOp<U,V,W>`は二項演算 U × V → W を表す型。`Plus`は+, `Times`は×, `And`は∧, `Or`は∨, `Eq`は=, `Lt`は<を表す。

```hx
package mylang;

enum BinOp<U,V,W> {
	Plus : BinOp<Int,Int,Int>;
	Times : BinOp<Int,Int,Int>;
	And : BinOp<Bool,Bool,Bool>;
	Or : BinOp<Bool,Bool,Bool>;
	Eq<X> : BinOp<X,X,Bool>;
	Lt : BinOp<Int,Int,Bool>;
}
```

ここから、`Plus`の型は`BinOp<Int,Int,Int>`だとか、`Eq<X>`の型は`BinOp<X,X,Bool>`だということが読み取れる。

# 二項演算の意味

二項演算子の意味を定義する。考えとしては `BinOps.denote<U,V,W> : BinOp<U,V,W> -> U -> V -> W` は `BinOp<U,V,W>` を受け取って、その意味 `U -> V -> W` を返す。クロージャーを作って返してもいいけど、特にその必要もないのでuncurry化してある。

```hx
package mylang;

class BinOps {
	public static function denote<U,V,W>(f : BinOp<U,V,W>, x : U, y : V): W {
		return switch(f) {
			case Plus: x + y;
			case Times: x * y;
			case And: x && y;
			case Or: x || y;
			case Eq: x == y;
			case Lt: x < y;
		}
	}
}
```

# ソース言語

ソース言語は式の抽象構文木として与える。`enum Exp<T>`はT型の値を持つ式を表す型。`ConstB`はブーリアンの定数式、`ConstI`は整数の定数式、`BinOp`は二項演算式を表す。

```hx
package mylang;

enum Exp<T> {
	ConstB(b : Bool) : Exp<Bool>;
	ConstI(i : Int) : Exp<Int>;
	BinOp<U,V,W>(f : BinOp<U,V,W>, e1 : Exp<U>, e2 : Exp<V>) : Exp<W>;
}
```

# ソース言語の意味

二項演算と同様、ソース言語にも意味を定義する。

```hx
package mylang;

class Exps {
	public static function denote<T>(exp : Exp<T>) : T {
		return switch(exp) {
			case ConstB(b): b;
			case ConstI(i): i;
			case BinOp(f, e1, e2): BinOps.denote(f, denote(e1), denote(e2));
		}
	}
}
```

# 式の評価

```hx
import mylang.BinOp;
import mylang.Exp;

using mylang.Exps;

class Ex0 {
	public static function main() {
		var x = BinOp(Plus, ConstI(10), ConstI(20));
		trace(x.denote());
		var y = BinOp(Eq, x, ConstI(30));
		trace(y.denote());
		/*var z = BinOp(Eq, x, ConstB(true));*/
	}
}
```

実行結果:

```
Ex0.hx:9: 30
Ex0.hx:11: true
```

コメントアウトしてある行は、コメントアウトを外すとコンパイルが通らない。

```
./Ex0.hx:12: characters 23-35 : mylang.Exp<Bool> should be mylang.Exp<Int>
./Ex0.hx:12: characters 23-35 : Type parameters are invariant
./Ex0.hx:12: characters 23-35 : Bool should be Int
./Ex0.hx:12: characters 23-35 : For function argument 'e2'
```

このように、型が正しくないプログラムはコンパイル時に型検査に引っかかる。

# スタック

次にターゲット言語の実装をする。ターゲット言語はスタックマシンへの命令列だ。今回は型付きの言語処理系を実装するので、スタックもまた型付きだ。

まず、これらは型のリストを作るための型 `enum Nil` と `enum Cons<U,V>` を定義する。

```hx
package mylang;

enum TNil {}
```

```hx
package mylang;

enum TCons<U,V> {}
```

そして、 `enum Stack<T>` を次のように定義する。

```hx
package mylang;

enum Stack<T> {
	Nil : Stack<TNil>;
	Cons<U,V>(x : U, xs : Stack<V>) : Stack<TCons<U,V>>;
}
```

これはどういうことをやっているのだろうか? 順番に見ていこう。

まず `Nil : Stack<TNil>` というのは、`Nil`という`Stack<TNil>`型のスタックがあるということだ。そして、`Cons<U,V>(x : U, xs : Stack<V>) : Stack<TCons<U,V>>` というのは、 `x : U` と `xs : Stack<V>` から新しいスタック `Cons<U,V>(x, xs) : Stack<TCons<U,V>>` が作れるということだ。

たとえば、 `Cons(2, Cons(1, Cons(true, Nil)))` というスタックは `Stack<TCons<Int, TCons<Int, TCons<Bool, TNil>>>>` という型を持つ。スタックのひとつひとつの要素の型の情報が、スタックの型に含まれていることになる。

# 命令

次に、スタックマシンの命令を定義する。

```hx
package mylang;

enum Instr<X,Y> {
	IConstB<S>(b : Bool) : Instr<S,TCons<Bool,S>>;
	IConstI<S>(i : Int) : Instr<S,TCons<Int,S>>;
	IBinOp<U,V,W,S>(f : BinOp<U,V,W>) : Instr<TCons<U,TCons<V,S>>,TCons<W,S>>;
}
```

`enum Instr<X,Y>`は状態が`Stack<X>`型のスタックであるスタックマシンに対しての命令で、命令を実行した後の状態が`Stack<Y>`型のスタックになる命令である。`IConstB<S>`はスタックへブーリアンの定数をプッシュする命令、`IConstI<S>`はスタックへ整数の定数をプッシュする命令、`IBinOp<U,V,W,S>`はスタックからU型, V型のデータをポップしてきて、二項演算の結果のW型の値をプッシュする命令である。

# 命令の意味

命令の意味を定義する。

```hx
package mylang;

class Instrs {
	public static function denote<X,Y>(instr : Instr<X,Y>, s : Stack<X>) : Stack<Y> {
		return switch(instr) {
			case IConstB(b): Cons(b, s);
			case IConstI(i): Cons(i, s);
			case IBinOp(f): switch(s) {
				case Cons(x, Cons(y, s0)): Cons(BinOps.denote(f, x, y), s0);
			}
		}
	}
}
```

`case IBinOp(f):`の処理で、スタックに対してのパターンマッチを行っていることに注目してほしい。`enum Instr<X,Y>`の定義から `IBinOp<U,V,W,S>(f : BinOp<U,V,W>) : Instr<TCons<U,TCons<V,S>>,TCons<W,S>>` だから、`denote<X,Y>`の`X`は`TCons<U,TCons<V,S>>`だということになる。すると、`s : Stack<TCons<U,TCons<V,S>>>`だから、`s`には必ず2つ以上のデータが積まれているとわかる。そういうわけで、このパターンマッチでは他のケースは不要なのだ。

# ターゲット言語

ターゲット言語であるスタックマシンのプログラムは命令列だ。

```hx
package mylang;

enum Program<X,Y> {
	End<A> : Program<A,A>;
	Instr<A,B,C>(instr : Instr<A,B>, cont : Program<B,C>) : Program<A,C>;
}
```

`End<A>`は空のプログラムで、初期状態が`Stack<A>`型のスタックであるスタックマシンに対してのプログラムで、終了状態も`Stack<A>`の何もしないプログラムだ。`Instr<A,B,C>`は命令`instr : Instr<A,B>`と継続`cont : Program<B,C>`から新しいプログラム`Instr<A,B,C>(instr, cont) : Program<A,C>`を作る。

# ターゲット言語の意味

いままでのように、ターゲット言語の意味も定義する。

```hx
package mylang;

class Programs {
	public static function denote<X,Y>(p : Program<X,Y>, s : Stack<X>) : Stack<Y> {
		return switch(p) {
			case End: s;
			case Instr(instr, cont): denote(cont, Instrs.denote(instr, s));
		}
	}
}
```

# スタックマシンプログラムの実行

スタックマシンの実行結果を取り出すのに便利なメソッドを定義しておこう。`Stacks.value<T>`は、`T`型の値が1つだけ積まれているスタックから値を取り出す。

```hx
package mylang;

class Stacks {
	public static function value<T>(s : Stack<TCons<T, TNil>>) : T {
		return switch(s) {
			case Cons(v, _): v;
		}
	}
}
```

これで、次のプログラムが実行できるようになった。

```hx
import mylang.BinOp;
import mylang.Instr;
import mylang.Program;
import mylang.Stack;

using mylang.Programs;
using mylang.Stacks;

class Ex1 {
	public static function main() {
		var x =
			Instr(IConstI(20),
			Instr(IConstI(10),
			Instr(IBinOp(Plus),
			End)));
		trace(x.denote(Nil).value());
		var y =
			Instr(IConstI(30),
			Instr(IConstI(20),
			Instr(IConstI(10),
			Instr(IBinOp(Plus),
			Instr(IBinOp(Eq),
			End)))));
		trace(y.denote(Nil).value());
	}
}
```

実行結果:

```
Ex1.hx:16: 30
Ex1.hx:24: true
```

# コンパイラー

ここまでで、ソース言語のインタープリター、ターゲット言語のインタープリターを実装した。最後に、ソース言語からターゲット言語へ変換するコンパイラーを実装しよう。

```hx
package mylang;

class Compiler {
	public static function compile<T,S,R>(exp : Exp<T>, cont : Program<TCons<T,S>,R>) : Program<S,R> {
		return switch(exp) {
			case ConstB(b): Instr(IConstB(b), cont);
			case ConstI(i): Instr(IConstI(i), cont);
			case BinOp(f, e1, e2): compile(e2, compile(e1, Instr(IBinOp(f), cont)));
		}
	}
}
```

```hx
import mylang.BinOp;
import mylang.Exp;
import mylang.Instr;
import mylang.Program;
import mylang.Stack;

using mylang.Compiler;
using mylang.Exps;
using mylang.Programs;
using mylang.Stacks;

class Main {
	public static function main() {
		var x = BinOp(Eq, BinOp(Plus, ConstI(10), ConstI(20)), ConstI(30));
		var v = x.denote();
		trace(v);
		var y = x.compile(End);
		var w = y.denote(Nil).value();
		trace(w);
	}
}
```

実行結果:

```
Main.hx:16: true
Main.hx:19: true
```

# リポジトリ

[mandel59/haxe-gadt-example](https://github.com/mandel59/haxe-gadt-example)

# 参考文献
- [CPDT] [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/)