Typesafe BST and AVL trees
Several implementations of binary search trees (BST) and balanced binary search trees (AVL).
Verify at compile time if the operations over BST/AVL trees preserves the order of the keys and the balance in the heights.
For both of them there's one unsafe implementation and three typesafe implementations. The last ones differ one how the structural invariants are handled at the type level.
Summary
Prerequisites
ghc (>= 8.10.2) # GHC Haskell compiler
cabal (>=3.0.0.0) # Haskell package manager
python3 (>=3.6.8) # Python interpreter (only needed for running the benchmarks)
Some python package manager (e.g., pip)
No external Haskell libraries are needed.
Installing
If you only want to use the library (without benchmarks), the easiest way to install it is through Hackage. The following command will download the library and install it:
cabal install lib balancedbinarysearchtree
If you also want to see or run the benchmarks, clone the repository:
git clone https://github.com/nicorodriguez/balancedbinarysearchtree.git
The project may be used locally (inside the folder with cabal repl
) or it may be install for system wide use:
cd balancedbinarysearchtree
cabal install lib
For usage examples see the Examples section.
Project Structure
balancedbinarysearchtree
│ README.md
└───benchmark
 │
│ └── ...
└───src/Data/Tree
│ ITree.hs
│ Node.hs
└───AVL
│ │ FullExtern.hs
│ │ Extern.hs
│ │ Intern.hs
│ │ Unsafe.hs
│ │ Invariants.hs
│ └───FullExtern
│ │ │ Examples.hs
│ └───Extern
│ │ │ Constructor.hs
│ │ │ Balance.hs, BalanceProofs.hs
│ │ │ Insert.hs, InsertProofs.hs
│ │ │ Lookup.hs
│ │ │ Delete.hs, DeleteProofs.hs
│ │ │ Examples.hs
│ └───Intern
│ │ │ Constructor.hs
│ │ │ Balance.hs
│ │ │ Insert.hs
│ │ │ Lookup.hs
│ │ │ Delete.hs
│ │ │ Examples.hs
│ └───Unsafe
│ │ Examples.hs
└───BST
│
└── ...

For details on the benchmark
directory, see the Benchmark section.

ITree.hs
implements the Tree
and ITree
data types.

Node.hs
implements the nodes of the trees.

Both ITree.hs
and Node.hs
are used in both BST and AVL typesafe trees.

The structure of Data/Tree/AVL/
and Data/Tree/BST/
is similar.

Data/Tree/{BST,AVL}/Invariants.hs
implements the BST/AVL invariants.

Data/Tree/{BST,AVL}/Unsafe.hs
contains an unsafe implementation of BST/AVL trees. The code was extracted and refactored from Data/Tree/AVL/Extern/{Balance,Insert,Lookup,Delete}.hs
, 'unlifting' the type level computations to the value level and removing all proof functions and terms.

Data/Tree/{BST,AVL}/FullExtern.hs
contains the implementation of the full externalist approach. It provides functionality for performing several operations in a row over trees and checking the invariants at the end.

Data/Tree/{BST,AVL}/Extern/
contains the implementation of BST/AVL trees and its operations for the externalist approach; likewise, Data/Tree/{BST,AVL}/Intern/
folder contains the implementation for the internalist approach. Notice that there are no *Proofs.hs
source files inside Data/Tree/{BST,AVL}/Intern/
. That's because the proofs and operations in the internalist approach are implemented together.

All four approaches, Data/Tree/{BST,AVL}/{Unsafe,FullExtern,Extern,Intern}/
, have an Examples.hs
with usage examples of the BST/AVL operations.

In order to use BST/AVL trees, only one of Data/Tree/{BST,AVL}/{Unsafe,FullExtern,Extern,Intern}.hs
need to be imported. They all export the basic functionality for inserting, looking and deleting on the corresponding BST/AVL tree. See the Interface section for exploring the functions exported by each of them.
Interface
Both externalist and internalist approaches have a common interface for manipulating BST/AVL trees. The difference in their implementation is the approach taken when defining the structural invariants that represent the conditions for a tree to be BST/AVL.
The interface for the unsafe and the full externalist approaches are only slightly different.
AVL trees (some function constraints omitted)
For the unsafe approach, the interface is

emptyAVL :: AVL a
, an empty ITree.

insertAVL :: Show a => Int > a > AVL a > AVL a
, inserts a node in a ITree. If the tree already has a node with the given key, the value is updated.

lookupAVL :: Int > AVL a > Maybe a
, returns the value stored in the node with the given key. Returns Nothing
if the key is not found.

deleteAVL :: Int > AVL a > AVL a
, delete a node with a given key. If the tree doesn't have a node with that key, it just returns the original tree.
For the full externalist approach, the interface is:

EmptyITree :: ITree 'EmptyTree
, an empty ITree.

insert :: Node x a > ITree t > ITree (Insert x a t)
, inserts a node in a ITree. If the tree already has a node with key x
, the value is updated.

lookup :: (t ~ 'ForkTree l (Node n a1) r, Member x t ~ 'True) => Proxy x > ITree t > a
, lookup a key in a ITree. The constraint t ~ 'ForkTree l (Node n a1) r
checks at compile time if the tree is not empty; the constraint Member x t ~ 'True
checks at compile time that the tree t
has a node with key x
(ensuring that the lookup will return some value).

delete :: Proxy x > ITree t > (Delete x t)
, delete a node with a given key in a ITree. If the tree doesn't have a node with key x
, it just returns the original tree.

AVL :: ITree t > IsBSTT t > IsBalancedT t > AVL t
, constructor for typesafe AVL trees.

mkAVL :: (IsBSTC t, IsBalancedC t) => ITree t > AVL t
, constructor for typesafe AVL from an ITree, with automatic proof term construction.
For the externalist and internalist approaches, the interface is the same and is as follows:

emptyAVL :: AVL 'EmptyTree
, an empty AVL tree.

insertAVL :: Proxy x > a > AVL t > AVL (Insert x a t)
, inserts a value of type a
with key x
in an AVL of type AVL t
. If the tree already has a node with key x
, the value is updated.

lookupAVL :: (t ~ 'ForkTree l (Node n a1) r, Member x t ~ 'True) => Proxy x > AVL t > a
, returns the value, of type a
, that is associated to the key x
in the AVL tree of type AVL t
. The constraint t ~ 'ForkTree l (Node n a1) r
checks at compile time if the tree is not empty; the constraint Member x t ~ 'True
checks at compile time that the tree t
has a node with key x
(ensuring that the lookup will return some value).

deleteAVL :: Proxy x > AVL t > AVL (Delete x t)
, deletes the node with key x
in an AVL of type AVL t
. If the tree doesn't have a node with key x
, it just returns the original tree.
BST trees
The interfaces are analogous to those for AVL trees. Just replace "AVL" for "BST" in the functions and modules names.
Examples
For more usage examples see the Examples.hs
file for each approach.
Unsafe
import Data.Tree.AVL.Unsafe (deleteAVL, emptyAVL, insertAVL,
lookupAVL)
import Prelude (Int, Float, Bool(True,False))
  Test Balanced Binary Tree
avle = emptyAVL
avlt1 = insertAVL 20 'f' avle
avlt2 = insertAVL 60 'o' avlt1
avlt3 = insertAVL 30 'l' avlt2
  Just 'l'
l1 = lookupAVL 30 avlt3
  Nothing: key 10 is not in the tree avlt8
n = lookupAVL 10 avlt3
avlt4 = deleteAVL 20 avlt3
avlt5 = deleteAVL 60 avlt3
  There's no error. Just return the same tree
avlt6 = deleteAVL 40 avlt3
Full Extern
A full externalist approach means grouping the operations over ITree
, only constructing the BST/AVL and verifying the invariants at the end:
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeFamilies #}
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.FullExtern (AVL (AVL), mkAVL, ITree (EmptyITree),
delete, insert, lookup)
import Data.Tree.ITree (ITree(EmptyITree,ForkITree))
import Data.Tree.Node (mkNode)
import Prelude (Bool (False, True), Float, Int, ($))
  Proxies for the node keys
p0 = Proxy :: Proxy 0
p1 = Proxy :: Proxy 1
p2 = Proxy :: Proxy 2
p3 = Proxy :: Proxy 3
p4 = Proxy :: Proxy 4
p5 = Proxy :: Proxy 5
p6 = Proxy :: Proxy 6
p7 = Proxy :: Proxy 7
  Insert several values in a row and check the BST and AVL invariants at the end
avl = mkAVL t
where
t = insert (mkNode p4 'f') $ insert (mkNode p2 (4::Int)) $
insert (mkNode p6 "lala") $ insert (mkNode p3 True) $
insert (mkNode p5 ([1,2,3]::[Int])) $ insert (mkNode p0 (1.8::Float)) $
insert (mkNode p7 [False]) EmptyITree
  For performing a lookup, it's necessary to take the ITree 't' out of the AVL constructor
l1' = case avl of
AVL t _ _ > lookup (Proxy::Proxy 3) t
  Compile time error: key 1 is not in the tree avl and left subtree at node with key 4 has height +2 greater than the right subtree
 avlError = mkAVL $
 ForkITree (ForkITree
 (ForkITree
 EmptyITree (mkNode p0 'a') EmptyITree)
 (mkNode p7 4)
 EmptyITree)
 (mkNode p4 'f')
 EmptyITree
  Delete several values in a row and check the BST and AVL invariants at the end
avlt2 = case avl of
AVL t _ _ > mkAVL t'
where
t' = delete p7 $ delete p4 $ delete p1 $ delete p0 $
delete p2 $ delete p6 $ delete p5 $ delete p3 t
Extern and Intern
In the externalist and internalist approaches, the invariants are checked after every operation performed over the tree.
Some examples for the externalist approach:
{# LANGUAGE DataKinds #}
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern (deleteAVL, emptyAVL, insertAVL,
lookupAVL)
import Prelude (Bool (False, True), Float, Int, String)
  Proxies for the node keys
p2 = Proxy :: Proxy 2
p4 = Proxy :: Proxy 4
p7 = Proxy :: Proxy 7
 Insert value 'f' with key 4
avlt1 = insertAVL p4 'f' emptyAVL
 Insert value [1,2] with key 2
avlt2 = insertAVL p2 [1,2] avlt1
 list = [1,2]
list = lookupAVL p2 avlt2
  Error: key 7 is not in the tree avlt2
 err = lookupAVL p7 avlt2
 Delete node with key 4
avlt3 = deleteAVL p4 avlt2
 Delete node with key 2. Returns the empty AVL
avlt4 = deleteAVL p2 avlt3
For using the internalist approach, the code example for the externalist approach works with the only difference in the import list:
import Data.Tree.AVL.Intern (emptyAVL,insertAVL,lookupAVL,deleteAVL)
 Instead of import Data.Tree.AVL.Extern (emptyAVL,insertAVL,lookupAVL,deleteAVL)
Examples: BST trees
The previous examples used AVL trees. For using AVL trees just replace the imported modules along with the functions:
mkAVL > mkBST
emptyAVL > emptyBST
insertAVL > insertBST
lookupAVL > lookupBST
deleteAVL > deleteBST
Notice that operations for BST may only be applied to BST trees, and operations for AVL trees may only be applied for AVL trees. For instance, this is not possible if bst2
is not an AVL tree:
deleteAVL (Proxy::Proxy 5) bst2
It gives an error at compile time.
Benchmark
Structure
balancedbinarysearchtree
│ README.md
└───benchmark
└───AVL
│ └───FullExtern
   Benchmark.hs
│ │ │
  └───Insert
│ │ │
  └───Lookup
│ │ │
  └───Delete
│ └───Extern
│ │ └── ...
│ └───Intern
│ │ └── ...
│ └───Unsafe
│ └── ...
└───BST
│
└── ...
There are benchmarks for both BST and AVL trees for each approach (clone the repository for viewing or using the benchmarks). For instance, in the folder benchmark/AVL/FullExtern/
there are three folders and one source file: Insert/
, Lookup/
, Delete/
and Benchmark.hs
.
Inside each folder there are different source files for benchmarking each operation under several tree sizes; they're split in different files
in order to be able to measure not only the running times but also the compile times.
The source files Benchmark.hs
performs all of the running time benchmarks defined inside the folders Insert/
, Lookup/
and Delete/
.
Running the benchmark
Given the compilation effort for running the benchmarks, the Hackage package comes without them.
In order to run the benchmarks, you should clone the repository and switch to benchmark
branch.
For running all the benchmarks, use benchmark/avgbench.py
script. There's a requirements.txt
file with all the python dependencies needed to run the script.
If you're using pip
, just run pip install r requirements.txt
.