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/tmrwiki/IssueFive>

[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