CODEWITHSUNDEEP
ocaml
Greg Nisbet
Greg Nisbet

Reputation: 6994

OCaml why does an empty array have polymorphic type?

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?

Upvotes: 4

Views: 514

Answers (2)

ivg
ivg

Reputation: 35210

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.

Upvotes: 4

gsg
gsg

Reputation: 9377

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 = []

Upvotes: 4

Related Questions