Выведенный тип, похоже, обнаруживает бесконечный цикл, но что происходит на самом деле?

Question

У Эндрю Кенига Анекдот про вывод типа ML, автор использует реализацию Сортировка слиянием в качестве учебного упражнения для ML и рад обнаружить «неправильный» вывод типа.

К моему большому удивлению, компилятор сообщил о типе

'a list -> int list

Другими словами, эта функция сортировки принимает список любого типа и возвращает список целых чисел.

Это невозможно.Выходные данные должны быть перестановкой входных данных;как он может иметь другой тип?Читатель наверняка найдет мой первый порыв знакомым:Мне стало интересно, не обнаружил ли я ошибку в компиляторе!

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

При переводе на Haskell

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge (mergesort p) (mergesort q)
  where (p,q) = split xs

GHC предполагает аналогичный тип:

*Main> :t mergesort
mergesort :: (Ord a) => [t] -> [a]

Как Алгоритм Дамаса – Хиндли – Милнера сделать вывод об этом типе?

Answer 1

Это действительно замечательный пример;бесконечный цикл обнаруживается, по сути, в время компиляции!В этом примере нет ничего особенного в выводе Хиндли-Милнера;все идет как обычно.

Обратите внимание, что ghc получает типы split и merge правильно:

*Main> :t split
split :: [a] -> ([a], [a])
*Main> :t merge
merge :: (Ord t) => [t] -> [t] -> [t]

Теперь, когда дело доходит до mergesort, это, вообще говоря, функция t₁→т₂ для некоторых типов т₁ и т₂.Затем он видит первую строку:

mergesort [] = []

и понимает, что т₁ и т₂ должны быть типами списков, скажем, t₁=[т₃] и т₂=[т₄].Таким образом, сортировка слиянием должна быть функцией [t₃]→[т₄].Следующая строка

mergesort xs = merge (mergesort p) (mergesort q) 
  where (p,q) = split xs

говорит это, что:

• xs должен быть входом для разделения, т. е. иметь тип [a] для некоторого a (который уже есть для a=t₃).
• Так p и q также имеют тип [t₃], с split это [a]→([a],[a])
• mergesort p, поэтому (напомним, что сортировка слиянием считается типа [t₃]→[т₄]) имеет тип [t₄].
• mergesort q имеет тип [t₄] по той же причине.
• Как merge имеет тип (Ord t) => [t] -> [t] -> [t], а входные данные в выражении merge (mergesort p) (mergesort q) оба типа [t₄], тип t₄ должно быть в Ord.
• Наконец, тип merge (mergesort p) (mergesort q) совпадает с обоими входными параметрами, а именно [t₄].Это соответствует ранее известному типу [t₃]→[т₄] для mergesort, поэтому больше не нужно делать никаких выводов, и «объединяющая» часть алгоритма Хиндли – Милнера завершена. mergesort имеет тип [t₃]→[т₄] с т₄ в Ord.

Вот почему вы получаете:

*Main> :t mergesort 
mergesort :: (Ord a) => [t] -> [a]

(Описание выше с точки зрения логического вывода эквивалентно тому, что делает алгоритм, но конкретная последовательность шагов, которой следует алгоритм, просто приведена, например, на странице Википедии.)

Answer 2

Этот тип можно определить, поскольку он видит, что вы передаете результат mergesort к merge, который, в свою очередь, сравнивает заголовки списков с <, который является частью класса типов Ord.Таким образом, вывод типа может привести к выводу, что он должен вернуть список экземпляров Ord.Конечно, поскольку на самом деле он рекурсивно бесконечно, мы не можем сделать никаких выводов о типе, который он на самом деле не возвращает.