Какие типы и / или термины в system-f не могут быть выражены в Hindley Milner?

Question

Я помню, как читал где-то, что Хиндли Милнер был ограничением для system-f.Если это так, не могли бы вы предоставить мне некоторые термины, которые можно ввести в system-f, но не в HM.

Answer 1

Все, что связано с более высоким рейтингом (то есть "первоклассным") полиморфизмом.Например:

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

Эта функция будет иметь тип (forall A. A -> A) -> Int * String, который не может быть выражен в HM, где все схемы полиморфного типа должны быть в форме «prenex» (т.е. квантификатор может присутствовать толькоснаружи, никогда не вложенный).