---
title: A Red-Black Tree Implementation with Provable Properties
---
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](http://www.haskell.org)'s type system to enforce several
properties of Red-Black trees.
![An example of a Red black tree. A leaf is drawn as two horizontal line
segments. The green numbers indicate the black-height of each
subtree.](/figures/red-black_tree/example_rb-tree.png)
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
1. every node is red or black,
2. the root is black,
3. every leaf is black,
4. if a node is red, then both its children are black, and
5. 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](http://haskell.org/ghc/):
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE GADTs #-}
This page is written as as literate haskell. The complete source code can be
found [here](/RedBlackTree.lhs).
> 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
> empty = Tree Leaf
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
> insertN x n@Leaf = BIns $ insertL x n
> insertN x n@(BNode _ _ _) = BIns $ insertB x n
> insertN x n@(RNode _ _ _) = RIns $ insertR 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
> insertL x Leaf = NewRed $ RNode Leaf x Leaf
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
> insertR x (RNode l y r)
> | 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
> insertB x n@Leaf = insertL x n
> insertB x (BNode l y r)
> | 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
> balanceL (LeftR (RNode lll llx llr) lx lr) x r = RNode l' lx r'
> where
> l' = BNode lll llx llr
> r' = BNode lr x r
> balanceL (RightR ll lx (RNode lrl lrx lrr)) x r = RNode l' lrx r'
> where
> l' = BNode ll lx lrl
> r' = BNode lrr x r
![The `LeftR` case of the balanceL function. A node/subtree is blue if we do
not know or care about its actual color.](
/figures/red-black_tree/balanceL_case_leftR.png)
`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
> balanceR l x (LeftR (RNode rll rlx rlr) rx rr) = RNode l' rlx r'
> where
> l' = BNode l x rll
> r' = BNode rlr rx rr
> balanceR l x (RightR rl rx (RNode rrl rrx rrr)) = RNode l' rx r'
> where
> l' = BNode l x rl
> r' = BNode rrl rrx rrr
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
> insert x (Tree n) = case insertB x n of
> 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
> turnBlack (RNode l x r) = BNode l x r
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
> insertAll = flip (foldr insert)
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 l x r = RDeleted $ RNode l x r
> newBlack :: Node lc h a -> a -> Node rc h a -> RedDelete (S h) a
> newBlack l x r = NewBlack $ BNode l x r
> bDeleted :: Node lc h a -> a -> Node rc h a -> BlackDelete (S h) a
> bDeleted l x r = BDeleted $ BNode 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
> deleteR x (RNode l y r)
> | 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
> redDeleteLeft (BDeleted l) = rDeleted l
> redDeleteLeft (BShallow l) = redBalanceL l
> redDeleteRight :: Node Black h a -> a -> BlackDelete h a
> -> RedDelete h a
> redDeleteRight l x (BDeleted r) = rDeleted l x r
> redDeleteRight l x (BShallow r) = redBalanceR l x r
![The operation of `redBalanceL` in case `rl` is
black.](/figures/red-black_tree/redBalanceL_case_black.png)
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
> redBalanceL l x (BNode rl rx rr) = case rl of
> Leaf -> blackCase rl
> BNode _ _ _ -> blackCase rl
> RNode _ _ _ -> let l' = RightR l x rl in
> RDeleted $ balanceL l' rx rr
> where
> blackCase rl' = let l' = RNode l x rl' in
> newBlack l' rx rr
![The operation of `redBalanceL` in case `rl` is
red.](/figures/red-black_tree/redBalanceL_case_red.png)
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
> redBalanceR (BNode ll lx lr) x r = case lr of
> Leaf -> blackCase lr
> BNode _ _ _ -> blackCase lr
> RNode _ _ _ -> let r' = LeftR lr x r in
> RDeleted $ balanceR ll lx r'
> where
> blackCase lr' = let r' = RNode lr' x r in
> 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
> deleteB _ Leaf = BDeleted $ Leaf
> deleteB x (BNode l y r)
> | 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
> blackDeleteLeftB (BDeleted l) = bDeleted l
> blackDeleteLeftB (BShallow l) = blackBalanceL l
> blackDeleteLeftR :: RedDelete h a -> a -> Node rc h a
> -> BlackDelete (S h) a
> blackDeleteLeftR (RDeleted l) = bDeleted l
> blackDeleteLeftR (NewBlack l) = bDeleted l
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
> blackDeleteRightB l x (BDeleted r) = bDeleted l x r
> blackDeleteRightB l x (BShallow r) = blackBalanceR l x r
> blackDeleteRightR :: Node rc h a -> a -> RedDelete h a
> -> BlackDelete (S h) a
> blackDeleteRightR l x (RDeleted r) = bDeleted l x r
> blackDeleteRightR l x (NewBlack r) = bDeleted l x r
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
> blackBalanceR l@(BNode _ _ _) = blackBalanceRB l
> blackBalanceR l@(RNode _ _ _) = blackBalanceRR l
![The operation in the `blackBalanceRB` function for the case that `lr` is
black.](/figures/red-black_tree/blackBalanceRB_case_black.png)
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
> blackBalanceRB (BNode ll lx lr) x r = case lr of
> Leaf -> blackCase lr
> BNode _ _ _ -> blackCase lr
> RNode _ _ _ -> let r' = LeftR lr x r
> t = balanceR ll lx r'
> in BDeleted $ turnBlack t
> where
> blackCase lr' = let r' = RNode lr' x r
> in BShallow $ BNode ll lx r'
![The operation in the `blackBalanceRB` function for the case that `lr` is
red.](/figures/red-black_tree/blackBalanceRB_case_red.png)
`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
> blackBalanceRR (RNode ll lx (BNode lrl lrx lrr)) x r = case lrr of
> Leaf -> blackCase lrr
> BNode _ _ _ -> blackCase lrr
> RNode _ _ _ -> let rr' = LeftR lrr x r
> r' = balanceR lrl lrx rr'
> in bDeleted ll lx r'
> where
> blackCase lrr' = let rr' = RNode lrr' x r
> r' = BNode lrl lrx rr'
> in bDeleted ll lx r'
![The operation in the `blackBalanceRR` function for the case that `lrr` is
black.](/figures/red-black_tree/blackBalanceRR_case_black.png)
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
> blackBalanceLB l x (BNode rl rx rr) = case rl of
> Leaf -> blackCase rl
> BNode _ _ _ -> blackCase rl
> RNode _ _ _ -> let l' = RightR l x rl
> t = balanceL l' rx rr
> in BDeleted $ turnBlack t
> where
> blackCase rl' = let l' = RNode l x rl'
> in BShallow $ BNode l' rx rr
![The operation in the `blackBalanceRR` function for the case that `lrr` is
red.](/figures/red-black_tree/blackBalanceRR_case_red.png)
> blackBalanceLR :: Node Black h a -> a -> Node Red (S h) a
> -> BlackDelete (S (S h)) a
> blackBalanceLR l x (RNode (BNode rll rlx rlr) rx rr) = case rll of
> Leaf -> blackCase rll
> BNode _ _ _ -> blackCase rll
> RNode _ _ _ -> let ll' = RightR l x rll
> l' = balanceL ll' rlx rlr
> in bDeleted l' rx rr
> where
> blackCase rll' = let ll' = RNode l x rll'
> l' = BNode ll' rlx rlr
> 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)
> extractMinR (RNode Leaf x r) = (x, NewBlack r)
> extractMinR (RNode l@(BNode _ _ _) x r) =
> (\l' -> redDeleteLeft l' x r) <$> extractMinB 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)
> extractMinB (BNode Leaf x r) = case r of
> Leaf -> (x, BShallow r)
> RNode _ _ _ -> (x, BDeleted $ turnBlack r)
> extractMinB (BNode l@(BNode _ _ _) x r) =
> (\l' -> blackDeleteLeftB l' x r) <$> extractMinB l
> extractMinB (BNode l@(RNode _ _ _) x r) =
> (\l' -> blackDeleteLeftR l' x r) <$> extractMinR 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
> delete x (Tree bn) = case deleteB x bn of
> 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](http://www.eecs.usma.edu/webs/people/okasaki/jfp99.ps). I also looked at
[Stefan Kahrs](http://www.cs.kent.ac.uk/people/staff/smk/) and [Matt
Might's](http://www.cs.kent.ac.uk/people/staff/smk/) 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.