Archive for 29th January 2011

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

``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