previous   next   up   top

Number-parameterized types


Decimal numbers in types
More type arithmetic
Lightweight static resources, for safe embedded and systems programming


Decimal numbers in types

[The Abstract of the paper]
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.

The current version is October 2005.
number-parameterized-types.pdf [124K]
Number-parameterized types
The Monad.Reader. IssueFive. Oct 2nd, 2005
< >

number-param-vector-code.tar.gz [10K]
The source code accompanying the paper


Binary type arithmetic, from addition to GCD

We introduce the type-level Haskell library for arbitrary precision binary arithmetic over natural kinds. The library supports addition/subtraction, predecessor/successor, multiplication/division, exp2, all 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.

Here are the definitions of the well-formedness condition on binary type numerals -- the kind predicate -- and of a few operations on them:

     class Nat0 a where toInt :: a -> Int
     class Nat0 a => Nat a                   -- (positive) naturals
     class (Nat0 x, Nat y) => Succ x y | x -> y, y -> x
     -- GCD over natural _kinds_
     class (Nat0 x, Nat0 y, Nat0 z) => GCD x y z | x y -> z
The numerals are specified in the familiar big-endian bit notation. The sequence of B0 and B1 is the bit-string of the number, whereas the number of Us is the binary logarithm.
     type N2 = U B1 B0;               nat2 = undefined::N2
     type N4 = U (U B1 B0) B0;        nat4 = undefined::N4
     add :: Add x y z => x -> y -> z; add = undefined
     sub :: Add x y z => z -> x -> y; sub = undefined
     mul :: Mul x y z => x -> y -> z; mul = undefined
     div :: Mul x y z => z -> x -> y; div = undefined
     *BinaryNumber> :type mul (add nat2 nat4) (succ nat2)
     mul (add nat2 nat4) (succ nat2) :: U (U (U (U B1 B0) B0) B1) B0
     *BinaryNumber> :type div (add nat2 nat4) (succ nat2)
     div (add nat2 nat4) (succ nat2) :: U B1 B0
     *BinaryNumber> :type gcd (add nat2 nat4) (succ nat2)
     gcd (add nat2 nat4) (succ nat2) :: U B1 B1
We stress that all multiplication, GCD, etc. computations above are performed as part of type checking: the reported numeral is the type of the expression. The expression's value is undefined: despite the familiar term-level notation, expressions like (add nat2 nat4) are meant to be evaluated at compile time and have no executable content. Also despite the familiar functional term-level notation, the type computations are invertible. We may ask, for example, what must be the type of x such that multiplying it by three gives six:
     x = undefined where _ = mul x (succ nat2) `asTypeOf` (add nat2 nat4)
     *BinaryNumber> :type x
     x :: U B1 B0

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. Our paper `Lightweight static resources' describes the arithmetic type library, type-level records, type-level programming with regular Haskell terms, and two sample applications.

Joint work with Chung-chieh Shan.

The current version is February 2, 2007.
BinaryNumber.hs [10K]
The commented Haskell source code with tests


Lightweight static resources, for safe embedded and systems programming

This 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.
The current version is February 2, 2007.
tfp.pdf [129K]
Proc. Trends in Functional Programming. New York, Apr 2-4, 2007.


Typed memory areas

We introduce memory areas built around raw pointers, to track and arbitrate the size, alignment, write permission, and other properties of memory areas across indexing and casting.

The type of memory areas 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. 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.

Binary type arithmetic, from addition to GCD

Areas.hs [20K]
Strongly typed memory areas. The implementation of the library

AreaTests.hs [4K]
Sample strongly typed memory areas and examples of type records

VideoRAM.hs [5K]
Extensive example of strongly typed memory areas: safe and efficient access to videoRAM, with casts, pointer arithmetic and iterations


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.
RealTime.hs [8K]
Statically tracking ticks: enforcing timing and protocol restrictions when writing device drivers and their generators

Last updated August 9, 2015

This site's top page is
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML