OCaml why does an empty array have polymorphic type?

4
votes

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?

2
ocaml
You kind of answered the question in your title yourself: An empty array has polymorphic type because it is immutable ("the length of an array can't change"). – melpomene
@melpomene yes, but a user-defined container that happens to be non-resizable wouldn’t have this property. I’m wondering about the nature of the special case for arrays and if there’s a motivating use case for it – Gregory Nisbet
I think the way to look at it is just that the types are correct :-) A 0-length array should be polymorphic. A reference or hash table should never be polymorphic even if they happen to have nothing interesting in them at the moment. An array of length 1 with nothing interesting in it will also fail to be polymorphic :[| None |] – Jeffrey Scofield

2 Answers

4
votes

I don't believe so. Similar situations arise with user-defined data types, and the behaviour is the same.

As an example, consider:

type 'a t = Empty | One of { mutable contents : 'a }

As with an array, an 'a t is mutable. However, the Empty constructor can be used in a polymorphic way just like an empty array:

# let n = Empty in n, n;;
- : 'a t * 'b t = (Empty, Empty)

# let o = One {contents = None};;
val o : '_weak1 option t = One {contents = None}

This works even when there is a value of type 'a present, so long as it is not in a nonvariant position:

type 'a t = NonMut of 'a | Mut of { mutable contents : 'a }

# let n = NonMut None in n, n;;
- : 'a option t * 'b option t = (NonMut None, NonMut None)

Note that the argument of 'a t is still nonvariant and you will lose polymorphism when hiding the constructor inside a function or module (roughly because variance will be inferred from arguments of the type constructor).

# (fun () -> Empty) ();;
- : '_weak1 t = Empty

Compare with the empty list:

# (fun () -> []) ();;
- : 'a list = []
4
votes

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.