OCaml why does an empty array have polymorphic type?

Question

OCaml arrays are mutable. For most mutable types, even an "empty" value does not have polymorphic type.

For example,

# ref None;;
- : '_a option ref = {contents = None}
# Hashtbl.create 0;;
- : ('_a, '_b) Hashtbl.t = <abstr>

However, an empty array does have a polymorphic type

# [||];;
- : 'a array = [||]

This seems like it should be impossible since arrays are mutable.

It happens to work out in this case because the length of an array can't change and thus there's no opportunity to break soundness.

Are arrays special-cased in the type system to allow this?

Answer 1

The answer is simple -- an empty array has the polymorphic type because it is a constant. Is it special-cased? Well, sort of, mostly because an array is a built-in type, that is not represented as an ADT, so yes, in the typecore.ml in the is_nonexpansive function, there is a case for the array

  | Texp_array [] -> true

However, this is not a special case, it is just a matter of inferring which syntactic expressions form constants.

Note, in general, the relaxed value restriction allows generalization of expressions that are non-expansive (not just syntactic constants as in classical value restriction). Where non-expansive expression is either a expression in the normal form (i.e., a constant) or an expression whose computation wouldn't have any observable side effects. In our case, [||] is a perfect constant.

The OCaml value restriction is even more relaxed than that, as it allows the generalization of some expansive expressions, in case if type variables have positive variance. But this is a completely different story.

Also,ref None is not an empty value. A ref value by itself, is just a record with one mutable field, type 'a ref = {mutable contents : 'a} so it can never be empty. The fact that it contains an immutable value (or references the immutable value, if you like) doesn't make it either empty or polymorphic. The same as [|None|] that is also non-empty. It is a singleton. Besides, the latter has the weak polymorphic type.