Пример типа в Системе F, который недоступен в выводе типа Хиндли Милнера

Question

В разделе "Что такое Хиндли Милнер" говорится:

Хиндли-Милнер - это ограничение System F, которое допускает больше типов, но требует от программиста аннотаций.

У меня вопрос: что является примером типа, доступного в системе F, который недоступен в Hindley Milner (вывод типа)?

(Предполагается, что вывод типов System F оказался неразрешимым)

Answer 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-комбинатора высшего порядка в полиморфном типе, что снова потребует (непредсказуемого) полиморфизма первого класса.

Answer 2

Да, вывод типа System F был доказан неразрешимым Дж. Б. Уэллсом в " Типичности", а проверка типов в System F эквивалентна и неразрешима.

Система типов HM допускает квантификаторы типов только на верхнем уровне выражений типов. Точнее, HM различает типы, которые не могут содержать квантификаторы, и схемы типов:

тип:= переменная типа | тип → тип

схема типа:= тип | ∀α . схема типа

А полиморфные выражения набираются с использованием схем типов.

Таким образом, любой тип, имеющий квантификаторы типов внутри выражения типа (в частности, внутри левой части →), не может быть выражен в системе типов HM.

Одним из примеров может быть набор церковных цифр. Их тип в Системе F ∀α.(α→α)→(α→α)и хотя это одно можно выразить в HM, мы не можем выразить типы, в которых в качестве аргумента используется церковная цифра. Например, если определить возведение по церковным цифрам

(λmn.nm) : (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α))

этот тип не может быть выражен в системе типов HM из-за квантификаторов типов в аргументах.