再帰データ型

ウィキペディア

再帰データ型

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/17 16:09 UTC 版)

型システム
主要カテゴリ
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング
マイナーカテゴリ
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け
型理論のコンセプト
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型

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

例

再帰データ型

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

class Tree {
    Tree[] children;
}

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

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

再帰型エイリアス

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

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

type Tree = number | Tree[];
let tree: Tree = [1, [2, 3]];

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

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

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

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

理論

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

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

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

data Nat = Zero | Succ Nat

また、型理論では $nat=\mu \alpha .1+\alpha$カテゴリ