Abgeleitete Typ erscheint eine Endlosschleife zu erkennen, aber was geschieht wirklich?

Question

In Andrew Koenig eine Anekdote über Typinferenz ML verwendet der Autor Implementierung von für ML Art als Lernübung fusionieren und freut sich, ein finden „falsch“ Typinferenz.

  

Zu meiner großen Überraschung, der Compiler berichtete eine Art

'a list -> int list

     

Mit anderen Worten, diese Sortierfunktion akzeptiert eine Liste von jeder Art überhaupt und gibt eine Liste von ganzen Zahlen.

     

Das ist unmöglich. Der Ausgang muss eine Permutation der Eingabe sein; wie kann es möglicherweise eine andere Art haben? Der Leser wird sicherlich meinen ersten Impuls vertraut finden: Ich fragte mich, ob ich einen Fehler im Compiler aufgedeckt hatte

     

darüber etwas mehr Nach einigem Nachdenken erkannte ich, dass es eine andere Art und Weise war, in der die Funktion ihr Argument ignorieren könnte: vielleicht manchmal ist es gar nicht zurück. Ja, als ich es versuchte, das ist genau das, was passiert ist. sort(nil) haben nil zurück, aber jede nicht-leere Liste Sortierung in eine unendliche Rekursion Schleife gehen würde

Wenn übersetzt 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 folgert eine ähnliche Art:

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

Wie funktioniert die Damas-Hindley-Milner-Algorithmus dieser Art schließen ?

Answer 1

Dies ist in der Tat ein bemerkenswertes Beispiel; eine unendliche Schleife erkannt wird, im Wesentlichen in kompilieren Zeit ! Es ist nichts Besonderes über die Hindley-Milner-Inferenz in diesem Beispiel; es geht nur wie üblich.

Beachten Sie, dass ghc die Arten von split und merge bekommt richtig:

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

Nun, wenn es um mergesort kommt, ist es in der Regel eine Funktion t ₁ → t ₂ für einige Typen t ₁ und t ₂ . Dann sieht er die erste Zeile:

mergesort [] = []

und erkennt, dass t ₁ und t ₂ muss Listentypen sein, sagt t ₁ = [t ₃ ] und t ₂ = [t ₄ ]. So muss mergesort eine Funktion sein [t ₃ ] → [t ₄ ]. Die nächste Zeile

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

sagt, dass:

• xs muss ein Eingang zu spalten, das heißt, vom Typ [A] für ein a (was es ohnehin schon ist, für a = t ₃ ).
• So p und q sind ebenfalls vom Typ [t ₃ ], da split ist [a] → ([a], [a])
• mergesort p daher (man erinnere sich, dass mergesort angenommen wird vom Typ sein [t ₃ ] → [t ₄ ]) vom Typ [t ₄ ].
• mergesort q ist vom Typ [t ₄ ] für genau den gleichen Grund.
• AS merge hat (Ord t) => [t] -> [t] -> [t] eingeben, und die Eingänge in der Expression merge (mergesort p) (mergesort q) sind beide vom Typ [t ₄ ], der Typ t ₄ muss in Ord werden.
• Schließlich ist die Art der merge (mergesort p) (mergesort q) dieselben wie beide seiner Eingänge, nämlich [t ₄ ]. Das paßt mit der bisher bekannten Art [t ₃ ] → [t ₄ ] für mergesort, so gibt es keine mehr Schlüsse und die "Vereinigung" Teil der getan werden Hindley-Milner-Algorithmus ist abgeschlossen. mergesort ist vom Typ [t ₃ ] → [t ₄ ] mit t ₄ in Ord.

Das ist, warum Sie bekommen:

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

(Die obige Beschreibung in Bezug auf die logische Folgerung ist, entspricht dem, was der Algorithmus tut, aber die spezifische Abfolge von Schritten der Algorithmus folgt, ist einfach, dass zum Beispiel auf der Wikipedia-Seite angegeben.)

Answer 2

können Diese Art abgeleitet werden, weil sie sieht, dass Sie das Ergebnis der mergesort merge passieren, was wiederum die Köpfe der Listen mit < vergleicht, die einen Teil des Ord ist typeclass. So ist die Typinferenz kann vermuten, dass es eine Liste von einer Instanz von Ord zurückkehren. Natürlich, da es tatsächlich unendlich recurses, können wir nichts anderes über die Art schließen es nicht tatsächlich zurück.