# Why is this type weak?

**URL:** <https://discuss.ocaml.org/t/why-is-this-type-weak/3963>\
**Category:** Learning\
**Created:** [June 19, 2019, 6:25pm UTC](https://discuss.ocaml.org/t/why-is-this-type-weak/3963 "2019-06-19T18:25:17Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![giltho](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/giltho/32/3521_2.png) [@giltho](https://discuss.ocaml.org/u/giltho)\
**Post date:** [June 19, 2019, 6:25pm UTC](https://discuss.ocaml.org/t/why-is-this-type-weak/3963/1 "2019-06-19T18:25:17Z")

</div>

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 :

```auto
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 :

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

```

However, if I do that, `extend_right` has the type

```auto
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

```auto
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,

```auto
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

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [June 19, 2019, 6:42pm UTC](https://discuss.ocaml.org/t/why-is-this-type-weak/3963/2 "2019-06-19T18:42:34Z")

</div>

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:

```auto
let id = fun x -> x

```

However, if we compute a new `id` function with

```auto
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

```auto
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](https://caml.inria.fr/pub/docs/manual-ocaml-4.08/polymorphism.html) or [ocamlverse](https://ocamlverse.github.io/content/weak_type_variables.html).

---

<div class="post-metadata">

**Author:** ![giltho](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/giltho/32/3521_2.png) [@giltho](https://discuss.ocaml.org/u/giltho)\
**Post date:** [June 19, 2019, 10:46pm UTC](https://discuss.ocaml.org/t/why-is-this-type-weak/3963/3 "2019-06-19T22:46:17Z")

</div>

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

Thanks !