ヒンドレー・ミルナー型分類システム

単純型ラムダ計算では、型Tは原子型定数または次の形式の関数型のいずれかである。${\displaystyle T\rightarrow T}$このような型は単相型である。典型的な例としては、算術演算で使用される型が挙げられる。

${\displaystyle {\begin{array}{ll}3&:{\mathtt {Number}}\\{\mathtt {add}}\ 3\ 4&:{\mathtt {Number}}\\{\mathtt {add}}&:{\mathtt {Number}}\rightarrow {\mathtt {Number}}\rightarrow {\mathtt {Number}}\end{array}}}$

これとは対照的に、型付けのないラムダ計算は型付けに全く依存せず、その多くの関数はあらゆる型の引数に意味のある形で適用できる。自明な例としては恒等関数が挙げられる。

${\displaystyle {\mathtt {id}}\equiv \lambda xx}$

これは、適用された値をそのまま返します。より単純な例としては、リストなどのパラメトリック型があります。

一般的に多相性とは、演算が複数の型の値を受け入れることを意味しますが、ここで使用されている多相性はパラメトリックです。文献には、多相性のパラメトリックな性質を強調する型スキームの表記法も見られます。さらに、定数は（量化された）型変数で型付けできます。たとえば、次の型スキームは、普遍的にを量化します。${\displaystyle \alpha }$つまり、それらはすべての可能な場合に真である${\displaystyle \alpha }$:

${\displaystyle {\begin{array}{ll}{\mathtt {cons}}&:\forall \alpha .\alpha \rightarrow {\mathtt {List}}\ \alpha \rightarrow {\mathtt {List}}\ \alpha \\{\mathtt {nil}}&:\forall \alpha .{\mathtt {List}}\ \alpha \\{\mathtt {id}}&:\forall \alpha .\alpha \rightarrow \alpha \end{array}}}$

多相型は、変数の一貫した置換によって単相型になることができます。単相型のインスタンスの例は次のとおりです。

${\displaystyle {\begin{array}{ll}{\mathtt {id}}'&:{\mathtt {String}}\rightarrow {\mathtt {String}}\\{\mathtt {nil}}'&:{\mathtt {List}}\ {\mathtt {Number}}\end{array}}}$

より一般的に言えば、型変数を含む型は多相型であり、型変数を含まない型は単相型である。

例えばPascal（1970年）やC（1972年）で使用されている型システムは単相型のみをサポートしていますが、HMはパラメトリック多相性を重視して設計されています。これらの言語の後継であるC++ （1985年）は、オブジェクト指向プログラミングに関連したサブタイピングやオーバーロードなど、異なるタイプの多相性に焦点を当てています。サブタイピングはHMとは互換性がありませんが、HaskellのHMベースの型システムでは、体系的なオーバーロードのバリアントが利用可能です。

単純型ラムダ計算の型推論を多相性へと拡張する場合、多相性型を式の型としてだけでなく、λに束縛された変数の型としても割り当てることが許容されるかどうかを決定する必要がある。これにより、以下の式において、汎用的な同一性型を変数「id」に割り当てることが可能になる。

(λ id . ... (id 3) ... (id "text") ... ) (λ x . x)

これを許容すると多相ラムダ計算が実現するが、このシステムにおける型推論は決定不可能である。^{[ 5 ]}代わりに、HMは式に直接束縛される変数とより一般的なλ束縛変数を区別し、前者をlet束縛変数と呼び、多相型をこれらの変数にのみ割り当てることを可能にする。これによりlet多相が実現し、上記の例は次の形式をとる。

let id = λ x . x in ... (id 3) ... (id "text") ...

これは、'id' に多相型を付けることができます。示されているように、式構文は、let で束縛された変数を明示的にするために拡張され、型システムを制限して、let で束縛された変数のみが多相型を持つことを許可し、ラムダ抽象のパラメータは単相型を取得しなければならないようにすることで、型推論が決定可能になります。

入力する式は、隣接する表に示すように、let式で拡張されたラムダ計算の式と全く同じです。括弧を使用して式を区別することができます。このアプリケーションは左拘束であり、抽象化やlet-in構文よりも強い拘束力を持ちます。

型は構文的にモノタイプとポリタイプの2つのグループに分けられます。^{[注2 ]}

多相性とは、同一の式が（おそらく無限に）多くの型を持つことができることを意味します。しかし、この型システムでは、これらの型は完全に無関係ではなく、パラメトリック多相性によって調整されています。

例えば、恒等式${\displaystyle \lambda x.x}$持つことができる${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$その種類と同様に ${\displaystyle {\texttt {string}}\rightarrow {\texttt {string}}}$または${\displaystyle {\texttt {int}}\rightarrow {\texttt {int}}}$その他多数だが、${\displaystyle {\texttt {int}}\rightarrow {\texttt {string}}}$この関数の最も一般的な型は ${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$一方、他のものはより具体的であり、型パラメータ、つまり量化変数を別の型に一貫して置き換えることによって、一般的なものから導き出すことができる。${\displaystyle \alpha }$反例は、置換が一貫性を欠いているため、成り立たない。

一貫した置換は、置換を適用することによって正式なものにすることができる。${\displaystyle S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}}$タイプの用語に${\displaystyle \tau }$書かれた${\displaystyle S\tau }$例が示唆するように、置換は、型が多かれ少なかれ特別であることを示す順序と密接に関連しているだけでなく、置換の適用を可能にする全量化とも密接に関連しています。

正式には、HM では、タイプ${\displaystyle \sigma '}$より一般的${\displaystyle \sigma }$正式には${\displaystyle \sigma '\sqsubseteq \sigma }$定量化された変数が${\displaystyle \sigma '}$一貫して置き換えられ、${\displaystyle \sigma }$サイドバーに示されているとおりです。この順序は、型システムの型定義の一部です。

前の例では、置換を適用すると${\displaystyle S=\left\{\alpha \mapsto {\texttt {string}}\right\}}$結果として${\displaystyle \forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}}$。

量化変数を単相型（基底型）に置き換えるのは簡単ですが、多相型に置き換える場合は、自由変数の存在によっていくつかの落とし穴があります。特に、非束縛変数は置き換えてはなりません。ここでは定数として扱われます。さらに、量化はトップレベルでのみ可能です。パラメトリック型に置き換える場合は、その量化子をリフトする必要があります。右側の表は、この規則を明確に示しています。

あるいは、量化子を持たない多型に対して、量化変数を別の記号セットで表す同等の表記法を考えてみましょう。このような表記法では、特殊化は、量化変数を単純に一貫性のある形で置き換えることに帰着します。

関係${\displaystyle \sqsubseteq }$は半順序 で あり、${\displaystyle \forall \alpha .\alpha }$それはその最小要素である。

HMの構文は、型付けを判断として用いることで、形式体系の本体を構成する推論規則の構文へと引き継がれる。各規則は、どのような前提からどのような結論が導き出せるかを定義する。判断に加えて、上述の追加条件も前提として用いられる場合がある。

規則を用いた証明は、すべての前提が結論の前に列挙されるような一連の判断です。以下の例は、証明の可能な形式を示しています。左から右へ、各行は結論、${\displaystyle [{\mathtt {Name}}]}$適用された規則と前提について、前提が判断である場合は前の行（番号）を参照するか、述語を明示することによって示します。

すぐには見えないが、ルールセットは、ルール内で単一型と多型をわずかに異なる方法で使用することにより、どのような状況下で型が一般化されるかされないかを規定する規則をエンコードしている。${\displaystyle [{\mathtt {Abs}}]}$そして${\displaystyle [{\mathtt {Let}}]}$覚えておいてください${\displaystyle \sigma }$そして${\displaystyle \tau }$それぞれ多型と単型を表す。

ルールでは${\displaystyle [{\mathtt {Abs}}]}$関数のパラメータの値変数${\displaystyle \lambda x.e}$前提を通して単相型でコンテキストに追加されます${\displaystyle \Gamma ,\ x:\tau \vdash _{D}e:\tau '}$規則では ${\displaystyle [{\mathtt {Let}}]}$変数は多形形式で環境に入る${\displaystyle \Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau }$どちらの場合も、${\displaystyle x}$この文脈では、割り当て内の自由変数に対する一般化ルールの使用が禁止され、この規則はパラメータの型を強制します。${\displaystyle x}$で${\displaystyle \lambda }$-式は単相のままですが、let式では変数を多相的に導入することができ、特殊化が可能になります。

この規制の結果、${\displaystyle \lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})}$パラメータが${\displaystyle f}$は単型位置にあり、${\displaystyle {\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})}$型を持つ${\displaystyle (bool,int)}$、 なぜなら${\displaystyle f}$let式に導入されているため、多相として扱われます。

一般化規則も詳しく見てみる価値がある。ここでは、前提に暗黙的に含まれる全量化が${\displaystyle \Gamma \vdash _{D}e:\sigma }$単に右側に移動されます${\displaystyle \vdash _{D}}$結論では、明示的な全称量化子によって束縛される。これは可能である。${\displaystyle \alpha }$文脈上、自由形式は存在しない。繰り返しになるが、これは一般化規則をもっともらしく見せるものの、実際には結果ではない。それどころか、一般化規則はHMの型システムの定義の一部であり、暗黙の全量化はその結果である。

証明の中で、決定が全く不可能な点を分離すると、構文を中心とした最初の規則群は選択肢を残しません。なぜなら、各構文規則には一意の型付け規則が対応し、それが証明の一部を決定するからです。一方、これらの固定部分の結論と前提の間には、${\displaystyle [{\mathtt {Inst}}]}$そして${\displaystyle [{\mathtt {Gen}}]}$ 起こり得る。このような連鎖は、証明の結論と最上位式の規則の間にも存在し得る。すべての証明は、このように概略的に示された形状を持たなければならない。

証明におけるルール選択の唯一の選択肢は ${\displaystyle [{\mathtt {Inst}}]}$そして${\displaystyle [{\mathtt {Gen}}]}$連鎖的な証明形式は、このような連鎖が不要になるような、より精密な証明が可能かどうかという疑問を提起する。実際、これは可能であり、そのような規則を持たない規則体系の変種につながる。

現代における人文管理の扱いでは、クレメント^{[ 6 ]}による純粋に構文指向のルールシステムを 中間段階として用いる。このシステムでは、特殊化は元のルールの直後に配置される。${\displaystyle [{\mathtt {Var}}]}$ルールに統合され、一般化は${\displaystyle [{\mathtt {Let}}]}$ルール。そこでは、関数を導入することで、常に最も一般的な型を生成するように一般化も決定されます。${\displaystyle {\bar {\Gamma }}(\tau )}$これは、バインドされていないすべてのモノタイプ変数を定量化します。${\displaystyle \Gamma }$。

正式には、この新しいルールシステムが${\displaystyle \vdash _{S}}$オリジナルと同等${\displaystyle \vdash _{D}}$示さなければならないのは${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma }$これは、2つの部分証明に分解される。

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma }$（一貫性）
• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma }$（完全性）

規則を分解することで一貫性が確認できる${\displaystyle [{\mathtt {Let}}]}$そして${\displaystyle [{\mathtt {Var}}]}$ の${\displaystyle \vdash _{S}}$証明に${\displaystyle \vdash _{D}}$おそらく、${\displaystyle \vdash _{S}}$不完全である、示すことができない${\displaystyle \lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha }$で${\displaystyle \vdash _{S}}$例えば、 ${\displaystyle \lambda \ x.x:\alpha \rightarrow \alpha }$完全性のわずかに弱いバージョンは証明可能である ^{[ 7 ]} 。すなわち、

• ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma }$

つまり、式の主要な型を導出できる。${\displaystyle \vdash _{S}}$最終的に証明を一般化することができる。

比較する${\displaystyle \vdash _{D}}$そして${\displaystyle \vdash _{S}}$今では、すべての規則の判断において、単一型のみが現れます。さらに、演繹システムを用いたあらゆる可能な証明の形状は、式の形状と同一になります（どちらも木として見た場合）。したがって、式は証明の形状を完全に決定します。${\displaystyle \vdash _{D}}$形状は、以下のすべての規則に関して決定される可能性が高い${\displaystyle [{\mathtt {Inst}}]}$そして${\displaystyle [{\mathtt {Gen}}]}$これにより、他のノード間に任意の長さのブランチ（チェーン）を構築することが可能になります。

証明の構造がわかったので、型推論アルゴリズムの定式化にかなり近づいたと言える。与えられた式に対する証明はすべて同じ構造を持つはずなので、証明の判断における単一型は未決定であると仮定し、それらをどのように決定するかを検討することができる。

ここで、置換（特殊化）順序が重要になります。一見すると、局所的に型を決定することはできませんが、証明ツリーをたどる際に順序を利用して型を洗練できると期待されています。さらに、結果として得られるアルゴリズムは推論方法となるため、どの前提においても型は可能な限り最良のものとして決定されると仮定します。そして実際、規則を見ると、${\displaystyle \vdash _{S}}$提案する:

• [ Abs ]：重要な選択はτです。現時点ではτについては何もわかっていないので、最も一般的なタイプを仮定するしかありません。${\displaystyle \forall \alpha .\alpha }$必要に応じて型を特殊化する計画です。この場所ではポリタイプは許可されていないため、当面はαで対応する必要があります。意図しないキャプチャを避けるため、証明にまだ含まれていない型変数を使用するのが安全な選択です。さらに、このモノタイプはまだ確定しておらず、今後さらに改良される可能性があることに留意する必要があります。
• [ Var ] : 選択肢はσをどのように改良するかです。ここで型τを選択するかどうかは変数の使用法に依存しますが、その使用法は局所的に不明であるため、最も安全なのは最も一般的な型を選択することです。上記と同じ方法を使用すると、 σ内のすべての量化変数を新しい単一型変数で、さらに改良できるようにしておくことができます。
• [ ] : このルールでは選択肢は残されていません。完了。
• [アプリ] : アプリケーションルールのみが、両方の前提条件で要求されるように、これまでに「開かれた」変数の改良を強制する可能性があります。
  1. 最初の前提により、推論の結果は次の形式になる。${\displaystyle \tau \rightarrow \tau '}$。
     • そうであれば、それで構いません。結果を得るために、後でそのτ 'を選択すればよいのです。
     • そうでない場合は、未定義変数である可能性があります。その場合、以前と同様に2つの新しい変数を用いて、必要な形式に修正することができます。
     • そうでなければ、最初の前提が推論した型が関数型ではなく、関数型にすることもできないため、型チェックは失敗します。
  2. 2番目の前提では、推論された型が最初の前提のτと等しいことが求められます。ここで、おそらくオープン型変数を持つ2つの異なる型が手元にあり、比較して可能であれば等しくする必要があります。等しくできれば改良が見つかり、そうでなければ型エラーが再び検出されます。置換によって「2つの項を等しくする」効果的な方法として、ロビンソンのユニフィケーションと、いわゆるUnion-Findアルゴリズムの組み合わせが知られています。

ユニオンファインドアルゴリズムを簡単にまとめると、証明に含まれるすべての型の集合が与えられた場合、ユニオン手続きによってそれらを同値類にグループ化し、ファインド手続き によって各同値類の代表を選択することができます。ここで「手続き」という言葉を副作用という意味で強調すると、効果的なアルゴリズムを準備するために、明らかに論理の領域から離れていることがわかります。${\displaystyle {\mathtt {union}}(a,b)}$aとbの両方が型変数である場合、代表はどちらか一方になりますが、変数と項を結合する際には、項が代表になります。union-findの実装を前提とすると、2つのモノタイプの結合は次のように定式化できます。

unify(ta, tb): ta = find(ta) tb = find(tb) ta、tb の両方が D p1..pn の形式で、D、n が同一である場合、対応するi番目のパラメータ ごと に unify(ta[i]、tb[i]) を実行する。そうでない場合、 ta、tb の少なくとも 1 つが型変数である場合、 union(ta, tb) それ以外の場合は 「型が一致しません」というエラーが表示されます。

推論アルゴリズムの概略がわかったので、次のセクションでより正式な説明を行います。これは、Milner ^{[ 2 ]}の 370 ページ以降でアルゴリズム J として説明されています。

アルゴリズム J の提示は、副作用を含みながらも直接比較を可能にするため、論理規則の表記法の誤用である。${\displaystyle \vdash _{S}}$同時に効率的な実装を表現している。ルールでは、パラメータを持つ手順が指定される。${\displaystyle \Gamma ,e}$降伏${\displaystyle \tau }$結論では、前提の実行は左から右へと進む。

手順${\displaystyle inst(\sigma )}$多型を特殊化する${\displaystyle \sigma }$用語をコピーし、バインドされた型変数を新しいモノタイプ変数に一貫して置き換えることによって。${\displaystyle newvar}$' は新しいモノタイプ変数を生成します。おそらく、${\displaystyle {\bar {\Gamma }}(\tau )}$不要なキャプチャを避けるために、量化のための新しい変数を導入する型をコピーする必要があります。全体として、アルゴリズムは常に最も一般的な選択を行い、特殊化は単一化に任せることで進行し、単一化自体が最も一般的な結果を生成します。上記のように、最終結果は${\displaystyle \tau }$一般化する必要がある${\displaystyle {\bar {\Gamma }}(\tau )}$最終的には、与えられた式に対して最も一般的な型を得るため。

アルゴリズムで使用される手順のコストがほぼ O(1) であるため、アルゴリズム全体のコストは、型推論の対象となる式のサイズに対してほぼ線形になります。これは、終了性に関して決定不能ではないにしても、NP 困難となることが多かった他の多くの型推論アルゴリズムの導出の試みとは大きく異なります。したがって、 HM は、最も優れた完全情報型チェックアルゴリズムと同等の性能を発揮します。ここでの型チェックとは、アルゴリズムが証明を見つける必要はなく、与えられた証明を検証するだけでよいことを意味します。

コンテキスト内の型変数の束縛を維持して計算を可能にする必要があるため、効率はわずかに低下します。${\displaystyle {\bar {\Gamma }}(\tau )}$また、再帰型の構築中に発生チェックを有効にして、${\displaystyle {\mathit {unify}}(\alpha ,\tau )}$その一例は${\displaystyle \lambda \ x.(x\ x)}$型は HM を使用して導出することはできません。実際には、型は小さな項にすぎず、拡張構造を構築しません。したがって、複雑性分析では、型の比較を定数として扱い、O(1) のコストを維持できます。

そこから、アルゴリズム J の証明によりアルゴリズム W が得られ、これは手順によって課される副作用のみを生じさせる。${\displaystyle {\textit {union}}}$置換によってその直列構成を表現することで明示的になる ${\displaystyle S_{i}}$サイドバーのアルゴリズム W の提示では、斜体で示された操作セットに副作用がまだ使用されていますが、これらは新しいシンボルを生成することに限定されています。判断の形式は${\displaystyle \Gamma \vdash e:\tau ,S}$、これは、コンテキストと式をパラメータとして持つ関数を表し、置換とともに単一型を生成します。${\displaystyle {\textsf {mgu}}}$副作用のないバージョンです${\displaystyle {\textit {union}}}$最も一般的な統一子である置換を生成する。

アルゴリズムWは通常HMアルゴリズムと考えられており、文献ではルールシステムの直後に提示されることが多いが、その目的はミルナー^{[ 2 ]}によって369ページで次のように説明されている。

現状では、Wは効率的なアルゴリズムとは言い難い。置換処理が頻繁に行われているためだ。これは健全性の証明を補助するために考案されたアルゴリズムである。そこで、Wを厳密にシミュレートする、より単純なアルゴリズムJを提示する。

彼はWの方が複雑で効率が悪いと考えていたが、Jよりも先に自身の論文でWを紹介した。副作用が利用できない場合や望ましくない場合には、Wには利点がある。また、Wは完全性を証明するためにも必要であり、彼はそれを健全性証明に組み込んでいる。

証明義務を定式化する前に、規則体系DとSと提示されたアルゴリズムとの間の相違点を強調する必要がある。

上記の開発では、モノタイプを「オープン」な証明変数として誤用した側面があったものの、本来のモノタイプ変数が損なわれる可能性は、新たな変数を導入して最善を尽くすことで回避された。しかし、落とし穴がある。これらの新たな変数は「そのように認識される」という約束があったにもかかわらず、このアルゴリズムはその約束を果たしていないのだ。

文脈を持つ${\displaystyle 1:int,\ f:\alpha }$表現${\displaystyle f\ 1}$ どちらも入力できません${\displaystyle \vdash _{D}}$または${\displaystyle \vdash _{S}}$しかし、アルゴリズムは次のようなタイプを生成します${\displaystyle \beta }$ここで、Wはさらに置換を提供する${\displaystyle \left\{\alpha \mapsto int\rightarrow \beta \right\}}$つまり、このアルゴリズムはすべての型エラーを検出できないということです。この欠点は、証明変数と単一型変数をより注意深く区別することで簡単に修正できます。

著者らはこの問題を十分に認識していたが、修正しないことに決めた。これには実用的な理由があったと考えられる。型推論をより適切に実装すれば、アルゴリズムは抽象モノタイプを扱えるようになるが、既存のコンテキスト内のどの項目にも自由変数がないという想定されるアプリケーションでは、それらは必要なかった。この観点から、不要な複雑さを排除し、より単純なアルゴリズムを採用した。残る欠点は、ルールシステムに関するアルゴリズムの証明が汎用性に欠け、特定のコンテキストに対してのみ証明できるということである。${\displaystyle free(\Gamma )=\emptyset }$付随条件として。

${\displaystyle {\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}}$

完全性義務における付随条件は、推論によって複数の型が生成される可能性がある一方で、アルゴリズムは常に単一の型を生成するという点に対処するものである。同時に、この付随条件は、推論された型が実際に最も一般的な型であることを要求している。

義務を適切に証明するには、まず義務を強化して置換補題を活性化し、置換をスレッド化する必要がある。${\displaystyle S}$を通して${\displaystyle \vdash _{S}}$そして${\displaystyle \vdash _{W}}$そこからは、式に関する帰納法によって証明を行う。

もう一つの証明義務は、置換補題そのもの、すなわち型付けの置換であり、これによって最終的に全量化が確立される。後者は、そのような構文が存在しないため、形式的に証明することはできない。

プログラミングを実用的にするためには、再帰関数が必要です。ラムダ計算の重要な特性は、再帰定義が直接利用できないものの、不動点コンビネータで表現できる点です。しかし、不動点コンビネータは、後述するようにシステムに深刻な影響を与えることなく、型付きラムダ計算で定式化することはできません。

オーバーロードとは、同じ名前で異なる関数を定義して使用できることを意味します。ほとんどのプログラミング言語では、少なくとも組み込みの算術演算（+、<など）のオーバーロードが提供されており、プログラマーは、異なる数値型（例えば、または）であっても、同じ形式で算術式を記述できますint。real同じ式内でこれらの異なる型が混在すると暗黙的な型変換も必要となるため、特にこれらの演算のオーバーロードは、多くの場合、プログラミング言語自体に組み込まれています。一部の言語では、この機能が一般化され、ユーザーが利用できるようになっています（例：C++）。

関数型プログラミングでは、型チェックと型推論の両方における計算コストのため、アドホックなオーバーロードは避けられてきましたが、オーバーロードを体系化する手段として、形式と命名規則の両面でオブジェクト指向プログラミングに似たものが導入されました。ただし、これは1つ上のレベルで機能します。この体系における「インスタンス」はオブジェクト（つまり値レベル）ではなく、型です。序論で述べたクイックソートの例では、順序にオーバーロードが使用されており、Haskellでは次の型注釈が付けられています。

quickSort :: Ord a => [ a ] -> [ a ]

ここで、型はa多相的であるだけでなく、Ord順序述語を提供し<、>=関数本体で使用される何らかの型クラスのインスタンスであるように制限されています。これらの述語の適切な実装は、オーバーロードされた関数 quickSort の単一の実装を提供するより具体的な型に対してクイックソートが使用されるとすぐに、追加のパラメータとしてクイックソートに渡されます。

「クラス」は引数として単一の型しか受け付けないため、結果として得られる型システムは推論機能を提供できます。さらに、型クラスには何らかのオーバーロード順序を持たせることができ、クラスを格子状に配置することが可能です。

パラメトリック多相性とは、型自体が適切な値であるかのようにパラメータとして渡されることを意味します。適切な関数への引数として渡されるだけでなく、「パラメトリック」型定数のように「型関数」にも渡されるため、型自体をより適切に型付けする方法が問われます。高階型は、さらに表現力豊かな型システムを作成するために使用されます。

メタ型が存在する場合、単一化はもはや決定不可能となり、この程度の一般性では型推論は不可能となる。さらに、自身を型として含むすべての型の型を仮定すると、すべての集合の集合の場合と同様にパラドックスに陥るため、抽象化のレベルを段階的に上げていく必要がある。一段階上の二階ラムダ計算の研究により、この一般性では型推論が決定不可能であることが示された。

Haskell では、 kindという上位レベルが導入されています。標準 Haskell では、kind は推論され、型コンストラクタの引数の数を記述する以外にはほとんど使用されません。たとえば、リスト型コンストラクタは、型 (その要素の型) を別の型 (その要素を含むリストの型) にマッピングするものと考えられています。表記上は、次のように表されます。${\displaystyle *\to *}$依存型システムの機能を模倣するために型を拡張する言語拡張機能が利用可能です。^{[ 8 ]}

サブタイピングと型推論を組み合わせようとする試みは、かなりのフラストレーションを引き起こしてきました。サブタイピング制約（型等価制約とは対照的に）を蓄積して伝播させることは容易であり、結果として得られる制約を推論された型スキームの一部にすることができます。たとえば、${\displaystyle \forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha }$、 どこ${\displaystyle \alpha \leq T}$型変数に対する制約です${\displaystyle \alpha }$しかし、このアプローチでは型変数が積極的に統一されないため、多くの役に立たない型変数と制約を含む、大きくて扱いにくい型付けスキームが生成され、読みにくく理解しにくくなる傾向がある。そのため、非決定性有限オートマトン(NFA) の簡略化 (推論された再帰型が存在する場合に有用) と同様の手法を使用して、このような型付けスキームとその制約を簡略化するためにかなりの努力が払われた。^{[ 9 ]} 最近では、Dolan と Mycroft ^{[ 10 ]} が型付けスキームの簡略化と NFA の簡略化の関係を形式化し、サブタイピングの形式化に対する代数的アプローチにより、ML ライクな言語 (MLsub と呼ばれる) のコンパクトな主型付けスキームを生成できることを示した。注目すべきは、彼らが提案した型付けスキームでは、明示的な制約の代わりに、制限された形式のユニオン型とインターセクション型が使用されたことである。パローは後に^{[ 11 ]} 、この代数的な定式化はアルゴリズムWに似た比較的単純なアルゴリズムと同等であり、和集合型と積集合型の使用は必須ではないと主張した。

一方、オブジェクト指向プログラミング言語のコンテキストでは、型推論はより困難であることがわかっています。これは、オブジェクトのメソッドがSystem F（型推論が決定不能）スタイルの第一級多相性を必要とする傾向があること、およびF境界多相性などの機能があるためです。したがって、 Cardelliのシステムのように、サブタイピングによってオブジェクト指向プログラミングを可能にする型システム${\displaystyle F_{<:}}$[ ^{12 ]は}HMスタイルの型推論をサポートしていません。

行多相性は、構造レコードなどの言語機能をサポートするためにサブタイピングの代替として使用できます。^{[ 13 ]} このスタイルの多相性は、型制約の方向性の欠如に対処するために厳密に必要な以上の多相性を必要とするなど、いくつかの点でサブタイピングよりも柔軟性に劣りますが、標準的な HM アルゴリズムと非常に簡単に統合できるという利点があります。