Refセルを使用した動的バインディング

Question

私はあなたがこれをすることはできないが、なぜ正確に理解したいのか理解しています。中

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 

結果：

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 

はなぜ抽象型は、ここでは互換性がありませんか？

私の腸は、早い対遅い拘束とは関係がありますが、タイプシステムがここで何をしているのか正確な説明を探しています。

Answer 1

視野の1つは、フィールドstateは、変更可能な値を多態性にすることができないため、それに従う多形値を持つことができないことです。参照は最大単相性である（変数型の表記で'_aと表記）。

あなただけのトップレベルで、同様の参照を宣言しようとした場合、あなたは同じ効果わかります

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

を型変数'_aがまだ決定されていないいくつかのシングルタイプを示します。

参照が多型であることができない理由は、それが不健全であるということです。参照を一般化（多型）できるようにすると、ひどく間違っているプログラムを作成するのは簡単です。 （実際には、これは通常、クラッシュやコアダンプを意味します。）

健全性の問題は、この論文の冒頭近くで議論されている：Jacques Garrigue, Relaxing the Value Restriction（私は定期的に、私は物事がどのように働くか忘れてたときに参照しています）。

更新

私はあなたが欲しいと思うもの "ランク2多型" です。つまり、型が多相であるフィールドが必要です。型を宣言している限り、実際にOCamlでこれを得ることができます。 ` '_a`はそれがあることを意味していることを知りませんでした、

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