Is it possible to bypass the value restriction using type annotations?

user_11314026 0
Viewed 48

I originally wrote a reverse function like this:

let reverse =
  let rec aux acc = function
    | [] -> acc
    | h :: t -> aux (h :: acc) t
  in
  aux []

However, it does not get a polymorphic type, due to the value restriction (utop gives the actual type as val reverse : '_weak1 list -> '_weak1 list = <fun>).

I can, however, make it work by taking an explicit list argument:

let reverse list =
  let rec aux acc = function
    | [] -> acc
    | h :: t -> aux (h :: acc) t
  in
  aux [] list

But I am still curious if it is possible to force reverse to be polymorphic using a type signature. I tried making it explicitly polymorphic:

let reverse : 'a. 'a list -> 'a list =
  let rec aux acc = function
    | [] -> acc
    | h :: t -> aux (h :: acc) t
  in
  aux []

But then I get the following error

Error: This definition has type 'a list -> 'a list which is less general than
         'a0. 'a0 list -> 'a0 list

It seems the weak types have disappeared - is the 'a0 type variable a truly polymorphic type, or is it another name for '_weak1? And is it possible to allow this function with the value restriction by changing its signature?

ocaml types
2 Answers

The short answer is no, you can't get around the value restriction by ascribing a type.

As you see, if you try this the type inferencer notices what you're trying to do and diagnoses it as an error.

It's worth noting (maybe) that the value restriction is based on the syntactic form of a definition, not on any type analysis. You can't change the syntax with a type ascription.

The reason your rewrite (known as "eta expansion") works is that it changes the syntax. It causes the name reverse to be defined as a lambda (a function) rather than an application (aux []).

user_8216790

The value restriction exists to avoid an unsoundness in the type system. Typically, the function not_id should not be polymorphic

let make_fake_id () =
  let store = ref None in
  fun x ->
    match !store with
    | Some y -> y 
    | None -> store := Some x; y

let not_id = make_fake_id ()

Type annotations don't help in detecting those issues, thus you cannot avoid the value restriction by adding type annotations.

What happens here is that when checking an annotation with an explicit universal quantification, the typechecker uses an explicit form for the type of the body of the let too. For instance,

let k = ref None
let f: 'a 'b. 'a -> 'b * 'c = fun x -> x, k

yields

Error: This definition has type 'c. 'c -> 'c * 'weak1 option ref
       which is less general than 'a 'b. 'a -> 'b * 'weak1 option ref

Notice that in the error message, the type of the body is written as 'c. 'c -> 'c * 'weak2 option ref: all polymorphic types (aka 'c) in the let are explicitly quantified: 'c, and the non-polymorphic types (aka weak1) are those that are not quantified.

user_73693660
Related