# A Red-Black Tree Implementation with Provable Properties

We algorithms people usually go trough great lengths to prove properties of our algorithms, for example, that they are correct, and that they run in \(O(...)\) time, etc. Unfortunately, we hardly ever implement our algorithms, and even if we implement them, we mostly forget about our proofs. So who is to say that our implementation actually has all these nice properties? Wouldn’t it be nice if our implementation came with its own proofs, showing that it is correct? This page shows how we can use the type system of our programming language to provide proofs of properties of our algorithm. In particular, we will show how we can use Haskell’s type system to enforce several properties of Red-Black trees.

A Red-Black tree is a well known data structure to store an ordered sequence of values. It is a balanced binary search tree that stores values in its internal nodes. Each node has a color, either red or black, and there are some invariants that guarantee that a Red-Black tree is balanced. The five invariants are

- every node is red or black,
- the root is black,
- every leaf is black,
- if a node is red, then both its children are black, and
- for each node, the
*black-height*of the left child is the same as the black-height of the right child. The black height is the number of black nodes on a path from the node to a leaf.

We will use Haskell’s type system to enforce these invariants. Our implementation will use some of the, fairly new, features/extentions in GHC:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
```

This page is written as as literate haskell. The complete source code can be found here.

`module RedBlackTree where`

`import Control.Applicative((<$>))`

## Defining Data Types

We start by defining a type representing the colors. We will not construct values of the type color at all, instead we will use Red and Black only as types, and Color only as a kind. Hence, we do not bother deriving instances for type classes such as Show and Eq.

`data Color = Red | Black`

The same for type level natural numbers. For now we will roll out our own Nat kind, which just models Peano numbers. GHC 7.8 has proper support for type level natural numbers, so then we can instead use 0, 1, 2, … as types. Until then, we will use this instead.

`data Nat = Z | S Nat`

Now onto the real stuff. A data type representing a node in our tree. Nodes are
parameterized by three things: their color (of kind Color), their black height
(of kind Nat), and the type of the values that are stored (of kind *). The
color and the black-height are “Phantom types”. They don’t (directly)
influence the data that is stored. Instead, they are only used to enforce our
invariants: For example, the associated color phantom-type immediately enforces
invariant 1): Each node *has* a color, and since its kind is Color, this is
either Red or Black.

```
data Node (c :: Color) (h :: Nat) (a :: *) where
Leaf :: Node Black Z a
-- 3) Every leaf is black (and has black height 0)
BNode :: Node lc h a -> a -> Node rc h a -> Node Black (S h) a
-- 5) The black height left and right is the same.
-- Adding a black node increases the black height
RNode :: Node Black h a -> a -> Node Black h a -> Node Red h a
-- 4) If a node is red, its children must be black
```

As we can see, a Node is either a Leaf, a BNode, or a RNode. Leaves are black
(invariant 3), and have black-height zero. A BNode (black node) can be
constructed from a left child, a value, and a right child. There are no
restrictions on the colors of the left and right child, and they may even
differ. However, we do enforce that the black height of both children is the
same: namely `h`

(invariant 5). Since this node itself is black as well, we
produce a ndoe of black-height `h + 1`

. The Red `RNodes`

have the same structure as
the BNodes, however, we not only enforce that the children have the same
black-height, but also that they are both black!

The invariant we have not enforced yet is invariant 2: the root of a red black
tree must be black. So, we introduce a type `RedBlackTree`

that models a
proper Red-Black tree, whose root is black, and hides the black-height phantom
type from the user:

```
data RedBlackTree (a :: *) where
Tree :: Node Black h a -> RedBlackTree a
```

The `RedBlackTree`

type enforces all our invariants. Hence, if an operation
returns something of type RedBlackTree: it is guaranteed that all invariants
hold. Hence, the result is a proper Red-Black tree.

## Inserting Into Red-Black Trees

Construction an empty red black tree is trivial.

```
empty :: RedBlackTree a
= Tree Leaf empty
```

Let’s see if we can also insert elements, so we can construct more interesting trees. To do so, we introduce some more types :D

When we insert something into a subtree rooted at a black node, the color of
the root may change to red, thus potentially invalidating an invariant. To
distinguish between the two cases (whether or not the root of the (sub)tree is
indeed black) we have two cases. `BDone`

, that tells us that the root is still
black (and that all other invariants hold as well), or `NewRed`

, which tells us
that the insert required us to color this node red (but it is a proper
red-node: so all our invariants (except invariant 2) hold for this subtree).

```
data BlackInsert (h :: Nat) (a :: *) where
BDone :: Node Black h a -> BlackInsert h a
NewRed :: Node Red h a -> BlackInsert h a
```

When we insert into a red node, we end up with a proper RedBlack tree with a
red node as root (`RDone`

), or a red node that has a red child:

```
data RedInsert (h :: Nat) (a :: *) where
RDone :: Node Red h a -> RedInsert h a
RedRed :: RedRed h a -> RedInsert h a
```

Since we cannot construct a red `Node`

with a Red child. We introduce the
`RedRed`

data type, which models a red node in which one of its children is also
red. Note that the type enforces that only one of the children violates
invariant 4, not both, and that all other invariants still hold (i.e. that the
black-height of both subtrees is the same).

```
data RedRed (h :: Nat) (a :: *) where
LeftR :: Node Red h a -> a -> Node Black h a -> RedRed h a
RightR :: Node Black h a -> a -> Node Red h a -> RedRed h a
```

Also note that the children of the red child do form a proper red-black tree, so the only violation is in the current node.

If we want to insert something into a node whose color we do not know (such as
for the children of a Black node). We do not know if we get something of type
BlackInsert, or of type `RedInsert`

. Hence, we introduce a new type `InsertN`

that
captures this:

```
data InsertN (h :: Nat) (a :: *) where
RIns :: RedInsert h a -> InsertN h a
BIns :: BlackInsert h a -> InsertN h a
```

Now that we have all these data types, we can actually implement inserting an element into a subtree. We start with the most general case, in which we do not know the color of the node. In this case, we determine what sort of node we have, and delegate the insert to an other function.

```
insertN :: Ord a => a -> Node c h a -> InsertN h a
@Leaf = BIns $ insertL x n
insertN x n@(BNode _ _ _) = BIns $ insertB x n
insertN x n@(RNode _ _ _) = RIns $ insertR x n insertN x n
```

Inserting something in a leaf creates a new red node. Furthermore, note that leaves specifically have black height zero.

```
insertL :: a -> Node Black Z a -> BlackInsert Z a
Leaf = NewRed $ RNode Leaf x Leaf insertL x
```

Inserting into a red node is also easy: we know that our children are black, so
we just use `insertB`

on the proper child to do the actual inserting. If it
turns out that the child is still black after inserting then we are happy because
we are done. We simply tell our parent and that is it.

If turns out that the child has become red then we are being lazy: when we started the tree was a proper red-black tree which did not have any red nodes with red children. Hence, my parent must be black. So, we are just going to tell it that we are in trouble and we let it figure out how to deal with the problem.

```
insertR :: Ord a => a -> Node Red h a -> RedInsert h a
RNode l y r)
insertR x (| x <= y = case insertB x l of
BDone l' -> RDone $ RNode l' y r
NewRed l' -> RedRed $ LeftR l' y r
| otherwise = case insertB x r of
BDone r' -> RDone $ RNode l y r'
NewRed r' -> RedRed $ RightR l y r'
```

Inserting in a black node is the most complicated. For two reasons: 1) we don’t know what color our children are, and 2) if we happen to have red children, then they might force their problems onto us. So, we have a few cases that we have to handle. Let’s start with the easy ones.

The first and third cases in the case statement on insertN are easy: all the interesting stuff happened somewhere down the tree, and currently we are only walking back up the tree plugging in the updated child.

The second case is where the interestingness stops (or starts, depending on your viewpoint ;)): inserting the new value in the child caused it to be recolored. However, since its black-height is still the same, and since we are a black node ourselves, we can remain a black node. This also means that for everything further up the tree the colors will remain the same.

The (only) interesting case is the last one: after inserting the new value, we
ended up with a RedRed violation in that child, so we have to do some work to
restore the invariants. The `balanceL`

and `balanceR`

functions which we will see
next take care of that work. However, in doing so they have to color the
current node red. Hence, we “tell our parent” that we have become red.

```
insertB :: Ord a => a -> Node Black h a -> BlackInsert h a
@Leaf = insertL x n
insertB x nBNode l y r)
insertB x (| x <= y = case insertN x l of
BIns (BDone l') -> BDone $ BNode l' y r
BIns (NewRed l') -> BDone $ BNode l' y r
RIns (RDone l') -> BDone $ BNode l' y r
RIns (RedRed l') -> NewRed $ balanceL l' y r
| otherwise = case insertN x r of
BIns (BDone r') -> BDone $ BNode l y r'
BIns (NewRed r') -> BDone $ BNode l y r'
RIns (RDone r') -> BDone $ BNode l y r'
RIns (RedRed r') -> NewRed $ balanceR l y r'
```

Note that `insertB`

promisses that the black height remains the same. So in
particular, we we recolor this node from black to red, then the black-height of
both children must increase. Indeed, the `balanceL`

and `balanceR`

functions take a
left and right child (one of which violates the Red-Red invariant) of height
`h'=h-1`

, and produces a red node whose height is `h'+1=h`

.

`balanceL`

takes a `RedRed`

as the left child, a value, and a proper subtree
(of which we don’t care what color its root has) and we construct a new Red
node. This is essentially a left-rotate in which we color the new root red, and
the two children black. See Figure 2 for an illustration.

```
balanceL :: RedRed h a -> a -> Node c h a -> Node Red (S h) a
LeftR (RNode lll llx llr) lx lr) x r = RNode l' lx r'
balanceL (where
= BNode lll llx llr
l' = BNode lr x r
r' RightR ll lx (RNode lrl lrx lrr)) x r = RNode l' lrx r'
balanceL (where
= BNode ll lx lrl
l' = BNode lrr x r r'
```

`balanceR`

is it’s symmetric companion which does a right-rotate and a
recoloring.

```
balanceR :: Node c h a -> a -> RedRed h a -> Node Red (S h) a
LeftR (RNode rll rlx rlr) rx rr) = RNode l' rlx r'
balanceR l x (where
= BNode l x rll
l' = BNode rlr rx rr
r' RightR rl rx (RNode rrl rrx rrr)) = RNode l' rx r'
balanceR l x (where
= BNode l x rl
l' = BNode rrl rrx rrr r'
```

So now that we know how to insert something into a node. Inserting into a
`RedBlackTree`

is easy:

```
insert :: Ord a => a -> RedBlackTree a -> RedBlackTree a
Tree n) = case insertB x n of
insert x (BDone bn -> Tree bn
NewRed rn -> Tree $ turnBlack rn
```

`turnBlack`

makes sure that the root is black: if the insert would have
returned a subtree rooted at a red node, we recolor it.

```
turnBlack :: Node Red h a -> Node Black (S h) a
RNode l x r) = BNode l x r turnBlack (
```

Now that we know how to insert one node, we can of course also insert many of them:

```
insertAll :: Ord a => [a] -> RedBlackTree a -> RedBlackTree a
= flip (foldr insert) insertAll
```

## Deleting Elements

Everyone can do insertions into Red-Black trees. So let’s do deletions as well. We again start by defining data types. After inserting an element into the tree we observed that after inserting the element the black-height either stayed the same, or it increased by one. When we remove an element, we see the reverse: either the height stays the same, or it is decreased by one.

If we delete something from a subtree rooted at a red node, we can locally fix the problem, and increase the height to its original value, by coloring the root black. Hence, we represent the result of deleting something from a red-subtree by the following data type.

```
data RedDelete (h :: Nat) (a :: *) where
RDeleted :: Node Red h a -> RedDelete h a
NewBlack :: Node Black h a -> RedDelete h a
```

If we remove something from a black subtree, we cannot use this trick of
recoloring the root. So this is the place where we may end up with a subtree
that is too shallow. We expres this in the `BlackDelete`

data type.

```
data BlackDelete (h :: Nat) (a :: *) where
BDeleted :: Node Black h a -> BlackDelete h a
BShallow :: Node Black h a -> BlackDelete (S h) a
```

The type signature of the `BShallow`

is best interpeted as: if you give me a
black node of height `h`

, I can pretend to be a `BlackDelete`

of height `h+1`

. We
also add some shorthands to construct `RedDelete`

and `BlackDelete`

values:

```
rDeleted :: Node Black h a -> a -> Node Black h a -> RedDelete h a
= RDeleted $ RNode l x r rDeleted l x r
```

```
newBlack :: Node lc h a -> a -> Node rc h a -> RedDelete (S h) a
= NewBlack $ BNode l x r newBlack l x r
```

```
bDeleted :: Node lc h a -> a -> Node rc h a -> BlackDelete (S h) a
= BDeleted $ BNode l x r bDeleted l x r
```

Now that we have the data types, let’s start with the easiest case. Deleting
something from a red subtree. Once we have found the node containing the
element that we want to delete, we distinguish two cases. If this subtree does
not contain any other elements, i.e. if its left and right children are
leaves. We can easily delete the element: we simply return a leaf, which has
the same black-height as our original subtree, wrapped in a `NewBlack`

constructor.

If however we want to delete an element in an internal node, we extract the
smallest element `m`

in the right subtree, and replace the value in the current
node by `m`

.

```
deleteR :: Ord a => a -> Node Red h a -> RedDelete h a
RNode l y r)
deleteR x (| x == y = case (l, r) of
Leaf, Leaf) -> NewBlack Leaf
(BNode _ _ _) -> let (m,r') = extractMinB r in
(_,
redDeleteRight l m r'| x < y = redDeleteLeft (deleteB x l) y r
| x > y = redDeleteRight l y (deleteB x r)
```

We will cover `extractMinB`

(and its counterpart `extractMinR`

) later. The
`redDeleteRight`

and `redDeleteLeft`

functions are convienience functions to
construct new `RedDelete`

values. `redDeleteLeft`

takes a `BlackDelete`

value
representing left child after deleting an element, a value, and a right child,
and constructs a new node wrapped in a `RedDelete`

. The `redDeleteRight`

function is symmetric.

```
redDeleteLeft :: BlackDelete h a -> a -> Node Black h a
-> RedDelete h a
BDeleted l) = rDeleted l
redDeleteLeft (BShallow l) = redBalanceL l redDeleteLeft (
```

```
redDeleteRight :: Node Black h a -> a -> BlackDelete h a
-> RedDelete h a
BDeleted r) = rDeleted l x r
redDeleteRight l x (BShallow r) = redBalanceR l x r redDeleteRight l x (
```

If the left subtree after deletion is of the form `BDeleted _`

we can directly
reconstruct the current node. However, if the left subtree after deletion is
too shallow, i.e. it only has black-height `h-1`

, then we have to rebalance the
tree in order to construct a proper subtree. The `redBalanceL`

and
`redBalanceR`

functions take care of this.

```
redBalanceL :: Node Black h a -> a -> Node Black (S h) a
-> RedDelete (S h) a
BNode rl rx rr) = case rl of
redBalanceL l x (Leaf -> blackCase rl
BNode _ _ _ -> blackCase rl
RNode _ _ _ -> let l' = RightR l x rl in
RDeleted $ balanceL l' rx rr
where
= let l' = RNode l x rl' in
blackCase rl' newBlack l' rx rr
```

The operations of `redBalanceL`

are depicted in Figures 3 and 4. In case `rl`

is black, a simple left-rotate suffices. In case `rl`

is red we also do a
left-rotate. This leads to a red-red subtree, which we fix using the `balanceL`

function. The function `redBalanceR`

is symmetric:

```
redBalanceR :: Node Black (S h) a -> a -> Node Black h a
-> RedDelete (S h) a
BNode ll lx lr) x r = case lr of
redBalanceR (Leaf -> blackCase lr
BNode _ _ _ -> blackCase lr
RNode _ _ _ -> let r' = LeftR lr x r in
RDeleted $ balanceR ll lx r'
where
= let r' = RNode lr' x r in
blackCase lr' newBlack ll lx r'
```

To delete an element in a black subtree we essentially use the same approach as before. However, since we do not know the color of the children, we have a few more cases to consider, which makes our code slightly more messy.

```
deleteB :: Ord a => a -> Node Black h a -> BlackDelete h a
Leaf = BDeleted $ Leaf
deleteB _ BNode l y r)
deleteB x (| x == y = case (l, r) of
Leaf, Leaf ) -> BShallow Leaf
(Leaf, RNode Leaf z Leaf) -> bDeleted Leaf z Leaf
(RNode Leaf z Leaf, Leaf ) -> bDeleted Leaf z Leaf
(RNode _ _ _ ) ->
(_, let (m,r') = extractMinR r in
blackDeleteRightR l m r'BNode _ _ _ ) ->
(_, let (m,r') = extractMinB r in
blackDeleteRightB l m r'| x < y = case l of
Leaf -> blackDeleteLeftB (deleteB x l) y r
BNode _ _ _ -> blackDeleteLeftB (deleteB x l) y r
RNode _ _ _ -> blackDeleteLeftR (deleteR x l) y r
| x > y = case r of
Leaf -> blackDeleteRightB l y (deleteB x r)
BNode _ _ _ -> blackDeleteRightB l y (deleteB x r)
RNode _ _ _ -> blackDeleteRightR l y (deleteR x r)
```

In the case both `l`

and `r`

are leaves, the black-height of the tree after
deletion –a single leaf– has black-height zero, whereas black-height one is
required. Thus, we use our `BShalow`

constructor. In the other two leaf cases
there is still one remaining value in the subtree, one that is stored at a red
node. We can “recolor” this node black to obtain something of black-height
one. The final two cases for when `x == y`

we again extract the minimum value
`m`

in the right subtree, and replace the value stored in this node by `m`

.

In the cases that `x < y`

or `x > y`

, we delete the value in the appropriate
subtree. We need the pattern matching on `l`

and `r`

to convince the compiler
that these subtrees have the right color for us to use the blackDelete
functions.

As with the deletes in Red subtrees, we have a few functions that describe how
to construct a new `BlackDelete`

value from a left-subtree in which an element
is deleted, an element that we wish to store in the current node, and a regular
right subtree. These functions are fairly straight forward: if one of the
subtrees (after deletion) is a `BShallow`

we rebalance, and otherwise we
directly recmobine and construct a `BlackDelete`

value using the `BDeleted`

constructor.

```
blackDeleteLeftB :: BlackDelete h a -> a -> Node rc h a
-> BlackDelete (S h) a
BDeleted l) = bDeleted l
blackDeleteLeftB (BShallow l) = blackBalanceL l blackDeleteLeftB (
```

```
blackDeleteLeftR :: RedDelete h a -> a -> Node rc h a
-> BlackDelete (S h) a
RDeleted l) = bDeleted l
blackDeleteLeftR (NewBlack l) = bDeleted l blackDeleteLeftR (
```

And of course we also have these functions in case we deleted something in the right subtree instead.

```
blackDeleteRightB :: Node rc h a -> a -> BlackDelete h a
-> BlackDelete (S h) a
BDeleted r) = bDeleted l x r
blackDeleteRightB l x (BShallow r) = blackBalanceR l x r blackDeleteRightB l x (
```

```
blackDeleteRightR :: Node rc h a -> a -> RedDelete h a
-> BlackDelete (S h) a
RDeleted r) = bDeleted l x r
blackDeleteRightR l x (NewBlack r) = bDeleted l x r blackDeleteRightR l x (
```

The most difficult part is rebalancing in black nodes. We balance based on the color of the node.

```
blackBalanceR :: Node c (S h) a -> a -> Node Black h a
-> BlackDelete (S (S h)) a
@(BNode _ _ _) = blackBalanceRB l
blackBalanceR l@(RNode _ _ _) = blackBalanceRR l blackBalanceR l
```

The actual balancing operations are best explained using figures. In both
variants `blackBalanceR`

, we do a right-rotate. Based on the color of a
particular subtree this may introduce a `RedRed`

subtree, which we fix using
another rebalancing operation. See Figures 5 and 6 for the operation of
`blackBalanceRB`

.

```
blackBalanceRB :: Node Black (S h) a -> a -> Node Black h a
-> BlackDelete (S (S h)) a
BNode ll lx lr) x r = case lr of
blackBalanceRB (Leaf -> blackCase lr
BNode _ _ _ -> blackCase lr
RNode _ _ _ -> let r' = LeftR lr x r
= balanceR ll lx r'
t in BDeleted $ turnBlack t
where
= let r' = RNode lr' x r
blackCase lr' in BShallow $ BNode ll lx r'
```

`blackBalanceRR`

handles the case that we want to construct a black node of
height `h+2`

, but our right subchild is of height only `h`

, and our left child
is red. We again do a right-rotation and recoloring that is depicted in Figures
7 and 8.

```
blackBalanceRR :: Node Red (S h) a -> a -> Node Black h a
-> BlackDelete (S (S h)) a
RNode ll lx (BNode lrl lrx lrr)) x r = case lrr of
blackBalanceRR (Leaf -> blackCase lrr
BNode _ _ _ -> blackCase lrr
RNode _ _ _ -> let rr' = LeftR lrr x r
= balanceR lrl lrx rr'
r' in bDeleted ll lx r'
where
= let rr' = RNode lrr' x r
blackCase lrr' = BNode lrl lrx rr'
r' in bDeleted ll lx r'
```

Again we have symmetric balancing functions for left-rotates that we use when
we deleted stuff in the left subtree.
> blackBalanceL :: Node Black h a -> a -> Node c (S h) a
> -> BlackDelete (S (S h)) a
> blackBalanceL l x r@(BNode _ _ *) = blackBalanceLB l x r
> blackBalanceL l x r@(RNode * _ _) = blackBalanceLR l x r

```
blackBalanceLB :: Node Black h a -> a -> Node Black (S h) a
-> BlackDelete (S (S h)) a
BNode rl rx rr) = case rl of
blackBalanceLB l x (Leaf -> blackCase rl
BNode _ _ _ -> blackCase rl
RNode _ _ _ -> let l' = RightR l x rl
= balanceL l' rx rr
t in BDeleted $ turnBlack t
where
= let l' = RNode l x rl'
blackCase rl' in BShallow $ BNode l' rx rr
```

```
blackBalanceLR :: Node Black h a -> a -> Node Red (S h) a
-> BlackDelete (S (S h)) a
RNode (BNode rll rlx rlr) rx rr) = case rll of
blackBalanceLR l x (Leaf -> blackCase rll
BNode _ _ _ -> blackCase rll
RNode _ _ _ -> let ll' = RightR l x rll
= balanceL ll' rlx rlr
l' in bDeleted l' rx rr
where
= let ll' = RNode l x rll'
blackCase rll' = BNode ll' rlx rlr
l' in bDeleted l' rx rr
```

Recall that to delete a (value in a) non-leaf node `n`

, we actually extracted
the smallest element `m`

from the right subtree of `n`

and replaced the value
in `n`

by `m`

. We used the functions `extractMinR`

and `extractMinB`

to extract
this minimum. So what remains is to actually implement these
functions. Extracting an element is fairly similar to deleting one, so we can
reuse a large part of the code we have already seen. Let’s start with
extracting the minimum from a red node:

```
extractMinR :: Node Red h a -> (a, RedDelete h a)
RNode Leaf x r) = (x, NewBlack r)
extractMinR (RNode l@(BNode _ _ _) x r) =
extractMinR (-> redDeleteLeft l' x r) <$> extractMinB l (\l'
```

In case the left child of the current (red) node is a leaf, this node contains
the minimum. So we return it, and the remainder of this subtree, that is, the
right child. Otherwise, the left subtree is a black, non-leaf, node so we can
extract the minimum in that subtree using the function `extractMinB`

. This
produces a tuple `(m,l')`

with the minimum `m`

and the remainder of the left
subtree `l'`

. We use the `<$>`

operator to apply the `redDeleteLeft`

function
on this second element of the tuple, the remainder `l'`

, and combine it with
our right child to produce a subtree without element `m`

. The `extractMinB’
function that extracts the minimum from a black subtree works analogously.

```
extractMinB :: Node Black (S h) a -> (a, BlackDelete (S h) a)
BNode Leaf x r) = case r of
extractMinB (Leaf -> (x, BShallow r)
RNode _ _ _ -> (x, BDeleted $ turnBlack r)
BNode l@(BNode _ _ _) x r) =
extractMinB (-> blackDeleteLeftB l' x r) <$> extractMinB l
(\l' BNode l@(RNode _ _ _) x r) =
extractMinB (-> blackDeleteLeftR l' x r) <$> extractMinR l (\l'
```

With all of this in place we then get the following function to delete an
element from a `RedBlackTree`

.

```
delete :: Ord a => a -> RedBlackTree a -> RedBlackTree a
Tree bn) = case deleteB x bn of
delete x (BDeleted bn' -> Tree bn'
BShallow bn' -> Tree bn'
```

Note that we cannot move the Tree constructor, that occurs in both cases of the case distinction, before the case pattern, since the two cases produce values of a different type: the trees that they return have different black heights.

## Concluding Remarks

We have seen how to enforce several properties of Red-Black trees in the type system. This gives us certain guarantees about the correctness of our implementation. However, you may have noticed that we still miss one property to provide us a proof that this implementation is correct. Namely, that the Red-Black tree is a binary search tree (i.e. for each node, the values in the left (right) subtree are smaller (larger) than the value stored in this node). So can we also enforce that in the type system? The answer is yes. To do this, we will need dependent types; types that depend on the values in our tree. This is currently possible, even in Haskell (using singletons), however at the moment that does not lead to very elegant code. Hopefully, this will improve in the future, so I can return to this at a later time.

## Acknowledgments and Related Work

The implementation of the inserts is based on Okasaki’s famous work on purely functional Red-Black trees. I also looked at Stefan Kahrs and Matt Might’s implementations for inspirations on the delete operations. However, the setup with the types as I presented here requires fairly different code than that is used in their solutions.