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

[oleg at pobox.com]

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).