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

Question

В Andrew Koenig's Анекдот о выводе типа ML , автор использует реализацию сортировка слиянием в качестве учебного упражнения для ML и рад найти & ldquo; неверный & rdquo; вывод типа.

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

'a list -> int list

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

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

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

При переводе на Хаскелл

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]

Как алгоритм Damas - Hindley - Milner выводит этот тип?

Answer 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 _{2 * 1 031 * = [т * 1 032 * 4 * 1 033 *]. Таким образом, сортировка слиянием должна быть функцией [t 3 ] → [t 4 ]. Следующая строка}

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 ₄ ].
• 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]

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

Answer 2

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