Safe Haskell | None |
---|---|

Language | Haskell2010 |

Statically verified, type-indexed, weight-biased leftist heaps.

# Documentation

data Leftist n a where Source #

A size-indexed weight-biased leftist heap. Somewhat based on the implementation from here.

Type-level natural numbers are used to maintain the invariants
in the size of the structure, but these are backed by
`Natural`

at runtime, maintaining some
efficiency.

For instance, the `<=.`

function is used, which compares two
numbers (runtime integers), but provides a boolean singleton
as its result: when matched on, this provides a *type-level-proof*
of the ordering.