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