OCaml variance (+'a, -'a) and invariance

Question

After writing this piece of code

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

I realised I needed info to be mutable.

I wrote, then :

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

But, surprise,

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

Oh, I remember hearing about variance. It was something about covariance and contravariance. I'm a brave person, I'll find about my problem alone!

I found these two interesting articles (here and here) and I understood!

I can write

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

But then I wondered. How come that mutable datatypes are invariant and not just covariant?

I mean, I understand that an 'A list can be considered as a subtype of an ('A | 'B) list because my list can't change. Same thing for a function, if I have a function of type 'A | 'B -> 'C it can be considered as a subtype of a function of type 'A -> 'C | 'D because if my function can handle 'A and 'B's it can handle only 'A's and if I only return 'C's I can for sure expect 'C or 'D's (but I'll only get 'C's).

But for an array? If I have an 'A array I can't consider it as a an ('A | 'B) array because if I modify an element in the array putting a 'B then my array type is wrong because it truly is an ('A | 'B) array and not an 'A array anymore. But what about a ('A | 'B) array as an 'A array. Yes, it would be strange because my array can contain 'B but strangely I thought it was the same as a function. Maybe, in the end, I didn't understand everything but I wanted to put my thoughts on it here because it took me long to understand it.

TL;DR :

persistent : +'a

functions : -'a

mutable : invariant ('a) ? Why can't I force it to be -'a ?

Answer 1

I think that the easiest explanation is that a mutable value has two intrinsic operations: getter and setter, that are expressed using field access and field set syntaxes:

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

let x = {data = 42}

(* getter *)
x.data

(* setter *)
x.data <- 56

Getter has a type 'a t -> 'a, where 'a type variable occurs on the right-hand side (so it imposes a covariance constraint), and the setter has type 'a t -> 'a -> unit where the type variable occurs to the left of the arrow, that imposes a contravariant constraint. So, we have a type that is both covariant and contravariant, that means that type variable 'a is invariant.