runST mit Hindley-Milner-Typ-System

Question

Wenn ich die ST-Monade in Haskell richtig verstehe, verwendet runST Rank-2-Typen in einer cleveren Weise, um sicherzustellen, dass eine Berechnung keinen anderen Thread bei der Flucht aus der Monade verweist.

Ich habe eine Spielzeugsprache mit einem Hindley-Milner-System, und meine Frage ist folgende: Ist es möglich, das HM-System mit einer Ad-hoc-Regel für die Eingabe von runST Anwendungen zu erweitern, so dass die ST Monad sicher ist Escapeable, ohne Einführung von Rang-2-Typen?

Genauer gesagt, würde runST Art hat forall s a. ST s a -> a (dh Rang-1) und die Typisierung Regel würde zuerst versuchen, die Berechnungsart in der gleichen Art und Weise HM-Typen zu verallgemeinern in let-Ausdrücke verallgemeinert, aber eine Art Fehler, wenn die erhöhen s Typ Variable wird gefunden, gebunden zu sein.

Das obige beschränkt nur akzeptiert Programme im Vergleich zu Vanille HM, so scheint es gesund, aber ich bin mir nicht sicher. Würde das funktionieren?

Answer 1

Gerade falls die Kommentare auf die Frage nicht ganz klar, das Urteil man braucht ist

Dies ist natürlich in Verbindung mit den anderen üblichen Typisierung Urteilen, die mit Hindley-Milner kommen. Interessanterweise haben wir da keine von diesen erfordern Typ nicht am Ende brauchen, um spezielle Regeln für etwas Einführung eine ST Art zu machen, Unterschriften von Rang 2:

newSTRef :: a -> ST s (STRef s a) 
readSTRef :: STRef s a -> ST s a 
writeSTRef :: STRef s a -> a -> ST s() 
...