Zenn
Open9

OCaml の GADTs について

OCaml
#
型システム
Kodai MatsumotoKodai Matsumoto

関数型プログラミング言語 OCaml の GADTs (Generalized Algebraic Datatypes) に関して、何となく意味論を想像しながらサンプルコードを写経してみても全然しっくりこなかったので、わかったことと疑問点をまとめていこうと思います。

Kodai MatsumotoKodai Matsumoto

GADTs は、直和型 (Sum type) を以下のような特徴を持つように拡張したもの

  • 値コンストラクタに依存して、型パラメータの制約が変化しうる
  • 型変数が存在量化されうる
Kodai MatsumotoKodai Matsumoto

直和型

  • とりうる値がすべて列挙されている
  • 必ずどれか一つの値になり、複数にまたがることはない

タグ付き共用型、ヴァリアント型とも呼ばれるらしい

サンプル

直和型 bin_op, expr

type bin_op = Add | Sub | Mul | Div
(* 値コンストラクタ: Add, Sub, Mul, Div *)

type expr =
  | IntLiteral of int
  | BinExpr of expr * bin_op * expr
(* 値コンストラクタ: IntLiteral, BinExpr *)
Kodai MatsumotoKodai Matsumoto

存在量化

「ある○○について、△△である」のように、特定の議論領域において少なくとも1つのメンバーが特定の条件を満たすことを示す

Kodai MatsumotoKodai Matsumoto

型パラメータのインスタンス化が起こる明示的な戻り値型を指定することで、制約が追加される。この戻り値型は、定義されている型と同じ型コンストラクタを用い、同数のパラメータを持たなければならない。

型変数は、コンストラクタの引数に含まれていて戻り値型に含まれていない場合に存在量化される。

直和型では以下のような定義ができない。

type 'a ty =
  | A of 'a
  | B of 'a ty * 'b ty

Error: The type variable 'b is unbound in this type declaration.

GADTs では以下のように定義できる。

type _ ty =
  | A : 'a -> 'a ty
  | B : ('a ty * 'b ty) -> ('a * 'b) ty

↑の定義に従うと、以下のような型付けが行われる。

# A 1;;
- : int ty = A 1
# A "foo";;
- : string ty = A "foo"
# B (A 1, A "foo");;
- : (int * string) ty = B (A 1, A "foo")
Kodai MatsumotoKodai Matsumoto

ペアノ自然数

type z = Z

type 'a s = S of 'a

type _ nat =
  | Nz : z -> z nat
  | Ns : 'a nat -> 'a s nat

# Nz Z;;
- : z nat = Nz Z
# Ns (Nz Z);;
- : z s nat = Ns (Nz Z)
# Ns (Ns (Nz Z));;
- : z s s nat = Ns (Ns (Nz Z))

ちなみに z, 'a s 型の値コンストラクタを取り除くと、

type z

type 'a s

type _ nat =
  | Nz : z -> z nat
  | Ns : 'a nat -> 'a s nat

type _ nat = ... に対して以下のコンパイルエラーが出る。

Error: In this definition, a type variable cannot be deduced
       from the type parameters.
Kodai MatsumotoKodai Matsumoto

型定義関連の構文

構文定義
type-definition ::= type ["norec"] typedef { "and" typedef }
typedef ::= [type-params] typeconstr-name type-information
type-params ::= type-param | ( type-param { "," type-param } )