runST und functionszusammensetzung

Warum überprüft diese Art:

runST $ return $ True 

Während das Folgende nicht gilt:

 runST . return $ True 

GHCI beschwert sich:

 Couldn't match expected type `forall s. ST s c0' with actual type `m0 a0' Expected type: a0 -> forall s. ST s c0 Actual type: a0 -> m0 a0 In the second argument of `(.)', namely `return' In the expression: runST . return 

Die kurze Antwort ist, dass Typinferenz nicht immer mit höherrangigen Typen arbeitet. In diesem Fall ist es nicht möglich, den Typ von (.) Abzuleiten, aber der Typ prüft, ob wir eine explizite Typannotation hinzufügen:

 > :m + Control.Monad.ST > :set -XRankNTypes > :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool 

Das gleiche Problem tritt auch bei Ihrem ersten Beispiel auf, wenn wir ($) durch unsere eigene Version ersetzen:

 > let app fx = fx > :t runST `app` (return `app` True) :1:14: Couldn't match expected type `forall s. ST s t0' with actual type `m0 t10' Expected type: t10 -> forall s. ST s t0 Actual type: t10 -> m0 t10 In the first argument of `app', namely `return' In the second argument of `app', namely `(return `app` True)' 

Dies kann wiederum durch Hinzufügen von Typanmerkungen behoben werden:

 > :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool 

In GHC 7 gibt es eine spezielle Typisierungsregel, die nur für den Standardoperator ($) . Simon Peyton-Jones erläutert dieses Verhalten in einer Antwort auf die GHC-Benutzer-Mailingliste :

Dies ist ein motivierendes Beispiel für Typinferenz, das mit impredikativen Typen umgehen kann. Betrachten Sie den Typ von ($) :

 ($) :: forall p q. (p -> q) -> p -> q 

Im Beispiel müssen wir p mit (forall s. ST sa) instanziieren, und das bedeutet impredikativer Polymorphismus: Instanziieren einer Typvariablen mit einem polymorphen Typ.

Leider kenne ich kein System von vernünftiger Komplexität, das ohne Hilfe eine Überprüfung vornehmen kann. Es gibt viele komplizierte Systeme, und ich war Co-Autor in Papieren über mindestens zwei, aber sie sind alle zu Jolly Complicated, um in GHC zu leben. Wir hatten eine Implementierung von Boxy-Typen, aber ich nahm es bei der Implementierung des neuen Typcheckers heraus. Niemand hat es verstanden.

Aber die Leute schreiben so oft

 runST $ do ... 

dass ich in GHC 7 eine spezielle Tippregel implementiert habe, nur für Infix-Verwendungen von ($) . Stellen Sie sich einfach (f $ x) als neue syntaktische Form vor, mit der offensichtlichen Tippregel, und schon kann es losgehen.

Ihr zweites Beispiel schlägt fehl, weil es keine solche Regel für (.) .

Das Muster runST $ do { ... } ist so gebräuchlich, und die Tatsache, dass es normalerweise nicht runST $ do { ... } , ist so ärgerlich, dass GHC einige ST spezifische Typprüfungs-Hacks eingebaut hat, damit es funktioniert. Diese Hacks feuern wahrscheinlich hier für die ($) Version, aber nicht für die (.) Version.

Die Nachrichten sind ein wenig verwirrend den Punkt (oder so fühle ich). Lass mich deinen Code umschreiben:

 runST (return True) -- return True is ST s Bool (runST . return) True -- cannot work 

Eine andere Möglichkeit, dies zu setzen, ist, dass das monomorphe m0 a0 (das Ergebnis von return, wenn es ein a0 erhalten würde) nicht mit (forall s.ST sa) vereinheitlicht werden kann.