プリンシパルタイプ

型理論では、用語と環境が与えられた場合、この環境におけるこの用語の主型、つまりこの環境におけるこの用語の他のすべての型が主型のインスタンスとなるような型が存在する場合、型システムは主型プロパティを持つと言われます。

主型プロパティは、比較できない可能性のある複数の型を持つのではなく、式の可能性のあるすべての型を網羅する型を使用して、特定の環境で式を型付けする方法を提供するため、型システムにとって望ましいものです。主型プロパティを持つシステムの型推論では、通常、主型の推論が試行されます。

たとえば、MLシステムには主型プロパティがあり、式の主な型はRobinson の統一アルゴリズムによって計算できます。これは、 Hindley-Milner 型推論アルゴリズムで使用されます。ただし、ML の型システムに対する多くの拡張機能(多態的再帰など) により、主な型の推論が決定不能になる可能性があります。Haskellの一般化された代数的データ型などの他の拡張機能は、言語の主な型プロパティを破壊し、型注釈を使用するか、コンパイラが複数のオプションの中から目的の型を「推測」する必要があります。

主型付けプロパティは、用語が与えられた場合、その用語のすべての可能な型付けのインスタンスである型付け（つまり、コンテキストと型のペア）が存在することを要求します。主型付けプロパティは主型プロパティと混同される可能性がありますが、異なります。主型プロパティは、型を決定するために入力としてコンテキストに依存しますが、主型付けプロパティは結果としてコンテキストを出力します。^[1]