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