Why is this type weak?

Learning
1

Hello,
I’m writing a program in OCaml, where sometimes I have to extend an array on the right or on the left.
I want to create two functions (extend_right and extend_left) with the following signatures
int -> 'a -> 'a array -> 'a array.
For example

  • extend_left 3 0 [|1; 2; 3; 4|] is expected to produce [|0; 0; 0; 1; 2; 3; 4|]
  • extend_right 3 0 [|1; 2; 3; 4|] is expected to produce [|1; 2; 3; 4; 0; 0; 0|]

Since the code is extremely repetitive, I created the following function :

let extend st_cop sz el arr =
    let sz_arr = Array.length arr in
    let n_arr = Array.make (sz + sz_arr) el in
    let () = Array.blit arr 0 n_arr st_cop sz_arr in
    n_arr

Then, I can simply define :

let extend_left sz = extend sz sz;;
let extend_right = extend 0;;

However, if I do that, extend_right has the type

val extend_right : int -> '_weak1 -> '_weak1 array -> '_weak1 array = <fun>

Which means that as soon as I use it, let’s say on an int array, its type becomes

val extend_right : int -> int -> int array -> int array = <fun>

and I cannot use it with any other type anymore (which I want to do).

Now comes the extremely surprising part : If I define extend_right as follow instead,

let extend_right sz = extend 0 sz;;

The type isn’t weak anymore ! It stays polymorphic as I want. Although the semantics is strictly equivalent (I assume).

I’m very curious about why the type checker has this behaviour. (Although I’m not really looking for help, since I have a solution).

Thank you !
Giltho

2

This is called the value restriction: only syntactic values can be polymorphic and not the result of computations (notwithstanding the relaxed value restriction). For instance, id is a syntactic value of type 'a -> 'a here, because there is visibly no computation going-on:

let id = fun x -> x

However, if we compute a new id function with

let weak_id = id id

The function weak_id is not polymorphic. The reason is that otherwise computation could capture polymorphic references. For instance, consider this fake_id function

let fake_id =
  let memory = ref None in
   fun x -> match !memory with
   | Some y -> y
   | None -> memory := Some x; x

The problem with fake_id is that it captures it first argument and keep returning it. Such functions cannot be polymorphic.

By rewriting your function extend_right, you transformed it from the result of a computation to a function declaration, which is a syntactic value and thus can be polymorphic.

There is more information in the reference manual or ocamlverse.

6 Likes
3

Thank you for your answer !
That is a very interesting behaviour, the reason is fascinating !

Thanks !