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]
(), 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
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.
- 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.
As a first crack, we might replace the
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
Nary, and to perform arithmetic operation on
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 "
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
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
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)
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
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)
*BNat> toBNat 10 ∷ Maybe (BNat EightT)
Later blog posts will include another solution for
toBNat as well as some applications of
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