std.heap

Heaps, by an order of their elements: a priority queue, its least element always at hand. A pairing heap, persistent: an insertion and a merge take a step each, and taking the least out takes as many as the log of the size, amortised. The order is the elements’ Order, found as an instance argument is, always the same one for a heap. Import it by a name, import std.heap as Heap, as the list module has a null and a merge. The heap comes first, as a set’s does: Heap.insert h x.

import std.heap as Heap

-- | the three least, in order
-- | >>> least3 [5, 1, 4, 2, 3]
-- | Cons 1 (Cons 2 (Cons 3 Nil))
least3 : List Int -> List Int
least3 xs = List.take 3 (Heap.toList (Heap.fromList xs))

Heap

data Heap a

A heap: none, or its least element at the root, how many it holds in all, and the heaps of the rest, none of whose elements is less.

empty

empty : {a : Type} -> Heap a

The heap of nothing.

singleton

singleton : {a : Type} -> a -> Heap a

The heap of x alone.

null

null : {a : Type} -> Heap a -> Bool

Whether it holds nothing.

size

size : {a : Type} -> Heap a -> Int

How many elements it holds: kept at its root, so a step.

merge

merge : {a : Type} -> {{ord : Order a}} -> Heap a -> Heap a -> Heap a

The elements of both: the root with the lesser element over the other (the first’s, of two as small).

insert

insert : {a : Type} -> {{ord : Order a}} -> Heap a -> a -> Heap a

The heap with x in it too.

findMin

findMin : {a : Type} -> Heap a -> Maybe a

Its least element, if it is not empty.

>>> findMin (insert (insert (insert empty 3) 1) 2)
Just 1
>>> findMin (empty : Heap Int)
Nothing

deleteMin

deleteMin : {a : Type} -> {{ord : Order a}} -> Heap a -> Heap a

The heap without its least element (of the empty heap, the empty heap).

>>> findMin (deleteMin (insert (insert (insert empty 3) 1) 2))
Just 2

popMin

popMin : {a : Type} -> {{ord : Order a}} -> Heap a -> Maybe (a, Heap a)

Its least element and the heap without it, if it is not empty.

>>> (maybe Nil (\p -> [fst p, size (snd p)]) (popMin (insert (insert (insert empty 3) 1) 2)) : List Int)
Cons 1 (Cons 2 Nil)

fromList

fromList : {a : Type} -> {{ord : Order a}} -> List a -> Heap a

The heap of a list’s elements.

>>> size (fromList [3, 1, 3])
3

toList

toList : {a : Type} -> {{ord : Order a}} -> Heap a -> List a

The elements, least first (a heapsort).

>>> toList (fromList [3, 1, 4, 1, 5, 9, 2, 6])
Cons 1 (Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 (Cons 6 (Cons 9 Nil)))))))
>>> toList (merge (fromList ["b", "d"]) (fromList ["c", "a"]))
Cons "a" (Cons "b" (Cons "c" (Cons "d" Nil)))