Hindley–Milner型システム

Hindley –Milner ( HM )型システムは、パラメトリック多態性を持つラムダ計算のための古典的な型システムです。Damas –Milner型、またはDamas–Hindley–Milner型とも呼ばれます。J . Roger Hindley ^{[ 1 ]}によって最初に記述され、後にRobin Milner ^{[ 2 ]}によって再発見されました。Luis Damasは、博士論文においてこの手法の詳細な形式的分析と証明を行いました。^{[ 3 ] [ 4 ]}

HMの注目すべき特性としては、その完全性と、プログラマが提供する型注釈やその他のヒントなしに、与えられたプログラムの最も一般的な型を推論する能力が挙げられる。アルゴリズムWは、理論的には複雑度が高いものの、実践上は効率的な型推論手法であり、大規模なコードベースにも適用されてきている。^{[注1 ]} HMは関数型プログラミング言語で好適に用いられる。これは、プログラミング言語MLの型システムの一部として初めて実装された。それ以来、HMは様々な方法で拡張されてきたが、最も顕著な例としては、Haskellのような型クラス制約が挙げられる。

導入

型推論手法であるHindley-Milnerは、完全に型付けされていない形式で書かれたプログラムから、変数、式、関数の型を推論することができます。スコープ依存であるため、ソースコードのごく一部からだけでなく、プログラム全体やモジュール全体から型を推論できます。パラメトリック型にも対応できるため、多くの関数型プログラミング言語の型システムの中核を成しています。この方法で初めて適用されたのは、MLプログラミング言語です。

起源は、 1958年にハスケル・カリーとロバート・フェイズによって考案された単純型ラムダ計算のための型推論アルゴリズムである。 1969年、J・ロジャー・ヒンドリーはこの研究を拡張し、彼らのアルゴリズムが常に最も一般的な型を推論することを証明した。1978年、ロビン・ミルナー^{[ 2 ]}はヒンドリーの研究とは独立して、同等のアルゴリズムであるアルゴリズムWを提供した。1982年、ルイス・ダマス^{[ 4 ]}はついにミルナーのアルゴリズムが完全であることを証明し、それを多態的参照を持つシステムをサポートするように拡張した。

モノモーフィズムとポリモーフィズム

単純型ラムダ計算において、型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と互換性がありませんが、HMベースのHaskell型システムでは、体系的なオーバーロードの一種が利用可能です。

Let多態性

単純型ラムダ計算の型推論を多態性へと拡張する場合、多態型を式の型としてだけでなく、λ束縛変数の型としても代入できるかどうかを判断する必要があります。これにより、以下の式において、ジェネリックな同一性型を変数 'id' に代入することが可能になります。

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

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

id = λ x . x in ... (id 3) ... (id "text") ... とします。

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

概要

この記事の残りの部分は次のように進みます。

• HM型システムが定義されています。これは、どの式がどの型を持つか（もしあれば）を明確にする演繹システムを記述することによって行われます。
• そこから、型推論法の実装へと進みます。上記の演繹システムの構文駆動型バリアントを導入した後、読者のメタ論理的直感に訴えかける効率的な実装（アルゴリズムJ）を概説します。
• アルゴリズム J が実際に初期演繹システムを実現しているかどうかは不明であるため、効率の低い実装 (アルゴリズム W) が導入され、証明での使用が示唆されています。
• 最後に、アルゴリズムに関連するさらなるトピックについて説明します。

HM メソッドが提示されるさまざまな形式を直接比較できるように、2 つのアルゴリズムの場合でも、全体で同じ演繹システムの説明が使用されています。

Hindley-Milner型システム

型システムは、式や型などを扱う言語を規定する構文規則によって形式的に記述できます。ここでの構文の表現は、表層文法ではなく深層文法を研究するために記述されているため、形式的すぎず、構文の詳細の一部は未公開のままです。このような表現形式は一般的です。これに基づいて、型付け規則を用いて式と型の関係を定義します。前述のように、ここでも多少自由な形式が用いられています。

構文

表現

${\displaystyle {\begin{array}{lrll}\\e&=&x&{\textrm {変数}}\\&\vert &e_{1}\ e_{2}&{\textrm {適用}}\\&\vert &\lambda \ x\ .\ e&{\textrm {抽象化}}\\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\\\end{array}}}$

種類

${\displaystyle {\begin{array}{llrll}\\{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {variable}}\\&&\vert &C\ \tau \dots \tau &\ {\textrm {application}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {quantifier}}\\\\\end{array}}}$

コンテキストとタイピング

${\displaystyle {\begin{array}{llrl}\\{\text{Context}}&\Gamma &=&\epsilon \ {\mathtt {(empty)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typing}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}}$

自由型変数

${\displaystyle {\begin{array}{ll}\\{\text{free}}(\ \alpha \ )&=\ \left\{\alpha \right\}\\{\text{free}}(\ C\ \tau _{1}\dots \tau _{n}\ )&=\ \bigcup \limits _{i=1}^{n}{{\text{free}}(\ \tau _{i}\ )}\\{\text{free}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{free}}(\ \sigma \ )\\\\{\text{free}}(\ \forall \ \alpha \ .\ \sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ \left\{\alpha \right\}\\{\text{free}}(\ \Gamma \vdash e:\sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ {\text{free}}(\ \Gamma \ )\\\\\end{array}}}$

型付けされる式は、隣の表に示すように、let式で拡張されたラムダ計算の式と全く同じです。括弧は式の曖昧性を解消するために使用できます。適用は左束縛であり、抽象化やlet-in構造よりも強い束縛となります。

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

モノタイプ

モノタイプは常に特定の型を示します。モノタイプは構文的には項として表現されます。 ${\displaystyle \tau}$

モノタイプの例としては、 や のような型定数や、 のようなパラメトリック型が挙げられます。後者の型は、例えば の集合からの 型関数の適用例であり、上付き文字は型パラメータの数を示します。型関数の完全な集合は、少なくとも、つまり関数の型を含んでいなければならない点を除いて、HM では任意です^{[注 3 ]} 。これは便宜上、中置記法で記述されることが多いです。例えば、整数を文字列にマッピングする関数は 型です。この場合も、括弧を使用して型式の曖昧性を解消できます。この適用は、右結合である中置矢印よりも強く結合します。 ${\displaystyle {\mathtt {int}}}$ ${\displaystyle {\mathtt {文字列}}}$ ${\displaystyle {\mathtt {Map\ (Set\ string)\ int}}}$ ${\displaystyle \{{\mathtt {Map^{2},\ Set^{1},\ string^{0},\ int^{0}}},\ \rightarrow ^{2}\}}$ ${\displaystyle C}$ ${\displaystyle \rightarrow ^{2}}$ ${\displaystyle {\mathtt {int}}\rightarrow {\mathtt {string}}}$

型変数はモノタイプとして認められます。モノタイプは、変数を含まず基底項のみを許容する単相型と混同しないでください。

2 つのモノタイプは、同一の用語を持つ場合、同等です。

ポリタイプ

ポリタイプ(または型スキーム) は、0 個以上の for-all 量指定子によってバインドされた変数を含む型です (例: ) 。 ${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$

polytype を持つ関数は、同じ型の任意の値をそれ自体にマッピングすることができ、恒等関数はこの型の値です。 ${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$

別の例として、これはすべての有限集合を整数にマッピングする関数の型です。集合の 基数を返す関数はこの型の値になります。${\displaystyle \forall \alpha .({\mathtt {Set}}\ \alpha )\rightarrow {\mathtt {int}}}$

量指定子は最上位レベルにのみ出現できます。例えば、型は型の構文からは除外されます。また、モノタイプはポリタイプに含まれます。したがって、型は一般的な形式 を持ちます。ここで、 とはモノタイプです。 ${\displaystyle \forall \alpha .\alpha \rightarrow \forall \alpha .\alpha }$ ${\displaystyle \forall \alpha _{1}\dots \forall \alpha _{n}.\tau }$ ${\displaystyle n\geq 0}$ ${\displaystyle \tau }$

ポリタイプの等価性は、量化の順序を変更し、量化変数の名前を変更する（-conversion）ことによって実現されます。さらに、モノタイプに出現しない量化変数は削除できます。 ${\displaystyle \alpha }$

コンテキストとタイピング

まだ分​​離している部分（構文式と型）を意味のある形でまとめるには、3つ目の部分であるコンテキストが必要です。構文的には、コンテキストは代入、仮定、または束縛と呼ばれるペアのリストであり、各ペアは値変数の型が であることを示します。これら3つの部分を組み合わせると、という形式の型判定が得られ、仮定の下では式の型が であることを示します。 ${\displaystyle x:\sigma }$ ${\displaystyle x_{i}}$ ${\displaystyle \sigma _{i}.}$ ${\displaystyle \Gamma \ \vdash \ e:\sigma }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \sigma }$

自由型変数

型 において、記号 はモノタイプ 内の型変数を束縛する量指定子です。変数は量化されているとされ、内の量化された型変数の出現は束縛されているとされ、 内の束縛されていない型変数はすべて自由であると呼ばれます。ポリタイプにおける量化に加えて、型変数はコンテキスト内で が発生することで束縛されることもありますが、 の右辺では逆の効果があります。このような変数は、そこでは型定数のように振舞います。最後に、型変数は型付けにおいて束縛されていない状態でも合法的に発生する可能性があり、その場合、それらは暗黙的にすべて量化されます。 ${\displaystyle \forall \alpha _{1}\dots \forall \alpha _{n}.\tau }$ ${\displaystyle \forall }$ ${\displaystyle \alpha _{i}}$ ${\displaystyle \tau }$ ${\displaystyle \alpha _{i}}$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \forall }$ ${\displaystyle \vdash }$

プログラミング言語において、束縛型変数と非束縛型変数の両方が存在することはあまり一般的ではありません。多くの場合、すべての型変数は暗黙的に量化されて扱われます。例えば、Prologには自由変数を含む節はありません。Haskellでも同様に、^{[注4 ]}ではすべての型変数が暗黙的に量化されて出現します。つまり、Haskell型とは「ここ」a -> aを意味します。これに関連して、これも非常に珍しいのは、代入の 右辺の束縛効果です​​。${\displaystyle \forall \alpha .\alpha \rightarrow \alpha }$ ${\displaystyle \sigma }$

通常、束縛型変数と非束縛型変数の両方が式の中で混在する状況は、自由変数を式の中で使用することで発生します。定数関数K =がその一例です。これはモノタイプ を持ちます。 によって多態性を強制できます。ここで、は型 を持ちます。モノタイプの自由変数は、周囲のスコープ内で束縛されている変数の型に由来します。は型 を持ちます。の型の自由型変数がの型の によって束縛されていると想像できます。しかし、そのようなスコープはHMでは表現できません。むしろ、束縛はコンテキストによって実現されます。 ${\displaystyle \lambda x.\lambda y.x}$ ${\displaystyle \alpha \rightarrow \beta \rightarrow \alpha }$ ${\displaystyle \mathbf {let} \ k=\lambda x.(\mathbf {let} \ f=\lambda y.x\ \mathbf {in} \ f)\ \mathbf {in} \ k}$ ${\displaystyle f}$ ${\displaystyle \forall \gamma .\gamma \rightarrow \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle x}$ ${\displaystyle k}$ ${\displaystyle \forall \alpha \forall \beta .\alpha \rightarrow \beta \rightarrow \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle f}$ ${\displaystyle \forall \alpha }$ ${\displaystyle k}$

入力順序

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

例えば、恒等関数はをその型として持つことができますが、 や、その他多くの を持つことができますが、 を持つことはできません。この関数の最も一般的な型は ですが 、他の型はより具体的であり、型パラメータ（つまり量化変数）を別の型に一貫して置き換えることで、一般的な型から派生させることができます。この反例は、置き換えが一貫していないため、失敗します。 ${\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 }$

特化ルール

${\displaystyle \displaystyle {\frac {\tau '=\left\{\alpha _{i}\mapsto \tau _{i}\right\}\tau \quad \beta _{i}\not \in {\textrm {free}}(\forall \alpha _{1}...\forall \alpha _{n}.\tau )}{\forall \alpha _{1}...\forall \alpha _{n}.\tau \sqsubseteq \forall \beta _{1}...\forall \beta _{m}.\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 }$

プリンシパルタイプ

型スキームの特殊化は順序の用途の一つですが、型システムにおいてもう一つの重要な役割を担っています。多態性を伴う型推論では、式が取り得るすべての型を要約するという課題に直面します。順序は、そのような要約が式の最も一般的な型として存在することを保証します。

型付けにおける置換

上記で定義した型順序は型付けに拡張できます。型付けの暗黙的な全量化により、一貫した置換が可能になるからです。

${\displaystyle \Gamma \vdash e:\sigma \quad \Longrightarrow \quad S\Gamma \vdash e:S\sigma }$

特殊化規則とは対照的に、これは定義の一部ではなく、暗黙の全量化と同様に、次に定義される型規則の結果です。型付けにおける自由型変数は、改良のためのプレースホルダーとして機能します。その右側にある自由型変数に対する環境の束縛効果は、特殊化規則におけるそれらの置換を禁止します。つまり、置換は一貫性を保ち、型付け全体を含む必要があるということです。 ${\displaystyle \vdash }$

この記事では、4 つの異なるルール セットについて説明します。

1. ${\displaystyle \vdash _{D}}$ 宣言型システム
2. ${\displaystyle \vdash _{S}}$ 統語体系
3. ${\displaystyle \vdash _{J}}$ アルゴリズムJ
4. ${\displaystyle \vdash _{W}}$ アルゴリズムW

演繹システム

ルールの構文

${\displaystyle {\begin{array}{lrl}{\text{Predicate}}&=&\sigma \sqsubseteq \sigma '\\&\vert \ &\alpha \not \in free(\Gamma )\\&\vert \ &x:\alpha \in \Gamma \\\\{\text{Judgment}}&=&{\text{Typing}}\\{\text{Premise}}&=&{\text{Judgment}}\ \vert \ {\text{Predicate}}\\{\text{Conclusion}}&=&{\text{Judgment}}\\\\{\text{Rule}}&=&\displaystyle {\frac {{\textrm {Premise}}\ \dots }{\textrm {Conclusion}}}\quad [{\mathtt {Name}}]\end{array}}}$

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

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

入力ルール

入力規則も参照

宣言型ルールシステム

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{D}e:\tau '}{\Gamma \vdash _{D}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e:\sigma }}&[{\mathtt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma \quad \alpha \notin {\text{free}}(\Gamma )}{\Gamma \vdash _{D}e:\forall \ \alpha \ .\ \sigma }}&[{\mathtt {Gen}}]\\\\\end{array}}}$

サイドボックスには、HM型システムの演繹規則が示されています。これらの規則は、おおよそ2つのグループに分けられます。

最初の4つの規則（変数または関数へのアクセス）、（適用、つまり1つの引数を持つ関数呼び出し）、（抽象化、つまり関数の宣言）、そして（変数の宣言）は構文を中心に据えており、それぞれの式形式に対して1つの規則を提示しています。これらの規則の意味は一目瞭然で、各式を分解し、その部分式を証明し、最後に前提にある個々の型を結論の型と組み合わせるというものです。 ${\displaystyle [{\mathtt {Var}}]}$ ${\displaystyle [{\mathtt {App}}]}$ ${\displaystyle [{\mathtt {Abs}}]}$ ${\displaystyle [{\mathtt {Let}}]}$

2つ目のグループは、残りの2つの規則とによって構成されます。これらは型の特殊化と一般化を扱います。この規則は上記の特殊化のセクションから明らかですが、は前者を補完し、逆方向に作用します。これにより一般化、つまりコンテキストで束縛されていないモノタイプ変数を量化することが可能になります。 ${\displaystyle [{\mathtt {Inst}}]}$ ${\displaystyle [{\mathtt {Gen}}]}$ ${\displaystyle [{\mathtt {Inst}}]}$ ${\displaystyle [{\mathtt {Gen}}]}$

以下の2つの例は、ルールシステムを実際に動作させる例です。式と型の両方が与えられているため、ルールの型チェックに使用されています。

例: の証明は次のように書ける。 ${\displaystyle \Gamma \vdash _{D}id(n):int}$ ${\displaystyle \Gamma =id:\forall \alpha .\alpha \rightarrow \alpha ,\ n:int}$

${\displaystyle {\begin{array}{llll}1:&\Gamma \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash _{D}id:int\rightarrow int&[{\mathtt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash _{D}n:int&[{\mathtt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}]&(2),\ (3)\\\end{array}}}$

例: 一般化を示すために、 以下に示します。 ${\displaystyle \vdash _{D}\ {\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha }$

${\displaystyle {\begin{array}{llll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}]&(1)\\3:&id:\alpha \rightarrow \alpha \vdash _{D}id:\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\alpha \rightarrow \alpha \in \left\{id:\alpha \rightarrow \alpha \right\})\\4:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\alpha \rightarrow \alpha &[{\mathtt {Let}}]&(2),\ (3)\\5:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Gen}}]&(4),\ (\alpha \not \in free(\epsilon ))\\\end{array}}}$

Let多態性

すぐには目に見えませんが、ルールセットは、ルールとにおけるモノタイプとポリタイプの微妙な使用法の違いによって、どのような状況下で型が一般化されるか、あるいはされないかという規制をエンコードします。 とはそれぞれポリタイプとモノタイプを表すことに注意してください。 ${\displaystyle [{\mathtt {Abs}}]}$ ${\displaystyle [{\mathtt {Let}}]}$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$

規則 では、関数のパラメータの値変数は前提 を通して単相型でコンテキストに追加されますが、規則 では 、変数は多相型 で環境に入ります。どちらの場合も、コンテキストに が存在するため、代入における自由変数の一般化規則は適用されませんが、この規則により、 -式ではパラメータの型は単相型のままになります。一方、let式では変数を多相型に導入できるため、特殊化が可能になります。 ${\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}$

一般化ルール

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

推論アルゴリズム

HMの演繹システムが完成したので、アルゴリズムを提示し、それを規則に基づいて検証することができます。あるいは、規則がどのように相互作用し、証明がどのように形成されるかを詳しく調べることで、アルゴリズムを導出することも可能です。本稿の残りの部分では、型付けの証明中に起こり得る意思決定に焦点を当てながら、アルゴリズムを導出します。

ルールを選択する自由度

証明において、全く決定が不可能な点を分離すると、構文を中心とする最初の規則群は選択の余地を残しません。なぜなら、それぞれの構文規則には、証明の一部を規定する固有の型付け規則が対応しているからです。一方、これらの固定された部分の結論と前提の間には、 と の連鎖が生じる 可能性があります。このような連鎖は、証明の結論と最上位表現の規則の間にも存在する可能性があります。すべての証明は、このように描かれた形をとらなければなりません。 ${\displaystyle [{\mathtt {Inst}}]}$ ${\displaystyle [{\mathtt {Gen}}]}$

証明において規則選択に関する選択肢は と の連鎖のみであるため、証明の形式から、これらの連鎖を必要としないより正確な証明が可能かどうかという疑問が生じます。これは実際に可能であり、そのような規則を持たない規則体系の変種につながります。 ${\displaystyle [{\mathtt {Inst}}]}$ ${\displaystyle [{\mathtt {Gen}}]}$

構文指向ルールシステム

統語規則システム

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau }{\Gamma \vdash _{S}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{S}e_{1}:\tau }{\Gamma \vdash _{S}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{S}e:\tau '}{\Gamma \vdash _{S}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{S}e_{1}:\tau '}{\Gamma \vdash _{S}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}}$

一般化

${\displaystyle {\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {free}}(\tau )-{\textrm {free}}(\Gamma )}$

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

正式には、この新しいルール システムが元の と同等であることを検証するには、 を示さなければなりません。これは、次の 2 つのサブ証明に分解されます。 ${\displaystyle \vdash _{S}}$ ${\displaystyle \vdash _{D}}$ ${\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma }$

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

の規則と を の証明に分解することで一貫性を見ることができるが、が不完全であることは明らかである。例えば では証明できず のみで証明できるからである。しかし、 完全性のよりわずかに弱いバージョンは証明可能である ^{[ 7 ]}。すなわち、 ${\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 }$

• ${\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 ] : σ をどのように洗練させるかが問題です。ここでのτ型の選択は、局所的には未知である変数の用法に依存するため、最も安全なのは最も一般的な型を選択することです。上記と同じ方法を用いることで、σ内のすべての量化変数を新たな単一型変数でインスタンス化することができ、これにより、さらなる洗練化が可能になります。
• [ Let ] : ルールでは選択の余地はありません。完了。
• [アプリ] : 両方の前提で要求されているように、アプリケーション ルールのみが、これまで「開かれた」変数の改良を強制する可能性があります。
  1. 最初の前提により、推論の結果は という形式になります。 ${\displaystyle \tau \rightarrow \tau '}$
     • もしそうなら、それでいい。後で結果のτ'を選ぶことができる。
     • そうでない場合、それはオープン変数である可能性があります。その場合、前と同じように2つの新しい変数を使用して、必要な形式に調整できます。
     • それ以外の場合、最初の前提で推論された型は関数型ではなく、関数型にすることもできないため、型チェックは失敗します。
  2. 第二の前提は、推論された型が第一の前提のτと等しいことを要求します。今、おそらく異なる型（おそらくオープン型変数を持つ）が2つ存在し、これらを比較し、可能であれば等しくする必要があります。等しくすることが可能であれば、改良点が見つかり、不可能であれば、再び型エラーが検出されます。置換によって「2つの項を等しくする」効果的な方法として、ロビンソンの統一化といわゆるUnion-Findアルゴリズムを組み合わせた方法が知られています。

簡単にunion-findアルゴリズムをまとめると、証明に含まれるすべての型の集合が与えられれば、union手続きによってそれらを同値クラスにグループ化し、 find手続き を使用して各クラスの代表を選ぶことができる。副作用の意味で手続きという言葉を強調すると、効果的なアルゴリズムを準備するために論理の領域を離れていることは明らかである。aの代表は、 aとbの両方が型変数である場合に代表が任意にどちらか一方になるように決定されるが、変数と項を結合すると項が代表になる。手元にunion-findの実装があると仮定すると、2つのモノタイプの統合を次のように定式化できる。 ${\displaystyle {\mathtt {union}}(a,b)}$

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つが型変数である場合、 ユニオン(ta, tb) それ以外 エラー「タイプが一致しません」 

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

アルゴリズムJ

アルゴリズムJ

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{J}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau _{0}\quad \Gamma \vdash _{J}e_{1}:\tau _{1}\quad \tau '={\mathit {newvar}}\quad {\mathit {unify}}(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash _{J}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{J}e:\tau '}{\Gamma \vdash _{J}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{J}e_{1}:\tau '}{\Gamma \vdash _{J}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}}$

アルゴリズム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は、完全な情報に基づく型検査アルゴリズムの最良のものと同等の性能を発揮します。ここでの型検査とは、アルゴリズムが証明を見つける必要はなく、与えられた証明を検証するだけでよいことを意味します。

の計算を可能にし、中に再帰的な型が構築されるのを防ぐためのoccurs チェックを有効にするために、コンテキストにおける型変数の束縛を維持する必要があるため、効率はわずかに低下します。このようなケースの一例として が挙げられますが、これはHMを用いて型を導出できません。実際には、型は小さな項に過ぎず、拡張構造を構築することはありません。したがって、計算量解析においては、それらの比較を定数として扱い、O(1)のコストを維持できます。 ${\displaystyle {\bar {\Gamma }}(\tau )}$ ${\displaystyle {\mathit {unify}}(\alpha ,\tau )}$ ${\displaystyle \lambda \ x.(x\ x)}$

アルゴリズムの証明

前の節では、アルゴリズムの概要を説明しながら、メタ論理的議論によってその証明を示唆しました。これは効率的なアルゴリズムJにつながりますが、そのアルゴリズムが意味論的ベースラインとして機能する演繹システムDまたはSを適切に反映しているかどうかは明らかではありません。

上記の議論において最も重要な点は、コンテキストに束縛されたモノタイプ変数の精緻化です。例えば、アルゴリズムはegを推論する際にコンテキストを大胆に変更します。これは、パラメータのためにコンテキストに後から追加されたモノタイプ変数は、適用処理の際に に精緻化する必要があるためです。問題は、演繹規則がそのような精緻化を許容していないことです。モノタイプ変数の代わりに、精緻化された型を先に追加できたはずだと主張するのは、せいぜい便宜的なものです。 ${\displaystyle \lambda f.(f\ 1)}$ ${\displaystyle f}$ ${\displaystyle int\rightarrow \beta }$

形式的に満足できる議論に到達するための鍵は、文脈を適切に精緻化の中に含めることです。形式的には、型付けは自由型変数の置換と互換性があります。

${\displaystyle \Gamma \vdash _{S}e:\tau \quad \Longrightarrow \quad S\Gamma \vdash _{S}e:S\tau }$

したがって、自由変数を改良することは、型付け全体を改良することを意味します。

アルゴリズムW

アルゴリズムW

${\displaystyle {\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{W}x:\tau ,\emptyset }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\begin{array}{ll}\Gamma \vdash _{W}e_{0}:\tau _{0},S_{0}&S_{0}\Gamma \vdash _{W}e_{1}:\tau _{1},S_{1}\\\tau '={\mathit {newvar}}&S_{2}={\mathsf {mgu}}(S_{1}\tau _{0},\ \tau _{1}\rightarrow \tau ')\end{array}}{\Gamma \vdash _{W}e_{0}\ e_{1}:S_{2}\tau ',S_{2}S_{1}S_{0}}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{W}e:\tau ',S}{\Gamma \vdash _{W}\lambda \ x\ .\ e:S\tau \rightarrow \tau ',S}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{W}e_{0}:\tau ,S_{0}\quad S_{0}\Gamma ,\,x:{\overline {S_{0}\Gamma }}(\tau )\vdash _{W}e_{1}:\tau ',S_{1}}{\Gamma \vdash _{W}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau ',S_{1}S_{0}}}&[{\mathtt {Let}}]\end{array}}}$

そこから、アルゴリズムJの証明はアルゴリズムWへとつながります。Wは、置換 を用いて逐次合成を表現することで、手続きによって課される副作用のみを明示的に 示します。サイドバーにおけるアルゴリズムWの表現では、斜体で示した演算において副作用が依然として利用されていますが、これらは新たなシンボルの生成に限定されています。判定形式は であり、コンテキストと式をパラメータとして持ち、置換とともにモノタイプを生成する関数を表します。は、最も一般的なユニファイアである置換を生成する副作用のないバージョンです。 ${\displaystyle {\textit {union}}}$ ${\displaystyle S_{i}}$ ${\displaystyle \Gamma \vdash e:\tau ,S}$ ${\displaystyle {\textsf {mgu}}}$ ${\displaystyle {\textit {union}}}$

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

現状では、W は効率的なアルゴリズムとは言い難い。置換が頻繁に適用されすぎるからだ。これは健全性の証明を支援するために定式化された。そこで、W を正確にシミュレートする、より単純なアルゴリズム J を提示する。

彼はWの方が複雑で効率が悪いと考えていたが、J.O.に先立つ論文でそれを発表した。副作用が利用できない、あるいは望ましくない場合、Wには利点がある。また、Wは完全性を証明するためにも必要であり、彼はこれを健全性証明に組み入れている。

証明義務

証明義務を定式化する前に、ルール システム D と S および提示されたアルゴリズム間の相違を強調する必要があります。

上記の展開では、モノタイプを「オープン」な証明変数として誤用していた面もありますが、新しい変数を導入することで、本来のモノタイプ変数が損なわれる可能性を回避し、最善の結果に期待しました。しかし、落とし穴があります。新しい変数は「記憶される」という約束がありましたが、この約束はアルゴリズムによって果たされていません。

コンテキスト を持つ式はまたはの どちらにも型付けできませんが、アルゴリズムは という型を生成します。ここで W はさらに置換 を生成します。つまり、アルゴリズムはすべての型エラーを検出できないことになります。この欠陥は、証明変数とモノタイプ変数をより注意深く区別することで簡単に修正できます。 ${\displaystyle 1:int,\ f:\alpha }$ ${\displaystyle f\ 1}$ ${\displaystyle \vdash _{D}}$ ${\displaystyle \vdash _{S}}$ ${\displaystyle \beta }$ ${\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}}}$

完全性義務における副条件は、アルゴリズムが常に1つの型を生成するにもかかわらず、推論によって複数の型が生成される可能性があることを規定しています。同時に、副条件は推論される型が実際に最も一般的な型であることを要求します。

義務を適切に証明するには、まず義務を強化して、とに代入を通す代入補題を有効化できるようにする必要があります。そこから、式 に関する帰納法によって証明を行います。 ${\displaystyle S}$ ${\displaystyle \vdash _{S}}$ ${\displaystyle \vdash _{W}}$

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

拡張機能

再帰定義

プログラミングを実用的にするには、再帰関数が必要です。ラムダ計算の中心的な特性は、再帰定義を直接利用できず、代わりに固定小数点コンビネータで表現できることです。しかし、固定小数点コンビネータをラムダ計算の型付きバージョンで定式化すると、以下に概説するように、システムに壊滅的な影響を与えることになります。

入力ルール

原著論文^{[ 4 ]}では、再帰はコンビネータによって実現できることが示されている 。したがって、再帰定義は次のように定式化できる 。 ${\displaystyle {\mathit {fix}}:\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha }$ ${\displaystyle {\mathtt {rec}}\ v=e_{1}\ {\mathtt {in}}\ e_{2}\ ::={\mathtt {let}}\ v={\mathit {fix}}(\lambda v.e_{1})\ {\mathtt {in}}\ e_{2}}$

あるいは、式構文の拡張と追加の型付け規則も可能です。

${\displaystyle \displaystyle {\frac {\Gamma ,\Gamma '\vdash e_{1}:\tau _{1}\quad \dots \quad \Gamma ,\Gamma '\vdash e_{n}:\tau _{n}\quad \Gamma ,\Gamma ''\vdash e:\tau }{\Gamma \ \vdash \ {\mathtt {rec}}\ v_{1}=e_{1}\ {\mathtt {and}}\ \dots \ {\mathtt {and}}\ v_{n}=e_{n}\ {\mathtt {in}}\ e:\tau }}\quad [{\mathtt {Rec}}]}$

どこ

• ${\displaystyle \Gamma '=v_{1}:\tau _{1},\ \dots ,\ v_{n}:\tau _{n}}$
• ${\displaystyle \Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )}$

基本的には、再帰的に定義された変数を、モノタイプの位置に含めながら、左側に出現しますが、右側にはポリタイプとして含めます。 ${\displaystyle [{\mathtt {Abs}}]}$ ${\displaystyle [{\mathtt {Let}}]}$ ${\displaystyle {\mathtt {in}}}$

結果

上記は簡単ですが、それにはコストがかかります。

型理論はラムダ計算と計算および論理を結び付けます。上記の簡単な変更は両方に影響を与えます。

• 非終了項を定式化できるため、強い正規化プロパティは無効になります。
• 型が占有されてしまうため、論理が崩壊してしまいます。${\displaystyle \forall a.a}$

過負荷

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

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

クイックソート:: Ord a => [ a ] -> [ a ]

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

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

高階型

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

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

Haskellは、より高次の種類（ kind）を導入する。標準的なHaskellでは、種類は推論され、型構築子のアリティを記述する以上の用途はほとんどない。例えば、リスト型構築子は、ある型（その要素の型）を別の型（その要素を含むリストの型）にマッピングするものと考えられており、記法的には と表現される。依存型システムの機能をエミュレートするために種類を拡張する言語拡張が利用可能である。^{[ 8 ]}${\displaystyle *\to *}$

サブタイプ

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

一方、オブジェクト指向プログラミング言語の文脈では、型推論はより困難であることが証明されている。これは、オブジェクトメソッドがSystem F（型推論が決定不能）のような第一級多態性を必要とする傾向があり、またF-bounded polymorphismのような機能があるためである。その結果、 Cardelliのシステム^{[ 12 ]}のような、サブタイプ化によってオブジェクト指向プログラミングを可能にする型システムは、HMスタイルの型推論をサポートしていない。 ${\displaystyle F_{<:}}$

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

注記

1. Hindley–Milner型推論はDEXPTIME完全である。実際、MLプログラムが型付け可能かどうかを（型推論を必要とせずに）判定するだけでも、それ自体がDEXPTIME完全である。非線形な挙動は確かに現れるが、それは主に異常な入力に対してである。そのため、 Mairson (1990)とKfoury, Tiuryn & Urzyczyn (1990)による計算量理論的証明は、研究コミュニティにとって驚きであった。
2. ポリタイプは、元の記事では「タイプ スキーム」と呼ばれています。
3. パラメトリック型はHMの原論文には存在せず、本手法の提示には必要ありません。以下の推論規則はいずれもパラメトリック型を考慮しておらず、言及すらしていません。同論文における非パラメトリックな「プリミティブ型」についても同様です。多態的型推論の仕組みはすべて、パラメトリック型がなくても定義できます。パラメトリック型は例としてここに含めていますが、HMの本質はパラメトリック型にあるためです。これは、以下の推論規則に組み込まれている関数 type に由来します。この関数は既に2つのパラメータを持ち、ここでは特別なケースとしてのみ提示されています。${\displaystyle C\ \tau \dots \tau }$ ${\displaystyle \tau \rightarrow \tau }$
4. Haskell は、すべての量化された型変数をスコープ内に取り込むことを可能にする ScopedTypeVariables 言語拡張機能を提供します。

参考文献

1. Hindley, J. Roger (1969). 「組合せ論理におけるオブジェクトの主要な型スキーム」.アメリカ数学会誌. 146 : 29–60 . doi : 10.2307/1995158 . JSTOR  1995158 .
2. ミルナー、ロビン(1978). 「プログラミングにおける型多態性の理論」.コンピュータとシステム科学ジャーナル. 17 (3): 348– 374. CiteSeerX 10.1.1.67.5276 . doi : 10.1016/0022-0000(78)90014-4 . hdl : 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66 . S2CID 388583 .  
3. Damas, Luis (1985).プログラミング言語における型の割り当て（博士論文）. エディンバラ大学. hdl : 1842/13555 . CST-33-85.
4. Damas, Luis; Milner, Robin (1982).関数型プログラムのための主要な型スキーム(PDF) . 第9回プログラミング言語原理シンポジウム (POPL'82). ACM. pp.  207– 212. doi : 10.1145/582153.582176 . ISBN 978-0-89791-065-1. 2022年3月22日時点のオリジナル（PDF）からアーカイブ。2012年12月3日閲覧。
5. Wells, JB (1994). 「二階ラムダ計算における型付け可能性と型検査は同値かつ決定不能である」 .第9回IEEEコンピュータサイエンス論理シンポジウム (LICS) の議事録. pp.  176– 185. doi : 10.1109/LICS.1994.316068 . ISBN 0-8186-6310-3. S2CID  15078292 .
6. Clement (1986).シンプルな応用言語：Mini-ML (PDF) . LFP'86. ACM. doi : 10.1145/319838.319847 . ISBN 978-0-89791-200-6。
7. Vaughan, Jeff (2008年7月23日) [2005年5月5日]. 「Hindley–Milner型推論アルゴリズムの正しさの証明」(PDF) . 2012年3月24日時点のオリジナル(PDF)からのアーカイブ。{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）が必要です
8. Yorgey; Brent; Weirich; Stephanie; Cretin; Julien; Peyton Jones; Simin; Vytiniotis; Dmitrios; Magalhaes; José Pedro (2012年1月). 「Haskellの昇格」 .第8回ACM SIGPLANワークショップ「言語設計と実装における型」の議事録. pp.  53– 66. doi : 10.1145/2103786.2103795 . ISBN 978-1-4503-1120-5。
9. Pottier, François (1998).サブタイプが存在する場合の型推論：理論から実践へ（論文） . 2021年8月10日閲覧。
10. Dolan, Stephen; Mycroft, Alan (2017). 「MLsubにおけるポリモーフィズム、サブタイピング、型推論」(PDF) . POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages . doi : 10.1145/3009837.3009882 .
11. Parreaux, Lionel (2020). 「代数的サブタイピングのシンプルなエッセンス：サブタイピングによる主型推論の容易化」 .第25回 ACM SIGPLAN 国際関数型プログラミング会議 - ICFP 2020, [オンラインイベント], 2020年8月24日～26日. doi : 10.1145/3409006 .
12. Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). 「サブタイプ化によるシステムFの拡張」. Information and Computation, vol. 9 . 北ホラント州アムステルダム. pp.  4– 56. doi : 10.1006/inco.1994.1013 .
13. Daan Leijen、「スコープ付きラベル付き拡張レコード」、ユトレヒト大学情報・計算科学研究所、草稿、改訂第76号、2005年7月23日

• ハリー・G・メアソン(1990). 「決定論的指数時間におけるML型付け可能性の決定は完全である」.第17回ACM SIGPLAN-SIGACTシンポジウム「プログラミング言語の原理 - POPL '90」の議事録. ACM. pp.  382– 401. doi : 10.1145/96709.96748 . ISBN 978-0-89791-343-0. S2CID  75336 .
• Kfoury, AJ; Tiuryn, J.; Urzyczyn, P. (1990). 「ML型付け可能性はdexptime完全である」. Caap '90 . コンピュータサイエンス講義ノート. 第431巻. pp.  206– 220. doi : 10.1007/3-540-52590-4_50 . ISBN 978-3-540-52590-5。

外部リンク

• アルゴリズム W の文芸的な Haskell 実装とソース コードは GitHub にあります。
• Python での Hindley-Milner アルゴリズムの簡単な実装。