[Agda] Feature request: array primitives

[Permjacov Evgeniy]

 Fast arrays may be very interesting, as they may allow rapid correct
prototyping of numerical software in Agda. Moreover, with use of GPGPU
bindings they may be of production speed. The rest are some random
thoughts about how to bring arrays into agda, keeping in ming ghc as
target language

1. Arrays are indexed collection of values with fast access operations.
There is no need for fast updates of arrays in many computational
scenarios, only for function like haskell's accumArray. The only things
arrays require for sure are built-in operations accumArray and
arrayIndex, all others (including tracing array sizes) may be written in
Agda on top of it. GHC features some primitive built-ins for arrays, so
we do not need to rely on haskell standard library, rewriting model in
agda almost entirely.

2. Sometimes need for compact, strict storage of primitive types arises.
Storing links to boxes at least triples memory usage for primitive types
(in case of doubles on 64-bit machines). To store such types, either
unboxed array primitives or raw memory access is needed. I cannot
remember any primitives fitting first purpose, but effective direct raw
memory access is possible in haskell. So, unboxed strict arrays of
primitive values may be represented as chunks of raw memory. IO impurity
is dealt in haskell libraries using unsafePerformIO and keeping in mind
operational semantics.

3. Sometimes need for compact storage of tuples of primitive types
arises. This can be done easily by decomposing tuples into components
and storing them in different arrays. This allows storage of some
datatypes (i.e. ones without recursive definitions in their direct and
indirect components) possible.

4. Mutable arrays may be useful in many computational scenrios, for
example, in eigenvector problem. So, they are needed as well, a pity.

5. GPGPU and many computational libraries may be binded only throw C.
thus, C ffi interface and C 'foreign arrays' are needed. The latter can
be done using raw memory acces, however.

Finally:
 - Array primitives accumArray and arrayIndex and primitive array types
are needed definitly.
 - Raw memory access with pointer finalization (there are ghc facilities
for it) primitives are needed for production-quality numerical software.