GADTによるHaskellの型付きDSLの構築 - プログラミングの実験場

GADTについて、この解説が分かりやすい（英語）。 http://en.wikibooks.org/wiki/Haskell/GADT

背景

Haskell（というか関数型言語一般）の素晴らしい機能の一つ、代数的データ型を使うと、抽象構文木(AST)をHaskellの枠組みの中で表現できる。
例えば、整数の足し算・引き算ならば、

data Exp = Const Int | Add Exp Exp | Subtract Exp Exp

さらにこのASTを数値一般に使いたいので型パラメータrをつけて多相にしてみる。

data Exp r = Const r | Add (Exp r) (Exp r) | Subtract (Exp r) (Exp r)

これを使えば、例えば(3 + 4) - 2という数式は、Subtract (Add (Const 3) (Const 4)) (Const 2) :: Num r => Exp rというHaskellの（多相の）値として表現できる。Exp r型は、rという型パラメータによって型安全性が保たれていて、Add (Const (3::Int)) (Const (4::Double))というのはコンパイルが通らない。

いったんHaskellの値として表現出来れば、あとはパターンマッチを用いるなどしてHaskellの枠組みで型安全に、自由に操作できる。たとえばこのASTを元に、コードの評価をしたり、他の言語の表現として出力したり、といった様々なことができる。つまり、Haskellの中に小さな言語を構築し、Haskellをホスト言語・処理系として使う、一種のDSLといえる。

たとえば評価ならば、

eval :: (Num r) => Exp r -> r
eval (Const v) = v
eval (Add e1 e2) = (eval e1) + (eval e2)
eval (Subtract e1 e2) = (eval e1) - (eval e2)

といった具合。

コード生成だったら、

reify :: (Show r) => Exp r -> String
reify (Const v) = show v
reify (Add e1 e2) = concat ["(",reify e1,"+",reify e2,")"]
reify (Subtract e1 e2) = concat ["(",reify e1,"-",reify e2,")"]

もちろん、掛け算・割り算にも、データコンストラクタとそれに対応する実装をeval,reifyに追加することで簡単に対応できる。

ここまでのコードと実行例は： https://gist.github.com/nebuta/6096315

ASTを型付きにする。

ここで、先のDSLを拡張して、式の評価結果を比較するEq演算子を使えるようにしてみたい。

data Exp r = Const r | Add (Exp r) (Exp r) | Subtract (Exp r) (Exp r)
			| Eq (Exp r) (Exp r) -- ??

ここで問題が発生する。上のような通常のデータ型の定義だと、すべてのデータコンストラクタは引数を適用するとExp r型になり、このEqデータコンストラクタが返す型は、たとえば、(Eq (Const (1::Int)) (Const 1)) :: Exp IntとようにEqのオペランドと同じ型になってしまう。欲しいのはExp IntではなくてExp Boolである。

そこで使えるのがGADTである。GADT(Generalized algebraic datatype)とは、多相のデータ型に対し、データコンストラクタの型を特化することができる仕組み（というのが私の理解）。
まずは元のExp rの定義をGADTのスタイルに書き換える。

{-# LANGUAGE GADTs #-} -- GADTsのプラグマが必要。
data Exp r where
	Const :: r -> Exp r
	Add :: Exp r -> Exp r -> Exp r
	Subtract :: Exp r -> Exp r -> Exp r
	Eq :: Exp r -> Exp r -> Exp r

この時点では、前の例と意味は全く同じ。データコンストラクタが関数の型シグネチャのスタイルに書換えられているのが分かる。型シグネチャの右端に現れるのが、データコンストラクタに引数を完全に適用した際に得られる型。つまりどれもExp r型である。

今やりたいのは、Eq (Exp r) (Exp r)の型をExp rではなくて、より特化したExp Boolにしたいということ。GADTでは、このデータコンストラクタが返す値の型を、Exp rを特化した任意の型に置き換えることができる。

	Eq :: Exp r -> Exp r -> Exp Bool

に書き換えれば良い。

data Exp r where
	Const :: r -> Exp r
	Add :: Exp r -> Exp r -> Exp r
	Subtract :: Exp r -> Exp r -> Exp r
	Eq :: Exp r -> Exp r -> Exp Bool

さらに、２つのExp Boolを引数にとるような、AndとOrも定義してみる。

	And :: Exp Bool -> Exp Bool -> Exp Bool
	Or :: Exp Bool -> Exp Bool -> Exp Bool

GADTを使わないバージョンではrは数値型というのを仮定していたが、この新しいバージョンではrはBoolもありうる。だが、AddやSubtractの引数にはExp Boolは取りたくない。そこで、以下のようにAdd, Subtractの型パラメータrに制限をつけてやる。

data Exp r where
	Const :: (Show r) => r -> Exp r
	Add :: (Num r) => Exp r -> Exp r -> Exp r
	Subtract :: (Num r) => Exp r -> Exp r -> Exp r
	Eq :: (Eq r) => Exp r -> Exp r -> Exp Bool
	And :: Exp Bool -> Exp Bool -> Exp Bool
	Or :: Exp Bool -> Exp Bool -> Exp Bool

こういうことができるのもGADTの強み。
そして、evalの実装は以下のように変わる。

eval :: Exp r -> r
eval (Eq e1 e2) = eval e1 == eval e2
eval (And e1 e2) = eval e1 && eval e2
eval (Or e1 e2) = eval e1 || eval e2
{- 他のパターンは前と同じ -}

evalの定義に(Num r)の制限がなくなったことに注意。これは、型クラスの制限がデータコンストラクタについたために、関数定義には制限をつける必要がなくなったからである。

これによって、And (Eq (Const 3) (Const (2::Int))) (Const True) :: Exp Bool のような、内部に複数の型が混ざったような構文木が型安全に表現できる。内側にあるConst (2::Int)の型はExp Intだが、最終的にAndを適用した後はExp Boolになる。Exp rという多相型の枠組みの中で、型を柔軟かつ強力に付けられる利点がある。

GADTに書き換えたコードと実行例は：https://gist.github.com/nebuta/6096345

コード生成

この型付きASTから手続き型言語のコードを生成する方法についても調査・検討したので別の記事で書く予定。この記事にあるように、WriterモナドとStateモナドを組み合わせることで、一意な変数名の生成などの複雑な処理が書ける。
http://d.hatena.ne.jp/keigoi/20111206/haskell_tagless_dsl

この手法を使うことで、画像処理、JavaScript、いろいろな型安全DSLをHaskell内で構築できると思われ、いろいろなアイデアが浮かんでくる。

また、この論文（Haskell Symposium 2010および2009）はlet-sharingとlambda-sharingという、HaskellのDSLからのコード生成についての２つの問題についての解決法がわかりやすく書いてある。
http://www.eecs.harvard.edu/~mainland/publications/mainland10nikola.pdf
http://www.cs.uu.nl/wiki/pub/Afp/CourseLiterature/Gill-09-TypeSafeReification.pdf