[Agda] Agda bindings for raw JS arrays and objects

[Alan Jeffrey]

Some more low-level hackery...

There's now bindings from Agda to raw JS arrays and objects:

> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Array.agda
> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Object.agda

Both of these provide list-like views of data, for example arrays are 
typed as:

  data IArray {α} (A : Set α) : ℕ → ℕ → Set α where
    [] : ∀ {n} → IArray A n n
    _∷_ : ∀ {m n} → (a : A) → (as : IArray A (suc m) n) → IArray A m n

  data Array {α} (A : Set α) : Set α where
    array : ∀ {n} → (as : IArray A 0 n) → Array A

The FFI binding for (IArray A m n) is a wrapper around a JS array of 
length n, at offset m. The type of the wrapper allows native arrays to 
be preallocated with the right number of elements, for example []{n} is 
a wrapper around (new Array(n)).

The FFI binding for (Array A) is an unwrapped JS array, and what looks 
on the surface to be a data constructor (array) is actually an unwrapper 
(when used in an expression) or a wrapper (when used in a pattern). 
Essentially this is a view pattern in the FFI.

As far as I know, this is the first binding of arrays to a functional 
language which binds unwrapped arrays to a datatype, and so supports 
pattern matching on arrays. Binding arrays to datatypes doesn't matter 
so much in languages like Haskell, but for Agda it's needed to get 
functions over arrays to play nicely with the termination checker.

There's a similar binding for objects, which uses a bit of data 
dependency to maintain the invariant that key arrays are always sorted 
(so for example filter needs a proof that filtering keys maintains 
sortedness).

Not exactly deep uses of dependent types, but still nice.

We now return you to your regularly scheduled programme, WWE: 
Coinduction Versus Sized Types.

A.