OCaml дисперсии (+ 'а, -'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. 

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

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

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

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

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

Но потом я подумал. Как получилось, что mutable datatypes являются инвариантными, а не только ковариантными?

Я понимаю, что 'A list можно рассматривать как подтип ('A | 'B) list, потому что мой список не может измениться. То же самое для функции, если у меня есть функция типа 'A | 'B -> 'C, ее можно рассматривать как подтип функции типа 'A -> 'C | 'D, потому что если моя функция может обрабатывать 'A и 'B, она может обрабатывать только 'A и если я только вернусь 'C Я могу с уверенностью ожидать 'C или 'D (но я получу только 'C).

Но для массива? Если у меня есть '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

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

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

let x = {data = 42} 

(* getter *) 
x.data 

(* setter *) 
x.data <- 56 

Getter имеет тип '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 является инвариантным.