Empty array + `Js.Array.push` is unsound

[alex35mil]

This compiles:

let arr = [||];
arr->Js.Array2.push(1);
arr->Js.Array2.push("2");

To fix it arr requires explicit type annotation.

[yawaramin]

Looks like the immediate short-term mitigation is to put a big warning in the doc comment of Js.Array.push that it's unsound. For the long-term fix–the only thing I can think of is to not equate the types array and Js.Array.t.

[cristianoc]

Kind of similar to: https://github.com/cristianoc/genType/blob/master/examples/typescript-react-example/src/ImmutableArray.rei

Non-extensible arrays are those without push, and extensible ones would have different type for empty. Looks like conversion between the 2 kinds would require a copy.

Mutability and extensibility look like orthogonal properties, so one gets 4 kinds. Kind of heavy.

[bobzhang]

The binding of push is not safe, this is a known issue, we should wrap it into an abstract type, Js.Vector etc.

[bobzhang]

From practical point of view, push is quite convenient in JS context.
An easy fix is giving a warning/error to empty array literal, which should be enough:

utop # let f () = [||];;
val f : unit -> 'a array = <fun>
─( 10:42:12 )─< command 3 >──────────{ counter: 0 }─
utop # let a  = f ();;
val a : '_weak1 array = [||]
─( 11:21:05 )─< command 4 >──────────{ counter: 0 }─
utop # 

Note empty array literal is barely useful except as a place holder we can provide Array.empty instead

[bobzhang]

the least intrusive approach is to make [||] weakly typed