19

このコードを書いた後

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

infoミュータブルである必要があることに気づきました。

私は書いた：

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.

ああ、分散について聞いた覚えがあります。それは共分散と反分散に関するものでした。私は勇敢な人です、私は自分の問題を一人で見つけます！

この 2 つの興味深い記事 (こことここ) を見つけて、理解しました!

私は書くことができます

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

しかし、私は疑問に思いました。変更可能なデータ型が共変ではなく不変なのはなぜですか?

つまり、私のリストは変更できないため、'A listan は an のサブタイプと見なすことができることを理解しています。('A | 'B) list関数についても同じことが言えます。タイプの関数がある場合、'A | 'B -> 'Cタイプの関数のサブタイプと見なすことができます。これは、関数がとを処理できる場合は のみを処理でき、 のみを返す場合は を処理できるためです。確かにまたはが期待されます（ただし、私はのみを取得します）。'A -> 'C | 'D'A'B'A'C'C'D'C

しかし、配列の場合は？を持っている場合、それを anと'A array見なすことはできません。('A | 'B) arrayなぜなら、配列内の要素を変更して a を入れると'B、配列型が間違っているからです。しかし、としてのa はどうでしょうか。はい、配列に含めることができるので奇妙ですが、奇妙なことに、関数と同じだと思いました。結局、すべてを理解できなかったかもしれませんが、理解するのに時間がかかったので、ここで考えを述べたいと思いました。('A | 'B) array'A array('A | 'B) array'A array'B

TL;DR :

持続的に ：+'a

機能 ：-'a

可変: 不変 ( 'a) ? 強制できないのはなぜ-'aですか？

4

2 に答える 2

18

最も簡単な説明は、変更可能な値には、フィールド アクセスとフィールド セットの構文を使用して表現される getter と setter という 2 つの組み込み操作があるということだと思います。

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

let x = {data = 42}

(* getter *)
x.data

(* setter *)
x.data <- 56

ゲッターには type'a t -> 'aがあり、'a型変数は右側にあり (したがって、共分散制約が課せられます)、セッターには'a t -> 'a -> unit型変数が矢印の左側にあり、反変制約を課します。したがって、共変と反変の両方である型があります。つまり、型変数'aは不変です。

于 2016-11-09T15:47:27.180 に答える
6

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

[編集: 以下は、私が最初に書いたものの (できれば) より明確なバージョンです。優れていると思うので、以前のバージョンを削除しました。]

私はそれをより明確にしようとします。が の適切subなサブタイプでsuperあり、が typeの値ではないwitnesstypeの値であるとします。ここで、 value で失敗する関数を考えてみましょう。タイプ セーフは、 が に渡されないようにするためにあります。のサブタイプとして扱うことを許可されている場合、またはその逆を許可されている場合、型の安全性が失敗することを例で示します。supersubf : sub -> unitwitnesswitnessfsub tsuper 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. *)

したがって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. *)

したがって、 をsub tサブタイプとして扱うsuper tこともできず、反変性を示します。一緒に、'a t不変です。

于 2016-11-09T16:10:30.927 に答える