ダメな例

まずはうまくいかない例。素直に存在型を記述しようと思ったらこんな感じになるかと思う：

type t = {create:int->'a; to_int: 'a->int; add:'a->'a->'a}

(* あるいは *)

type t = E of {create:int->'a; to_int: 'a->int; add:'a->'a->'a}

右辺で型変数を持ったレコードを定義するが、左辺には型変数が出てこない。

しかしこれは：

Line 1, characters 22-24:
Error: The type variable 'a is unbound in this type declaration.

と怒られてしまう。普通の型だと右辺に出てくる型変数は左辺にも出てくる必要がある。

GADTを使った実装

GADTにはそんな制約はない。なのでこういう存在型の書き方ができる：

type t = E : {create:int->'a; to_int: 'a->int; add:'a->'a->'a} -> t

統一的な存在型tに型変数aとその型を使った値create、to_int、addが定義されているレコードを閉じ込めることに成功している。

この存在型に合致する、OCamlのnativeなintを使った実装は：

let ints = E {create=(fun x -> x); to_int=(fun x -> x); add=(+)}

そして同じくこの存在型に合致するペアノ数を使った実装は：

type peano =
| Zero
| Succ of peano

let rec peano_create n =
    if n = 0 then Zero
    else Succ (peano_create (n-1))

let rec peano_to_int = function
  | Zero -> 0
  | Succ x -> 1 + (peano_to_int x)

let rec peano_add x = function
  | Zero -> x
  | Succ y -> peano_add (Succ x) y

let peanos = 
E {  create=peano_create
; to_int=peano_to_int
; add=peano_add
}

となる。

使ってみる

注目する点としては、これらは両方まったく同じt型であること。

なので同じリストに放り込めるし、この値を引数にする関数も作れる：

let glist = [ints; peanos]
let f x y (E r) = r.to_int @@ r.add (r.create x) (r.create y)

List.mapで関数を適用してみる：

utop # List.map (f 3 4) glist;;
- : int list = [7; 7]

成功。

また、'a型の値がリークするような処理は書けない：

utop # let E r = ints in r.add (r.create 3) (r.create 4);;
Line 1, characters 18-49:
Error: This expression has type $E_'a but an expression was expected of type 'a
       The type constructor $E_'a would escape its scope

そしてもちろん'a型の内部実装を前提としたコードも書けない：

utop # let E r = ints in r.to_int @@ r.add 3 4;;
Line 1, characters 36-37:
Error: This expression has type int but an expression was expected of type
         $E_'a

存在型との対応

type tが存在型{∃X, {create:int->X; to_int:X->int; add:X->X->X}}に、let x = E { ... }がpackに、let E r = x in ...がunpackに対応しており、type tがリークできないことも含めて、しっかりと存在型で拡張されたシステムFに合致する挙動となっている。

というわけで過不足なく存在型がエンコードできるという意味で、GADTの方がモジュール機構を使うより直接に存在型に対応する書き方だと言える。

参考文献

Advanced Functional Programming: Abstraction and parametricity, Leo White https://www.cl.cam.ac.uk/teaching/1415/L28/abstraction.pdf

Arantium Maestum

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

OCamlで存在型を試してみた（その４ーーGADT）

ダメな例

GADTを使った実装

使ってみる

存在型との対応

参考文献