再帰データ型

出典: フリー百科事典『ウィキペディア（Wikipedia）』

再帰データ型または再帰型（Recursive Type）とは、プログラミング言語におけるデータ型の一種であり、同型の複数の値を含む構造になっているデータ型を指す。

目次 1 例 2 理論 2.1 同形再帰データ型 2.2 等価再帰データ型 3 関連項目

[編集] 例

例として、Haskell言語でのリスト型を示す:

data List a = Nil | Cons a (List a)

これは、リスト a は空のリストの場合と 'a' を先頭に持つリストの場合があることを示している。

Miranda や Haskell のシノニム型では再帰は許されていないので、以下のような Haskell での型定義は不正である:

type Bad = (Int, Bad)
type Evil = Bool -> Evil

逆に、見た目は等価に思える代数データ型は正当であり利用可能である:

data Good = Pair Int Good
data Fine = Fun (Bool->Fine)

[編集] 理論

型理論では、再帰データ型の一般形は μα.T で表される。ここで型変数 α は型そのものであると共に、型 T の中にも現われる可能性がある。

例えば、自然数を Haskell のデータ型として表すと次のようになる（ペアノの公理参照）:

  data Nat = Zero | Succ Nat

また、型理論では nat = μα.1 + α となる。ここでは、Zero と Succ コンストラクタで表現されており、Zero は引数をとらず（型理論の定義の αに相当）、Succ は別の Nat を引数としている（型理論での定義の1 + αに相当）。

再帰データ型には、同形再帰データ型（isorecursive type）と等価再帰データ型（equirecursive type）の2つの形式がある。これらは、再帰データ型の定義における項の排除の仕方に違いがある。

[編集] 同形再帰データ型

同形再帰データ型では、再帰データ型 μα.T とその拡張（展開）である T[μα.T / α] は別の型であり、特殊な項構成 roll と unroll で識別され、これらの間で同型写像を構成する。正確に記せば、 と であり、これらは互いに逆関数である。

[編集] 等価再帰データ型

等価再帰規則では、再帰データ型 μα.T とその展開 T[μα.T / α] は「等価」である。ここで等価とは、この2つの型表現が同じ型を表していると理解されることを示す。実際、等価再帰型の理論ではさらに、無限に展開したときに等価となる2つの型表現は等価であるとするのが一般的である。このような規則の結果として、等価再帰データ型は同形再帰データ型よりも遥かに複雑な型システムを提供する。型検査のようなアルゴリズム上の問題や型推論も等価再帰データ型の方が難しい。

等価再帰データ型は、自己参照形式や相互参照形式の型定義が可能である。これは手続き的かつオブジェクト指向言語ではオブジェクトやクラスの型理論的意味論問題を生じる。関数型言語では、等価再帰データ型はさらに普遍的に使われている。

[編集] 関連項目

• 再帰呼び出し
• 代数データ型

この記述は GNU Free Documentation License のもとに公開されているコンピュータ用語辞典『 Free On-line Dictionary of Computing (FOLDOC) 』に基づいています。