Conal Elliott

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.

type Digit = Integer

type Nary = [Digit]

type Nary n = [BNat n]

data Z    -- zero
data S n  -- successor

type ZeroT = Z
type OneT  = S ZeroT
type TwoT  = S OneT
⋯
type TenT  = S NineT

data BNat ∷ * → * where
  BZero ∷          BNat (S n)
  BSucc ∷ BNat n → BNat (S n)

fromBNat ∷ BNat n → Integer
fromBNat BZero     = 0
fromBNat (BSucc n) = (succ ∘ fromBNat) n

fromBNat ∘ BSucc = succ ∘ fromBNat

fromBNat ∷ (Enum a, Num a) ⇒ BNat n → a

instance Show (BNat n) where show = show ∘ fromBNat

toBNat ∷ Integer → Maybe (BNat n)

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

*BNat> :ty BSucc (BSucc BZero)
BSucc (BSucc BZero) ∷ BNat (S (S (S n)))

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

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