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

В 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 1 → t 2 для некоторых типов t 1 и t 2. Затем он видит первую строку:

mergesort [] = []

и понимает, что t 1 и t 2 должны быть типами списков, например t 1= [t 3] и t 2= [t 4]. Поэтому mergesort должен быть функцией [t 3] → [t 4]. Следующая строка

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

сообщает, что:

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

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

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

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

Ответ 2

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