代数的データ型
集合論において代数的データ型と等価なものとして直和がある。この集合の各元はタグ(コンストラクタと等価)とそのタグに対応する型のオブジェクト(コンストラクタの引数と等価)で構成される。
一般に代数的データ型は直積型の総和であり、再帰的に定義されることもある。各コンストラクタは直積型のタグとなって他と区別されるか、1つしかコンストラクタがない場合は、そのデータ型自体が直積型となる。さらにコンストラクタの引数の型が直積型の要素となる。引数のないコンストラクタは空に対応する。データ型が再帰的であるなら、その直積型の総和は再帰データ型となり、各コンストラクタによって再帰データ型が構成される。
例えば、以下のような Haskell のデータ型
を型理論的に表すと次のようになる。
λ α . μ β .1 + α × β {\displaystyle \lambda \alpha .\mu \beta .1+\alpha \times \beta }
コンストラクタは次のようになる。
n i l α = r o l l ( i n l ⟨ ⟩ ) {\displaystyle \mathrm {nil} _{\alpha }=\mathrm {roll} \ (\mathrm {inl} \ \langle \rangle )} c o n s α x l = r o l l ( i n r ⟨ x , l ⟩ ) {\displaystyle \mathrm {cons} _{\alpha }\ x\ l=\mathrm {roll} \ (\mathrm {inr} \ \langle x,l\rangle )}