OCaml - Was ist ein ungesunder Typ?

Question

Vor kurzem wurde ich den Code gegeben

List.fold_left (fun acc x -> raise x ; acc) 3 

Ich bin völlig in Ordnung mit dieser Teil Anwendung einen funktionalen Wert von> Typ EXN Liste mit -> int, und der Tatsache, dass es eine Warnung liefert, ist nicht überraschend, . Ich bin> aber nicht sicher, was die Hälfte der Warnung bedeutet:

Warning 21: this statement never returns (or has an unsound type.) 

Ich kann nicht wirklich auf diese Warnung jeden Hinweis finden, wo es nicht das Ergebnis einer nicht-wiederkehrende Aussage. Selbst die man-Seite für ocamlc erwähnt nur nicht zurückkehrende Anweisungen für diese Warnung und warnings.ml verweist darauf lediglich als Nonreturning-Anweisung.

Ich bin mit dem Konzept der Solidität vertraut, da es sich auf Typsysteme bezieht, aber die Vorstellung, dass ein Typ an sich inhärent ist, erscheint mir seltsam.

Also meine Fragen sind:

Was genau eine unsolide Typ ist? In welcher Situation würde es zu einem unsauberen Typ kommen, wenn OCaml nur eine Warnung ausgibt und nicht sofort ausfällt?

Jemand hat diese Frage gepostet, und während ich eine Antwort schrieb, wurde sie gelöscht. Ich glaube, die Frage ist sehr interessant und lohnt sich für das Umschreiben. Bitte beachten Sie haben jemanden, der bereit ist, Ihnen zu helfen :-(

Answer 1

Wie Warning 21

Zuerst berichtet wird, lassen Sie uns von Funktionen denken, die in keinem Zusammenhang 'a zurückgibt: Ich meine nicht funktionieren wie let id x = x hier da es 'a -> 'a Typ und der Rückgabetyp 'a bezieht sich mit der Eingabe. I-Funktionen bedeuten, wie raise : exn -> 'a und exit : int -> 'a.

Diese Funktionen geben in keinem Zusammenhang 'a gelten als nie wiederkommen. Da der Typ 'a (genauer forall 'a. 'a) hat keine Bürger. Die Funktionen können nur das Programm beenden (beenden oder eine Ausnahme auslösen) oder in eine Endlosschleife fallen: let rec loop() = loop().

Warnung 21 wird erwähnt, wenn der Typ einer Anweisung 'a ist. (Eigentlich ist es eine weitere Bedingung, aber ich einfach überspringen für Einfachheit.) Zum Beispiel

# loop(); print_string "end of the infinite loop";; 
Warning 21: this statement never returns (or has an unsound type.) 

Dies ist der Hauptzweck 21. Dann der Warnung, was in der zweiten Hälfte ist?

"Unsound Typ"

Warnung 21 kann, selbst wenn die Aussage kehrt etwas tatsächlich gemeldet werden. In diesem Fall weist die Warnmeldung darauf hin, dass die Anweisung einen ungültigen Typ aufweist.

Warum unsäglich? Da der Ausdruck einen Wert vom Typ forall 'a. 'a zurückgibt, der keinen Bürger hat. Es bricht die Basis der Typtheorie, von der OCaml abhängt.

In OCaml gibt sind mehrere Möglichkeiten, einen Ausdruck mit einer solchen ungesunden Art zu schreiben:

Verwendung von Obj.magic. Es Schrauben Typ-System daher können Sie einen Ausdruck des Typs 'a schreiben, die zurückgibt:

(Obj.magic 1); print_string "2" 

Verwendung von external. Die gleichen wie Obj.magic können Sie beliebige Art an externen Werten und Funktionen geben:

external crazy : unit -> 'a = "%identity" 
let f() = crazy() (* val f : unit -> 'a *) 
let _ = f(); print_string "3" 

Für OCaml Typ-System, ist es unmöglich, nicht-wiederkehrende Ausdrücke und Ausdrücke mit ungesunden Typen zu unterscheiden. Aus diesem Grund kann es nicht ausschließen, dass unrichtige Dinge als Fehler angesehen werden. Das Verfolgen der Definitionen, um eine Aussage zu sagen, hat einen ungesunden Typ oder nicht, ist im Allgemeinen auch unmöglich und kostet viel, selbst wenn es möglich ist.