types - Hindley Milner で表現できない system-f のいくつかのタイプおよび/または用語は何ですか?

Question

Hindley Milner が system-f の制限であるとどこかで読んだことを覚えています。その場合、system-f では入力できるが HM では入力できない用語を誰か教えてください。

Answer 1

高ランク (つまり、「ファーストクラス」) のポリモーフィズムに関係するもの。例えば：

lambda (f : forall A. A -> A). (f Int 1, f String "hello")

この関数は type を持ちますが(forall A. A -> A) -> Int * String、これは HM では表現できません。すべての多相型スキームは「プレネックス」形式でなければなりません (つまり、量指定子は外側でのみ発生し、ネストすることはできません)。