Polymorphic stanamically balanced binary trees

[Okasaki, C. DR EECS]

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 run-time 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 h-1 (t1) and for trees of 
height h-2 (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 h-1 and h-2.

  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 run-time checks in this approach.

That last statement is a little bit of a lie.  There is no
run-time typechecking going on, but there are run-time 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 run-time.

-- Chris