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 ?

Reno

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.

Milieu

Exactly the kind of answer I expected so this post can help future OCaml developers to understand easily and rapidly this variance matter. – Reno

I think you meant “and the setter as type …” — submitted an edit, hope I didn't get the fix wrong! Really stumbled over that for a few minutes. – Castellanos

yeah, definitely :) Thanks! – Milieu

Answer 2

Your type t basically allows two operations: getting and setting. Informally, getting has type 'a t -> 'a list and setting has type 'a t -> 'a list -> unit. Combined, 'a occurs both in a positive and in a negative position.

[EDIT: The following is a (hopefully) clearer version of what I wrote in the first place. I consider it superior, so I deleted the previous version.]

I will try to make it more explicit. Suppose sub is a proper subtype of super and witness is some value of type super which is not a value of type sub. Now let f : sub -> unit be some function which fails on the value witness. Type safety is there to ensure that witness is never passed to f. I will show by example that type safety fails if one is allowed to either treat sub t as a subtype of super t, or the other way around.

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. *)

So treating super t as a subtype of sub t cannot be allowed. This shows covariance, which you already knew. Now for contravariance.

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. *)

So, treating sub t as a subtype of super t cannot be allowed either, showing contravariance. Together, 'a t is invariant.

Gsuit

Well, your answer is like the unrolling of ivg's answer but it's a nice addition ;-) – Reno