OCamlでGADTを試してみた
なんとなく幽霊型がわかったので、その勢いに乗ってGeneralized Algebraic Data Typesについても調べてみた。
OCamlの言語機能としては:
OCaml 4.00から導入された(ちなみに2021/3で最新版は4.12)とのことで、リリーススケジュールを見てみると:
4.00がリリースされGADTが使えるようになったのは2012年のようだ。
GADTとは
簡潔な解説としてはこちらのreddit投稿がすごくよかった:
ちょっとアレンジして説明してみる。
例えばこんな型を定義したとする:
type t = Int of int | Char of char
ゲッターもほしい。が、どう定義すればいいのか。
簡単なのは返ってくる型ごとに定義してみる方式:
let getInt = function | Int x -> x | _ -> failwith "cannot getInt on non-Int" let getChat = function | Char x -> x | _ -> failwith "cannot getChar on non-Char"
これはちゃんとコンパイルする。が二つ関数を定義することになるし、さらに型が合わないバリアントの場合は実行時エラーを投げることになる(静的型の恩恵を受けない)
多相的なget
を定義しようとすると:
let get = function | Int x -> x | Char x -> x Line 3, characters 12-13: Error: This expression has type char but an expression was expected of type int
と怒られてしまう。
つまり問題点は二つ:
- 特定の型とバリアントを対象に考えてパターンマッチする時に、それ以外のバリアントで実行時エラーを投げるような処理を書くことになる
- 返り値の型が多相的な関数が書けない
この二点を解決するのがGeneralized Algebraic Data Typeだ。
GADTに直接いく前に少し回り道をして考えてみたい。返り値の多相に関しては
type 'a t = 'a list let f = function [] -> None | x :: _ -> Some x
のような形ならパラメトリック多相に書ける。
だったら
type 'a t = Int of int | Char of char
ならどうか?というとこれは前回見た幽霊型で、例えばlet x : bool t = Int 5
のような値が型システム上は作れてしまう。なので
let f : 'a t -> a = function Int x -> x | Char x -> x
という関数が書けない(let x : bool t = Int 5 in f x
がbool
にならないといけないので型チェックが通らない)。
なんとかして
type 'a t = (Int of int) : int t | (Char of char) : char t
のようにバリアントごとに型をきっちり決めることができれば・・・
というわけでそれができるのがGADTだ。
実際の構文はちょっと変わっている:
type 'a t = Int : int -> int t | Char : char -> char t
コンストラクタを関数とみなして、その関数の型を書くような形で定義している。これで例えばInt 5
は必ずint t
f型になる。
このGADTに対してgetInt
やgetChar
を書くと:
let getInt = function Int x -> x let getChar = function Char x -> x
関数一つにつき一つのバリアントについてだけパターンを書くだけで済む。
コンパイラはgetInt : int t -> int
、getChar : char t -> char
と推論して、その場合はパターンマッチが網羅的であると型チェックを通す。
そして多相的なget
:
let get : type a. a t -> a = function Int x -> x | Char x -> x
ここでは一工夫必要になっていて、get : type a. a t -> a
でa
というlocally abstract typeを使うことでちゃんと多相性を保つようにする。
これで
get @@ Int 5 get @@ Char 'c'
と入力されるバリアントが違えば返り値の型も変わる関数が書けた。
前述の問題点2つが
- 特定の型とバリアントを対象に考えてパターンマッチする時に、それ以外のバリアントは書かなくてもいい(書かなくても網羅的であると型システムが判断してくれる)
- 返り値の型が多相的な関数が書ける(locally abstract typeも使えば)
としっかり解決されている。
ASTをGADTで表現してみる
前回の記事の終わり、「隠蔽しないと幽霊型にならない」という話題で言及した記事:
とその元である:
こちらの例は(記事が書かれた時点ではOCamlになかった)GADTで書くと非常に綺麗になる。
型はこんな定義:
type 'a term = | Lit : int -> int term | Inc : int term -> int term | IsZ : int term -> bool term | If : (bool term * 'a term * 'a term) -> 'a term | Pair : ('a term * 'b term) -> ('a * 'b) term | Fst : ('a * 'b) term -> 'a term | Snd : ('a * 'b) term -> 'b term
幽霊型を使う場合はいちいちコンストラクタを関数でwrapしてその関数の返り値の型を幽霊型にして、という作業が必要だったがGADTの場合はバリアント定義そのものにしっかり型を指定するのでそういったwrapperはいらない。
上記の定義だけで:
utop # Lit 0;; - : int term = Lit 0 utop # Inc (Lit 0);; - : int term = Inc (Lit 0) utop # IsZ (Lit 0);; - : bool term = IsZ (Lit 0) utop # IsZ (IsZ (Lit 0));; Line 1, characters 4-17: Error: This expression has type bool term but an expression was expected of type int term Type bool is not compatible with type int
とダメなケースは型システムで静的に弾いてくれる。
GADTが幽霊型に対してこのケースでさらに優れている点としては、この型を使った関数でも静的型検査がうまく作動してくれること。
例えばこのASTを評価するeval
関数を作成する:
let rec eval : type a. a term -> a = function | Lit n -> n | Inc e -> eval e + 1 | IsZ e -> eval e = 0 | If(cond, t, f) -> if eval cond then eval t else eval f | Pair(e1, e2) -> (eval e1), (eval e2) | Fst e -> fst @@ eval e | Snd e -> snd @@ eval e
まあ非常にスムーズに書ける。GADTではなくただのバリアントで書いた場合はIf(cond, t, f)
などでeval cond
がちゃんとbool
(をwrapしたバリアント)になっているかチェック、bool
じゃなければエラー、といった処理を書く必要が出てくるものだが、ここでは必要ない。If
バリアントの定義からcond
はbool term
型でしかありえず、ということはeval cond
はbool
型でしかありえない、ということが型システムに保証される。
さらには、例えばうっかり
let rec eval : type a. a term -> a = function | Lit n -> n | Inc e -> eval e + 1 | IsZ e -> eval e = 0 | If(cond, t, f) -> if eval t then eval cond else eval f (* ここ *) | Pair(e1, e2) -> (eval e1), (eval e2) | Fst e -> fst @@ eval e | Snd e -> snd @@ eval e
とIf(cond, t, f)
の部分の順序を間違えてeval t
を分岐条件に持ってこようとした場合:
Line 5, characters 23-29: Error: This expression has type a but an expression was expected of type bool because it is in the condition of an if-statement
と「eval t
はbool
型であるとは限りません」と静的に弾かれる。
他の使い方
前回の記事でも出たYaron MinskyのJane Street BlogにもGADTの(言語実装以外の実用的な)活用事例が載っている:
多相的なarray
とchar
型しか格納できないbyte
を統一的なバリアント型とインターフェイスで扱うのにGADTが非常に便利、という話。Jane Street Blogはこういう実用的・少し泥臭い話題も出てくるから面白い。