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

В Andrew Koenig & ss Анекдот о выводах типа ML автор использует реализацию merge sort как учебное упражнение для 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 [email protected](x:xs) [email protected](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]

Как Damas – Hindley – алгоритм Милнера вывести этот тип?

Ответ 1

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

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

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

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

mergesort [] = []

и понимает, что t ₁ и t ₂ должны быть типами списков, например t ₁= [t ₃] и t ₂= [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 ₄]) имеет тип [t _{4суб > ].}
mergesort q имеет тип [t ₄] по той же причине.
Как merge имеет тип (Ord t) => [t] -> [t] -> [t], а входы в выражении merge (mergesort p) (mergesort q) являются типами [t ₄], тип t ₄ должен быть в Ord.
Наконец, тип merge (mergesort p) (mergesort q) является таким же, как и его входы, а именно [t ₄]. Это соответствует уже известному типу [t ₃] → [t ₄] для mergesort, поэтому больше не нужно делать никаких выводов, а часть "унификация" алгоритма Хиндли-Милнера завершена. mergesort имеет тип [t ₃] → [t ₄] с t ₄ в Ord.

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

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

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

Ответ 2

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