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.