Types and Programming Languagesの24章の主題は存在型（Existential Types）である。

私は何回読んでもここでつまづく。

この章に到達するまでに部分型やら再帰型やら型推論やら全称型やら出てくるが、まあ難しくとも、なんとなくどういった言語機能に関連する型なのかがそれなりにイメージできた。

しかし存在型に関してはまったくイメージがわかず困っていた。

To understand existential types, we need to know two things: how to build (or introduce, in the jargon of 9.4) elements that inhabit them, and how to use (or eliminate) these values in computations

とか言われて目が回ったり（useとeliminateが同じ意味なのか？）。ある存在型に含まれる値というのが「型と値の組」というのもよくわからなかった（型の値として型が出てきていいのか？）

最近OCamlのモジュール周りをいろいろ試してきてようやく直観がついてきた気がする。

というわけで復習がてらOCamlで存在型が出てくる局面を：

第１級モジュール
ファンクタ
一般的なモジュール
GADT

を使って示してみる。

第１級モジュール

第１級モジュールはまさに存在型！という感じの機能だ。

module type ADDABLE_INT = sig
  type t
  val create : int -> t
  val to_int : t -> int
  val add : t -> t -> t
end

というシグニチャが{∃X, {create:int->X; to_int:X->int; add:X->X->X}}という存在型に対応している。

このシグニチャを満たし得る実装を二つ用意する：

module IntInt = struct
  type t = int
  let create x = x
  let to_int x = x
  let add = (+)
end

module PeanoInt = struct
  type t =
  | Zero
  | Succ of t

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

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

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

最初のものはOCamlのnativeな整数型であるintをそのまま使った実装、もう一つはペアノ数を使った実装となる。

第１級モジュールの機能を使うとこれらモジュールを普通の値のように扱える：

let ints = (module IntInt : ADDABLE_INT)
let peanos = (module PeanoInt : ADDABLE_INT)

let mlist = [ints; peanos]

intsとpeanoは元となるモジュールの内部実装は相当違うが、第１級モジュール化した時点で型が同じmodule ADDABLE_INTになる。なので両方を同一のリストに入れることができる。

そして多相的（？）に関数に渡せる：

let f x y m =
  let module M = (val m : ADDABLE_INT) in
  M.to_int @@ M.add (M.create x) (M.create y)

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

ただし戻り値は多相にはできない：

utop # let g x y m =
  let module M = (val m : ADDABLE_INT) in
  M.add (M.create x) (M.create y);;
Line 3, characters 2-33:
Error: This expression has type M.t but an expression was expected of type 'a
       The type constructor M.t would escape its scope

詳細はTaPL24章を参考にしてほしいが、明確に

let ints = (module IntInt : ADDABLE_INT)
let module M = (val ints : ADDABLE_INT)

が存在型のpack/unpackに対応している。

存在型のポイントとなる言語機能は：

実装が異なる型とその型に関連する値を、統一的な存在型の値に変換するpack
packされた値を再度分解して使えるようにするunpack
unpackされたものも存在型に明示されたインタフェースのみで扱える

といったところ。抽象的データ型（代数的データ型ではないのに注意！）をカプセル化して外部インタフェースのみアクセス可能にするような機能である。

長くなってきたのでファンクタ以降の話は次回。

Arantium Maestum

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

OCamlで存在型を試してみた（その１ーー第１級モジュール）

第１級モジュール