型推論

型推論は、式の型を自動的に再構築する機能であり、プログラマーが型注釈を省略しても、コンパイラが最も一般的な型を計算することを可能にする。

Definition

型推論（型再構築）とは、プログラマーがすべての型注釈を提供することなく、式の構造と使用法から、その式に対する有効かつ最も一般的な型を推論するプロセスである。

Scope

このトピックでは、明示的な型注釈なしに型を推論するためのアルゴリズムと理論を扱い、Hindley-Milnerシステムと、単一化およびlet多相性を用いるAlgorithm Wを中心に説明する。主要型、決定可能性と計算量、および部分型付け、高階多相性、依存型などのよりリッチなシステムへの推論の拡張における困難さについても触れる。

Core questions

• コンパイラは、型が記述されていない場合にどのように型を再構築できるのか？
• 主要型とは何か、そしてそれはいつ常に存在するのか？
• 単一化はHindley-Milner型推論をどのように推進するのか？
• よりリッチな型システムにおいて、型推論が決定不能または不完全になるのはなぜか？

Key theories

Hindley-Milner型推論

Milnerの多相型規律は、Algorithm Wとともに、単一化を用いてlet束縛多相性を持つラムダ計算の型を推論し、ML系言語における型推論の基礎を形成している。

主要型スキーム

DamasとMilnerは、型付け可能なすべての式が主要型スキーム（そのすべての有効な型がそのインスタンスである最も一般的な型）を持つこと、およびAlgorithm Wがそれを計算することを証明した。

コンビネータ論理における主要型

Hindleyは、型付け可能な項に対する主要型の存在を確立した。これは、後のプログラミング言語の型推論の基礎となる先行する結果である。

Clinical relevance

型推論は、型注釈の負担を軽減しつつ安全性を維持することで、静的型付け言語をはるかに便利にし、型ヒントやオートコンプリートのような最新のエディタ機能の基盤となっている。表現力の高いシステムにおけるその限界は、プログラマーが依然として型注釈を提供しなければならない箇所を形成している。

History

Hindleyによる1969年のコンビネータ論理における主要型に関する研究は、実用的な型推論を予見していた。Milnerの1978年の論文は、MLのための多相型システムとAlgorithm Wを導入し、DamasとMilnerの1982年の論文は主要性（principality）を証明した。Hindley-Milnerシステムは、ML、Haskell、およびその後の多くの言語の標準となり、よりリッチな設定への推論を拡張するための研究が現在も進行中である。

Debates

推論する量と注釈する量のバランス

型システムが表現力を増すにつれて、完全な型推論は決定不能になるため、推論を扱いやすく予測可能に保つために、自動的に推論されるべき量と明示的な注釈として要求されるべき量について議論がなされている。

Key figures

• Robin Milner
• Luis Damas
• Roger Hindley
• Benjamin Pierce

Seminal works

• milner1978
• damas1982
• hindley1969
• pierce2002

Frequently asked questions

主要型とは何か？

主要型とは、式の最も一般的な型であり、その式に対する他のすべての有効な型がその代入インスタンスとなるものである。Hindley-Milner型推論は、主要型が存在する場合、常にそれを計算する。

なぜすべての型システムが型を自動的に推論できないのか？

型推論は可解な制約に依存する。高階型や依存型のような表現力の高いシステムでは、完全な型推論は決定不能になるため、プログラマーが一部の型注釈を提供する必要がある。