Il tipo dedotto sembra rilevare un ciclo infinito, ma cosa sta realmente accadendo?

Question

In Andrew Koenig Un aneddoto sull'inferenza del tipo ML, l'autore utilizza l'implementazione di unisci ordinamento come esercizio di apprendimento per il ML ed è lieto di trovare un'inferenza di tipo "errato".

Con mia grande sorpresa, il compilatore ha riportato un tipo di

'a list -> int list

In altre parole, questa funzione di ordinamento accetta un elenco di qualsiasi tipo e restituisce un elenco di numeri interi.

Questo è impossibile.L'output deve essere una permutazione dell'input;come può essere di tipo diverso?Il lettore troverà sicuramente familiare il mio primo impulso:Mi chiedevo se avevo scoperto un bug nel compilatore!

Dopo averci pensato ancora un po', mi sono reso conto che esisteva un altro modo in cui la funzione poteva ignorare il proprio argomento:forse a volte non ritornava affatto.In effetti, quando l'ho provato, è esattamente quello che è successo: sort(nil) è tornato nil, ma l'ordinamento di qualsiasi elenco non vuoto entrerebbe in un ciclo di ricorsione infinito.

Quando tradotto in 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 deduce un tipo simile:

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

Come funziona il Algoritmo di Damas-Hindley-Milner dedurre questo tipo?

Answer 1

Questo è davvero un esempio notevole;viene rilevato un ciclo infinito, essenzialmente, a tempo di compilazione!Non c'è nulla di speciale nell'inferenza Hindley-Milner in questo esempio;procede come al solito.

Tieni presente che ghc ottiene i tipi di split E merge correttamente:

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

Ora quando si tratta di mergesort, è, in generale, una funzione t₁→ t₂ per alcuni tipi t₁ e T₂.Quindi vede la prima riga:

mergesort [] = []

e si rende conto che t₁ e T₂ devono essere tipi di elenco, ad esempio t₁=[t₃] e T₂=[t₄].Quindi il mergesort deve essere una funzione [t₃]→[t₄].La riga successiva

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

gli dice che:

• xs deve essere un input da dividere, cioè di tipo [a] per qualche a (che lo è già, per a=t₃).
• COSÌ p E q sono anche del tipo [t₃], Da split è [a]→([a],[a])
• mergesort p, quindi, (ricordiamo che si ritiene che il mergesort sia di tipo [t₃]→[t₄]) è del tipo [t₄].
• mergesort q è del tipo [t₄] esattamente per lo stesso motivo.
• COME merge ha tipo (Ord t) => [t] -> [t] -> [t], e gli input nell'espressione merge (mergesort p) (mergesort q) sono entrambi del tipo [t₄], il tipo t₄ deve essere dentro Ord.
• Infine, il tipo di merge (mergesort p) (mergesort q) è uguale ad entrambi i suoi input, vale a dire [t₄].Questo si adatta al tipo precedentemente noto [t₃]→[t₄] per mergesort, quindi non ci sono più inferenze da fare e la parte di "unificazione" dell'algoritmo Hindley-Milner è completa. mergesort è del tipo [t₃]→[t₄] con T₄ In Ord.

Ecco perché ottieni:

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

(La descrizione sopra in termini di inferenza logica è equivalente a ciò che fa l'algoritmo, ma la sequenza specifica di passaggi che l'algoritmo segue è semplicemente quella fornita nella pagina Wikipedia, ad esempio.)

Answer 2

Quel tipo può essere dedotto perché vede che passi il risultato di mergesort A merge, che a sua volta confronta i capilista con <, che fa parte della classe tipografica Ord.Quindi l'inferenza del tipo può far sì che debba restituire un elenco di un'istanza di Ord.Naturalmente, dal momento che in realtà ricorre all'infinito, non possiamo dedurre nient'altro sul tipo che in realtà non restituisce.