Hat Haskell einen "de-facto" Laufzeittyp?

Die Sprachfunktionen von Haskell unterstützen das Löschen von vollständigen -Typen. Die Idee ist, dass die Typisierungsregeln garantieren dass Code, der Typprüfung besteht, die folgenden zwei Eigenschaften ¹ :

1. Ein Wert eines Typs wird niemals an eine Funktion übergeben, die einen anderen Typ erwartet
2. Eine Funktion, die angibt, mit Werten eines Typs umzugehen, behandelt jeden möglichen Wert in diesem Typ

Die 2. Eigenschaft trägt sich weiter aus. Offensichtlich behandeln partielle Funktionen wie fromJust und head tatsächlich keinen möglichen Wert; Sie explodieren zur Laufzeit, wenn sie den falschen Wert erhalten. Aber sie explodieren auf "wohldefinierte" Weise, nachdem sie die Annahmen überprüft haben, von denen sie abhängen. Es ist nicht möglich, Code zu schreiben, der versucht, auf Unterstrukturen in Werten zuzugreifen, die diese Unterstruktur möglicherweise nicht haben, was Segmentierungsfehler verursachen oder zufällige Speicherbereiche interpretieren könnte, als wären sie eine andere Art von Daten.

Nachdem die Typprüfung erfolgreich ist, müssen keine Typinformationen im kompilierten Programm gespeichert werden. Ich fahre einfach die Typen weg. Ich habe bereits bewiesen, dass, wenn ich Code erzeuge, der Operationen an Daten blind ausführt, vorausgesetzt, dass es die erforderliche Form hat, dass nichts wirklich falsch läuft.

Beispiel Zeit!

Werte von Foo und Bar werden wahrscheinlich im Speicher identisch dargestellt ² ; Sobald Sie wissen, dass alle Werte korrekt sind, sind alle Informationen, die zum Definieren dieser Werte benötigt werden, jeweils Int und String . Wenn Sie sich einen Speicherabzug eines laufenden Haskell-Programms ansehen, können Sie nicht erkennen, ob ein bestimmtes Speicherobjekt, das einen Verweis auf ein Int und ein String enthält, ein Foo oder ein Bar ist (oder in der Tat ein (Int, String) oder irgendein anderer einfacher Konstruktortyp mit zwei Feldern, die Int bzw. String sind).

Also nein, Haskell-Typen existieren zur Laufzeit in keiner Form.

¹ Sie können diese Eigenschaften natürlich mit unsicheren Features wie unsafeCoerce ; Ich spreche von "normalem" Haskell-Code hier.

2 Oder sie dürfen nicht. Haskell-the-Language macht keinerlei Garantie für die Darstellung zur Laufzeit, und es wäre durchaus möglich, die Felder in einer anderen Reihenfolge zu speichern oder etwas anderes zu tun, das die beiden unterscheiden könnte. Aber ich gehe davon aus, dass es in Abwesenheit von irgendeinem Grund, diese beiden Arten gleich zu behandeln.

Die "Run-Time-Typen", die in beliebigen kompilierten Programmen verwendet werden, sind unabhängig von der Ausgangssprache die vom Zielprozessor nativ unterstützten Typen: In der Regel Ganzzahlen (signiert und unsigniert), Zeiger (wirklich einfach eine spezielle Verwendung von Ganzzahlen) und Fließkommazahlen (typischerweise IEEE754 ). Der Compiler übersetzt alle Operationen im Quellprogramm in eine äquivalente Reihe von Operationen unter Verwendung dieser grundlegenden hardwaregestützten Typen.

Anspruchsvollere Datentypen (z. B. Haskell-Listen) werden zur Laufzeit als Datenstrukturen dargestellt, die aus Basistypen erstellt werden. Zum Beispiel kann jeder Knoten in einer Liste durch ein Paar von Zeigern repräsentiert werden: einen zu dem Wert, der von diesem Knoten gehalten wird (oder ein Thunk zum Berechnen desselben), und einer zum nächsten Knoten (oder einem Thunk). Durch die statische Typprüfung des Compilers kann sichergestellt werden, dass auf jede dieser Laufzeitdatenstrukturen nur durch Code zugegriffen wird, der sie richtig verarbeitet. Beispielsweise wird eine Speicherregion, die ein Zeigerpaar für einen Listenknoten enthält, nicht fälschlicherweise als Thunk zum Berechnen einer Ganzzahl behandelt, da der Compiler nur die Übergabe der Liste an Funktionen ermöglicht, die ein Listenargument erwarten.

Informationen zur Laufzeit finden sich häufig in Implementierungen von OOP-Sprachen, die mit jedem Objekt ein "Typ-Tag" enthalten. Mit solchen Informationen kann man beispielsweise Code wie

ist eine Form der Laufzeittypprüfung. Das "type tag" kommt oft kostenlos, da jedes Objekt einen Zeiger auf die virtuelle Methodentabelle benötigt und das allein den Laufzeittyp des Objekts identifiziert.

In Haskell besteht jedoch keine Notwendigkeit für ein solches Tag oder für Zeiger auf VMTs. Die Sprache wurde ohne irgendeine Art von instanceof -Operator entworfen, so dass Implementierungen zur Laufzeit kein Typen-Tag bereitstellen müssen. Dies führt auch zu einer schöneren zugrundeliegenden Theorie, da wir Parameter-Garantien auf Code erhalten, auch bekannt als "Theoreme for free!". Zum Beispiel die folgende Funktion

kann nicht implementiert werden, sodass f [1,2] = [2,3] . Dies liegt daran, dass es nachweislich keine Möglichkeit gibt, 3 für f zu erzeugen. Die Intuition ist, dass f ein a erzeugen muss und nicht a=Int zur Laufzeit prüfen kann (keine Typ-Tags), sodass die Ausgabe von f nur Elemente enthalten kann, die in der Eingabe gefunden werden. Diese Garantie kommt nur von der obigen Eingabe, ohne auch nur darauf zu achten, wie f tatsächlich implementiert ist.

Wenn Sie wirklich eine instanceof Entsprechung möchten, können Sie Typeable dafür verwenden:

Dies gibt [2,3] für alle nicht leeren Listen zurück, wenn ganze Zahlen angegeben sind. Zur Laufzeit wird ein Typ-Tag übergeben, sodass a=Int überprüft werden kann.

Nein. Eine grundlegende Eigenschaft von Haskell ist newtype Deklarationen, wie

haben keinen Laufzeit-Overhead, was bedeutet, dass der Konstruktor MyInt im wahrsten Sinne des Wortes das gleiche Argument (was auch immer es ist) zurückgibt, und der Compiler behandelt es wie einen anderen Typ. (Wenn Sie sich den kompilierten Code anschauen, sehen Sie nach der Optimierung keine Anweisungen, um den Funktionsaufruf MyInt zu implementieren.) Dies bedeutet, dass nur ein "De-Faktor" -Laufzeittyp eines Objekts in Haskell verwendet werden kann bis zur Äquivalenz zwischen einem newtype und seiner Implementierung definiert werden.