ℂDuce: Documentation: Tutorial: Polymorphism in CDuce (in progress)

## Deep flatten

*What follows is available ONLY in the unstable version. The implementation is available on the git but the code is not stable enough to be released and used in production.*In CDuce there is a

**operator that transforms a sequence of sequences into a sequence. To show the power of the polymorphic typing of CDuce let us define the deep variant of flatten, that we call**

`flatten`**, which recursively flattens all nested sequences into a single flat one. Nested sequences are a convenient representation of trees, whose leaves are values that are not sequences. So let us first define the type of α-trees, that is of trees whose leaves are of type α:**

`flatten_d`type Tree('a) = ('a\[Any*]) | [ (Tree('a))* ]

**is a type variable (read "alpha") and**

`'a`**is the type of trees whose leaves are of type**

`Tree('a)`**. These are either a leaf (i.e., any**

`'a`**value that is not a sequence:**

`'a`**) or a (possibly empty) sequence of**

`'a\[Any*]`**. The deep flatten function can then be defined as**

`Tree('a)`let flatten_d ( (Tree('a)) -> ['a*] ) | [] -> [] | [h ; t] -> (flatten_d h)@(flatten_d t) | x -> [x]

Notice that it is possible to unify the type

**with**

`Tree('a)`*every*type (in particular

**is a subtype of**

`Any`**). Therefore**

`Tree(Any)`**can be applied to every well-typed expression. So for instance we have:**

`flatten_d`# flatten_d [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];; - : [ (Bool | 3--5 | 'o'--'u')* ] = [ 3 'r' 4 true 5 'quo' false 'stop' ]

**was unified with the union of all the types of the leaves of the tree. Without polymorphism the best type we can give to**

`'a`**would be**

`flatten_d`**, which is not very useful (it just states that the function returns a sequence that does not contain other sequences).**

`Any->[(Any/[Any*])*]`If we want to define a version of deep flatten that can be applied only to sequences, then this can be done by the following further definition

let flatten_tree (x: [(Tree('a))*]) : ['a*] = flatten_d x;;

## Red-Black trees

As a second 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.

*by typing*that the operations on red-black trees (notably, the insertion) satisfy the first three invariants, as well as, that the

**function, local to insertion, never returns empty trees (yet another important property that, in ML/Haskell Okasaki's version, types cannot ensure). To enhance readability use α and β to denote the**

`ins_aux`*type variables*

**and**

`'a`**respectively.**

`'b`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 ]

**s) are black-rooted**

`Btree`**s (invariant 1), which are themselves black-rooted trees or red-rooted trees. The difference between the last two is that the latter cannot be leaves (invariant 2) and their children can only be black-rooted trees (invariant 3).**

`RBtree`The

**function takes an element**

`insert`**of type**

`x`*α*, and returns a function that maps red-black trees into red-black trees.

insert ::α-> Btree(α) -> Btree(α)

**is empty a red-rooted tree is returned, otherwise the element is inserted in the appropriate subtree and the whole tree is then balanced by the function**

`tree`**. This has the following type (which follows the same typing pattern as the function even defined in the introduction):**

`balance`balance :: ( Unbalanced(α) -> Rtree(α) ) & (β\Unbalanced(α) ->β\Unbalanced(α) )

**transforms an unbalanced tree into a (balanced) red-rooted tree and leaves all other trees (in particular the balanced ones) unchanged. The core of our definition is the type of**

`balance`**:**

`ins_aux`ins_aux :: ( [] -> Rtree(α) ) & ( Btree(α)\[] -> RBtree(α)\[] ) & ( Rtree(α) -> Rtree(α)|Wrongtree(α) )

**(which is the union of the three domains of the arrows forming its intersection type) is exactly**

`ins_aux`**. The intersection type describes the behaviour of**

`RBtree`**for each form of an**

`ins_aux`**—**

`RBtree`*ie*, empty, black-rooted, and red-rooted—. The type system needs the full precision of this type to infer whether the calls to

**in the body of**

`balance`**are applied to a balanced or an unbalanced tree: even a slight approximation of this type, such as**

`ins_aux`ins_aux :: ( Btree(α)\[] -> RBtree(α)\[] ) & ( Rtree(α)|[] -> Rtree(α)|Wrongtree(α) )

**it is easy to see that**

`ins_aux`**always returns either a (balanced) black-rooted tree or a tree with a red root in which one of the children may be a**

`ins_aux`**. In case of a tree with a red root, a balanced red-black tree is then obtained by changing the color of the root to black, as it is done in the last line of**

`Rtree`**.**

`insert`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 ]

**and**

`Wrongleft`**) in order to describe the polymorphic behavior of**

`Wrongright`**—whose type results, thus, much more obscure—. As far as we know ours types are the only system that can statically ensure the invariants above simply by decorating (with types) the original Okasaki's code without any further modification.**

`balance`ℂDuce: Documentation: Tutorial: Polymorphism in CDuce (in progress)