Do OCaml 'underscore types' (e.g. '_a) introduce the possibility of runtime type errors / soundness violations?

Question

I was reading a little bit about the value restriction in Standard ML and tried translating the example to OCaml to see what it would do. It seems like OCaml produces these types in contexts where SML would reject a program due to the value restriction. I've also seen them in other contexts like empty hash tables that haven't been "specialized" to a particular type yet.

http://mlton.org/ValueRestriction

Here's an example of a rejected program in SML:

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

If you enter the first line verbatim into the SML of New Jersey repl you get the following error:

- val r: 'a option ref = ref NONE;
stdIn:1.6-1.33 Error: explicit type variable cannot be generalized at its binding declaration: 'a

If you leave off the explicit type annotation you get

- val r = ref NONE

stdIn:1.6-1.18 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val r = ref NONE : ?.X1 option ref

What exactly is this dummy type? It seems like it's completely inaccessible and fails to unify with anything

- r := SOME 5;

stdIn:1.2-1.13 Error: operator and operand don't agree [overload conflict]
  operator domain: ?.X1 option ref * ?.X1 option
  operand:         ?.X1 option ref * [int ty] option
  in expression:
    r := SOME 5

In OCaml, by contrast, the dummy type variable is accessible and unifies with the first thing it can.

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

# r := Some 5;;
- : unit = ()
# r ;;
- : int option ref = {contents = Some 5}

This is sort of confusing and raises a few questions.

1) Could a conforming SML implementation choose to make the "dummy" type above accessible?

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

3) The type '_a option ref seems less polymorphic than 'a option ref. Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

Answer 1

Weakly polymorphic types (the '_-style types) are a programming convenience rather than a true extension of the type system.

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

OCaml does not sacrifice value restriction, it rather implements a heuristic that saves you from systematically annotating the type of values like ref None whose type is only “weekly” polymorphic. This heuristic by looking at the current “compilation unit”: if it can determine the actual type for a weekly polymorphic type, then everything works as if the initial declaration had the appropriate type annotation, otherwise the compilation unit is rejected with the message:

Error: The type of this expression, '_a option ref,
       contains type variables that cannot be generalized

3) The type '_a option ref seems less polymorphic than 'a option ref. Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

This is because '_a is not a “real” type, for instance it is forbidden to write a signature explicitly defining values of this “type”:

# module A : sig val table : '_a option ref end = struct let option = ref None end;;
Characters 27-30:
  module A : sig val table : '_a option ref end = struct let option = ref None end;;
                             ^^^
Error: The type variable name '_a is not allowed in programs

It is possible to avoid using these weakly polymorphic types by using recursive declarations to pack together the weakly polymorphic variable declaration and the later function usage that completes the type definition, e.g.:

# let rec r = ref None and set x = r := Some(x + 1);;
val r : int option ref = {contents = None}
val set : int -> unit = <fun>

Answer 2

1) Could a conforming SML implementation choose to make the "dummy" type above accessible?

The revised Definition (SML97) doesn't specify that there be a "dummy" type; all it formally specifies is that the val can't introduce a polymorphic type variable, since the right-hand-side expression isn't a non-expansive expression. (There are also some comments about type variables not leaking into the top level, but as Andreas Rossberg points out in his Defects in the Revised Definition of Standard ML, those comments are really about undetermined types rather than the type variables that appear in the definition's formalism, so they can't really be taken as part of the requirements.)

In practice, I think there are four approaches that implementations take:

• some implementations reject the affected declarations during type-checking, and force the programmer to specify a monomorphic type.
• some implementations, such as MLton, prevent generalization, but defer unification, so that the appropriate monomorphic type can become clear later in the program.
• SML/NJ, as you've seen, issues a warning and instantiates a dummy type that cannot subsequently be unified with any other type.
• I think I've heard that some implementation defaults to int? I'm not sure.

All of these options are presumably permitted and apparently sound, though the "defer unification" approach does require care to ensure that the type doesn't unify with an as-yet-ungenerated type name (especially a type name from inside a functor, since then the monomorphic type may correspond to different types in different applications of the functor, which would of course have the same sorts of problems as a regular polymorphic type).

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

I'm not very familiar with OCaml, but from what you write, it sounds like it uses the same approach as MLton; so, it should not have to sacrifice soundness.

(By the way, despite what you imply, OCaml does have the value restriction. There are some differences between the value restriction in OCaml and the one in SML, but none of your code-snippets relates to those differences. Your code snippets just demonstrate some differences in how the restriction is enforced in OCaml vs. one implementation of SML.)

3) The type '_a option ref seems less polymorphic than 'a option ref. Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

Again, I'm not very familiar with OCaml, but — yeah, that seems like a mistake to me!