Dependently Typed Red-Black Tree (incomplete, based on a great talk by Stephanie Weirich)

Maple.hs

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

-- https://www.youtube.com/watch?v=n-b1PYbRUOY

module Maple where

data Nat :: * where
  Z :: Nat
  S :: Nat -> Nat

data Color :: * where
  R :: Color
  B :: Color

data Tree :: Color -> Nat -> * where
  E  :: Tree B Z
  TR :: Int -> Tree B n -> Tree B n -> Tree R n
  TB :: Int -> Tree a n -> Tree b n -> Tree B (S n)

data RBT where
  Root :: Tree B n -> RBT

data HiddenTree :: Nat -> * where
  HR :: Tree R n -> HiddenTree n
  HB :: Tree B (S n) -> HiddenTree (S n)

type family Increment (c :: Color) (n :: Nat) :: Nat where
  Increment R x = x
  Increment B x = S x

data Sing :: Color -> * where
  SR :: Sing R
  SB :: Sing B

data AlmostTree :: Nat -> * where
  AT :: Sing c -> Int -> Tree a n -> Tree b n -> AlmostTree (Increment c n)

balanceLB :: Int -> AlmostTree n -> Tree c n -> HiddenTree (S n)
balanceLB x (AT SR y (TR z a b) c) d = HR (TR y (TB z a b) (TB x c d))

{-
insert :: RBT -> Int -> RBT
insert (Root s) x = Root (go s)
  where go :: Tree a n -> Tree b m
        go E = TB x E E
        go s@(TR y l r)
          | x > y = undefined
          | x < y = undefined
          | otherwise = s
-}