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.
number-param-vector-code.tar.gz [10K]
The source code accompanying the paper
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 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.
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
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML