再帰データ型

再帰型（英: recursive type）とは、型の定義中にそれ自身の型が出現するような再帰する型のこと。相互再帰により直接は現れないものもある。再帰データ型（英: recursive data type）とは、データ型における再帰型のこと。

例

再帰データ型

多くのプログラミング言語では名前付きクラスで再帰型を扱うことが出来る。下記は Java での例。Tree のクラス定義の中で Tree を使用している。

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

再帰型エイリアス

型エイリアスや型シノニムで再帰が使えるかどうかはプログラミング言語次第である。

TypeScript などでは型エイリアスの中でも再帰が利用可能である。下記は TypeScript の例だが、型エイリアスだけで木構造の型を表現できる。

しかしながら、HaskellやOCamlやMirandaの型シノニム宣言では再帰は許されていないので、以下のような Haskell での型定義は不正である。

それに対し、見た目は等価に思える代数的データ型は正当であり利用可能である。

理論

型システムは名前的型システムと構造的型システムに分かれる。名前的型システムは Java を始め、多くのプログラミング言語で採用されていて、型に名前を付け、Java なら extends で何を継承しているか型の名前を使って記載する方法で、それを見れば再帰型であっても部分型関係（継承しているかどうか）は簡単に分かる。構造的型システムは、型の名前で判定するのではなく、型の構造で部分型関係にあるかどうか（関数の引数に渡せるかどうかなど）を判定する。以下、ここで述べるのは、構造的型システムでの再帰型の理論である。

型理論では、再帰型の一般形はμ型構築子を用いて μα.T で表される。ここで型変数 α は型そのものであると共に、型 T の中にも現われる可能性がある。部分型関係かどうかは S <: T と記載する。名前的型システムの Java ならば S extends T または S implements T （ただし親クラスを Object までたどる）であることを意味する。

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

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

構造的型システムでの再帰型には、同型再帰型（iso-recursive type）と同値再帰型（equi-recursive type）の2つの形式がある。同型再帰型の実装は簡単であるが、同値再帰型は議論と証明が複雑で、ほとんどのプログラミング言語は名前的型システムか構造的型システムの同型再帰型を使用している。

同型再帰型

同型再帰型では、再帰型 $\mu \alpha .T$ とその展開結果である $T[\mu \alpha .T/\alpha ]$ は別の型であり、特殊な項構成 fold と unfold で識別され、これらの間で同型写像を構成する。正確に記せば、 ${\mbox{fold}}:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T$ と ${\mbox{unfold}}:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]$ であり、これらは互いに逆関数である。

部分型付けにおいてよく使われる方法として Amber 規則があり、μX.S <: μY.T かどうかを判定するにあたり、X <: Y という仮定を置いた上で、S <: T であれば、μX.S <: μY.T とする、という判定方法である。Java は構造的型システムではないが、分かりやすくするために Java の表記方法を使うと、

で、ListA <: ListB であるかの判定をするにあたり、X は ListA の内側で再帰的に使っている ListA を指し、Y は ListB の内側で再帰的に使っている ListB を指すので、X <: Y であるという仮定を置いて、残りの value の部分が Integer <: Object なので、ListA <: ListB であると判定する方法である。再帰型同士しか比較しなく、再帰型を内部で利用している場合はそれを展開したりしないので、部分型付けの判定が有限時間で終わることが分かる。Amber 規則で出来ることは、概ね名前的型システムに近い。書籍『型システム入門』の「21.11 同型再帰型の部分型付け」で解説されている。

同値再帰型

同値再帰規則では、再帰型 $\mu \alpha .T$ とその展開結果の $T[\mu \alpha .T/\alpha ]$ は「等価」である。ここで等価とは、この2つの型表現が同じ型を表していると理解されることを示す。実際、同値再帰型の理論ではさらに、無限に展開したときに等価となる2つの型表現は等価であるとするのが一般的である。型を木構造で表現したときに、当然であるが、無限の大きさの木構造同士が部分型関係にあるかどうかを有限時間で判定することは不可能である。しかしながら、再帰型の表現方法を正則型に制限すると、部分型関係にあるかどうかを、有限時間で判定出来るアルゴリズムが存在する。そして、そのアルゴリズムの正しさの証明は、無限を厳密に扱うために、余帰納法を使用する。正則型がなんであるかや、判定アルゴリズムとその証明は、書籍『型システム入門』の「第21章再帰型のメタ理論」で解説されている。