Tipo inferir parece detectar um loop infinito, mas o que está realmente acontecendo?

Question

Uma anedota de Em Andrew Koenig sobre o tipo ML inferência , a usos autor implementação de merge sort como um exercício de aprendizagem para ML e tem o prazer de encontrar um “incorreto” inferência de tipos.

Para minha surpresa, o compilador relatado um tipo de

'a list -> int list

Em outras palavras, essa função tipo aceita uma lista de qualquer tipo em tudo e retorna uma lista de números inteiros.

Isso é impossível. A saída deve ser uma permutação de entrada; como pode, eventualmente, ter um tipo diferente? O leitor certamente irá encontrar o meu primeiro impulso familiar: Eu me perguntava se eu tinha descoberto um bug no compilador

Depois de pensar um pouco mais, eu percebi que não havia outra maneira em que a função poderia ignorar o seu argumento: talvez, por vezes, não retornou em tudo. Na verdade, quando eu tentei, que é exatamente o que aconteceu:. sort(nil) fez retorno nil, mas classificar qualquer lista não-vazia iria entrar em um loop de recursão infinita

Quando traduzido para 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 infere um tipo similar:

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

Como o Damas-Hindley-Milner algoritmo inferir este tipo ?

Answer 1

Este é realmente um exemplo notável; um loop infinito ser detectado, essencialmente, em tempo de compilação ! Não há nada de especial sobre a inferência Hindley-Milner neste exemplo; ele só procede como de costume.

Note que ghc recebe os tipos de split e merge corretamente:

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

Agora, quando se trata de mergesort, é, em geral, uma função de t ₁ ? t ₂ para alguns tipos de t ₁ e t ₂ . Em seguida, ele vê a primeira linha:

mergesort [] = []

e percebe que t ₁ e t ₂ devem ser do tipo da lista, dizem t ₁ = [t ₃ ] e t ₂ = [t ₄ ]. Então mergesort deve ser uma função [t ₃ ] ? [t ₄ ]. A próxima linha

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

diz-se que:

• xs deve ser uma entrada de separação, isto é, do tipo [a] para algumas um (o que já é, para a = t ₃ ).
• Assim p e q também são do tipo [t ₃ ], desde split é [a] ? ([a], [a])
• mergesort p, por conseguinte, (lembrar que mergesort acredita-se ser do tipo [t ₃ ] ? [t ₄ ]) é do tipo [t ₄ ].
• mergesort q é do tipo [t ₄ ] para exatamente a mesma razão.
• Como merge tem tipo (Ord t) => [t] -> [t] -> [t], e as entradas na merge (mergesort p) (mergesort q) expressão são tanto do tipo [t ₄ ], do tipo t ₄ devem estar em Ord.
• Finalmente, o tipo de merge (mergesort p) (mergesort q) é o mesmo que ambas as suas entradas, nomeadamente [t ₄ ]. Isso se encaixa com o tipo anteriormente conhecido [t ₃ ] ? [t ₄ ] para mergesort, para que não haja mais inferências a serem feitas e a parte "unificação" do algoritmo de Hindley-Milner está completa. mergesort é do tipo [t ₃ ] ? [t ₄ ] com t ₄ em Ord.

É por isso que você tem:

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

(A descrição acima em termos de inferência lógica é equivalente ao que o algoritmo faz, mas a seqüência específica de passos do algoritmo segue é simplesmente que, dada na página da Wikipedia, por exemplo.)

Answer 2

Esse tipo pode ser inferido porque vê que você passe o resultado de mergesort para merge, que por sua vez compara as cabeças das listas com <, que faz parte do typeclass Ord. Assim, o tipo de razão inferência lata que ele deve retornar uma lista de uma instância de Ord. Claro, desde que ele realmente recurses infinitamente, não podemos inferir que qualquer outra coisa sobre o tipo que na verdade não voltar.