For simplicity, we'll continue to work with heaps of `Int`

s.

```
type alias Rank = Int
type Heap = E | T Rank Int Heap Heap
```

The rank `r`

of a leftist heap is the length of its rightmost spine (that is, the number of edges on the path to the rightmost `E`

mpty node, or the number of non-`E`

nodes along this path).

The node `T r i left right`

stores its rank `r`

so that the `rank`

function below does not need to call `computeRank`

to recompute it.

```
computeRank : Heap -> Rank
computeRank h =
case h of
E -> 0
T r _ left right ->
let r' = 1 + computeRank right in
if r == r'
then r
else Debug.crash "incorrect rank"
rank h =
case h of
E -> 0
T r _ _ _ -> r
```

A few functions on leftist heaps that we will use to state invariants:

```
value h =
case h of
E -> maxInt
T _ i _ _ -> i
left h =
case h of
E -> E
T _ _ a _ -> a
right h =
case h of
E -> E
T _ _ _ b -> b
size h =
case h of
E -> 0
T _ _ a b -> 1 + size a + size b
```

*∀*`h`

. (`value(h)`

≤`value(left(h))`

) ∧ (`value(h)`

≤`value(right(h))`

)*∀*`h`

.`rank(left(h))`

≥`rank(right(h))`

**In-Class Exercise**

Let `log = logBase 2`

.

- Prove:
*∀*`h`

.`rank(h)`

=`r`

⇒`size(h)`

≥`2^r - 1`

- Prove:
*∀*`h`

.`size(h)`

=`n`

⇒`rank(h)`

≤`floor(log(n+1))`

Thus, the right spine of a leftist heap `h`

of size `n`

has *O( log n)* elements.

Unlike for regular min-heaps, merging leftist heaps runs quickly (faster than *O(n)*) by taking advantage of the fact that right spines are short (*O(log n)*).

The helper function `makeT`

creates a `T`

node that stores `x`

and positions `h1`

and `h2`

as its children depending on their rank.

```
makeT : Int -> Heap -> Heap -> Heap
makeT x h1 h2 =
let (r1,r2) = (rank h1, rank h2) in
if r1 >= r2
then T (1+r2) x h1 h2
else T (1+r1) x h2 h1
```

The following is an equivalent definition of `makeT`

.

```
makeT x h1 h2 =
let (left,right) =
if rank h1 >= rank h2
then (h1, h2)
else (h2, h1)
in
T (1 + rank right) x left right
```

The `merge`

function combines two non-empty heaps by choosing the smaller of their two minimum values and recursively merging, using `makeT`

to place "heavier" subtrees to the left.

```
merge : Heap -> Heap -> Heap
merge h1 h2 = case (h1, h2) of
(_, E) -> h1
(E, _) -> h2
(T _ x1 left1 right1, T _ x2 left2 right2) ->
if x1 <= x2
then makeT x1 left1 (merge right1 h2)
else makeT x2 left2 (merge h1 right2)
```

The `makeT`

function runs in *O(1)* time. The running time of `merge`

is dominated by its recursive calls. Let *n* be the size of the larger of the two heaps. The leftist property ensures that the right spine of each heap has *O(log n)* elements. Because the recursive calls traverse the right spine of one of the input heaps, there are at most *O(log n)* recursive calls, each of which performs *O(1)* work. Therefore, `merge`

runs in *O(log n)* time.

```
empty = E
singleton x = T 1 x E E
```

Insertion and deletion can be defined in terms of `merge`

, so each runs in *O(log n)* time.

```
insert : Int -> Heap -> Heap
insert x h = merge (singleton x) h
deleteMin : Heap -> Maybe Heap
deleteMin h = case h of
E -> Nothing
T r _ a b -> Just (merge a b)
```

Implementing the rest of the heap abstraction is straightforward.

```
findMin : Heap -> Maybe Int
findMin h = case h of
E -> Nothing
T _ i _ _ -> Just i
isEmpty : Heap -> Bool
isEmpty h = h == empty
```

Our implementation (`LeftistHeaps.elm`

) exports the same type signatures as the vanilla implementation of min-heaps from before.

```
module LeftistHeaps
(Heap, empty, isEmpty, findMin, insert, deleteMin, merge) where
...
```

Notice how sequences of `insert`

s pile up elements heavily to the left.

```
> import LeftistHeaps (..)
> insert 1 <| insert 2 <| insert 3 <| empty
T 1 1 (T 1 2 (T 1 3 E E) E) E : LeftistHeaps.Heap
```

- Okasaki, Chapter 3.1