Wann tritt in OCaml die lockere Wertbeschränkung ein?

Ich bin kein Typentheoretiker, aber hier ist meine Interpretation von Garrigues Erklärung. Sie haben einen Wert V. Beginnen Sie mit dem Typ, der V (in OCaml) unter der üblichen Werteinschränkung zugewiesen würde. Es wird eine Anzahl (vielleicht 0) monomorphe Typvariablen in dem Typ geben. Für jede solche Variable, die nur in kovarianter Position im Typ (auf der rechten Seite der Funktionspfeile) erscheint, können Sie sie durch eine vollständig polymorphe Typvariable ersetzen.

Das Argument lautet wie folgt. Da Ihre monomorphe Variable eine Variable ist, können Sie sich vorstellen, sie durch einen einzelnen Typ zu ersetzen. Sie wählen also einen unbewohnten Typ U. Jetzt, da er nur in kovarianter Position ist, kann U wiederum durch einen beliebigen Supertyp ersetzt werden. Aber jeder Typ ist ein Supertyp eines unbewohnten Typs, daher ist es sicher, ihn durch eine vollständig polymorphe Variable zu ersetzen.

Die lockere Werteinschränkung tritt also ein, wenn monomorphe Variablen vorhanden sind, die nur in kovarianten Positionen vorkommen.

(Ich hoffe, ich habe das richtig. Gewiss, @gasche würde es besser machen, wie Octref es vorschlägt.)

Jeffrey lieferte die intuitive Erklärung, warum die Entspannung richtig ist. Wenn es nützlich ist, denke ich, dass wir zuerst die Antwort octref reproduzieren können, die hilfreich verknüpft ist mit:

  

Sie können diese Feinheiten sicher ignorieren, bis Sie eines Tages ein Problem mit einem abstrakten Typ von Ihnen haben, der nicht so polymorph ist, wie Sie möchten, und dann sollten Sie sich daran erinnern, dass eine Kovarianz-Annotation in der Signatur helfen kann. p>      

Wir haben diese auf reddit / ocaml vor ein paar Monaten besprochen:

     

Betrachten Sie das folgende Codebeispiel:

%Vor%      

Der Typ, den Sie für test erhalten, ist '_a C.collection anstatt der 'a C.collection , die Sie erwarten würden. Es ist kein polymorpher Typ ( '_a ist eine monomorphe Inferenzvariable, die noch nicht vollständig bestimmt ist), und Sie werden in den meisten Fällen nicht damit zufrieden sein.

     

Dies liegt daran, dass C.empty () kein Wert ist, daher ist sein Typ nicht verallgemeinert (~ wurde polymorph gemacht). Um von der Lockerung der Wertbeschränkung zu profitieren, müssen Sie den abstrakten Typ 'a collection covariant:

markieren %Vor%      

Das passiert natürlich nur, weil das Modul C mit der Signatur S : module C : S = ... versiegelt ist. Wenn das Modul C keine explizite Signatur erhalten würde, würde das Typsystem die allgemeinste Varianz (hier Kovarianz) ableiten und das würde man nicht bemerken.

     

Das Programmieren gegen eine abstrakte Schnittstelle ist oft nützlich (wenn man einen Funktor definiert oder eine Disziplin vom Phantomtyp durchsetzt oder modulare Programme schreibt), so dass diese Art von Situation definitiv passiert und es dann nützlich ist, über die lockere Werteinschränkung Bescheid zu wissen / p>

Das ist ein Beispiel dafür, wenn Sie sich dessen bewusst sein müssen, um mehr Polymorphie zu erhalten, weil Sie eine Abstraktionsgrenze (eine Modul-Signatur mit einem abstrakten Typ) einrichten und es nicht automatisch funktioniert, müssen Sie dies explizit sagen Der abstrakte Typ ist kovariant.

In den meisten Fällen passiert es ohne Ihre Nachricht, wenn Sie polymorphe Datenstrukturen manipulieren. [] @ [] hat nur den polymorphen Typ 'a list dank der Relaxation.

Ein konkretes, aber fortgeschritteneres Beispiel ist Olegs Ber-MetaOCaml, die einen Typ ('cl, 'ty) code verwendet, um zitierte Ausdrücke darzustellen, die stückweise erstellt werden. 'ty repräsentiert den Typ des Ergebnisses des zitierten Codes, und 'cl ist eine Art Phantom-Region-Variable, die garantiert, dass das Scoping der Variablen im Code in Anführungszeichen korrekt ist, wenn es polymorph bleibt. Da dies in Situationen, in denen zitierte Ausdrücke durch das Zusammensetzen anderer zitierter Ausdrücke (also in der Regel keine Werte) erstellt werden, auf Polymorphismus beruht, würde es ohne die entspannte Werteinschränkung grundsätzlich nicht funktionieren (es ist eine Nebenbemerkung in seinem ausgezeichneten, aber technischen Dokument zu Typinferenz.

Die Frage, warum die beiden im Anhang genannten Beispiele anders getippt sind, hat mich ein paar Tage lang verwirrt. Hier ist, was ich gefunden habe, indem ich in den Code des OCaml-Compilers gegraben habe (Disclaimer: Ich bin weder ein Experte für OCaml noch für das ML-Typ-System).

Wiederholen

erhält einen polymorphen Typ (think ∀ α. unit → α option ref ) während

erhält einen monomorphen Typ (think unit → α option ref , dh die Typvariable α wird nicht allgemein quantifiziert).

Intuition

Zum Zweck der Typprüfung sieht der OCaml-Compiler keinen Unterschied zwischen Beispiel (2) und

da es nicht in den Körper von let schaut, um zu sehen, ob die gebundene Variable tatsächlich verwendet wird (wie man es erwarten könnte). Aber (3) muss eindeutig muss einen monomorphen Typ erhalten, andernfalls könnte eine polymorph eingegebene Referenzzelle entkommen, was möglicherweise zu einem fehlerhaften Verhalten wie Speicherkorruption führen könnte.

Erweiterbarkeit

Um zu verstehen, warum (1) und (2) so geschrieben sind, wie sie sind, sehen wir uns an, wie der OCaml-Compiler tatsächlich prüft, ob ein let -Ausdruck ein Wert ist (dh "nicht-expansiv") oder nicht (siehe is_nonexpansive ):

Also ein let -Ausdruck ist ein Wert, wenn sowohl sein Körper als auch alle gebundenen Variablen Werte sind.

In beiden im Addendum angegebenen Beispielen ist der Körper fun () -> ref None , was eine Funktion und somit ein Wert ist. Der Unterschied zwischen den beiden Codeteilen besteht darin, dass 3 ein Wert ist, während ref 3 dies nicht ist. Daher berücksichtigt OCaml den ersten let einen Wert, aber nicht den zweiten.

Eingabe

Wenn wir uns wieder den Code des OCaml-Compilers ansehen, können wir feststellen, ob ein Ausdruck als expansiv betrachtet wird, wie der Typ der let -Ausdrücke verallgemeinert wird (siehe Typ_Ausdruck ):

Da let _x = 3 in (fun () -> ref None) nicht erweiterbar ist, wird es mit generalize eingegeben, was einen polymorphen Typ ergibt. let _x = ref 3 in (fun () -> ref None) dagegen wird über generalize_expansive eingegeben und erhält einen monomorphen Typ.

Das ist soweit ich gekommen bin. Wenn Sie noch tiefer graben wollen, lesen Sie Oleg Kiselyovs Effiziente und aufschlussreiche Generalisierung neben generalize und generalize_expansive sei ein guter Anfang.

Vielen Dank an Leo White von OCaml Labs Cambridge für die Ermutigung, mit dem Graben zu beginnen!