On Wed, Mar 07, 2007 at 10:48:02PM -0800, oleg@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