haskell - El tipo inferido parece detectar un bucle infinito, pero ¿qué está sucediendo realmente?

type-inference type-systems

Question

En la anécdota sobre la inferencia de tipo ML de Andrew Koenig, el autor utiliza la implementación del tipo de combinación como un ejercicio de aprendizaje para ML y se complace en encontrar una inferencia de tipo "incorrecta".

Para mi sorpresa, el compilador reportó un tipo de

''a list -> int list

En otras palabras, esta función de clasificación acepta una lista de cualquier tipo y devuelve una lista de enteros.

Eso es imposible. La salida debe ser una permutación de la entrada; ¿Cómo puede tener un tipo diferente? El lector seguramente encontrará mi primer impulso familiar: ¡Me preguntaba si había descubierto un error en el compilador!

Después de pensarlo un poco más, me di cuenta de que había otra forma en que la función podía ignorar su argumento: tal vez a veces no regresaba en absoluto. De hecho, cuando lo probé, eso es exactamente lo que sucedió: sort(nil) devolvió nil , pero clasificar cualquier lista no vacía entraría en un bucle de recursión infinito.

Cuando traducido a 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 infiere un tipo similar:

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

¿Cómo infiere este tipo el algoritmo Damas-Hindley-Milner ?

Answer 1

Ese tipo se puede inferir porque ve que se pasa el resultado de mergesort to merge , que a su vez compara los encabezados de las listas con < , que forma parte de la clase de tipos Ord. Entonces, la inferencia de tipos puede razonar que debe devolver una lista de una instancia de Ord. Por supuesto, ya que en realidad recurre infinitamente, no podemos inferir nada más sobre el tipo que realmente no devuelve.

Answer 2

Este es ciertamente un ejemplo notable; Un bucle infinito siendo detectado, esencialmente, en tiempo de compilación ! No hay nada especial acerca de la inferencia de Hindley-Milner en este ejemplo; simplemente procede como de costumbre.

Tenga en cuenta que ghc obtiene los tipos de split y merge correctamente:

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

Ahora, cuando se trata de mergesort , es, en general, una función t ₁ → t ₂ para algunos tipos t ₁ y t ₂ . Entonces ve la primera línea:

mergesort [] = []

y se da cuenta de que t ₁ y t ₂ deben ser tipos de lista, digamos que t ₁ = [t ₃ ] y t ₂ = [t ₄ ]. Entonces mergesort debe ser una función [t ₃ ] → [t ₄ ]. La siguiente linea

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

le dice que

• xs debe ser una entrada para dividir, es decir, de tipo [a] para algunas a (que ya es, para a = t ₃ ).
• Entonces p y q también son del tipo [t ₃ ], ya que split es [a] → ([a], [a])
• mergesort p , por lo tanto, (recuerde que mergesort se cree que es del tipo [t ₃ ] → [t ₄ ]) es del tipo [t ₄ ].
• mergesort q es de tipo [t ₄ ] exactamente por el mismo motivo.
• Como la merge tiene tipo (Ord t) => [t] -> [t] -> [t] , y las entradas en la expresión merge (mergesort p) (mergesort q) son de tipo [t ₄ ], el tipo t ₄ debe estar en Ord .
• Finalmente, el tipo de merge (mergesort p) (mergesort q) es el mismo que sus entradas, es decir, [t ₄ ]. Esto encaja con el tipo conocido anteriormente [t ₃ ] → [t ₄ ] para mergesort , por lo que no hay más inferencias que hacer y la parte de "unificación" del algoritmo Hindley-Milner está completa. mergesort es de tipo [t ₃ ] → [t ₄ ] con t ₄ en Ord .

Es por eso que obtienes:

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

(La descripción anterior en términos de inferencia lógica es equivalente a lo que hace el algoritmo, pero la secuencia específica de pasos que sigue el algoritmo es simplemente la que figura en la página de Wikipedia, por ejemplo).