Polymorphic stanamically balanced binary trees
Okasaki, C. DR EECS
Christopher.Okasaki@usma.edu
Mon, 28 Apr 2003 08:34:37 0400
oleg describes an implementation of AVL trees that have
two main features:
1. The trees are heterogenous (elements within the same
tree can have different types).
2. The balance condition is partially enforced by the
type checker, and partially by runtime checks.
For feature 1, you can take your favorite solution for
heterogenous lists (existentials, type dynamic, ...) and
extend it to trees. This problem is orthogonal to the balance
problem, and I'll ignore it in the rest of this post.
For feature 2, there are lots of interesting approaches
to push this kind of check into the type checker. For
example, Hongwei Xi has several variations that do this
using dependent types. It can also be done entirely with
nested types. I think I first saw this done for AVL
trees by Ross Paterson in 1998.
First, here's a type that for trees of height h, given
types for trees of height h1 (t1) and for trees of
height h2 (t2).
data Node a t1 t2 = Left t1 a t2  Even t1 a t1  Right t2 a t1
Next, here's a type for trees of arbitrary height, given
types for trees of height h1 and h2.
data Tree a t1 t2 = Zero t2  Succ (Tree a (Node a t1 t2) t1)
To start things off, we set t2 to the type of trees of height 0
and t1 to the type of trees of height 1.
type AVLTree a = Tree a a ()
For example, a tree like
1
/
2
would be encoded as
Succ

Succ

Zero

Left(1)
/ \
Even(2) ()
/ \
() ()
Using polymorphic recursion, you can then implement typical tree
functions like insert and delete. The type checker will catch
any attempt to build an unbalanced tree. Note that there are
no runtime checks in this approach.
That last statement is a little bit of a lie. There is no
runtime typechecking going on, but there are runtime artifacts
of this algorithm, namely the Zero and Succ nodes which encode
the height of the tree. Zero and Succ are data constructors, not
type constructors as they are in oleg's version, so you have to
walk through them at runtime.
 Chris