red-black-tree

Here's an interesting partial implementation (no delete): https://github.com/yairchu/red-black-tree/blob/master/RedBla... The AVL has a fuller implementation: https://github.com/yairchu/red-black-tree/blob/master/AvlTre... It's significantly more complex, but it gives a type-level/compile-time guarantee that the RB tree invariants are kept, which is nice.

I wonder if Qi can express GADTs to allow proof of balance properties, as in this Haskell example: https://github.com/yairchu/red-black-tree/blob/master/RedBla...

Haskell's type system can also express interesting things most languages' type systems can't. For example: https://github.com/yairchu/red-black-tree/blob/master/AvlTre... -- in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system. If there's a mistake in these 9 lines, you may get a wrong program. But the nice thing is that if you get just these 9 lines right -- then the hundreds of lines below it that implement an AVL tree cannot get the AVL invariants wrong. The same is also true for Red Black Trees: https://github.com/yairchu/red-black-tree/blob/master/RedBla... Lines 26..36 inclusive encode the RBTree type such that the invariants are enforced by the type-checker. In case this is unclear: the type-checker enforcing the correctness of the invariants is at compile-time. A running program is a correc