Skip to content

Latest commit

 

History

History
228 lines (164 loc) · 13.5 KB

algebraictype.md

File metadata and controls

228 lines (164 loc) · 13.5 KB
Raw

代数的データ型

代数的データ型 (algebraic data type) は直積と直和と再帰によって構成される型である。

直積

既にある二つの値を纏めて一つの値として扱へる様にしたものが直積 (direct product) である。集合論的にはデカルト積 (Cartesian product) に、圏論的には積 (product) に相当する。 一般に、「積の積」や「積の積の積」を再び一つの値としてみなすことで、いくらでも多くの値を纏めることができる。

直積を言語内で使へるやうにするためのプリミティブとしては、直積を作るための構築関数が必要である。

Pair : * → * → *
Pair = λA. λB. ΠR. (A → B → R) → R
cons : ΠA. A → ΠB. B → Pair A B
cons = λA. λa. λB. λb. λR. λf. f a b

Pair の型定義が言語内で透過的でない場合は、直積から値を取り出すための射影関数も必要となる。

first : ΠA. ΠB. Pair A B → A
first = λA. λB. λp. p (λa. λb. a)
second : ΠA. ΠB. Pair A B → B
second = λA. λB. λp. p (λa. λb. b)

レコード

任意の個数の値を纏めることができる様に一般化された直積について、それぞれの値を識別子で区別できる様にしたものをレコード (record) といふ。

直和

二つの型が与へられた時、そのどちらかの型の値を持ってゐる値が直和 (direct sum) である。俗にバリアント (variant) とも言ふ。より正確には非交和 (disjoint union または discriminated union) と言った方が良い。C で union を共用体と訳すのに倣って discriminated union を判別共用体と訳す流儀もある。 一般に、「和の和」や「和の和の和」を再び一つの値としてみなすことで、いくらでも多くの型を扱ふことができる。

直和を言語内で使へるやうにするためのプリミティブとしては、直和を作るための注入関数が必要である。

Either : * → * → *
Either = λA. λB. ΠR. (A → R) → (B → R) → R
inLeft : ΠA. A → ΠB. Either A B
inLeft = λA. λa. λB. λR. λf. λg. f a
inRight : ΠB. B → ΠA. Either A B
inRight = λB. λb. λA. λR. λf. λg. g a

Either の型定義が言語内で透過的でない場合は、直和から値を取り出すためのプリミティブも必要となる。これは OCaml の match … with … や Haskell の case … of … の様に専用の構文によって書かれることになる。

タグ付き和

直和が持てる値の型を識別子で区別できる様にしたものをタグ付き和 (tagged union) といふ。 直和をサポートする言語では普通、直和はタグ付き和として実装される。識別子無しでは型を番号 (添字) によってしか区別できず、プログラムが読み難くなるためである。それ故、タグ付き和を直和とかバリアントなどと呼ぶことも多い。

使用できるタグの名前 (とそのタグに関連付ける値の型) を予め宣言させるタイプのものと、タグを即席で作ることのできるタイプのものとがある。 後者では、プログラム内の異なる箇所で作られた同じ識別子のタグが異なる型の値を持つ可能性があるが、その様なタグを同一箇所で混ぜて使ふことは禁じられる。

開かれた直和

通常のタグ付き和では、一つの直和の型の値が取れるタグの種類は有限個に制限され、それらは型付けにおいて全て特定される。 これに対し、取れるタグの種類を型付けにおいて(必ずしも全ては)特定しないタイプのものを開かれた直和と言ふ。

開かれた直和のパターンマッチングでは、取り得るタグの種類を具体名で網羅することはできないので、明示的にマッチングされないタグを全て処理できるワイルドカードパターンが必要となる。

開かれた直和の型は、「値が任意のタグを取れる」といふ点で本質的に一つしかない。ただしタグを即席で作れる場合は、タグに対する値の型の一意性を保証するためにタグの名前と型を直和の型に含めて管理する必要があり、名前と型の組み合はせごとに異なる型となる。

再帰型

型の定義の中にその型自身が現れるものを再帰型 (recursive type) または帰納的な型 (inductive type) といふ。

再帰型を表せる様にするために再帰演算子 μ を導入する。例へば OCaml で

type int_list = Nil | Cons of int * int_list

と定義される整数リスト型は、再帰演算子を用ゐて以下の様に表せる。

IntList = μT. Nil | Cons of int * T

理論的には、再帰演算子はその被演算子を型の生成関数と見た場合の最小不動点を求めるものである。これにより、生成関数が定義する繰り返しのパターンによって構成しうる全ての型を纏めた型が得られる。なほ、最小不動点の代はりに最大不動点を求める様にすると、型は無限の構造を持つ値をも含む様になる。この様な型を余帰納的な型 (coinductive type) といふ。(言語が余帰納的な型の宣言を認めたとしても、無限の構造を持つ項を生成する方法が無ければ意味が無いことに注意)

再帰型は必ずしも直積・直和と組み合はせて使ふものではない。例へば関数型と組み合はせると自分自身を引数とする関数の型 μT.T→U や自分自身を返す関数の型 μT.U→T を作れる。これを応用して項の不動点演算子に型を付けることができる。(この帰結として、再帰型を認める型システムは正規化性を持たないことになる。)

# 遅延評価版
fix : ΠT::*. (T→T)→T
fix = λT::*. λf:T→T. let r = λx:μU.U→T. f (x x) in r r

# 値呼び版
fix : ΠT1::*. ΠT2::*. ((T1→T2)→(T1→T2))→(T1→T2)
fix = λT1::*. λT2::*. λf:(T1→T2)→(T1→T2). let r = λx:μU.U→(T1→T2). f (λy:T1. x x y) in r r

とはいへ、実際の言語では再帰は直積・直和と組み合はせて代数的データ型を定義する時にしか使へない様に制限されるのが普通である。なぜなら、その様にすると以下に述べる同型再帰と相性が良いからである。 OCaml で再帰的な関数の型を作るにはダミーの直和の宣言を噛ますことになる。

(* μT. A → T *)
type 'a t = T of ('a -> 'a t)

再帰型の形式化

上で整数リスト型を定義したが、では IntList と Nil | Cons of int * IntList が「同じ」型であることを処理系はどの様に認識するのか。

同値再帰 (equi-recursive) による形式化では、この様な型式は (構文的に異なる式であっても) 「定義により等しい」と見做す。このやり方は理論的な型の同一性の概念に忠実で直観的に理解しやすいが、処理系に実装するのは相当難しい。

同型再帰 (iso-recursive) による形式化では、構文的に異なる型式は異なる型であるとみなす。同じ再帰型の異なる表現は、適当なタイミングで変換してやる必要がある。型式 μT. Nil | Cons of int * T を Nil | Cons of int * (μT. Nil | Cons of int * T) に変換する操作を展開 (unroll または unfold) と言ひ、その逆の変換を畳み込み (roll または fold) といふ。 展開と畳み込みを行ふ箇所は、項の中に明示することも可能だが、後述の名前的型システムでは処理系が自動的に補ふこともできる。すなはち、直和の値を生成するときおよび値を取り出すときにそれぞれ畳み込みと展開を行ふ。

再帰演算子を用ゐると再帰的な型を即席で作ることができる。この様な方式の型システムを構造的 (structural) 型システムといふ。 一方 OCaml や Haskell など多くの言語では再帰演算子はコード内に明示されず、代はりに再帰的な型には必ず名前が付けられる。型の定義の中でその名前を使用することで、自然に再帰を表現できる。この様な方式の型システムを名前的 (nominal) 型システムといふ。名前的型システムの主な利点は、

  • 再帰的な型 (特に、相互再帰する複数の型) をより直観的な書き方で宣言できる
  • 実行時型情報を取り扱ひやすい
  • 型の等価性や部分型関係の判定がより簡単になる
  • 再帰型の畳み込み・展開をすべき箇所を処理系が推論できる

ただし構造的型システムにも以下の様な特長がある。

  • 型の等価性や部分型関係をより厳密に判定できる
  • 型システムの性質について理論的に検証しやすい

代数的データ型の定義

言語内において直積・直和・再帰を独立して定義できる様にすることも可能であるが、一般的な関数型言語ではこれら(のうち特に直和と再帰)は合はせて一つの構文で宣言される。

例へば OCaml では、タグ付き和と再帰はどちらも「データ型の宣言」として纏めて一つの宣言構文で書かれる。

# 1, "abc";; (* 直積は即席で作れる *)
- : int * string = (1, "abc")
# type int_float_pair = { i : int; f : float; };; (* レコードは予め宣言が必要 *)
type int_float_pair = { i : int; f : float; }
# {i = 42; f = 0.};;
- : int_float_pair = {i = 42; f = 0.}
# type ('a, 'b) either = Left of 'a | Right of 'b;; (* 予め宣言が必要なタグ付き和 *)
type ('a, 'b) either = Left of 'a | Right of 'b
# Right 1;;
- : ('a, int) either = Right 1
# type int_list = Nil | Cons of int * int_list;; (* タグ付き和と直積と再帰の組み合はせ *)
type int_list = Nil | Cons of int * int_list
# Cons (1, Nil);;
- : int_list = Cons (1, Nil)
# `Int 0;; (* 即席でタグ付き和を作ることもできるが、再帰はできない *)
- : [> `Int of int ] = `Int 0

Haskell ではレコードの宣言もデータ型の宣言の中で行はれる。(レコードは直和のタグが取れる値としてのみ宣言できる)

data IntList = Nil | Cons {head :: Int, tail :: IntList}

直和と再帰を独立して宣言できる架空の言語を考へてみる。

(* タグとして既述の cons の他に nil を定義しておく *)
Nil : *
nil : Nil

(* Nil と Pair を使って IntList を宣言する *)
IntList : *
IntList = μT. Nil | Pair Int T

リストを生成するための cons が Pair 型の値を生成するのは不自然に見える。cons の第二引数が IntList であることを、cons を宣言する段階で明示したい。しかしそのためには、IntList といふ型があることが cons を宣言する段階で分かってゐなければならない。IntList の種の宣言と内容の定義を分けて書くことで対処しようとすると、以下の様になる。

(* 先に IntList の種を宣言する *)
IntList : *

(* cons を定義する *)
Cons : *
cons : Int → IntList → Cons

(* IntList を定義する *)
IntList = Nil | Cons

結局、cons の定義と IntList の定義が相互に依存してゐるためにそれらを分けて書かうとするとややこしくなる。故に、直和と再帰を一つの構文内で纏めて宣言する方式を採用する言語が多い。

相互依存する型

オブジェクト指向プログラミングでは、クラスの相互依存は一般に望ましくない設計であるとされる。どのオブジェクトがどのオブジェクトを支配してゐるのか分かりにくくなってしまふ為である。

// C++
class Controller;
class View {
  Controller *controller;
}
class Controller {
  View *view;
}

被支配者から支配者への依存をインターフェースとして抽象化するとこの様な相互依存を断ち切ることができる。

class ViewEventListener {
  ... // 抽象メソッドの定義
}
class View {
  ViewEventListener *listener;
}
class Controller : private ViewEventListener {
  View *view;
}

ここでクラスの事前宣言が不要になったことに注目する。事前宣言 (forward declaration) とは実体を定義する前にそのものの名前と型 (種) のみを宣言するもののことである。相互依存が無ければ型の事前宣言は不要である。

C++、Java、C# などクラスを主体とする言語の多くは、クラスの定義をクラスごとに独立して書く構文を採用してゐる。依存し合ふ複数のクラスを離れた場所に書くことができるため、相互依存関係があることをコードからすぐ読み取ることは難しい。 また Java や C# では相互依存するクラスの名前を事前宣言無しで処理系が自動的に解決する。これにより意図しない相互依存を発生させやすい。(Cycles and modularity in the wild)

OCaml では、相互依存する型は一度に纏めて定義しなければならない。

type even =
  | Zero
  | Even of odd
and odd =
  | Odd of even