Data.Queue.Indexed.Leftist

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

Documentation

data Leftist n a where

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.

Constructors

Leaf :: Leftist 0 a

Node :: !(The Nat ((n + m) + 1)) -> a -> Leftist n a -> Leftist m a -> !(m <= n) -> Leftist ((n + m) + 1) a

Instances

Ord a => MeldableIndexedQueue Leftist a

Methods

merge :: Leftist n a -> Leftist m a -> Leftist (n + m) a

Ord a => IndexedQueue Leftist a

Methods

empty :: Leftist 0 a

minView :: Leftist (1 + n) a -> (a, Leftist n a)

singleton :: a -> Leftist 1 a

insert :: a -> Leftist n a -> Leftist (1 + n) a

minViewMay :: Leftist n a -> ((Nat ~ n) 0 -> b) -> (forall m. (Nat ~ (1 + m)) n => a -> Leftist m a -> b) -> b

NFData a => NFData (Leftist n a)

Methods

rnf :: Leftist n a -> ()