OCamlの分散（+ '、-'a）及び不変

Question

私は可変であることinfoを必要実現コード

module type TS = sig 
    type +'a t 
end 

module T : TS = struct 
    type 'a t = {info : 'a list} 
end 

のこの部分を書き込んだ後。

私はその後、書いた：

module type TS = sig 
    type +'a t 
end 

module T : TS = struct 
    type 'a t = {mutable info : 'a list} 
end 

しかし、驚き、

Type declarations do not match: 
    type 'a t = { mutable info : 'a list; } 
is not included in 
    type +'a t 
Their variances do not agree. 

をああ、私は分散聞い覚えています。それは約共分散とcontavvarianceについてのものでした。私は勇敢な人です、私は自分の問題だけを見つけるでしょう！

これら2つの興味深い記事（hereとhere）が見つかりました。

私は

module type TS = sig 
    type (-'a, +'b) t 
end 

module T : TS = struct 
    type ('a, 'b) t = 'a -> 'b 
end 

を書くことができます。しかし、私は疑問に思いました。どのように可変のデータ型は不変であり、共変ではないでしょうか？

つまり、'A listは私のリストが変更できないため('A | 'B) listのサブタイプと見なすことができます。同じ機能の場合、タイプが'A | 'B -> 'Cの場合は、タイプが'A -> 'C | 'Dのサブタイプと見なすことができます。'Aと'Bを処理できるのは'Aです。返すだけなので'Cの私は確かに'Cまたは'Dの（しかし、私は'Cのを得ます）を期待することができます。

しかし、配列については？私が'A arrayを持っていれば、配列の要素を'Bに変更すると、本当に('A | 'B) arrayであり、もう'A arrayではないので配列型が間違っているので、('A | 'B) arrayと考えることはできません。しかしとして('A | 'B) arrayはどうでしょうか？はい、私の配列は'Bを含むことができますが、不思議なことに私はそれが関数と同じであると思いました。多分、私はすべてを理解していなかったかもしれませんが、私はそれを理解するのが間に合わなかったので、ここに私の考えを入れたいと思っていました。

TL; DR：

永続：+'a

機能：-'a

可変：不変（'a）？なぜそれを強制的に-'aにすることはできませんか？

Answer 1

私は最も簡単な説明は変更可能な値は、2つの固有の操作があることだと思い：ゲッターとセッター、フィールドアクセスおよびフィールドセットの構文を使用して表現されています

type 'a t = {mutable data : 'a} 

let x = {data = 42} 

(* getter *) 
x.data 

(* setter *) 
x.data <- 56 

ゲッターはタイプ'a t -> 'aを持ち、ここで'a型の変数が右側に出現するので（共分散制約を課す）、タイプ変数が矢印の左側に現れ、反変的な制約を課すタイプ'a t -> 'a -> unitがあります。したがって、我々は共変と反変の両方のタイプを持っています。つまり、タイプ変数'aは不変です。

Answer 2

あなたのタイプはtです。基本的には、取得と設定の2つの操作が可能です。非公式には、ゲットタイプは'a t -> 'a list、設定タイプは'a t -> 'a list -> unitです。組み合わせると、'aは、正の位置と負の位置の両方で発生します。

[編集：以下は、私が最初に書いたものの（うまくいけば）明確なバージョンです。私はそれが優れていると思うので、前のバージョンを削除しました。]

もっと明示しようとします。 subがsuperの適切なサブタイプであり、witnessがsubの値ではないタイプsuperの値であるとします。今度は、f : sub -> unitを値witnessで失敗する関数としましょう。タイプセーフティは、witnessがfに決して渡されないようにするためです。例では、sub tをサブタイプsuper tとして扱うか、それ以外の方法で扱うことができれば、型の安全性に問題があることを示します。だから、sub tのサブタイプとしてsuper tの治療

let v_super = ({ info = [witness]; } : super t) in 
let v_sub = (v_super : sub t) in (* Suppose this was allowed. *) 
List.map f v_sub.info (* Equivalent to f witness. Woops. *) 

は許可することはできません。これはあなたがすでに知っていた共分散を示しています。今contravarianceのために。 super tのサブタイプとしてsub tを処理するので、

let v_sub = ({ info = []; } : sub t) in 
let v_super = (v_sub : super t) in (* Suppose this was allowed. *) 
v_super.info <- [witness]; 
    (* As v_sub and v_super are the same thing, 
     we have v_sub.info=[witness] once more. *) 
List.map f v_sub.info (* Woops again. *) 

は、contravarianceを示す、いずれかの許可することはできません。一緒に、'a tは不変です。