[Haskell] ANN: binary arithmetic type library over natural kinds

[David Roundy]

On Wed, Mar 07, 2007 at 10:48:02PM -0800, oleg at pobox.com wrote:
> 
> Chung-chieh Shan and I would like to announce the type-level Haskell
> library for arbitrary precision binary arithmetic over natural kinds. The
> library supports addition/subtraction, predecessor/successor,
> multiplication/division, exp2, full comparisons, GCD, and the maximum.
> At the core of the library are multi-mode ternary relations Add and Mul
> where _any_ two arguments determine the third. Such relations are
> especially suitable for specifying static arithmetic constraints on
> computations. The type-level numerals have no run-time representation;
> correspondingly, all arithmetic operations are done at compile time and
> have no effect on run-time.

This looks pretty nice, but I'm curious as to whether it can be extended to
verify run-time checks?  i.e. I'd like to be able to use a natural number
determined at run-time to create arrays that are statically
bounds-checked.

i.e. I'm imagining something like this:

data Arr a n = ... -- n is a type-level variable describing the dimension
                   -- a is the data type stored
withArrayFromList :: [a] -> (Nat n => Arr a n -> b) -> b

which would allow me to initialize an array with static bounds checking,
and use it in a function.  Of course, to support this we'd also need
run-time comparison, add, etc.  But what I'm dreaming of is that the type
system would enforce those run-time checks when necesary.  e.g.

catArray :: Add n1 n2 n3 => Arr a n1 -> Arr a n2 -> Arr a n3

I imagine this is harder, but it's needed if these type-level binaries will
be useful for the sorts of programs I tend to write--which have run-time
sizes.
-- 
David Roundy
Department of Physics
Oregon State University