Ich bin auf viele Erklärungen des RunST-Rank-2-Typs gestoßen und wie er verhindert, dass die Referenz RunST entgeht. Aber ich konnte nicht herausfinden, warum dies auch den folgenden Code von Typprüfung verhindert (was richtig ist, aber ich will immer noch verstehen, wie es das macht):
%Vor%Im Vergleich zu:
%Vor% Mir scheint, dass der Typ von newSTRef für beide Fälle gleich ist: Λs. Bool → ST s (STRef s Bool) . Und der Typ von v ist in beiden Fällen auch ∃s. STRef s Bool , wenn ich es richtig verstehe. Aber dann bin ich verwirrt darüber, was ich als Nächstes tun soll, um zu zeigen, warum das erste Beispiel keine Überprüfung gibt. Ich sehe keine Unterschiede zwischen beiden Beispielen, außer dass v im ersten Beispiel außerhalb von runST gebunden ist und innerhalb der Zweitens, was ich vermute, ist der Schlüssel hier. Bitte helfen Sie mir, dies zu zeigen und / oder mich zu korrigieren, wenn ich mich irgendwo in meiner Argumentation irre.
Die Funktion runST :: (forall s . ST s a) -> a ist der Ort, an dem die Magie auftritt. Die richtige Frage ist, was es braucht, um eine Berechnung vom Typ forall s . ST s a zu erstellen.
Wenn Sie es als Englisch lesen, ist dies eine Berechnung, die für alle Optionen von s gilt, die Phantomvariable, die einen bestimmten "Thread" von ST computation anzeigt.
Wenn du newSTRef :: a -> ST s (STRef s a) benutzt, produzierst du STRef , das seine Thread-Variable mit dem ST -Thread teilt, der es generiert. Das bedeutet, dass der s -Typ für den Wert v identisch mit dem s -Typ für den größeren Thread ist. Diese Fixiertheit bedeutet, dass Operationen, die v enthalten, nicht mehr "für alle" Optionen des Threads s gültig sind. Daher verweigert runST Vorgänge mit v .
Umgekehrt ist eine Berechnung wie newSTRef True >>= \v -> readSTRef v in jedem ST -Thread sinnvoll. Die gesamte Berechnung hat einen Typ, der "für alle" ST threads s gilt. Dies bedeutet, dass es mit runST ausgeführt werden kann.
Im Allgemeinen muss runST die Erstellung aller ST -Threads umschließen. Dies bedeutet, dass alle Optionen von s im Argument bis runST beliebig sind. Wenn etwas aus dem Kontext von runST mit dem Argument von runST interagiert, dann werden wahrscheinlich einige dieser Optionen von s an den umgebenden Kontext angepasst und sind somit nicht länger "für alle" Optionen von% co_de frei anwendbar %.