Types.hs

{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}

{-|
Module      : HTree.Types
Description : The 'HTree' type and its instances.
Copyright   : (c) Tom Harding, 2018
License     : MIT
Maintainer  : tom.harding@habito.com
Stability   : experimental

As an 'HList' grows, repeated access can cause compile times to suffer
massively. The reason is that the GHC typechecker does no caching, so every
lookup requires the type-level list to be walked linearly. In a practical
setting, where one may use an HList to store user input, a few hundred items
being accessed throughout the codebase will make compile times insufferably
slow.

We /could/ solve this with a type-checker plugin, but let's try something a bit
more interesting: let's pick a data structure with better access times than a
regular list. Let's build a tree. Specifically, a red-black tree.

>>> :t HEmpty
HEmpty :: HTree 'Empty

>>> :t HNode HEmpty True HEmpty
HNode HEmpty True HEmpty :: HTree ('Node colour 'Empty Bool 'Empty)

>>> :t HNode (HNode HEmpty True HEmpty) 3 HEmpty
HNode (HNode HEmpty True HEmpty) 3 HEmpty
  :: Num centre =>
     HTree
       ('Node colour1 ('Node colour2 'Empty Bool 'Empty) centre 'Empty)

There's also a (pretty messy) 'Show' instance for debugging:

>>> HNode (HNode HEmpty True HEmpty) 3 HEmpty
((.)<-(True)->(.))<-(3)->(.)

Note that we won't expose these constructors, instead requiring that trees be
assembled through the provided methods.
-}
module HTree.Types where

import Data.Kind (Constraint, Type)


-- | Every node within a tree is either red or black. Here's me avoiding the
-- ol' boolean blindness with some domain types.
data Colour = Red | Black


-- | Our 'HTree' will be indexed by /this/ tree type, which holds a colour for
-- each node. These are used for tree-balancing, as per the literature.
data Tree a = Empty | Node Colour (Tree a) a (Tree a)


-- | Finally, the 'HTree' itself. The HTree itself isn't very interesting, as
-- all the type information exists within the index - a red/black tree of
-- types.
data HTree (tree :: Tree Type) where

  -- | An empty tree.
  HEmpty :: HTree 'Empty

  -- | A non-empty tree is two subtrees and a centre element. The colour isn't
  -- enforced in this type, just to make things easier. Invariants are
  -- maintained by the 'insert' and 'delete' functions.
  HNode
    :: HTree left
    -> centre
    -> HTree right
    -> HTree ('Node colour left centre right)


-- | An empty tree that we can expose to our users.


-- | We'll use a dot to represent an empty tree (and thus the leaves at the
-- extremeties of any non-empty tree). Note we can't write one 'Show' instance
-- for all 'HTree's as we want to drill into the type!
instance Show (HTree 'Empty) where
  show _
    = "."

-- | If we can show both sides of a tree, as well as the thing in the middle,
-- we can show a tree! This could be much more intelligent, but it's more than
-- enough for debugging purposes.
instance (Show (HTree left), Show centre, Show (HTree right))
    => Show (HTree ('Node colour left centre right)) where

  show (HNode left centre right)
    = "(" ++ show left ++ ")<-(" ++ show centre ++ ")->(" ++ show right ++ ")"


-- | HEmpty's semigroup instance is exactly the same as ()'s.
instance Semigroup (HTree 'Empty) where
  _ <> _ = HEmpty

-- | Similarly, the monoid empty tree is the empty tree.
instance Monoid (HTree 'Empty) where
  mempty = HEmpty


-- | For more complicated trees, we recurcse down the sides and append as
-- usual. Note that we're requiring the trees to have exactly the same shape!
instance (Semigroup (HTree left), Semigroup centre, Semigroup (HTree right))
    => Semigroup (HTree ('Node colour left centre right)) where

  -- | I think this is really neat...
  HNode left centre right <> HNode left' centre' right'
    = HNode (left <> left') (centre <> centre') (right <> right')


-- | Mempty is just a tree of mempty. As we know our subtrees are Monoid, we
-- don't even have to recurse by hand: GHC will do all the work for us.
instance (Monoid (HTree left), Monoid centre, Monoid (HTree right))
    => Monoid (HTree ('Node colour left centre right)) where

  mempty
    = HNode mempty mempty mempty


-- | All empty trees are equal!
instance Eq (HTree 'Empty) where
  _ == _ = True


-- | Hopefully, the pattern is becoming clear: we use constraints on our
-- subtrees to get GHC to do the recursion, and we write the (very declarative)
-- pattern-matching to define equality: if the left sides are the same, the
-- centres are the same, and the right sides are the same, they're the same.
instance (Eq (HTree left), Eq centre, Eq (HTree right))
    => Eq (HTree ('Node colour left centre right)) where

  HNode left centre right == HNode left' centre' right'
    = left == left' && centre == centre' && right == right'