Introduce a new `Array.empty () : array 'a` primitive, define Array.copy and Array.init

This patch introduces a new primitive function to create 0-length array without requiring an initialization element. This primitve makes it possible to define Array.copy and Array.init, which could previously not be implemented in the zero-size case.

Closes #342 (closed)