Data.Tree.AVL.Invariants

Type level restrictions for the key ordering in type safe AVL trees.

Documentation

data BS

Data type that represents the state of balance of the sub trees in a balanced tree:

LeftHeavy

height(left sub tree) = height(right sub tree) + 1

RightHeavy

height(right sub tree) = height(left sub tree) + 1

Balanced

height(left sub tree) = height(right sub tree)

Constructors

LeftHeavy

RightHeavy

Balanced

type family BalancedState (h1 :: Nat) (h2 :: Nat) :: BS where ...

Check from two type level natural numbers, that represent the heights of some left and right sub trees, if some of those sub trees have height larger than the other.

Equations

BalancedState 0 0 = 'Balanced

BalancedState 1 0 = 'LeftHeavy

BalancedState 0 1 = 'RightHeavy

BalancedState h1 h2 = BalancedState (h1 - 1) (h2 - 1)

type family Height (t :: Tree) :: Nat where ...

Get the height of a tree.

Equations

Height 'EmptyTree = 0

Height ('ForkTree l (Node _n _a) r) = 1 + Max (Height l) (Height r)

type family BalancedHeights (h1 :: Nat) (h2 :: Nat) (k :: Nat) :: Bool where ...

Check if two type level natural numbers, that represent the heights of some left and right sub trees, differ at most in one (i.e., the tree is balanced).

Equations

BalancedHeights 0 0 _k = 'True

BalancedHeights 1 0 _k = 'True

BalancedHeights _h1 0 k = TypeError (('Text "The left sub tree at node with key " :<>: 'ShowType k) :<>: 'Text " has +2 greater height!")

BalancedHeights 0 1 _k = 'True

BalancedHeights 0 _h2 k = TypeError (('Text "The right sub tree at node with key " :<>: 'ShowType k) :<>: 'Text " has +2 greater height!")

BalancedHeights h1 h2 k = BalancedHeights (h1 - 1) (h2 - 1) k

data US

Data type that represents the state of unbalance of the sub trees:

LeftUnbalanced

height(left sub tree) = height(right sub tree) + 2

RightUnbalanced

height(right sub tree) = height(left sub tree) + 2

NotUnbalanced

tree is not unbalanced

Constructors

LeftUnbalanced

RightUnbalanced

NotUnbalanced

type family UnbalancedState (h1 :: Nat) (h2 :: Nat) :: US where ...

Check from two type level natural numbers, that represent the heights of some left and right sub trees, if the tree is balanced or if some of those sub trees is unbalanced.

Equations

UnbalancedState 0 0 = 'NotUnbalanced

UnbalancedState 1 0 = 'NotUnbalanced

UnbalancedState 0 1 = 'NotUnbalanced

UnbalancedState 2 0 = 'LeftUnbalanced

UnbalancedState 0 2 = 'RightUnbalanced

UnbalancedState h1 h2 = UnbalancedState (h1 - 1) (h2 - 1)