Подтвердить что ты не робот

Рост определения типа в SML с использованием вывода типа Hindley Milner

Кто-то однажды показал мне небольшой "трюк" в SML, где они выписали около 3 или 4 функции в своем REPL, а полученный в результате тип для последнего значения был чрезвычайно длинным (как и многие прокрутки страниц).

Кто-нибудь знает, какой код генерирует такой длинный тип, или если есть имя для такого поведения?

4b9b3361

Ответ 1

Типы, которые выводятся методом вывода типа Хиндли/Милнера, могут быть экспоненциально большими, если вы их правильно составите. Например:

fun f x = (x, x, x)
val t = f (f (f (f (f 0))))

Здесь t является вложенной тройкой, глубина вложенности которой соответствует числу n вызовов f. Следовательно, общий тип имеет размер 3 ^ n.

Однако на самом деле это не самый худший случай, так как тип имеет регулярную структуру и может быть представлен графиком эффективно в линейном пространстве (поскольку на каждом уровне все три составляющих типа одинаковы и могут быть разделены).

В реальном худшем случае используется полиморфная инстанция, чтобы победить это:

fun f x y z = (x, y, z)
val p1 = (f, f, f)
val p2 = (p1, p1, p1)
val p3 = (p2, p2, p2)

В этом случае тип снова экспоненциально большой, но, в отличие от выше, все составляющие типы представляют собой переменные нового типа, так что даже представление графа растет экспоненциально (в числе объявлений pN).

Итак, да, вывод типа Hindley/Milner - наихудший экспоненциальный (в пространстве и времени). Однако стоит отметить, что экспоненциальные случаи могут возникать только там, где типы экспоненциально велики - то есть в тех случаях, когда вы не можете даже реалистично выражать без вывода типа.