runST mit Hindley-Milner-System
Wenn ich die ST-Monade in Haskell richtig verstehe, verwendet runST geschickt Rank-2-Typen, um sicherzustellen, dass eine Berechnung keinen anderen Thread referenziert, wenn sie der Monade entkommt.
Ich habe eine Spielzeugsprache mit einem System vom Typ Hindley-Milner, und meine Frage lautet wie folgt: Ist es möglich, das HM-Typsystem mit einer Ad-hoc-Regel zur Eingabe von runST -Anwendungen zu erweitern, so dass die ST-Monade ist sicher escapable, ohne Einführung von Rang-2-Typen?
Genauer gesagt hätte runST den Typ forall s a. ST s a -> a (dh rank-1) und die Typisierungsregel würde zuerst versuchen, den Berechnungstyp auf die gleiche Weise zu verallgemeinern. HM generalisiert Typen in let-Ausdrücken, löst aber einen Typfehler aus Wenn festgestellt wird, dass die Variable s type gebunden ist.
Das obige beschränkt nur akzeptierte Programme im Vergleich zu Vanilla HM, also klingt es vernünftig, aber ich bin unsicher. Würde das funktionieren?
1 Antwort
Nur für den Fall, dass die Kommentare zu der Frage nicht ganz klar sind, ist das Urteil, das Sie benötigen,
Dies steht natürlich in Verbindung mit den anderen üblichen Tippurteilen, die mit Hindley-Milner . Interessanterweise müssen wir schließlich keine speziellen Regeln für irgendeinen einführen, der einen ST -Typ einführt, da keiner von diesen Typensignaturen von Rang 2 benötigt:
Tags und Links haskell hindley-milner monads