Type-bounded numbers

I’ve been thinking a lot lately about how to derive low-level massively parallel programs from high-level specifications. One of the recurrent tools is folds (reductions) with an associative operator. Associativity allows a linear chain of computations to be restructured into a tree, exposing parallelism. I’ll write up some of my thoughts on deriving parallel programs, but first I’d like to share a few fun ideas I’ve encountered, relating natural numbers (represented in various bases), vectors (one-dimensional arrays), and trees. This material got rather long for a single blog post, so I’ve broken it up into six. A theme throughout will be using types to capture the sizes of the numbers, vectors, and trees.

In writing this series, I wanted to explore an idea for how binary numbers can emerge from simpler and/or more universal notions. And how trees can likewise emerge from binary numbers.

Let’s start with unary (Peano) natural numbers:

data Unary = Zero | Succ Unary

You might notice a similarity with the list type, which could be written as follows:

data List a = Nil | Cons a (List a)

or with a bit of renaming:

data [a] = [] | a : [a]

Specializing a to (), we could just as well have define Unary as a list of unit values:

type Unary = [()]

Though only if we're willing to ignore bottom elements (i.e., ⊥ ∷ ()).

Suppose, however, that we don't want to use unary. We could define and use a type for binary natural numbers. A binary number is either zero, or a zero bit followed by a binary number, or a one bit followed by a binary number:

data Binary = Zero | ZeroAnd Binary | OneAnd Binary

Alternatively, combine the latter two cases into one, making the bit type explicit:

data Binary = Zero | NonZero Bit Binary

Equivalently,

type Binary = [Bit]

We could define the Bit type as a synonym for Bool or as its own distinct, two-valued data type.

Next, how about ternary numbers, decimal numbers, etc? Rather than defining an ad hoc collection of data types, how might we define a single general type of n-ary numbers?

You can find the code for this post in a code repository.

Edits:

  • 2011-01-30: Example of finding the natural numbers greater than a given one
  • 2011-01-30: Equality and comparison
  • 2011-01-30: More section headings
  • 2011-01-30: Mention of correspondence to commutative diagram
  • 2011-01-30: Pointer to code repository.

First try

As a first crack, we might replace the () and Bit types above with a general Digit type, defined as an integer:

type Digit = Integer

type Nary = [Digit]

We could then define operations to convert between Integer and Nary, and to perform arithmetic operation on Nary.

This first approach has some drawbacks:

  • In each case, one parameter would have to be the number base.
  • One can accidentally produce a number as if in one base and then consume as if in another.
  • One can accidentally add numbers in different bases.
  • For base n, every digit is required to be in the range 0, ..., n - 1. This constraint is not enforced statically, and so would either have to be checked dynamically (costing time and code) or could be accidentally broken.

I'd rather have the number bases be statically apparent and statically checked.

What I'm looking for is a type of bounded natural numbers, where BNat n consists of values that correspond to 0, ..., n - 1. Then

type Nary n = [BNat n]

Since the base is now part of the static type, it does not have to be passed in explicitly (and perhaps incorrectly), and it cannot be used inconsistently.

But wait a minute! We don't have dependent types (i.e., types that depend on values) in Haskell, so what could I mean by "n" in "BNat n"?

Type-level natural numbers

A by-now-common trick is to build type-level unary natural numbers out of two data types.

data Z    -- zero
data S n -- successor

We won't use values of these types, so there are no corresponding value constructors.

Some handy aliases:

type ZeroT = Z
type OneT = S ZeroT
type TwoT = S OneT

type TenT = S NineT

For instance, FourT is the type S (S (S (S Z))).

Type-bounded unary numbers

We want our type BNat n to consist of (values corresponding to) 0, . . . , n - 1. To get an inductive perspective, note that (a) BNat Z is empty; and (b) an element of BNat (S n) is either 0, or it is one more than a number in the range 0, . . . , n - 1, i.e., an element of BNat n. These two possibilities lead directly to a representation for BNat, as a GADT (generalized algebraic data type):

data BNat  ** where
BZero BNat (S n)
BSucc BNat n → BNat (S n)

Conversion to and from integers

These two constructors correspond to two facts about inequality: 0 < n + 1, and m < n ⇒ m + 1 < n + 1. Elements of the type BNat n then correspond to canonoical proofs that m < n for various values of m, where the proofs are built out of the two facts and modus ponens (i.e., ((P ⇒ Q) ∧ P) ⇒ Q, which corresponds to function application).

We can extract the m of these proofs:

fromBNat  BNat n → Integer
fromBNat BZero = 0
fromBNat (BSucc n) = (succ ∘ fromBNat) n

I wrote the second clause strangely to emphasize the following lovely property, corresponding to a commutative diagram:

fromBNat ∘ BSucc = succ ∘ fromBNat

Note that the type of fromBNat may be generalized:

fromBNat  (Enum a, Num a) ⇒ BNat n → a

To present BNat values, convert them to integers:

instance Show (BNat n) where show = show ∘ fromBNat

The reverse mapping is handy also, i.e., for a number type n, given an integer m, generate a proof that m < n, or fail if m ≥ n.

toBNat  IntegerMaybe (BNat n)

Unlike fromBNat, toBNat doesn't have a structure to crawl over. It must create just the right structure anyway. What can we do?

One solution is to use a type class: with instances for Z and S:

class HasBNat n where toBNat  IntegerMaybe (BNat n)

instance HasBNat Z where toBNat _ = Nothing

instance HasBNat n ⇒ HasBNat (S n) where
toBNat m | m < 1 = Just BZero
| otherwise = fmap BSucc (toBNat (pred m))
*BNat> toBNat  3  Maybe (BNat EightT)
Just 3
*BNat> toBNat 10 Maybe (BNat EightT)
Nothing

Later blog posts will include another solution for toBNat as well as some applications of BNat.

We can also get a description of all natural numbers greater than a given one:

*BNat> :ty BSucc (BSucc BZero)
BSucc (BSucc BZero) BNat (S (S (S n)))

In words, the natural numbers greater than two are exactly those of the form 3 + n, for natural numbers n.

Equality and comparison

Equality and ordering are easily defined, all based on simple properties of numbers:

instance Eq (BNat n) where
BZeroBZero = True
BSucc m ≡ BSucc m' = m ≡ m'
_ ≡ _ = False
instance Ord (BNat n) where
BZero `compare` BZero = EQ
BSucc m `compare` BSucc m' = m `compare` m'
BZero `compare` BSucc _ = LT
BSucc _ `compare` BZero = GT

8 Comments

  1. Vlad Patryshev:

    I wonder if reading ncatlab (http://ncatlab.org/nlab/show/HomePage) might help grasping a general picture more clearly. There’s also an important (and small) book by Pierce: http://www.amazon.com/Category-Computer-Scientists-Foundations-Computing/dp/0262660717 that sheds like on things.

    Good luck!

  2. Conal Elliott » Blog Archive » Fixing lists:

    [...] About « Type-bounded numbers [...]

  3. sfvisser:

    Nice work, reminds of the Fin datatype in Agda.

    The nice thing about Agda is of course the numeric syntactic sugar, allowing you to write actual numbers at the type level.

  4. conal:

    Thanks to sfvisser and Elliott Hird who pointed out that my BNat type corresponds to the Fin type from Agda (though without full dependent types and with a less convenient notation). See, e.g., these notes.

  5. Conal Elliott » Blog Archive » Doing more with length-typed vectors:

    [...] Type-bounded numbers [...]

  6. Conal Elliott » Blog Archive » Reverse-engineering length-typed vectors:

    [...] Type-bounded numbers [...]

  7. Conal Elliott » Blog Archive » A trie for length-typed vectors:

    [...] Type-bounded numbers [...]

  8. Conal Elliott » Blog Archive » From tries to trees:

    [...] Type-bounded numbers [...]

Leave a comment