再帰データ型

再帰型とは

再帰型（recursive type）とは、型の定義の中でその型自身が出現するような、自己参照的な構造を持つ型のことです。直接的に自己参照するだけでなく、相互再帰によって間接的に参照する場合も含まれます。この概念は、特にデータ構造を定義する際に重要になり、再帰データ型（recursive data type）として知られています。

再帰データ型の例

多くのプログラミング言語では、名前付きクラスを用いて再帰型を表現できます。例えば、Javaでは以下のように`Tree`クラスの中で`Tree`自身を参照することで、木構造を表現できます。

java
class Tree {
Tree left;
Tree right;
Object value;
}


Haskellでは、リスト型を以下のように定義できます。これは、リスト`a`が空リストであるか、`a`型の要素を先頭に持つリストであることを示しています。

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

再帰型エイリアス

型エイリアス（型シノニム）で再帰が使用できるかは言語によって異なります。TypeScriptでは、型エイリアス内で再帰が可能です。以下の例では、型エイリアスだけで木構造の型を表現しています。

typescript
type Tree = T | { left: Tree; right: Tree };


一方、HaskellやOCamlなどでは、型シノニム宣言で再帰は許可されていません。以下のHaskellのコードは不正です。

haskell
type BadTree a = (a, BadTree a)


しかし、代数的データ型では同等の表現が可能であり、再帰的な定義が可能です。

haskell
data GoodTree a = Node a (GoodTree a) | Leaf a

型理論における再帰型

型システムは、大きく名前的型システムと構造的型システムに分けられます。名前的型システムは、Javaのように型に名前を付け、継承関係を明示的に記述する方法で、再帰型の場合でも部分型関係を容易に判断できます。一方、構造的型システムは、型の名前ではなく構造に基づいて部分型関係を判断します。

型理論では、再帰型はμ型構築子を用いて`μα.T`と表現されます。ここで、`α`は型変数であり、型`T`の中に現れる可能性があります。部分型関係は`S <: T`と記述されます。Javaの`S extends T`や`S implements T`のように、型`S`が`T`の部分型であることを意味します。

自然数を型理論で表現すると、以下のようになります。

`nat = μα. 1 + α`

ここで、`1`はゼロを表し、`α`は次の自然数を表します。つまり、`nat`は、ゼロであるか、別の`nat`の次の数であるという再帰的な定義になっています。

同型再帰型と等値再帰型

構造的型システムにおける再帰型には、同型再帰型（iso-recursive type）と同値再帰型（equi-recursive type）の2つの形式があります。

同型再帰型

同型再帰型では、再帰型`μα.T`とその展開結果`T[μα.T/α]`は別の型として扱われます。これらの型の間には、`fold`と`unfold`という特殊な操作で同型写像が構成されます。

`fold : T[μα.T/α] -> μα.T`
`unfold : μα.T -> T[μα.T/α]`

`fold`と`unfold`は互いに逆関数であり、同型性を保証します。

部分型付けでは、Amber規則がよく使われます。これは`μX.S <: μY.T`を判定する際に、`X <: Y`を仮定し、`S <: T`であれば`μX.S <: μY.T`と判断する手法です。これにより、再帰型同士の比較が効率的に行えます。

等値再帰型

等値再帰型では、再帰型`μα.T`とその展開結果`T[μα.T/α]`は等価であると見なされます。さらに、無限に展開した際に等価になる型表現も等価とされます。型を木構造で表現した場合、無限の大きさの木構造同士の部分型関係を有限時間で判定することは困難です。しかし、再帰型の表現を正則型に制限することで、有限時間で部分型関係を判定するアルゴリズムが存在します。

等値再帰型は、同型再帰型よりも複雑な型システムを提供し、型検査や型推論もより難しくなります。

まとめ

再帰型は、型システムにおいて重要な概念であり、特に再帰的なデータ構造を表現するのに役立ちます。同型再帰型と等値再帰型では、型の扱い方や部分型関係の判定方法が異なり、それぞれの特徴を理解することが重要です。プログラミング言語や型理論において、再帰型はより複雑なデータ構造やアルゴリズムを表現するための強力なツールとなっています。

参考文献

* 書籍『型システム入門』

もう一度検索