再帰データ型または再帰型（Recursive Type）とは、データ型の一種であり、代数的データ型として定義したならば、定義の右辺中にそれ自身の型が出現するような型である。直接は現れない（相互再帰）ものもある。例として、Haskellでのリスト型を示す:これは、リスト a は空のリストの場合と 'a' を先頭に持つリストの場合があることを示している。なお、MirandaやHaskellの型シノニム宣言では再帰は許されていないので、以下のような Haskell での型定義は不正である:それに対し、見た目は等価に思える代数データ型は正当であり利用可能である:型理論では、再帰データ型の一般形は μα.T で表される。ここで型変数 α は型そのものであると共に、型 T の中にも現われる可能性がある。例えば、自然数を Haskell のデータ型として表すと次のようになる（ペアノの公理参照）:また、型理論では formula_1 となる。ここでは、Zero と Succ コンストラクタで表現されており、Zero は引数をとらず（型理論の定義の formula_2に相当）、Succ は別の Nat を引数としている（型理論での定義のformula_3に相当）。再帰データ型には、同形再帰データ型（isorecursive type）と等価再帰データ型（equirecursive type）の2つの形式がある。これらは、再帰データ型の定義における項の排除の仕方に違いがある。同形再帰データ型では、再帰データ型 formula_4 とその拡張（展開）である formula_5 は別の型であり、特殊な項構成 "roll" と "unroll" で識別され、これらの間で同型写像を構成する。正確に記せば、formula_6 と formula_7 であり、これらは互いに逆関数である。等価再帰規則では、再帰データ型 formula_4 とその展開 formula_9 は「等価」である。ここで等価とは、この2つの型表現が同じ型を表していると理解されることを示す。実際、等価再帰型の理論ではさらに、無限に展開したときに等価となる2つの型表現は等価であるとするのが一般的である。このような規則の結果として、等価再帰データ型は同形再帰データ型よりも遥かに複雑な型システムを提供する。型検査のようなアルゴリズム上の問題や型推論も等価再帰データ型の方が難しい。等価再帰データ型は、自己参照形式や相互参照形式の型定義が可能である。これは手続き的かつオブジェクト指向言語ではオブジェクトやクラスの型理論的意味論問題を生じる。関数型言語では、同形再帰データ型がはるかに普遍的に使われている。

出典:wikipedia