ℂDuce: Documentation: Tutorial: Polymorphism in CDuce (in progress)
Red-Black trees
What follows is just mock-up code for polymorphic CDuce based on current research. The implementation is ongoing but not available yet.As a first example we show that the use of polymorphic set-theoretic types yields a better definition of Okasaki's implementation of red-black trees that can be found in his excellent monograph [1].
A red and black tree is a colored binary search tree in which all nodes are colored either black or red and that satisfies 4 invariants:
- the root of the tree is black;
- the leaves of the tree are black;
- no red node has a red child;
- very path from the root to a leaf contains the same number of black nodes.
type RBtree(α) = Btree(α) | Rtree(α) (* Black rooted RB tree: *) type Btree(α) = [] | <black elem=α>[ RBtree(α) RBtree(α) ] (* Red rooted RB tree: *) type Rtree(α) = <red elem=α>[ Btree(α) Btree(α) ] type Wrongtree(α) = <red elem=α>( [ Rtree(α) Btree(α) ] | [ Btree(α) Rtree(α) ]) type Unbalanced(α) = <black elem=α>( [ Wrongtree(α) RBtree(α) ] | [ RBtree(α) Wrongtree(α) ]) let balance ( Unbalanced(α) -> Rtree(α) ; β\Unbalanced(α) -> β\Unbalanced(α) ) | <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ] | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ] | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ] | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] -> <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ] | x -> x let insert (x : α) (t : Btree(α)) : Btree(α) = let ins_aux ( [] -> Rtree(α); Btree(α)\[] -> RBtree(α)\[]; Rtree(α) -> Rtree(α)|Wrongtree(α) ) | [] -> <red elem=x>[ [] [] ] | (<(color) elem=y>[ a b ]) & z -> if x << y then balance <(color) elem=y>[ (ins_aux a) b ] else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ] else z in match ins_aux t with | <_ (y)>[ a b ] -> <black (y)>[ a b ]
The insert function takes an element x of type α, and returns a function that maps red-black trees into red-black trees.
insert :: α -> Btree(α) -> Btree(α)
balance :: ( Unbalanced(α) -> Rtree(α) ) & ( β\Unbalanced(α) -> β\Unbalanced(α) )
ins_aux :: ( [] -> Rtree(α) ) & ( Btree(α)\[] -> RBtree(α)\[] ) & ( Rtree(α) -> Rtree(α)|Wrongtree(α) )
ins_aux :: ( Btree(α)\[] -> RBtree(α)\[] ) & ( Rtree(α)|[] -> Rtree(α)|Wrongtree(α) )
The implementation above must be compared with the corresponding version in monomorphic CDuce:
type RBtree = Btree | Rtree;; type Btree = [] | <black elem=Int>[ RBtree RBtree ];; type Rtree = <red elem=Int>[ Btree Btree ];; type Wrongtree = Wrongleft | Wrongright;; type Wrongleft = <red elem=Int>[ Rtree Btree ];; type Wrongright = <red elem=Int>[ Btree Rtree ];; type Unbalanced = <black elem=Int>([ Wrongtree RBtree ] | [ RBtree Wrongtree ]) let balance ( Unbalanced -> Rtree ; Rtree -> Rtree ; Btree\[] -> Btree\[] ; [] -> [] ; Wrongleft -> Wrongleft ; Wrongright -> Wrongright) | <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ] | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ] | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ] | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] -> <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ] | x -> x let insert (x : Int) (t : Btree) : Btree = let ins_aux ( [] -> Rtree ; Btree\[] -> RBtree\[]; Rtree -> Rtree|Wrongtree) | [] -> <red elem=x>[ [] [] ] | (<(color) elem=y>[ a b ]) & z -> if x << y then balance <(color) elem=y>[ (ins_aux a) b ] else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ] else z in match ins_aux t with | <_ (y)>[ a b ] -> <black (y)>[ a b ]
ℂDuce: Documentation: Tutorial: Polymorphism in CDuce (in progress)