# Number-parameterized types

**Abstract**

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 `Zn`

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
run-time checks.

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

## More number-parameterized types

The paper [ls-resources], joint work with Chung-chieh
Shan, uses number-parameterized types to statically assure the safety
of low-level code such as device drivers. We can ensure that
accessing a memory region through a pointer respects properties of the
region such as its size, array bounds, alignment, endianness, and
write permissions -- even when allowing pointer arithmetic and
casts. We can also enforce protocol and timing requirements, such as
that some device register must be read in some order or for some
number of times through any execution path in a device driver.

### Typed memory areas

We introduce memory areas whose type is parameterized by two
numbers: size and alignment. We can then form heterogeneous tuples as
well as (multi-dimensional) arrays of such areas; the type of an array
is indexed by the number of its elements. The type checker
computes the alignment of indexed areas, using binary type arithmetic
[binary-arithm]. The paper also introduces bounded naturals
whose type is parameterized by their upper bound. Such bounded naturals
then act as safe indices in any array that has at least as many
elements as the upper bound. Our approach supports general recursion.

### Monads parameterized by *time*

Another application of number-parameterized
types is to enforce timing and protocol-related restrictions. We
parameterize the type of the monad with the `time metric' describing
the progress of the computation. The time metric could be the
number of times a particular device register has been read. We may
then enforce that a register be read the same number of times in any
control path through the code. Alternatively, the type checker may
report the maximum number of register reads -- sort of a worst-time
complexity of the code.

## References

[Monad.Reader] Number-parameterized types

*The Monad.Reader.* IssueFive. Oct 2nd, 2005

<http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types>

[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

### Last updated May 4, 2007

This site's top page is **http://okmij.org/ftp/**

oleg-at-pobox.com or oleg-at-okmij.org

Your comments, problem reports, questions are very welcome!
Converted from SXML by SXML->HTML