balanced-binary-search-tree-1.0.0.0: Type safe BST and AVL trees
Copyright(c) Nicolás Rodríguez 2021
LicenseGPL-3
MaintainerNicolás Rodríguez
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

Data.Tree.AVL.Invariants

Description

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

Synopsis

Documentation

data BS Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 Source #

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

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

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.