Code review time! https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L27 https://github.com/yairchu/red-black-tree/blob/master/RedBla... Fir

Code review time! https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L27 https://github.com/yairchu/red-black-tree/blob/master/RedBla... First we create two differently typed tags for Red and Black. data Red data Black Note this differs from something like data Color = Red | Black in that Red and Black are distinct at the type level---the compiler will actually complain if one is used where the other ought to be. Now we state that Trees must have Black roots. This is done using a GADT (Generalized Algebraic Data Type) which allows us to build constructors of types which restrict some of the types. data Tree a where Tree :: Node Black n a -> Tree a For instance, compare PoorTree which would let us make Trees with Red roots data PoorTree c n a = PoorTree (Node c n a) It really does nothing more than wrap up a Node to hide it and change the interface (if you want). Now we need one last piece before digging in to the core. This is the existence of Type-level Naturals. The idea is that, like Red and Black, we introduce two new distinct types, one basic and one parametric. data Zero = Zero data Succ a = Succ a which lets us write (very verbose) naturals like (Succ (Succ (Succ Zero))) == 3 and have the type reflect this exact value (Succ (Succ (Succ Zero))) :: (Succ (Succ (Succ Zero))) (Note this is a little weird, since we can also form the value (Succ 'a' :: Succ Char) which doesn't make much sense. More powerful dependently typed features help here.) Now consider just a branch in the tree, we form that with a simple data type data NodeH l r n a = NodeH (Node l n a) a (Node r n a) which tracks the left and right colors in its type using the l and r type parameters. It also guarantees the constraint that both the left and right child trees have the same black-height. So, if (black3 :: Node Black (Succ Zero) Char) then (NodeH black3 'a' black3 :: NodeH Black Black (Succ Zero) Char). And if (black2 :: Node Black Zero Char) then (NodeH black3 'a' black2) is a compile time type error. So with all these pieces, we can encode the Red/Black criteria directly into our Nodes. Remember already that if we have a Tree it must have the first Node be Black. We can now construct new Nodes in three ways, each of these ways being constrained so as to enforce the balance rules. data Node t n a where -- If we construct a Node with Nil, it forms a leaf. -- Not only are we not allowed to associate left and -- right branches (we don't get to give it a NodeH type), -- we're forced to set the numerical type parameter to Zero ~= 0. Nil :: Node Black Zero a -- If we construct a Node with BlackNode, we can pass a -- subtree with the NodeH parameter, but the type of node we -- get back is necessarily going to increase its height -- since (Succ n) is like (n + 1). BlackNode :: NodeH t0 t1 n a -> Node Black (Succ n) a -- Or we can construct a Red node. In this case, our black-height -- remains unchanged, but we can ONLY do so when we've got a NodeH -- branch with two black subNodes. RedNode :: NodeH Black Black n a -> Node Red n a So, it's a type error to construct a tree in this format which doesn't obey the Red/Black balance rules. Any transformations you write on the tree will be rejected by the compiler if they break the rules.