Я помню, как где-то читал, что Хиндли Милнер был ограничением на систему-f. Если это так, может кто-то, пожалуйста, предоставит мне некоторые термины, которые можно ввести в system-f, но не в HM.Каковы некоторые типы и/или термины в системе-f, которые не могут быть выражены в Hindley Milner
Все, что связано с более высоким рангом (то есть «первоклассным») полиморфизмом. Например:
lambda f : (forall A. A -> A). (f Int 1, f String "hello")
Эта функция будет иметь тип (forall A. A -> A) -> Int * String, которая не выражается в HM, где все схемы полиморфных типа должны быть в «предваренной» форме (т.е. квантор может произойти только снаружи, не вложенный).
Не уверен, что вы имеете в виду, это выражение не является функцией. Определения (связанные через let) могут быть полиморфными с HM, но параметры функции не могут. –