Warum wird nicht standardmäßig (RankNTypes-Verwendung) angewendet?

8

Ich bin mit forall nicht so vertraut, habe aber kürzlich diese Frage gelesen: Was macht das 'forall' Keyword in Haskell / GHC?

In einer der Antworten ist dieses Beispiel:

%Vor%

Die Erklärung ist gut und ich verstehe was forall hier macht. Aber ich frage mich, gibt es einen bestimmten Grund, warum dies nicht das Standardverhalten ist. Gibt es jemals eine Zeit, in der es nachteilig wäre?

Edit: Ich meine, gibt es einen Grund, warum die Foralls nicht standardmäßig eingefügt werden können?

    
Peter Hall 12.04.2012, 17:58
quelle

2 Antworten

16

Nun, es ist nicht Teil des Haskell 2010-Standards, daher ist es standardmäßig nicht aktiviert und wird stattdessen als Spracherweiterung angeboten. Was die Gründe dafür betrifft, warum es nicht im Standard ist, sind Rang-n-Typen ziemlich viel schwieriger zu implementieren als der normale Rang-1-Typ-Standard, den Haskell hat; sie werden auch nicht so oft benötigt, so dass der Ausschuss sich aus Gründen der Sprache und der Einfachheit der Umsetzung wahrscheinlich nicht mit ihnen beschäftigen würde.

Das bedeutet natürlich nicht, dass Rang-n-Typen nicht nützlich sind; sie sind sehr, und ohne sie hätten wir keine wertvollen Werkzeuge wie die ST monad (bietet einen effizienten, lokal veränderbaren Zustand - wie IO , wo Sie nur IORef s verwenden können). Aber sie fügen der Sprache einiges an Komplexität hinzu und können merkwürdiges Verhalten verursachen, wenn scheinbar sinnvolle Code-Transformationen angewendet werden. Zum Beispiel erlauben einige Rang-n-Typüberprüfer runST (do { ... }) , aber ablehnen runST $ do { ... } , obwohl die zwei Ausdrücke immer gleich sind ohne Rang-n-Typen. Siehe diese SO-Frage für ein Beispiel für das Unerwartete (und manchmal lästiges) Verhalten, das es verursachen kann.

Wenn Sie, wie bei sepp2k gefragt, stattdessen fragen, warum forall explizit zu Typ-Signaturen hinzugefügt werden muss, um die erhöhte Allgemeinheit zu erhalten, ist das Problem, dass (forall x. x -> f x) -> (a, b) -> (f a, f b) tatsächlich ein restriktiverer Typ als (x -> f x) -> (a, b) -> (f a, f b) ist. Mit letzterem können Sie jede Funktion der Form x -> f x (für jede f und x ) übergeben, aber bei der ersten muss die übergebene Funktion für alle % funktionieren. Code%. So wäre zum Beispiel eine Funktion vom Typ x ein zulässiges Argument für die zweite Funktion, aber nicht die erste; Es müsste stattdessen der Typ String -> IO String sein. Es wäre ziemlich verwirrend, wenn letzterer automatisch in den ersten umgewandelt würde! Sie sind zwei sehr unterschiedliche Typen.

Es könnte sinnvoller sein, wenn das implizite a -> IO a s explizit gemacht wird:

%Vor%     
ehird 12.04.2012, 18:00
quelle
7

Ich vermute, dass Typen mit höherem Rang nicht standardmäßig aktiviert sind, weil die Typrückschlüsse unentscheidbar machen . Aus diesem Grund müssen Sie auch bei aktivierter Erweiterung das Schlüsselwort forall verwenden, um einen höherrangigen Typ zu erhalten. GHC geht davon aus, dass alle Typen Rang 1 sind, sofern nicht ausdrücklich anders angegeben, um so viele Typinformationen ableiten zu können möglich.

Mit anderen Worten, es gibt keine allgemeine Möglichkeit, einen höherrangigen Typ (forall x. x -> f x) -> (a,b) -> (f a, f b) abzuleiten. Der einzige Weg, diesen Typ zu erhalten, ist eine explizite Typ-Signatur.

Edit: Laut Vitus 'obigen Kommentaren ist der Typ-2-Inferenzwert entscheidbar, aber der Polymorphismus höheren Rangs ist dies nicht. Daher ist diese Typensignatur technisch ableitbar (obwohl der Algorithmus komplexer ist). Ob die zusätzliche Komplexität, die es ermöglicht, polymorphe Typ-2-Folgerungen zu ermöglichen, sinnvoll ist, ist fraglich ...

    
John L 12.04.2012 20:03
quelle

Tags und Links