代数的データ型

コンピュータプログラミング、特に関数型プログラミングや型理論において、代数的データ型（ADT）は複合データ型、つまり他の型を組み合わせることによって形成される型である。

代数的データ型は、和と積という2つの主要な構成要素によって定義されます。これらは「OR」型と「AND」型と呼ばれることもあります。

和型は、複数の選択肢の中から一つを選ぶものです。和型の値は、定義された複数のバリアントのいずれかに一致します。たとえば、信号機の状態を表す型はRed、、、AmberまたはのいずれかになりますGreen。形状型はCircle、（半径を格納する）または（幅を格納する）のいずれかになりますSquare。正式には、これらのバリアントはタグ付き共用体または非連結共用体と呼ばれます。各バリアントには、コンストラクタと呼ばれる名前があり、データも保持できます。列挙型は、コンストラクタがデータを保持しない、和型の単純な形式です。

積型は、複数の型を組み合わせたものです。積型の値は、その構成要素となる各型の値を含みます。例えば、ある型は、座標（整数）と座標（これも整数）Pointを含むように定義できます。積型の正式な例としては、タプルやレコードが挙げられます。積型の可能なすべての値の集合は、その構成要素となる各型の集合の直積です。xy

代数的データ型の値は、通常、パターンマッチングを使用して処理されます。この機能により、プログラマは値がどのコンストラクタで作成されたかを確認し、その値に含まれるデータを便利かつ型安全な方法で抽出できます。

代数的データ型は、1970年代にエジンバラ大学で開発された小さな関数型プログラミング言語であるHopeで導入されました。^{[ 1 ]}

代数的データ型は、複数の種類の値を表すために使用されます。それぞれの値には、コンストラクタと呼ばれる識別子が関連付けられており、これはその種類のデータに対するタグと考えることができます。各コンストラクタは、異なる種類のデータを保持することができます。

例えば、Tree上記のバイナリの例を考えると、コンストラクタはデータを持たない（例Empty：）、1つのデータを持つ（例：LeafInt 値が 1 つある）、または複数のデータを持つ（例： が1 つの値と 2 つの値をNode持つ）ことができます。IntTree

Treeこの代数的データ型の値に対して何らかの処理を行うには、パターンマッチングと呼ばれるプロセスを使用して値を分解します。これは、データを一連のパターンと照合する処理です。上記の例の関数は、引数を3つのパターンとパターンマッチングします。関数が呼び出されると、引数に一致する最初のパターンが見つかり、そのパターン内で見つかった変数バインディングが実行され、パターンに対応する式が評価されます。depth

上記の各パターンは、このデータ型の可能な値の構造に似た形式を持っています。最初のパターンは、コンストラクタの値に単純に一致しますEmpty。2 番目のパターンは、コンストラクタの値に一致しますLeaf。パターンは再帰的であるため、そのコンストラクタに関連付けられたデータは、パターン「n」に一致します。この場合、小文字の識別子は、任意の値に一致するパターンを表し、その名前の変数にバインドされます。この場合、変数「n」は、データ型に格納されている整数値にバインドされ、評価する式で使用されます。

この例におけるパターンの再帰は単純ですが、より複雑な再帰パターンとしては、次のようなものが考えられます。

Nodei(Nodej(Leaf4)x)(Nodeky(NodeEmptyz))

再帰的なパターンは、例えば赤黒木のバランス調整などに使用されます。赤黒木のバランス調整では、複数の階層にわたる色を調べる必要がある場合があります。

上記の例は、以下の擬似コードと操作的に同等です。

switch on ( data . constructor ) case Empty : return 0 case Leaf : let n = data . field1 return 1 case Node : let l = data . field2 let r = data . field3 return 1 + max ( depth l ) ( depth r )

代数的データ型の利点は、上記の擬似コードとパターンマッチングによる同等のコードを比較することで明確に示せる。

まず、型安全性があります。上記の擬似コード例では、プログラマーはアクセスしないように注意する必要があります。フィールド2コンストラクタが の場合、Leaf型システムは従来のレコードデータ構造に対して静的型を安全な方法で割り当てるのが困難になります。しかし、パターンマッチングでは、このような問題は発生しません。抽出された各値の型は、関連するコンストラクタによって宣言された型に基づいています。抽出できる値の数は、コンストラクタに基づいてわかります。

第二に、パターンマッチングにおいて、コンパイラは網羅性チェックを実行して、すべてのケースが処理されていることを確認します。上記の深度関数のケースのいずれかが欠落している場合、コンパイラは警告を発します。網羅性チェックは単純なパターンでは容易に思えるかもしれませんが、複雑な再帰パターンが多数存在すると、平均的な人間（あるいは、任意のネストされたif-else構造をチェックする必要があるコンパイラ）にとってはすぐに困難になります。同様に、決して一致しないパターン（つまり、既に以前のパターンでカバーされているパターン）が存在する可能性があります。コンパイラは、これらのパターンについてもチェックして警告を発することができます。これは、推論に誤りがあることを示している可能性があるためです。

代数的データ型のパターンマッチングは、正規表現による文字列パターンマッチングと混同してはいけません。両者の目的は似ていますが（特定の制約に一致するデータの一部を抽出する）、実装方法は大きく異なります。代数的データ型のパターンマッチングは、文字列の文字シーケンスではなく、オブジェクトの構造的特性に基づいてマッチングを行います。

一般的な代数的データ型は、積型の再帰的な和型です。各コンストラクタは、他の積型と区別するために積型にタグを付けます。コンストラクタが1つしかない場合は、そのデータ型は積型になります。さらに、コンストラクタのパラメータ型は、積型の因数です。パラメータのないコンストラクタは、空の積に対応します。データ型が再帰的である場合、積の和全体が再帰型でラップされ、各コンストラクタもデータ型を再帰型にロールします。

例えば、Haskellのデータ型は次のようになります。

データリストa = Nil | Cons a (リストa )

型理論では次のように 表される${\displaystyle \lambda \alpha .\mu \beta .1+\alpha \times \beta }$ コンストラクタ付き${\displaystyle \mathrm {nil} _{\alpha }=\mathrm {roll} \ (\mathrm {inl} \ \langle \rangle )}$そして${\displaystyle \mathrm {cons} _{\alpha }\ x\ l=\mathrm {roll} \ (\mathrm {inr} \ \langle x,l\rangle )}$。

Haskellのリストデータ型は、型理論において若干異なる形で表現することもできます。 ${\displaystyle \mu \phi .\lambda \alpha .1+\alpha \times \phi \ \alpha }$（${\displaystyle \mu }$そして${\displaystyle \lambda }$（元の構造とは逆になっています。）元の構造では、本体が再帰型である型関数が指定されていました。改訂版では、型に対する再帰関数が指定されています。（型変数${\displaystyle \phi }$は、基本型ではなく関数を提案するために使用されます。${\displaystyle \beta }$、 以来${\displaystyle \phi }$（ギリシャ文字のfに似ています。）この関数も適用する必要があります。${\displaystyle \phi }$その引数の型に${\displaystyle \alpha }$型の本体内。

リストの例においては、これら2つの表現に大きな違いはありませんが、2番目の形式では、いわゆるネストされたデータ型、つまり再帰型が元の型とパラメータ的に異なるデータ型を表現できます。（ネストされたデータ型の詳細については、 Richard Bird、Lambert Meertens 、Ross Patersonの著作を参照してください。）

集合論では、和型に相当するものは非交和であり、その要素はタグ（コンストラクタに相当）とタグに対応する型のオブジェクト（コンストラクタの引数に相当）のペアである集合である。^{[ 2 ]}

多くのプログラミング言語は、代数的データ型を第一級の概念として取り入れています。例えば、以下のような言語が挙げられます。

• 互いに素な和集合
• 一般化代数データ型
• 初等代数
• 商型
• タグ：組合
• 型理論
• 訪問者パターン