型コンストラクタ

型理論として知られる数理論理学とコンピュータサイエンスの分野において、型コンストラクタは、古い型から新しい型を構築する型付き形式言語の機能です。基本型は、nullary型コンストラクタを使用して構築されると考えられています。一部の型コンストラクタは、別の型を引数として受け取ります。たとえば、積型、関数型、累乗型、リスト型のコンストラクタなどです。新しい型は、型コンストラクタを再帰的に合成することで定義できます。

たとえば、単純に型付けされたラムダ計算は、関数型コンストラクタという単一の非基本型コンストラクタを持つ言語と見なすことができます。積型は一般に、カリー化によって型付けされたラムダ計算に「組み込まれている」と考えることができます。

抽象的には、型コンストラクタは、引数として 0 個以上の型を受け取り、別の型を返すn項型演算子です。カリー化を利用すると、 n項型演算子は、単項型演算子の適用のシーケンスとして (再) 記述できます。したがって、型演算子は、通常 と表記され、「型」と発音される 1 つの基本型のみを持つ、単純に型付けされたラムダ計算として考えることができます。これは、基礎となる言語のすべての型の型であり、現在は、独自の計算における型演算子の型 (種類と呼ばれます) と区別するために、適切な型と呼ばれています。 ${\displaystyle *}$

型演算子は型変数をバインドできます。たとえば、単純型 λ 計算の構造を型レベルで与えるには、バインド型演算子、つまり高階型演算子が必要です。これらのバインド型演算子は、 λ キューブの 2 番目の軸と、型演算子 λ _ωを含む単純型 λ 計算などの型理論に対応します。型演算子を多態的 λ 計算 ( System F )と組み合わせると、 System F _{ω が}生成されます。

一部の関数型プログラミング言語では、型コンストラクタを明示的に使用します。注目すべき例としてはHaskellがあり、Haskellではすべてのdata型宣言が型コンストラクタを宣言するものとみなされ、基本型（またはnull引数の型コンストラクタ）は型定数と呼ばれます。^{[1] [2]型コンストラクタは}、パラメトリック多態データ型とみなすこともできます。

• 種類（型理論）
• 代数データ型
• 再帰データ型