Data.Tree.BST.Utils

Type level search for a key and a value type in a type tree.

Documentation

type family Member (x :: Nat) (t :: Tree) (t' :: Tree) :: Bool where ...

Type family to test wether there is a node in the tree t with key x. | It assumes that t is a BST in order to perform the search.

Equations

Member x ('ForkTree l (Node n _a) r) t' = If (CmpNat x n == 'EQ) 'True (If (CmpNat x n == 'LT) (Member x l t') (Member x r t'))

Member x 'EmptyTree t' = TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " not found in tree ") :<>: 'ShowType t')

type family LookupValueType (x :: Nat) (t :: Tree) (t' :: Tree) :: Type where ...

Type family to search for the type of the value stored with key x in a tree t. | It assumes that t is a BST and that x is a member of t in order to perform the search | (so it always return a valid type).

Equations

LookupValueType x ('ForkTree l (Node n a) r) t' = If (CmpNat x n == 'EQ) a (If (CmpNat x n == 'LT) (LookupValueType x l t') (LookupValueType x r t'))

LookupValueType x 'EmptyTree t' = TypeError ((('Text "Key " :<>: 'ShowType x) :<>: 'Text " not found in tree ") :<>: 'ShowType t')