You can enforce all Red-Black tree invariants using GADTs and some type hackery (existential quantification, type arithmetic, data kinds). The properties are:
- A node is either red or black.
- The root is black.
- All leaves (NIL) are black.
- Every red node must have two black child nodes.
- Every path from a given node to any of its descendant
leaves contains the same number of black nodes.
And here is example code:
{-# LANGUAGE GADTs, StandaloneDeriving, ExistentialQuantification,
KindSignatures, DataKinds #-}
data Nat = Zero | Succ Nat
data Color = Red | Black
data Node :: Color -> Nat -> * -> * where
Nil :: Node Black Zero a
RedNode :: a -> Node Black n a -> Node Black n a -> Node Red n a
BlackNode :: a -> Node c1 n a -> Node c2 n a -> Node Black (Succ n) a
data RBTree a = forall n. RBTree (Node Black n a)
deriving instance (Show a) => Show (Node c n a)
deriving instance (Show a) => Show (RBTree a)
instance Functor (Node c n) where
fmap f Nil = Nil
fmap f (RedNode x l r) = RedNode (f x) (fmap f l) (fmap f r)
fmap f (BlackNode x l r) = BlackNode (f x) (fmap f l) (fmap f r)
instance Functor RBTree where
fmap f (RBTree t) = RBTree (fmap f t)
You can use it like this:
tree = RBTree $ BlackNode 3 (RedNode 4 Nil Nil) (RedNode 5 Nil Nil)
main = print $ fmap (*5) tree
Result:
RBTree (BlackNode 15 (RedNode 20 Nil Nil) (RedNode 25 Nil Nil))
But this won't compile:
tree = RBTree $ BlackNode 3 (RedNode 4 Nil Nil) (BlackNode 5 Nil Nil)
You will get a nice error message:
Couldn't match type `Succ Zero' with `Zero'
Expected type: Node Black Zero a0
Actual type: Node Black (Succ Zero) a0
In the return type of a call of `BlackNode'
In the third argument of `BlackNode', namely
`(BlackNode 5 Nil Nil)'
In the second argument of `($)', namely
`BlackNode 3 (RedNode 4 Nil Nil) (BlackNode 5 Nil Nil)'