## 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 ∷ Integer → Maybe (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 ∷ Integer → Maybe (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`

BZero ≡ BZero = 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

## 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!

29 January 2011, 2:01 pm## Conal Elliott » Blog Archive » Fixing lists:

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

30 January 2011, 10:54 am## 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.

30 January 2011, 1:15 pm## conal:

Thanks to sfvisser and Elliott Hird who pointed out that my

30 January 2011, 6:08 pm`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.## Conal Elliott » Blog Archive » Doing more with length-typed vectors:

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

31 January 2011, 9:42 am## Conal Elliott » Blog Archive » Reverse-engineering length-typed vectors:

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

31 January 2011, 9:53 am## Conal Elliott » Blog Archive » A trie for length-typed vectors:

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

31 January 2011, 3:04 pm## Conal Elliott » Blog Archive » From tries to trees:

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

6 February 2011, 1:36 pm