types - Hindley Milner 型推論で使用できない System F の型の例

Question

「ヒンドリー・ミルナーとは」の下に、次のように記載されています。

Hindley-Milner はSystem Fの制限であり、より多くの型を許可しますが、プログラマによる注釈が必要です。

私の質問は、Hindley Milner (型推論) では利用できない、System F で利用可能な型の例は何ですか?

(システム F 型の推論が決定不能であることが証明されているという仮定)

Answer 1

Hindley/Milner は、上位のポリモーフィック型、つまり、全称量指定子がより大きな型にネストされている型 (つまり、第一級ポリモーフィズムの概念) をサポートしていません。

最も単純な例の 1 つは、たとえば次のようになります。

f : (∀α. α → α) → int × string
f id = (id 4, id "boo")

上位多型の推論は、一般に決定不可能であることが知られています。同様の制限が再帰にも適用されます。再帰的な定義では、多相的な再帰的な使用を行うことはできません。不自然な例:

g : ∀α. int × α → int
g (n,x) = if n = 0 then 0 else if odd n then g (n-1, 3) else g (n-1, "boo")

上記のことを考えると、これは驚くべきことではありません。また、上記のような再帰的な定義は、多相型で高次の Y コンビネータを適用するための省略形にすぎないという事実もあり、この場合も (暗黙の) ファーストクラスの多相が必要になります。