Arrays

[aprocter]

Some kind of support for arrays (including bit vectors) would be extremely handy going forward. There are two main challenges here that I see:

1. The type system: we will need support for type-level nats in some form. For example, the array append operator has type a[n] -> a[m] -> a[n+m].
2. It may be difficult to ensure that the synthesis tools infer block/distributed RAMs for arrays when intended.

[aprocter]

Will need to think about what operators we want, as these will probably have to be implemented as primitives (though I suppose we could have array pattern matching). At a minimum I see:

 elem :: a[n] -> (m:Nat | 0 <= m < n) -> a
 append :: a[n] -> a[m] -> a[n+m]
 slice :: a[n] -> (x:Nat | 0 <= x < n) -> (y:Nat | x <= y < n) -> a[(n - (y - x)) + 1]

So a surprising amount of expressivity is needed where the type-level nats are concerned.

[aprocter]

A lightweight alternative that's still useful for many (maybe all!) purposes would be to implement finite map types. Then a register file or a memory could have types like:

 rf :: Reg=>Word
 mem :: Addr=>Word

Where Reg and Addr are "y'know, whatever." Semantically these are just functions, but maintaining a distinction between functions and maps in the type system would allow us to restrict the signature of => to simple update and read operations, and provides a critical optimization hint to the compiler. (Also it dances around the "Eq" issue.)