ANN: binary arithmetic type library over natural kinds
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. http://pobox.com/~oleg/ftp/Computation/resource-aware-prog/BinaryNumber.hs We used the arithmetic type library to statically enforce validity, range, size, and alignment constraints of raw memory pointers, and to statically enforce protocol and time-related constraints when accessing device registers. The following near final full paper http://pobox.com/~oleg/ftp/Computation/resource-aware-prog/tfp.pdf describes the arithmetic type library, type-level records, type-level programming with regular Haskell terms, and two sample applications. We will greatly appreciate all the comments (especially those received before noon on Friday).
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
On Thu, Mar 08, 2007 at 08:24:57AM -0800, David Roundy wrote:
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
I think the ST trick can be done here safely if you change the type to
withArrayFromList :: [a] -> (forall n . Nat n => Arr a n -> b) -> b
notice the rank-2 type, this ensures the argument is a function that can work on arrays of any size, without specifying any size in particular at compile time. run time checks would be needed only if you wanted to refine the type:
assertSize4 :: Arr a n -> Maybe Arr a N4
but what is cool is you just need to perform this run-time check once then all your code can work on 'Arr a N4' knowing that it has exactly 4 elements. the type system takes care of propegating the fact you already did the appropriate run-time check for you. quite nice.
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.
I think this sort of thing will 'just work' unless I am misunderstanding what you want. This all seems very interesting, I would like it if there were a standardish type level arithmetic library in base. though, I find it a little aethetically jarring without user defined kinds like in omega. John -- John Meacham - ⑆repetae.net⑆john⑈
participants (3)
-
David Roundy -
John Meacham -
oleg＠pobox.com