Dynamische Bindung mit einer Ref-Zelle

Question

Ich verstehe, dass Sie dies nicht tun können, aber genau warum verstehen wollen.

module M : sig 
    type 'a t 
    val call : 'a t -> 'a option 
end = struct 
    type 'a t 
    let state : ('a t -> 'a option) ref = ref (fun _ -> None) 
    let call : ('a t -> 'a option) = fun x -> !state x 
end 

Ergebnisse in:

Error: Signature mismatch: 
Modules do not match: 
    sig 
     type 'a t 
     val state : ('_a t -> '_a option) ref 
     val call : '_a t -> '_a option 
    end 
is not included in 
    sig 
     type 'a t 
     val call : 'a t -> 'a option 
    end 

    Values do not match: 
     val call : '_a t -> '_a option 
    is not included in 
     val call : 'a t -> 'a option 

Warum sind die abstrakten Typen hier nicht kompatibel?

Mein Bauchgefühl sagt mir, dass es alles mit der frühen vs späten Bindung zu tun hat, aber ich suche nach einer genauen Beschreibung dessen, was das Typsystem hier macht.

Answer 1

Eine Möglichkeit, es zu betrachten, ist, dass Ihr Feld state nicht den polymorphen Wert haben kann, den Sie ihm zuschreiben, weil veränderbare Werte nicht polymorph sein können. Referenzen sind höchstens monomorph (wie durch die Notation '_a für die Typvariable angegeben).

Wenn Sie nur versuchen, eine ähnliche Referenz in der Toplevel zu erklären, werden Sie den gleichen Effekt sehen:

# let lfr: ('a list -> 'a option) ref = ref (fun x -> None);; 
val lfr : ('_a list -> '_a option) ref = {contents = <fun>} 

Die Variable vom Typ '_a gibt einige einzelne Art, die noch nicht bestimmt worden ist.

Der Grund, warum Referenzen nicht polymorph sein können, ist, dass es nicht stichhaltig ist. Wenn Sie zulassen, dass Verweise verallgemeinert werden (polymorph), ist es einfach, Programme zu erzeugen, die schrecklich schief gehen. (In der Praxis bedeutet dies normalerweise einen Crash- und Core-Dump.)

Das Problem der Solidität wird am Anfang dieses Artikels diskutiert: Jacques Garrigue, Relaxing the Value Restriction (auf das ich mich regelmäßig beziehe, wenn ich vergesse, wie die Dinge funktionieren).

aktualisieren

Was ich glaube, Sie wollen, ist "Rang 2 Polymorphismus". Das heißt, Sie wollen ein Feld, dessen Typ polymorph ist. Sie können das in OCaml tatsächlich erhalten, solange Sie den Typ deklarieren. Die übliche Methode ist, einen Datensatztyp zu verwenden:

# type lfrec = { mutable f: 'a. 'a list -> 'a option };; 
type lfrec = { mutable f : 'a. 'a list -> 'a option; } 
# let x = { f = fun x -> None };; 
val x : lfrec = {f = <fun>} 
# x.f ;; 
- : 'a list -> 'a option = <fun> 

Der folgende Code kompiliert für mich lfrec anstelle eines Verweises mit:

module M : sig 
    type 'a t 
    val call : 'a t -> 'a option 
end = struct 
    type 'a t 
    type lfrec = { mutable f: 'a. 'a t -> 'a option } 
    let state: lfrec = { f = fun _ -> None } 
    let call : ('a t -> 'a option) = fun x -> state.f x 
end