Tipo inferido parece detectar un bucle infinito, pero lo que realmente está pasando?

Question

En Andrew Koenig una anécdota sobre la inferencia de tipos ML , el autor utiliza la aplicación de rel="noreferrer"> href="http://en.wikipedia.org/wiki/Merge_sort" como un ejercicio de aprendizaje para ML y se complace en encontrar una inferencia de tipos “incorrecto”.

  

Para mi sorpresa, el compilador informó un tipo de

'a list -> int list

     

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

     

Eso es imposible. La salida debe ser una permutación de la entrada; ¿cómo puede tener un tipo diferente? El lector encontrará seguramente mi primer impulso familiarizados: 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 podría ignorar su argumento: tal vez a veces no volvía en absoluto. De hecho, cuando lo probé, eso es exactamente lo que sucedió:. sort(nil) volvió nil, pero la clasificación de cualquier lista no vacía entraría en un bucle infinito recursividad

Cuando se traduce 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 funciona el algoritmo de Damas-Hindley-Milner inferir este tipo ?

Answer 1

Este es de hecho un ejemplo notable; un bucle infinito su detección, en esencia, en tiempo de compilación ! No hay nada especial acerca de la inferencia Hindley-Milner en este ejemplo; sólo 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 de t ₁ → t ₂ para algunos tipos t ₁ y t ₂ . Luego se ve la primera línea:

mergesort [] = []

y da cuenta de que t ₁ y t ₂ debe ser tipos de lista, por ejemplo t ₁ = [t ₃ ] y t ₂ = [t ₄ ]. Así mergesort debe ser una función [t ₃ ] → [t ₄ ]. La siguiente línea

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

le dice que:

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

Es por eso que se obtiene:

*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 del algoritmo que sigue es simplemente que, dada en la página de Wikipedia, por ejemplo.)

Answer 2

Ese tipo se puede deducir porque ve que se pasa el resultado de mergesort a merge, que a su vez se comparan las cabezas de las listas con los <, que es parte de la clase de tipos Ord. Por lo que la inferencia de tipos puede razonar que debe devolver una lista de una instancia de Ord. Por supuesto, ya que en realidad recursivamente infinitamente, no podemos inferir nada sobre el tipo en realidad no retorno.