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