This paper describes practical programming with types
parameterized by numbers: e.g., an array type parameterized by the
array's size or a modular group type
parameterized by the modulus. An attempt to add, for example, two
integers of different moduli should result in a compile-time error
with a clear error message. Number-parameterized types let the
programmer capture more invariants through types and eliminate some
We review several encodings of the numeric parameter but concentrate on the phantom type representation of a sequence of decimal digits. The decimal encoding makes programming with number-parameterized types convenient and error messages more comprehensible. We implement arithmetic on decimal number-parameterized types, which lets us statically typecheck operations such as array concatenation.
We compare our approach with the phantom type programming in SML by Matthias Blume, with a practical dependent-type system of Hongwei Xi, with statically-sized and generic arrays in Pascal and C, with the shape inference in array-oriented languages, and with C++ template meta-programming.
Overall we demonstrate a practical dependent-type-like system that is just a Haskell library. The basics of the number-parameterized types are written in Haskell98.
Keywords: Haskell, number-parameterized types, type arithmetic, decimal types..
[Monad.Reader] Number-parameterized types
The Monad.Reader. IssueFive. Oct 2nd, 2005
[PDF] number-parameterized-types.pdf [124K]
The paper in the PDF format
[source-code] number-param-vector-code.tar.gz [10K]
[complete-unary-arithm] Complete arithmetic on unary type-level numerals
including the logarithm, the n-th root and the inverse of the factorial
[binary-arithm] Binary type arithmetic
with full comparisons, GCD, and invertible addition and multiplication
[ls-resources] Lightweight static resources, for safe embedded and systems programming
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML