Дисперсия OCaml (+'a, -'a) и инвариантность

Question

После написания этого куска кода

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.

О, я помню, что слышал о дисперсии. Это было что-то о ковариации и контравариантности. Я смелый человек, я найду о своей проблеме в одиночку!

Я нашел эти две интересные статьи ( здесь и здесь) и понял!

я могу написать

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"S).

Но для массива? Если у меня есть 'A array Я не могу считать это ('A | 'B) array потому что если я изменяю элемент в массиве, помещая 'B тогда мой тип массива неправильный, потому что это действительно ('A | 'B) array и не 'A array больше. Но как насчет ('A | 'B) array как 'A array, Да, это было бы странно, потому что мой массив может содержать 'B но странно я думал, что это было то же самое как функция. Возможно, в конце концов, я не все понял, но я хотел изложить свои мысли здесь, потому что мне потребовалось много времени, чтобы понять это.

TL; DR:

постоянный: +'a

функции: -'a

изменяемый: инвариант ('a) Почему я не могу заставить его быть -'a?

Answer 1

Я думаю, что самое простое объяснение состоит в том, что изменяемое значение имеет две внутренние операции: getter и setter, которые выражаются с использованием синтаксиса доступа к полю и набора полей:

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 в основном позволяет две операции: получение и установка. Неформально, получение имеет тип 'a t -> 'a list и настройка имеет тип 'a t -> 'a list -> unit, Комбинированные, 'a встречается как в положительном, так и в отрицательном положении.

[РЕДАКТИРОВАТЬ: Ниже (надеюсь) более четкая версия того, что я написал в первую очередь. Я считаю, что это лучше, поэтому я удалил предыдущую версию.]

Я постараюсь сделать это более явным. предполагать sub это правильный подтип super а также witness какое-то значение типа super который не является значением типа sub, Теперь позвольте f : sub -> unit быть некоторой функцией, которая не на значение witness, Тип безопасности там, чтобы гарантировать, что witness никогда не передается f, Я покажу на примере, что безопасность типов терпит неудачу, если разрешено 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. *)

Так лечить 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 инвариантен