MLのモナドと値の制限

Question

の値の制限では、タイプの安全性を損なう可能性のあるコンテキストでのタイプの一般化が防止されます。コアの問題は、このOCamlのコードで、例えばように、配列決定、突然変異および多型の種類を組み合わせることから生じると思われる：

let x = ref [];; (* value restriction prevents generalization here *) 

x := 1::!x;;  (* type unification with int *) 
x := true::!x;; (* error *) 

値制限なしx用多型タイプで統一することになるため、最後の行はエラーなしです。TypeCheckなりますbool。これを防ぐには、xの型は単調なままでなければなりません。

私の質問は次のとおりです：操作のシーケンスを表現するためにモナドを使用して値の制限を取り除くことは可能でしょうか？

関数の引数として、モナドbindの操作で導入された変数は、シーケンス全体を通じて単相性のままであるため、一般化の際に特殊なケースを導入することなく値の制限と同じ効果が得られます。

これは機能しますか、そうでない場合、なぜですか？

Answer 1

はい、これは基本的に動作し、ハスケルはどのように動作しますか。しかし、ヒッチがあります：リファレンスが決してモナドを "エスケープ"しないようにする必要があります。擬似コード：

module MutMonad : sig 
    (* This is all sound: *) 
    type 'a t 
    type 'a ref 

    val mkref : 'a -> ('a ref) t 
    val read_ref : 'a ref -> 'a t 
    val write_ref : 'a -> 'a ref -> unit t 

    (* This breaks soundness: *) 
    val run : 'a t -> 'a 
end 

我々はスタート地点の実行の有無がすぐに戻って私たちを取得します。

let x = run (mkref []) in (* x is of type ('a list) ref *) 
run (read_ref x >>= fun list -> write_ref (1::list) x); 
run (read_ref x >>= fun list -> write_ref (true::list) x) 

Haskellは2つの方法で回避します：mainが既にモナドのタイプ（あるので

• IO）、それはちょうどがないrun0または同様のを持つことができます。
• STモナドは、モナドが一度終了するとリファレンスが使用不能になるようにランク2タイプのトリックを使用し、サウンドを残しながらローカルに変更可能な状態を可能にします。あなたが何か持っている後者の場合については

：タイプレベルで

module MutMonad : sig 
    (* The types now take an extra type parameter 's, 
    which is a phantom type. Otherwise, the first 
    bit is the same: *) 
    type 'a 's t 
    type 'a 's ref 

    val mkref : 'a -> ('a 's ref) 's t 
    val read_ref : 'a 's ref -> 'a 's t 
    val write_ref : 'a -> 'a 's ref -> unit 's t 

    (* This bit is the key. *) 
    val run : (forall 's. 'a 's t) -> 'a 
end 

forall 's. ...はfun x -> ...に似ています。の変数はローカルにバインドされているので、実行する引数は何も想定できません。実行するための引数は、それらが'sための同じタイプを渡されることを前提とすることはできませんので

let old_ref = run (mkref 3) in 
run (read_ref old_ref) 

：特に、これはチェックを入力しないであろう。

これには、ocamlには存在しない型システムの機能が必要であり、Haskellではlangugae拡張子（Rank2Types）が必要です。