最近OCamlをようやくversion4系列にアップデートしたのですが。
その際にGADTとかいう言葉が気になったので調べていたら、ちょうどわかりやすいエントリーが。
Detecting use-cases for GADTs in OCaml
上のエントリによると、どうやらGADTというのは「代数型に型の強制を付けるためのもの」らしいです。
どいういうことかというと、例えばとあるexprという代数型を
type expr = | Tint of int | Tbool of bool
と宣言した時、exprは中身がintの時もあれば、boolの時もある型ですよ、と宣言しているわけですが…
つまりTint 10
もTbool false
も、同じexpr型に属することになりますよ、としているわけですが…
このexpr型を使って構成される「別の代数型」というものを考えた時、単にexpr型とだけ宣言されると、表現としてイマイチになることがあるのですよね。
例えば次のようなAbstract Syntax Treeを定義したとき…
type ast = | Value of expr | IfExpr of expr * expr * expr
なんかIfExpr
のexpr * expr * expr
の部分の表現力が乏しくないですか?
exprが3つ並んでるんですけど、それぞれがどういう性質のexprを要求しているのか、よくわからないですよね。
もしこのIfExpr
を
IfExpr of (bool値のexpr) * (int値のexpr) * (int値のexpr)
みたいなニュアンスで型を制限できたら、安全だし、わかりやすくないですか?
これを、まさに可能にするのがGADTというやつらしく。
ちなみにGADTというのは、Generalized Algebraic Data Typeの略で日本語なら「汎用代数型」とでも訳すのでしょうか?
実際にexprとastをそれぞれGADTを使った型宣言(expr'とast'とする)に書き直すと、こういう感じになります。
type _ expr' = | Gint: int -> expr' | Gbool: bool -> expr' type _ ast' = | GValue: int expr' | GIfExpr: bool expr' -> int expr' -> int expr' -> int expr'
普通の代数型だとof
が来る部分に:
が来て、右側が「型の関数」みたいな記述になるのが特徴です。
で、構成される代数型に型の制約を付けたい場合はtype _ expr' = ...
みたいに宣言します。
アンダースコアの部分は「代数型に何かしらの型アノテーションがつくよ」みたいなニュアンスなんでしょうか?
こうやって作られたGADTを使うと、
let statement_by_gadt : ast' = GIfExpr (Gint 10) (Gint 20) (Gint 30)
は、IfExprの一つ目のexpr'が「bool expr'」じゃないので、コンパイルの段階でエラーになります。
一方で、GADTじゃない、普通の代数型のastを使った場合、次の
let statement_no_gadt : ast = IfExpr (Tint 10) (Tint 20) (Tint 30)
は(型の上では)エラーではありません。
IfExprを構成するメンバーは全てexpr型と規定されているだけなので、型の上では正しいからです。
これを構文エラーにするには、evalするときにundefned patternとして、型エラーを自前で書くしかないわけですが、GADTで制約していればコンパイルの段階でエラーにしてくれます。