今回はOCamlの現在のlatest versionである3.12.1には実装されていない、GADTについて試してみました。
とりあえず、現状でOCamlのGADTを試すにはOCamlのsvnリポジトリからgadtsをとってきてビルドとインストールを行う必要があります。
ただし、これを行うと、今まで入れていた標準でないライブラリのうち、cmiファイルが関係するライブラリはほぼ全滅します（多分）。つまり自力で入れ直しです。それにバージョン名が変更されたりする関係でoasisパッケージでOCamlのバージョン指定がある場合、そのままでは対応していないバージョンとして扱われるなどの問題があります。現状、そのまま普段の開発で使うにはかなり自力での解決が必要になりそうです。
それでは以上のことに注意しながら、GADT対応バージョンを入れてみます。
$ svn co http://caml.inria.fr/svn/ocaml/branches/gadts $ cd gadts $ ./configure $ make world.opt $ sudo make install
これでGADTを使えるようになりました。とりあえず、使う前にGADTがあることで何ができるか簡単に説明します。
たとえば次のようなヴァリアントの型を考えます。
type 'a ty = Int of int | String of string | List of 'a ty | Pair of ('a ty * 'b ty)
しかしこのような型は書くことができません。なぜなら戻る型には現れない 'b という存在型があるからです。
またもうひとつ、戻り型の型パラメータをヴァリアントごとに制約することができないという問題があります。
たとえば、先ほどの 'a ty をうけとる次のような型を定義してみます。
type 'a variant = VInt of int ty | VString of string ty
このような型を定義したとして次のコード
VInt (String "")
はどうなるでしょうか。型付けでエラーとなるでしょうか。
なりません。なぜなら、(String "")の戻り型を見れば一目瞭然です。
# (String "") - : 'a ty = String ""
つまり戻り型の制約はありません。（当たり前ではありますが）
さて、以上のことをふまえて、GADTで上のような場合にどのような解決が可能でしょうか。
type 'a ty = Int : int -> int ty | String : string -> string ty | List : 'a ty -> 'a list ty | Pair : ('a ty * 'b ty) -> ('a * 'b) ty
まずIntやStringでは、戻り型の型パラメータの制約ができます。そして、Pairに関しては戻り型に存在しない存在型を書くことができます。
IntやStringは型パラメータの制約ができたので、'a variant での問題も解決できます。
type 'a variant = VInt : int term -> int variant | VString : string -> string variant VInt (String "") (* 型エラー！ *)
GADTが使えると以上のような問題を解決できます。
さて、今度はGADTを使ってジェネリックプログラミングをしてみましょう。
ここではあまり説明はしませんが、読めばある程度理解できるのではないでしょうか。
type 'a term = Int : int term | String : string term | List : 'a term -> 'a list term (* ヴァリアントごとに返す関数を変える *) let rec subtype : type t s. t term -> s term -> (t -> s) = fun t s -> match t, s with | Int, Int -> (fun x -> x) | String, String -> (fun x -> x) | Int, String -> string_of_int | String, Int -> int_of_string | List t1, List s1 -> let sub = subtype t1 s1 in List.map sub | _, _ -> invalid_arg "subtype" let subtype t s = subtype t s (* 使い方 *) assert (subtype (Int String) 1 = "1") assert (subtype ((List Int) (List String)) [1; 2; 3] = ["1"; "2"; "3"])
上のコードのように
subtype (Int String) 10
のような形でコードを書くことができます。GADTはいろいろ夢が膨らみますが、ライブラリ等の関係で私はしばらくは使えなさそうです。次のバージョンに期待しましょう。
