Using GADTs, phantom types, quantification and empty data declarations to put constraints on nodes in red-black trees

README.md

A red-black tree has some constraints:

1. A node is either red or black.
2. The root is black.
3. All leaves are black.
4. Both children of every red node are black.
5. Every simple path from a given node to any of its descendant leaves contains the same number of black nodes.

Using the declarations in RBTree.hs, all these five constraints are implemented.

RBTree.hs

{-# LANGUAGE GADTs, EmptyDataDecls, ExistentialQuantification #-}

module RBTree where

	-- Node color
	data Red
	data Black
	

	-- Node depth
	data Zero
	data Succ a


	-- The data type and its constructors
	data RBNode color depth a where
		Leaf        :: RBNode Black Zero a
		RedBranch   :: a -> RBNode Black depth a -> RBNode Black depth a -> RBNode Red    depth       a
		BlackBranch :: a -> RBNode c1    depth a -> RBNode c2    depth a -> RBNode Black (Succ depth) a

	-- The tree itself
	data RBTree a = forall d . Root (RBNode Black d a)


	-- Just making the tree showable
	instance Show a => Show (RBNode c d a) where
		show Leaf = "Leaf"
		show (RedBranch   x t1 t2) = "RedBranch ("   ++ show x ++ ") (" ++ show t1 ++ ") (" ++ show t2 ++ ")"
		show (BlackBranch x t1 t2) = "BlackBranch (" ++ show x ++ ") (" ++ show t1 ++ ") (" ++ show t2 ++ ")"
			
	instance Show a => Show (RBTree a) where
		show (Root t) = "Root (" ++ show t ++ ")"

I found a complete implementation here on Github.

This seems to have a serious efficiency problem: searching for a key requires a three-way pattern match (Leaf/RedBranch/BlackBranch) at each node, rather than just a two-way match (Leaf/Branch) as in a standard red-black tree. Is there a way to avoid this without compromising type safety? Or would it be better to switch to 2-3-4 trees, whose invariant is easier to represent through types?

Is that really a problem? If the pattern match is implemented as a jump table, there's no time penalty.