# [Haskell-cafe] \Statically checked binomail heaps?

Fri Oct 30 14:17:54 EDT 2009

```Maciej Kotowicz wrote:
> I'm trying to implement a binomial heaps from okaski's book 
> but as most it's possible to be statically checked for correctness of
> definition.

data Tree a t = Tree { root :: a, children :: t }
data Nest a t = Nest { head :: Tree a t, tail :: t }

where
- Tree a () is a binomial tree of order 0
- Tree a (Nest a ()) is a binomial tree of order 1
- Tree a (Nest a (Nest a ())) is a binomial tree of order 2. and so on

data Heap' a t
= Z'
| D0' (Heap' a (Nest a t))
| D1' (Heap' a (Nest a t)) (Tree a t)

With (Tree a t) representing a binomial tree of rank n,
- Heap' a t  represents the list of binomial trees of rank >= n in a heap
- Z'         represents an empty list
- D0' xs     represents a list /without/ a tree of rank n
- D1' xs x   represents a list /with/ a tree of rank n, namely x.

Finally, define

type Heap a = Heap' a ()

This forces Heap to be a well-shaped binomial heap, up to the equality
D0' Z' = Z'.

The main difference to "standard" binomial heaps is the existence of the
D0' nodes which represent skipped ranks. This makes the type checking
much easier (no comparison of natural numbers is required). It also
makes rank calculations unecessary - the rank increases implicitely as
the heap is traversed.

Heap order can be maintained by using a smart constructor:

-- combine two binomial trees of rank n into one of rank n+1
mkTree' :: Ord a => Tree a t -> Tree a t -> Tree a (Nest a t)
mkTree' l@(Tree a x) r@(Tree b y)
| a < b = Tree a (Nest r x)
| True  = Tree b (Nest l y)

Here is insert, as an example of a non-trivial operation:

insert' :: Ord a => Heap' a t -> Tree a t -> Heap' a t
insert' Z'        b = D1' Z' b
insert' (D0' x)   b = D1' x b
insert' (D1' x a) b = D0' (x `insert'` mkTree' a b)

HTH,

Bertram

P.S. As a refinement, one can define
data Heap a = Z | D0 | D1 (Heap' a a) a

This improves memory efficiency at the cost of requiring more code, like

mkTree :: Ord a => a -> a -> Tree a a
mkTree a b | a < b = Tree a b
| True  = Tree b a

insert :: Ord a => Heap a -> a -> Heap a
insert Z        b = D1 Z' b
insert (D0 x)   b = D1 x b
insert (D1 x a) b = D0 (x `insert'` mkTree a b)
```