OCaml中空数组为何具备多态类型？

Great observation! This is a neat quirk of OCaml's type system that comes down to safety guarantees tied to array length immutability. Let's break this down clearly.

First, let's recap your examples to set the stage:

Weak polymorphism in other mutable types #

For most empty mutable containers, OCaml assigns a weakly polymorphic type (marked with '_a instead of 'a). This is the type system's way of saying: "I don't know the concrete type yet, but once you modify this value, I'll lock it to a specific type to keep things safe."

Take these cases:

# ref None;;
- : '_a option ref = {contents = None}

# Hashtbl.create 0;;
- : ('_a, '_b) Hashtbl.t = <abstr>

You can later fill these containers with concrete values, which fixes their type permanently:

# let r = ref None;;
val r : '_a option ref = {contents = None}

# r := Some 42;;
- : unit = ()

# r;;
- : int option ref = {contents = Some 42}

If these had full polymorphism ('a option ref), you could theoretically assign Some "hello" next—breaking type safety. Weak polymorphism prevents that risk.

Full polymorphism for the empty array #

The empty array is a special case:

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

It gets a fully polymorphic type 'a array! Why is this allowed even though arrays are mutable?

The critical detail here is that OCaml arrays have a fixed length once created. An empty array will always be empty—you can never add elements to it. Since there's no way to put any values into it, there's zero risk of type conflicts later. The type system recognizes this safety guarantee and grants it full polymorphism.

Does the type system treat arrays specially here? #

Yes, absolutely! This is an explicit exception in OCaml's type inference rules. The empty array is deemed a "safe" polymorphic value because its fixed length eliminates any possibility of type inconsistency. Other mutable containers (like refs or hashtables) don't have this constraint—you can always add elements to them later—so they get weak polymorphism instead.

To sum it up: the empty array can never hold any values, so the type system doesn't need to lock it to a concrete type. It's free to be polymorphic without compromising safety.

内容的提问来源于stack exchange，提问作者Greg Nisbet