29 Jun 2012 12:28

generalised arrays

```Screwing this up a lot so perhaps I should write the formula down :)

First the idea: an array length N has to be indexed by a value of type N.
If N is a unitsum, for example 3 = 1 + 1 + 1, then the values are
just 0,1,2 (mod 3). Note, these are NOT integers, they're things like

case 0 of 3
case 1 of 3
case 2 of 3

You know type 2 -- that's just bool (and the members false
and true are just aliases for case 0 of 2 and case 1 of 2).

If the array has length N * M, it's a matrix, and the index is a member
of N * M, that is, a tuple (i,j) where i is type N and j is type M.

If an array has length N + M it is the joining of two arrays, length
N and length M. So naturally the index has type N + M.
This type has two cases:

(case 0 of N + M) n  // where n in N
(case 1 of N + M) m // where m in M

in other words, you first choose which array to access,
then pick and index for it of the appropriate type.

Now, our array here is linear, but the indexes are structured terms,
so we must linearise them. The formulas are simple (despite the fact
I keep screwing this up .. :)

```