For our purposes here, an exponential tree is a tree where a nonempty node of the tree at depth \[ d \] has \[ 2^d \] children. For example, the node at depth 1 has 2, at depth 2 has 4, and at depth 3 has 8. (The root node is assumed to have depth 1.)

Today we’re going to be coming up with a way to create exponential trees such that this property is checked in the types. That is, we’re going to attempt to make it impossible for anyone to construct an invalid tree with the tree type we come up with. I’ll be revealing the code for this in bits and pieces, but if you’d like to see the whole implementation at once, please check out the github repo. You might also want to reference it if you’re following along—you may just be missing a language extension or something.

First, let’s talk about plain old trees. Here’s a type for a rose tree in Haskell:

`data RoseTree a = Empty | RoseTree a [RoseTree a]`

Because each node has a list of nodes, any level of the tree can have
any number of elements. There’s no bound on the size of these lists, so
that’s a good place for us to think about adding a bound in our type.
Let’s take a first stab at a type for exponential trees. Like the rose
trees, we’ll want some value of type `a`

in each node, but
let’s also store a depth counter as `d`

so we can get that
\[ 2^d \] elements property. We’ll
leave out what we’re not sure about yet with a `_`

hole.

```
data ExponentialTree a d
= Empty
| ExponentialTree a _
```

What goes in the hole? We need some kind of fixed-length list….
`VecPeano`

from `Data.Vector.Fixed`

should do the
trick! Let’s fill that in, and leave a hole for the length of the
vector. The depth of the next sublevel of the tree is \[ d + 1 \], or in Peano numerals the
successor to d, `S d`

.

```
data ExponentialTree a d
= Empty
| ExponentialTree a (VecPeano _ (ExponentialTree a (S d)))
```

This new hole is where we want to add in our constraint. What we want
is for a sublevel at depth \[ d \] to
have \[ 2^d \] elements. This is all
fine and dandy, but how do we do exponentiation in types? In this case,
we chose `VecPeano`

for our implementation, which uses Peano
numerals to encode natural numbers in types. So let’s take a quick
detour and figure out how to do \[ 2^d
\] using Peano numerals.

The place where `VecPeano`

’s numbers are defined is
`Data.Vector.Fixed.Cont`

. Peano numerals are either zero, or
the successor to another number. In this way, we can inductively define
all the natural numbers. Here’s the definition for them from that
library converting from natural numbers (`Nat`

) to
`PeanoNum`

(lightly modified).

```
type family Peano (n :: Nat) :: PeanoNum where
Peano 0 = Z
Peano n = S (Peano (n - 1))
```

Type families are sort of a way to sneak in extra knowledge about
data constructors to your types. In normal usage, types are either
parametric but give us no knowledge about their data constructors (think
`id :: a -> a`

), or the data constructors are fully known
(think of pattern matching a `Maybe`

…it’s either
`Just`

or `Nothing`

). Here we’re saying that a
`PeanoNum`

is a type constructed either as `Z`

or
as some nested succession that bottoms out in `Z`

.

This lets us represent the natural numbers. Zero is `Z`

,
one is `S Z`

, two is `S (S Z))`

, three is
`S (S (S Z))`

. You get the idea. Having these numbers in
types is nice, because the typechecker checks the rules that a
`PeanoVec (S (S Z))`

must have exactly two elements at
compile time. We cannot construct a `PeanoVec (S (S Z))`

with
any other number of elements.

`Data.Vector.Fixed.Cont`

also helpfully provides us with
Peano addition, so we don’t have to implement that from scratch. Zero
plus any natural number equals that number, so that’s our base case. Our
recursive case subtracts one from `n`

(by unwrapping it from
its former `S n`

) and adds one to `k`

(by taking
the successor of k). Eventually, `n`

will be zero, and we can
return the value of the addition. Here’s the definition in code:

```
type family Add (n :: PeanoNum) (k :: PeanoNum) :: PeanoNum where
Add Z k = k
Add (S n) k = S (Add n k)
```

As you can see, this satisfies the properties of addition on natural
numbers. \[ 0 + n = n \], and \[ (n + 1) + k = 1 + (n + k) \]. These
definitions are all we need for addition. In our recursive case,
eventually the first number bottoms out in `Z`

, and so the
addition works!

We can reason by analogy to come up with Peano multiplication. Zero times any number is zero. We can use addition in our recursive case, satisfying the equation \[ (n + 1) \cdot m = m + (n \cdot m) \].

```
type family Mul (n :: PeanoNum) (m :: PeanoNum) :: PeanoNum where
Mul Z _ = Z
Mul (S n) m = Add m (Mul n m)
```

Once we have multiplication, we can do something very similar to create exponentiation. (Note that we’re sidestepping the issue of what \[ 0^0 \] should be here.) Our equations are \[ 0^n = 0 \mid n \geq 1 \], \[ a ^ 0 = 1 \], and \[ a ^ {b+1} = a \cdot (a ^ b)\].

```
type family Exp (a :: PeanoNum) (b :: PeanoNum) :: PeanoNum where
Exp Z (S n) = Z
Exp a Z = S Z
Exp a (S b) = Mul a (Exp a b)
```

Fantastic! Now that we have exponentiation in types, we can write
\[2^d\] as
`Exp (S (S Z)) d`

in our types. Let’s go back to our
definition of `ExponentialTree`

, with the hole.

```
data ExponentialTree a d
= Empty
| ExponentialTree a (VecPeano _ (ExponentialTree a (S d)))
```

We can fill in the hole with \[ 2^d \].

```
data ExponentialTree a d
= Empty
| ExponentialTree a (VecPeano (Exp (S (S Z)) d) (ExponentialTree a (S d)))
```

Finally we have a type-safe exponential tree! Let’s quickly create a
`Show`

instance for it, so it’s easier to mess around with in
ghci. Because `Data.Vector.Fixed`

doesn’t provide it, we’ll
also have to make a `Show`

instance for
`VecPeano`

, but that shouldn’t be too bad.

```
instance Show a => Show (ExponentialTree a d) where
show Empty = "Empty"
show (ExponentialTree x v) =
"ExponentialTree " ++ show x ++ " (" ++ show v ++ ")"
instance Show x => Show (VecPeano n x) where
show Nil = "Nil"
show (Cons x y) = "Cons (" ++ show x ++ ") (" ++ show y ++ ")"
```

We can now demonstrate that the typechecker will catch invalid trees
for us. Let’s create the simplest non-`Empty`

tree. It’ll
have a root node with a value, and then has to point to 2 (because \[ 2 = 2^1 \]) empty nodes. The type
signature ensures a starting depth of 1.

```
ExponentialTree 7 (Cons Empty (Cons Empty Nil))
:: ExponentialTree Int (Peano 1)
```

If we try to create either of the following trees which aren’t exponential trees, we get a compilation failure. The first has too few nodes in the first layer down, and the second example has too many.

```
ExponentialTree 7 (Cons Empty Nil)
:: ExponentialTree Int (Peano 1)
```

```
ExponentialTree 7 (Cons Empty (Cons Empty (Cons Empty Nil)))
:: ExponentialTree Int (Peano 1)
```

Let’s build one slightly more complicated tree. Feel free to mess around with the numbers of nodes and make sure that our constraints are correctly enforced.

```
ExponentialTree 1
Cons Empty
(Cons (ExponentialTree 2
(Cons Empty
(Cons Empty
(Cons Empty
(Cons Empty
(Nil)))))
Nil))
:: ExponentialTree Int (Peano 1)
```

We can also define a few helper functions to help us build and play
with these trees. The most trivial one is `empty`

:

```
empty :: ExponentialTree a d
= Empty empty
```

If we had done the following instead, we would only be allowing Empty nodes in trees with depth one, enforced by the typechecker. (I made this mistake while implementing these trees, and was wondering why valid trees weren’t passing the typechecker.) You probably do, however, want to enforce a depth-one constraint when constructing the top-level node of non-empty trees.

```
empty :: ExponentialTree a (Peano 1)
= Empty empty
```

This is just to say it pays to be careful when you’re dealing with
type-level programming! You could try implementing functions like
`insert`

or `member`

or `size`

to
manipulate these trees.

Another fun exercise might be to come up with an ASCII
pretty-printer. Try it out! (I recommend adapting some of the code in
`Data.Tree.Pretty`

.) A sample solution is in the spoiler
block below.

```
-- Based on Data.Tree.Pretty
putTree :: Show a => ExponentialTree a d -> IO ()
= putStr . unlines . display
putTree
display :: Show a => ExponentialTree a d -> [String]
Empty = ["Empty"]
display ExponentialTree x v) =
display (show x : drawSubTrees v
where
drawSubTrees :: Show a => VecPeano n (ExponentialTree a d) -> [String]
Nil = []
drawSubTrees Cons x Nil) =
drawSubTrees ("|" : shift "`- " " " (display x)
Cons x xs) =
drawSubTrees ("|" : shift "+- " "| " (display x) ++ drawSubTrees xs
= Prelude.zipWith (++) (first : repeat other) shift first other
```