Arantium Maestum

プログラミング、囲碁、読書の話題

OCamlでGADTを試してみた

なんとなく幽霊型がわかったので、その勢いに乗ってGeneralized Algebraic Data Typesについても調べてみた。

OCamlの言語機能としては:

caml.inria.fr

OCaml 4.00から導入された(ちなみに2021/3で最新版は4.12)とのことで、リリーススケジュールを見てみると:

ocaml.org

4.00がリリースされGADTが使えるようになったのは2012年のようだ。

GADTとは

簡潔な解説としてはこちらのreddit投稿がすごくよかった:

www.reddit.com

ちょっとアレンジして説明してみる。

例えばこんな型を定義したとする:

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 xboolにならないといけないので型チェックが通らない)。

なんとかして

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 tf型になる。

このGADTに対してgetIntgetCharを書くと:

let getInt = function Int x -> x
let getChar = function Char x -> x

関数一つにつき一つのバリアントについてだけパターンを書くだけで済む。

コンパイラgetInt : int t -> intgetChar : char t -> charと推論して、その場合はパターンマッチが網羅的であると型チェックを通す。

そして多相的なget

let get : type a. a t -> a = function
  Int x -> x
| Char x -> x

ここでは一工夫必要になっていて、get : type a. a t -> aaというlocally abstract typeを使うことでちゃんと多相性を保つようにする。

これで

get @@ Int 5
get @@ Char 'c'

と入力されるバリアントが違えば返り値の型も変わる関数が書けた。

前述の問題点2つが

  • 特定の型とバリアントを対象に考えてパターンマッチする時に、それ以外のバリアントは書かなくてもいい(書かなくても網羅的であると型システムが判断してくれる)
  • 返り値の型が多相的な関数が書ける(locally abstract typeも使えば)

としっかり解決されている。

ASTをGADTで表現してみる

前回の記事の終わり、「隠蔽しないと幽霊型にならない」という話題で言及した記事:

camlspotter.hatenablog.com

とその元である:

tatta.hatenadiary.org

こちらの例は(記事が書かれた時点では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バリアントの定義からcondbool term型でしかありえず、ということはeval condbool型でしかありえない、ということが型システムに保証される。

さらには、例えばうっかり

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 tbool型であるとは限りません」と静的に弾かれる。

他の使い方

前回の記事でも出たYaron MinskyのJane Street BlogにもGADTの(言語実装以外の実用的な)活用事例が載っている:

blog.janestreet.com

多相的なarraychar型しか格納できないbyteを統一的なバリアント型とインターフェイスで扱うのにGADTが非常に便利、という話。Jane Street Blogはこういう実用的・少し泥臭い話題も出てくるから面白い。