Type_constructor
分野では、数学、論理と計算機科学として知られている型理論、型コンストラクタは、型付きの特徴である形式言語古いものから新しいタイプを構築します。基本型は、nullary型コンストラクターを使用して構築されていると見なされます。一部の型コンストラクターは、引数として別の型を取ります。たとえば、製品型、関数型、電力型、リスト型のコンストラクターなどです。新しい型は、型コンストラクターを再帰的に作成することで定義できます。
たとえば、単純に型付きラムダ計算は、単一の型コンストラクター（関数型コンストラクター）を持つ言語と見なすことができます。製品タイプは、一般に、カリー化によって型付きラムダ計算に「組み込まれている」と見なすことができます。
抽象的、型コンストラクタは、N進型演算子を引数としてゼロまたはそれ以上の種類を取り、別の型を返します。カリー化を利用して、単項型演算子の一連のアプリケーションとしてn型演算子を（再）記述できます。したがって、型演算子は、単純に型付きされたラムダ計算と見なすことができます。ラムダ計算には、通常は1つの基本型しかありません。 ∗ {*}
、そして今と呼ばれている基本的な言語、のすべての種類の一種である、「タイプ」と発音、適切なタイプを呼ばれ、独自の計算、内型演算子の型と区別するために種類。
型演算子は型変数をバインドできます。たとえば、型レベルで単純型付きラムダ計算の構造を与えるには、バインディングまたは高次の型演算子が必要です。これらの結合型オペレータは、第2の軸に対応するλキューブなど、タイプ理論単に型付けλ計算型演算子、λとω。多型λ計算（とタイプの演算子を組み合わせるシステムFは）が得られるシステムのF ωを。
も参照してください
カインド（型理論）
代数的データ型
再帰データ型
参考文献
ピアス、ベンジャミン（2002）。タイプとプログラミング言語。MITプレス。ISBN 0-262-16209-1。、第29章「型演算子と種類」
PTジョンストン、象のスケッチ、p。940