[Haskell] ANN: binary arithmetic type library over natural kinds
David Roundy
droundy at darcs.net
Thu Mar 8 11:24:57 EST 2007
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
More information about the Haskell
mailing list