読者です 読者をやめる 読者になる 読者になる

anti scroll

ブラウザと小説の新しい関係を模索する

GADTというものを知った

最近OCamlをようやくversion4系列にアップデートしたのですが。

その際にGADTとかいう言葉が気になったので調べていたら、ちょうどわかりやすいエントリーが。

Detecting use-cases for GADTs in OCaml

上のエントリによると、どうやらGADTというのは「代数型に型の強制を付けるためのもの」らしいです。

どいういうことかというと、例えばとあるexprという代数型を

type expr = 
  | Tint of int
  | Tbool of bool

と宣言した時、exprは中身がintの時もあれば、boolの時もある型ですよ、と宣言しているわけですが…

つまりTint 10Tbool falseも、同じexpr型に属することになりますよ、としているわけですが…

このexpr型を使って構成される「別の代数型」というものを考えた時、単にexpr型とだけ宣言されると、表現としてイマイチになることがあるのですよね。

例えば次のようなAbstract Syntax Treeを定義したとき…

type ast = 
  | Value of expr
  | IfExpr of expr * expr * expr

なんかIfExprexpr * 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で制約していればコンパイルの段階でエラーにしてくれます。