Overview
Atlassian Sourcetree is a free Git and Mercurial client for Windows.
Atlassian Sourcetree is a free Git and Mercurial client for Mac.
Weightbiased leftist heaps verified in Haskell using dependent types
This repo contains implementation of weightbiased leftist heap data
structure verified in Haskell using dependent types. This package is
intended to be a tutorial and technology demonstration. It is not
intended to be used in realworld applications (but if you find such a
use please let me know).
Weightbiased leftist heap is a binary tree that satisfies two
invariants:

Priority invariant: priority of every node is higher than
priority of its children. (This property is true for heaps in
general). 
Rank invariant: for every node size of its left child is not
smaller than the size of its right child.
These two invariants give us a data structure that provides O(1)
access to element with the highest priority and O(log2 n) insert and
merge operations. See chapter 3 of Chris Okasaki's "Purely Functional
Data Structures" for more discussion. Note that my implementation
represents priorities using natural numbers where 0 is the highest
priority (See Basics
and Nat
modules).
The main purpose of this implementation is to explain how proofs of
the two above invariants are constructed in Haskell. (The ideas
convey to other languages with dependent types.) You'll find lots of
comments in the source code. I assume that you already have been
exposed to basics of proofs with dependent types. In particular
you should be familiar with:

the concept of dataasevidence as described in "Why Dependent
Types Matter" paper. All the ideas here are taken from that
paper 
singleton types as described in "Dependently Typed Programming
with Singletons" paper. I don't make heavy use of singletons but
you should understand why do we need encodings like singleton
types in Haskell 
basics of formal reasoning (including refl). See online lecture
notes for the Computer Aided Formal Reasoning course by Thorsten
Altenkirch
You should begin studying of this repo by getting familiar with
modules in Basics
directory. Then go to TwoPassMerge
directory and
begin with NoProofs
module followed by RankProof
and
PriorityProof
(in any order) and finish with CombinedProofs
. Then
move to SinglePassMerge
and study the modules in the same order as
earlier. Alternatively, you might want to look at the singlepass
merge variant right after studying the twopass implementation.
Requirements and conventions

This code has been tested with GHC 7.6.3 and GHC 7.8.3. It only
depends onbase
library. No other dependencies are required. 
I'm not relying on anything from
Prelude
except for
undefined
function. 
I'm using GADT syntax for all data types, even if they are
ordinary ADTs. 
Whenever I say "See #XYZV" I'm referring to GHC bug report number
located under addresshttp://hackage.haskell.org/trac/ghc/ticket/XYZV
.
License
See LICENSE file in the root of the repository.
See also
I originally implemented verified weightbiased leftist heap in
Agda. This implementation is available
here.
I also wrote a companion blog post.