packages feed

type-indexed-queues (empty) → 0.1.0.0

raw patch · 28 files changed

+2932/−0 lines, 28 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, criterion, deepseq, doctest, ghc-typelits-natnormalise, pqueue, random, tasty, tasty-quickcheck, type-indexed-queues

Files

+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2017 Donnacha Oisín Kidney++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ README.md view
@@ -0,0 +1,102 @@+# type-indexed-heaps+## Heaps with verified and unverified versions.++[![Build Status](https://travis-ci.com/oisdk/type-indexed-heaps.svg?token=fXdGpZwjFQ87pr9zynKX&branch=master)](https://travis-ci.com/oisdk/type-indexed-heaps)++This library provides implementations of five different heaps+(binomial, pairing, skew, leftist, and Braun), each in two+flavours: one verified, and one not.++At the moment, only structural invariants are maintained.++## Comparisons of verified and unverified heaps+Both versions of each heap are provided for comparison: for+instance, compare the standard leftist heap (in+Data.Heap.Leftist):++```haskell+data Leftist a+  = Leaf+  | Node !Int+        a+        (Leftist a)+        (Leftist a)+```++To its size-indexed counterpart (in Data.Heap.Indexed.Leftist):++```haskell+data Leftist n a where+        Leaf :: Leftist 0 a+        Node :: !(The Nat (n + m + 1))+             -> a+             -> Leftist n a+             -> Leftist m a+             -> !(m <= n)+             -> Leftist (n + m + 1) a+```++The invariant here (that the size of the left heap must+always be less than that of the right) is encoded in the+proof `m <= n`.+ +With that in mind, compare the unverified and verified+implementatons of `merge`:++```haskell+merge Leaf h2 = h2+merge h1 Leaf = h1+merge h1@(Node w1 p1 l1 r1) h2@(Node w2 p2 l2 r2)+  | p1 < p2 =+      if ll <= lr+          then Node (w1 + w2) p1 l1 (merge r1 h2)+          else Node (w1 + w2) p1 (merge r1 h2) l1+  | otherwise =+      if rl <= rr+          then Node (w1 + w2) p2 l2 (merge r2 h1)+          else Node (w1 + w2) p2 (merge r2 h1) l2+  where+    ll = rank r1 + w2+    lr = rank l1+    rl = rank r2 + w1+    rr = rank l2+```++Verified:++```haskell+merge Leaf h2 = h2+merge h1 Leaf = h1+merge h1@(Node w1 p1 l1 r1 _) h2@(Node w2 p2 l2 r2 _)+  | p1 < p2 =+      if ll <=. lr+        then Node (w1 +. w2) p1 l1 (merge r1 h2)+        else Node (w1 +. w2) p1 (merge r1 h2) l1 . totalOrder ll lr+  | otherwise =+      if rl <=. rr+          then Node (w1 +. w2) p2 l2 (merge r2 h1)+          else Node (w1 +. w2) p2 (merge r2 h1) l2 . totalOrder rl rr+  where+    ll = rank r1 +. w2+    lr = rank l1+    rl = rank r2 +. w1+    rr = rank l2+```++## Using type families and typechecker plugins to encode the invariants+The similarity is accomplished through overloading, and some+handy functions. For instance, the second if-then-else works+on boolean *singletons*, and the `<=.` function provides a+proof of order along with its answer. The actual arithmetic+is carried out at runtime on normal integers, rather than+Peano numerals. These tricks are explained in more detail+TypeLevel.Singletons and TypeLevel.Bool.++A typechecker plugin does most of the heavy lifting, although+there are some (small) manual proofs.++## Uses of verified heaps+The main interesting use of these sturctures is total traversable+sorting ([sort-traversable](https://github.com/treeowl/sort-traversable)).+An implementation of this is provided in Data.Traversable.Sort. I'm+interested in finding out other uses for these kinds of structures.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ bench/bench.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE DataKinds #-}++import           Criterion.Main+import           System.Random++import           Data.Traversable.Parts+import           Data.Queue.Class++import qualified Data.Queue.Indexed.Binomial as Indexed+import qualified Data.Queue.Indexed.Pairing  as Indexed+import qualified Data.Queue.Indexed.Skew     as Indexed+import qualified Data.Queue.Indexed.Leftist  as Indexed+import qualified Data.Queue.Indexed.Braun    as Indexed++import           Data.Queue.Indexed.Erased++import           Data.Queue.Binomial+import           Data.Queue.Pairing+import           Data.Queue.Skew+import           Data.Queue.Leftist++import           Control.Monad              (replicateM)++import           Data.List                  (sort)+import qualified Data.Sequence              as Seq+import qualified Data.PQueue.Min            as P++import           Data.Proxy++import           TypeLevel.Nat++import           Data.BinaryTree++randInt :: IO Int+randInt = randomIO++testSize :: Int -> Benchmark+testSize n =+    bgroup+        (show n)+        [ env (Seq.replicateM n randInt) $+          \xs ->+               bgroup+                   "seq"+                   [ bench "trav binom"       $ nf (queueTraversable (Proxy :: Proxy (Indexed.Binomial 0))) xs+                   , bench "trav pairing"     $ nf (queueTraversable (Proxy :: Proxy Indexed.Pairing)) xs+                   , bench "trav skew"        $ nf (queueTraversable (Proxy :: Proxy Indexed.Skew)) xs+                   , bench "trav leftist"     $ nf (queueTraversable (Proxy :: Proxy Indexed.Leftist)) xs+                   , bench "Seq.sort"         $ nf Seq.sort xs+                   , bench "Seq.unstableSort" $ nf Seq.unstableSort xs+                   ]+        , env (replicateA n randInt) $+          \xs ->+               bgroup+                   "tree"+                   [ bench "trav binom"       $ nf (queueTraversable (Proxy :: Proxy (Indexed.Binomial 0))) xs+                   , bench "trav pairing"     $ nf (queueTraversable (Proxy :: Proxy Indexed.Pairing)) xs+                   , bench "trav skew"        $ nf (queueTraversable (Proxy :: Proxy Indexed.Skew)) xs+                   , bench "trav leftist"     $ nf (queueTraversable (Proxy :: Proxy Indexed.Leftist)) xs+                   ]+        , env (replicateM n randInt) $+          \xs ->+               bgroup+                   "list"+                   [ bench "sort braun"   $ nf (heapSort (Proxy :: Proxy (ErasedSize Indexed.Braun))) xs+                   , bench "Data.List"    $ nf sort xs+                   , bench "sort pairing" $ nf (heapSort (Proxy :: Proxy Pairing)) xs+                   , bench "sort leftist" $ nf (heapSort (Proxy :: Proxy Leftist)) xs+                   , bench "sort binom"   $ nf (heapSort (Proxy :: Proxy (Binomial 'Z))) xs+                   , bench "sort skew"    $ nf (heapSort (Proxy :: Proxy Skew)) xs+                   , bench "sort pqueue"  $ nf (P.toList . P.fromList) xs+                   , bench "trav pairing" $ nf (queueTraversable (Proxy :: Proxy Indexed.Pairing)) xs+                   , bench "trav leftist" $ nf (queueTraversable (Proxy :: Proxy Indexed.Leftist)) xs+                   , bench "trav binom"   $ nf (queueTraversable (Proxy :: Proxy (Indexed.Binomial 0))) xs+                   , bench "trav skew"    $ nf (queueTraversable (Proxy :: Proxy Indexed.Skew)) xs+                   ]+        ]++main :: IO ()+main =+    defaultMain $+    map+        testSize+        [500, 1000, 10000, 100000, 500000]
+ src/Data/BinaryTree.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable     #-}+{-# LANGUAGE DeriveFunctor      #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE DeriveTraversable  #-}+{-# LANGUAGE Safe               #-}++-- | A simple, generic binary tree and some operations. Used in some of+-- the heaps.+module Data.BinaryTree+  (Tree(..)+  ,foldTree+  ,isHeap+  ,unfoldTree+  ,replicateTree+  ,replicateA+  ,treeFromList+  ,zygoTree+  ,drawBinaryTree)+  where++import           Control.DeepSeq      (NFData (..))+import           Data.Data            (Data)+import           Data.Functor.Classes+import           Data.Monoid+import           Data.Typeable        (Typeable)+import           GHC.Generics         (Generic, Generic1)++import           Data.Bifunctor+import           Data.Bool+import           Data.Function++import qualified Data.Tree            as Rose++-- | A simple binary tree for use in some of the heaps.+data Tree a+    = Leaf+    | Node a+           (Tree a)+           (Tree a)+    deriving (Show,Read,Eq,Ord,Functor,Foldable,Traversable,Typeable+             ,Generic,Generic1,Data)++instance NFData a =>+         NFData (Tree a) where+    rnf Leaf         = ()+    rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r `seq` ()++instance Eq1 Tree where+    liftEq _ Leaf Leaf = True+    liftEq eq (Node x xl xr) (Node y yl yr) =+        eq x y && liftEq eq xl yl && liftEq eq xr yr+    liftEq _ _ _ = False++instance Ord1 Tree where+    liftCompare _ Leaf Leaf = EQ+    liftCompare cmp (Node x xl xr) (Node y yl yr) =+        cmp x y <> liftCompare cmp xl yl <> liftCompare cmp xr yr+    liftCompare _ Leaf _ = LT+    liftCompare _ _ Leaf = GT++instance Show1 Tree where+    liftShowsPrec s _ = go where+      go _ Leaf = showString "Leaf"+      go d (Node x l r)+        = showParen (d >= 11)+        $ showString "Node "+        . s 11 x+        . showChar ' '+        . go 11 l+        . showChar ' '+        . go 11 r++instance Read1 Tree where+    liftReadsPrec r _ = go+      where+        go d ss =+            readParen+                (d > 11)+                (\xs ->+                      [ (Leaf, ys)+                      | ("Leaf",ys) <- lex xs ])+                ss +++            readParen+                (d > 10)+                (\vs ->+                      [ (Node x lx rx, zs)+                      | ("Node",ws) <- lex vs+                      , (x,xs) <- r 11 ws+                      , (lx,ys) <- go 11 xs+                      , (rx,zs) <- go 11 ys ])+                ss++-- | Fold over a tree.+foldTree :: b -> (a -> b -> b -> b) -> Tree a -> b+foldTree b f = go where+  go Leaf         = b+  go (Node x l r) = f x (go l) (go r)++-- | Check to see if this tree maintains the+-- <https://en.wikipedia.org/wiki/Heap_(data_structure) heap property>.+isHeap :: Ord a => Tree a -> Bool+isHeap =+    zygoTree+        Nothing+        (\x _ _ ->+              Just x)+        True+        go+  where+    go x lroot lproper rroot rproper =+        isAbove x lroot && isAbove x rroot && lproper && rproper+    isAbove x = all (>=x)++-- | A zygomorphism over a tree. Used if you want perform two folds+-- over a tree in one pass.+--+-- As an example, checking if a tree is balanced can be performed like+-- this using explicit recursion:+--+-- @+-- isBalanced :: 'Tree' a -> Bool+-- isBalanced 'Leaf' = True+-- isBalanced ('Node' _ l r)+--   = 'length' l == 'length' r && isBalanced l && isBalanced r+-- @+--+-- However, this algorithm performs several extra passes over the+-- tree. A more efficient version is much harder to read, however:+--+-- @+-- isBalanced :: Tree a -> Bool+-- isBalanced = snd . go where+--   go 'Leaf' = (0 :: Int,True)+--   go ('Node' _ l r) =+--       let (llen,lbal) = go l+--           (rlen,rbal) = go r+--       in (llen + rlen + 1, llen == rlen && lbal && rbal)+-- @+--+-- This same algorithm (the one pass version) can be expressed as a+-- zygomorphism:+--+-- @+-- isBalanced :: 'Tree' a -> Bool+-- isBalanced =+--     'zygoTree'+--         (0 :: Int)+--         (\\_ x y -> 1 + x + y)+--         True+--         go+--   where+--     go _ llen lbal rlen rbal = llen == rlen && lbal && rbal+-- @+zygoTree+    :: b1+    -> (a -> b1 -> b1 -> b1)+    -> b+    -> (a -> b1 -> b -> b1 -> b -> b)+    -> Tree a+    -> b+zygoTree b1 f1 b f = snd . go where+  go Leaf = (b1,b)+  go (Node x l r) =+      let (lr1,lr) = go l+          (rr1,rr) = go r+      in (f1 x lr1 rr1, f x lr1 lr rr1 rr)++-- | Unfold a tree from a seed.+unfoldTree :: (b -> Maybe (a, b, b)) -> b -> Tree a+unfoldTree f = go where+  go = maybe Leaf (\(x,l,r) -> Node x (go l) (go r)) . f++-- | @'replicateTree' n a@ creates a tree of size @n@ filled @a@.+--+-- >>> replicateTree 4 ()+-- Node () (Node () (Node () Leaf Leaf) Leaf) (Node () Leaf Leaf)+--+-- prop> n >= 0 ==> length (replicateTree n x) == n+replicateTree :: Int -> a -> Tree a+replicateTree n x = go n+  where+    go m+      | m <= 0 = Leaf+      | otherwise =+          case quotRem m 2 of+              (o,1) ->+                  let r = go o+                  in Node x r r+              (e,_) -> Node x (go e) (go (e - 1))++-- | @'replicateA' n a@ replicates the action @a@ @n@ times.+replicateA :: Applicative f => Int -> f a -> f (Tree a)+replicateA n x = go n+  where+    go m+      | m <= 0 = pure Leaf+      | otherwise =+          case quotRem m 2 of+              (o,1) ->+                  let r = go o+                  in Node <$> x <*> r <*> r+              (e,_) -> Node <$> x <*> go e <*> go (e - 1)++instance Monoid (Tree a) where+    mappend Leaf y         = y+    mappend (Node x l r) y = Node x l (mappend r y)+    mempty = Leaf++-- | Construct a tree from a list, putting each even-positioned+-- element to the left.+treeFromList :: [a] -> Tree a+treeFromList [] = Leaf+treeFromList (x:xs) = uncurry (Node x `on` treeFromList) (pairs xs) where+  pairs ys = foldr f (const ([],[])) ys True+  f e a b = bool first second b (e:) (a (not b))++-- | Pretty-print a tree.+drawBinaryTree :: Show a => Tree a -> String+drawBinaryTree = Rose.drawForest . foldTree [] f where+  f x l r = [Rose.Node (show x) (l ++ r)]
+ src/Data/Queue/Binomial.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE BangPatterns          #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}++-- | Simple binomial heaps, with a statically-enforced shape.+module Data.Queue.Binomial+  (Binomial(..)+  ,Node(..)+  ,Tree(..))+  where++import           TypeLevel.Nat+import           Data.Queue.Class++import           Data.Typeable (Typeable)+import           GHC.Generics (Generic, Generic1)+import           Control.DeepSeq (NFData(rnf))++infixr 5 :-+-- | A binomial heap, where the sizes of the nodes are enforced in the types.+--+-- The implementation is based on:+--+-- * <http://www.cs.ox.ac.uk/ralf.hinze/publications/#J1 Hinze, Ralf. “Functional Pearls: Explaining Binomial Heaps.” Journal of Functional Programming 9, no. 1 (January 1999): 93–104. doi:10.1017/S0956796899003317.>+-- * <https://themonadreader.files.wordpress.com/2010/05/issue16.pdf Wasserman, Louis. “Playing with Priority Queues.” The Monad.Reader, May 12, 2010.>+--+-- It is a list of binomial trees, equivalent to a binary number (stored+-- least-significant-bit first).++data Binomial rk a+    -- | The empty heap+    = Nil+    -- | Skip a child tree (equivalent to a zero in the binary representation+    -- of the data structure).+    | Skip (Binomial ('S rk) a)+    -- | A child tree. Equivalent to a one in the binary representation.+    | (:-) {-# UNPACK #-} !(Tree rk a)+           (Binomial ('S rk) a)++-- | A rose tree, where the children are indexed.+data Tree rk a = Root a (Node rk a)++-- | A list of binomial trees, indexed by their sizes in ascending order.+data Node n a where+        NilN :: Node 'Z a+        (:<) :: {-# UNPACK #-} !(Tree n a) -> Node n a -> Node ('S n) a++mergeTree :: Ord a => Tree rk a -> Tree rk a -> Tree ('S rk) a+mergeTree xr@(Root x xs) yr@(Root y ys)+  | x <= y    = Root x (yr :< xs)+  | otherwise = Root y (xr :< ys)++instance Ord a =>+         Monoid (Binomial rk a) where+    mappend Nil ys              = ys+    mappend xs Nil              = xs+    mappend (Skip xs) (Skip ys) = Skip (mappend xs ys)+    mappend (Skip xs) (y :- ys) = y :- mappend xs ys+    mappend (x :- xs) (Skip ys) = x :- mappend xs ys+    mappend (x :- xs) (y :- ys) = Skip (mergeCarry (mergeTree x y) xs ys)+    mempty = Nil++mergeCarry+    :: Ord a+    => Tree rk a -> Binomial rk a -> Binomial rk a -> Binomial rk a+mergeCarry !t Nil ys              = carryLonger t ys+mergeCarry !t xs Nil              = carryLonger t xs+mergeCarry !t (Skip xs) (Skip ys) = t :- mappend xs ys+mergeCarry !t (Skip xs) (y :- ys) = Skip (mergeCarry (mergeTree t y) xs ys)+mergeCarry !t (x :- xs) (Skip ys) = Skip (mergeCarry (mergeTree t x) xs ys)+mergeCarry !t (x :- xs) (y :- ys) = t :- mergeCarry (mergeTree x y) xs ys++carryLonger :: Ord a => Tree rk a -> Binomial rk a -> Binomial rk a+carryLonger !t Nil       = t :- Nil+carryLonger !t (Skip xs) = t :- xs+carryLonger !t (x :- xs) = Skip (carryLonger (mergeTree t x) xs)++data Zipper a rk = Zipper (Node rk a) (Binomial rk a)++data MinViewZipper a rk+    = Infty+    | Min !a {-# UNPACK #-} !(Zipper a rk)++slideLeft :: Zipper a ('S rk) -> Zipper a rk+slideLeft (Zipper (t :< ts) hs) = Zipper ts (t :- hs)++pushLeft :: Ord a => Tree rk a -> Zipper a ('S rk) -> Zipper a rk+pushLeft t (Zipper (x :< xs) ts)+  = Zipper xs (Skip (carryLonger (mergeTree t x) ts))++minViewZip :: Ord a => Binomial rk a -> MinViewZipper a rk+minViewZip Nil = Infty+minViewZip (Skip xs) = case minViewZip xs of+  Infty   -> Infty+  Min e x -> Min e (slideLeft x)+minViewZip (t@(Root x ts) :- f) =+    case minViewZip f of+        Min minKey ex+          | minKey < x -> Min minKey (pushLeft t ex)+        _ -> Min x (Zipper ts (Skip f))++instance Ord a => Queue (Binomial 'Z) a where+    minView hs =+        case minViewZip hs of+            Infty               -> Nothing+            Min x (Zipper _ ts) -> Just (x, ts)+    singleton x = Root x NilN :- Nil+    insert x = carryLonger (Root x NilN)+    empty = mempty+    {-# INLINE empty #-}++instance Ord a => MeldableQueue (Binomial 'Z) a where+    merge = mappend+    {-# INLINE merge #-}++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------++instance NFData a => NFData (Binomial rk a) where+    rnf Nil = ()+    rnf (Skip xs) = rnf xs `seq` ()+    rnf (x :- xs) = rnf x `seq` rnf xs `seq` ()++deriving instance Foldable (Binomial rk)+deriving instance Functor (Binomial rk)+deriving instance Traversable (Binomial rk)+deriving instance Generic (Binomial n a)+deriving instance Generic1 (Binomial n)+deriving instance Typeable a => Typeable (Binomial n a)++deriving instance Foldable (Tree rk)+deriving instance Functor (Tree rk)+deriving instance Traversable (Tree rk)+deriving instance Generic (Tree n a)+deriving instance Generic1 (Tree n)+deriving instance Typeable a => Typeable (Tree n a)++instance NFData a => NFData (Tree rk a) where+    rnf (Root x xs) = rnf x `seq` rnf xs `seq` ()++deriving instance Typeable a => Typeable (Node n a)+deriving instance Foldable (Node rk)+deriving instance Functor (Node rk)+deriving instance Traversable (Node rk)++instance NFData a => NFData (Node rk a) where+    rnf NilN = ()+    rnf (x :< xs) = rnf x `seq` rnf xs `seq` ()++instance Ord a => Eq (Binomial 'Z a) where+    (==) = eqQueue++instance Ord a => Ord (Binomial 'Z a) where+    compare = cmpQueue++instance (Show a, Ord a) => Show (Binomial 'Z a) where+    showsPrec = showsPrecQueue++instance (Read a, Ord a) => Read (Binomial 'Z a) where+    readsPrec = readPrecQueue
+ src/Data/Queue/Braun.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | Simple, unchecked braun heaps.+module Data.Queue.Braun+  (Braun(..))+  where++import           Data.BinaryTree+import           Data.Queue.Class++import           Control.DeepSeq (NFData (rnf))+import           Data.Data       (Data)+import           Data.Typeable   (Typeable)+import           GHC.Generics    (Generic, Generic1)++-- | A Braun heap. Based on+-- <https://github.com/coq/coq/blob/d8a07b44f5245f8e2f3a47095c70bb3cc85e3d99/lib/heap.ml this implementation>.+--+-- A braun tree is a /nearly balanced/ binary tree: the left branch can+-- be either exactly the same size as the right, or one element larger.+--+-- This version is unchecked (/very/ unchecked), and is provided mainly+-- for comparison to the checked version.+newtype Braun a = Braun+    { runBraun :: Tree a+    } deriving (Typeable,Generic,Data,Generic1,Functor,Foldable,Traversable)++insertTree :: Ord a => a -> Tree a -> Tree a+insertTree x Leaf = Node x Leaf Leaf+insertTree x (Node y l r)+    | x <= y    = Node x (insertTree y r) l+    | otherwise = Node y (insertTree x r) l++instance Ord a => Queue Braun a where+    insert x (Braun ys) = Braun (insertTree x ys)+    empty = Braun Leaf+    minView (Braun xs) = (fmap.fmap) Braun (minViewTree xs)++extract :: Ord a => Tree a -> (a, Tree a)+extract (Node y Leaf Leaf) = (y, Leaf)+extract (Node y l r)       = let (x,l') = extract l in (x, Node y r l')+extract Leaf               = error "extract called on empty braun tree"++mergeTree :: Ord a => Tree a -> Tree a -> Tree a+mergeTree xs Leaf = xs+mergeTree Leaf ys = ys+mergeTree l@(Node lx ll lr) r@(Node ly _ _)+  | lx <= ly = Node lx r (mergeTree ll lr)+  | otherwise = let (x,l') = extract l in+    Node ly (replaceMax x r) l'++replaceMax :: Ord a => a -> Tree a -> Tree a+replaceMax x (Node _ l r)+  | isAbove x l, isAbove x r = Node x l r+replaceMax x (Node _ l@(Node lx _ _) r)+  | isAbove lx r = Node lx (replaceMax x l) r+replaceMax x (Node _ l r@(Node rx _ _)) = Node rx l (replaceMax x r)+replaceMax _ _ = error "impossible"++isAbove :: Ord a => a -> Tree a -> Bool+isAbove _ Leaf         = True+isAbove x (Node y _ _) = x <= y++minViewTree :: Ord a => Tree a -> Maybe (a, Tree a)+minViewTree Leaf         = Nothing+minViewTree (Node x l r) = Just (x, mergeTree l r)++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData a => NFData (Braun a) where+    rnf (Braun xs) = rnf xs `seq` ()++instance Ord a => Eq (Braun a) where+    (==) = eqQueue++instance Ord a => Ord (Braun a) where+    compare = cmpQueue++instance (Show a, Ord a) => Show (Braun a) where+    showsPrec = showsPrecQueue++instance (Read a, Ord a) => Read (Braun a) where+    readsPrec = readPrecQueue
+ src/Data/Queue/Class.hs view
@@ -0,0 +1,143 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE ScopedTypeVariables   #-}++-- | Classes for the various heaps, mainly to avoid name clashing.+module Data.Queue.Class+  (Queue(..)+  ,MeldableQueue(..)+  ,showsPrecQueue+  ,readPrecQueue+  ,eqQueue+  ,cmpQueue)+  where++import           Data.List (unfoldr)+import           Data.Function (on)+import           Data.Coerce (Coercible,coerce)++import           Data.Set (Set)+import qualified Data.Set as Set++-- | A class for queues. Conforming members can have their own+-- definition of order on their contents. (i.e., 'Ord' is not required)+class Queue h a where++    {-# MINIMAL minView , insert , empty #-}++    -- | Return the first element, and the remaining elements,+    -- or 'Nothing' if the queue is empty. For most queues,+    -- this will be the minimal element+    minView+        :: h a -> Maybe (a, h a)++    -- | Insert an element into the queue.+    insert+        :: a -> h a -> h a++    -- | The empty queue.+    empty+        :: h a++    -- | A queue with one element.+    singleton+        :: a -> h a+    singleton = flip insert empty++    -- | Return a list of the contents of the queue, in order, from+    -- smallest to largest.+    toList :: h a -> [a]+    toList = unfoldr minView++    -- | Create a heap from a list.+    fromList :: [a] -> h a+    fromList = foldr insert empty++    -- | Perform heap sort on a list of items.+    heapSort :: p h -> [a] -> [a]+    heapSort (_ :: p h) = toList . (fromList :: [a] -> h a)++-- | A class for meldable queues. Conforming members should+-- form a monoid under 'merge' and 'empty'.+class Queue h a => MeldableQueue h a where++    {-# MINIMAL merge #-}+    -- | Merge two heaps. This operation is associative, and has the+    -- identity of 'empty'.+    --+    -- @'merge' x ('merge' y z) = 'merge' ('merge' x y) z@+    --+    -- @'merge' x 'empty' = 'merge' 'empty' x = x@+    merge :: h a -> h a -> h a++    -- | Create a heap from a 'Foldable' container. This operation is+    -- provided to allow the use of 'foldMap', which may be+    -- asymptotically more efficient. The default definition uses+    -- 'foldMap'.+    fromFoldable :: (Foldable f) => f a -> h a+    fromFoldable = runQueueWrapper #. foldMap (QueueWrapper #. singleton)++newtype QueueWrapper h a = QueueWrapper+    { runQueueWrapper :: h a+    }++instance MeldableQueue h a =>+         Monoid (QueueWrapper h a) where+    mempty = QueueWrapper empty+    mappend =+        (coerce :: (h a -> h a -> h a) -> QueueWrapper h a -> QueueWrapper h a -> QueueWrapper h a)+            merge+    {-# INLINE mempty #-}+    {-# INLINE mappend #-}++-- | A default definition for 'showsPrec'.+showsPrecQueue :: (Queue h a, Show a) => Int -> h a -> ShowS+showsPrecQueue d xs =+    showParen (d >= 11) (showString "fromList " . showList (toList xs))++-- | A default definition for 'readsPrec'.+readPrecQueue+  :: (Read a, Queue h a) => Int -> ReadS (h a)+readPrecQueue d =+    readParen+        (d > 10)+        (\xs ->+              [ (fromList x, zs)+              | ("fromList",ys) <- lex xs+              , (x,zs) <- readList ys ])++-- | A default definition of '=='.+eqQueue :: (Eq a, Queue h a) => h a -> h a -> Bool+eqQueue = (==) `on` toList++-- | A default definition of 'compare'.+cmpQueue :: (Ord a, Queue h a) => h a -> h a -> Ordering+cmpQueue = compare `on` toList++infixr 9 #.+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c+(#.) _ = coerce++instance Ord a => Queue Set a where+    insert = Set.insert+    empty = Set.empty+    fromList = Set.fromList+    singleton = Set.singleton+    minView = Set.minView+    toList = Set.toList++instance Ord a => MeldableQueue Set a where+    merge = Set.union++instance Queue [] a where+    insert = (:)+    empty = []+    fromList = id+    singleton = (:[])+    minView [] = Nothing+    minView (x:xs) = Just (x,xs)+    toList = id++instance MeldableQueue [] a where+    merge = (++)+    fromFoldable = foldr (:) []
+ src/Data/Queue/Indexed/Binomial.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE BangPatterns          #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveTraversable     #-}++{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}++-- | Size-indexed binomial heaps.+module Data.Queue.Indexed.Binomial+  (Tree(..)+  ,Node(..)+  ,Binomial(..))+  where++import           GHC.TypeLits++import           Data.Queue.Indexed.Class++import           Data.Typeable (Typeable)+import           GHC.Generics (Generic, Generic1)+import           Control.DeepSeq (NFData(rnf))++-- | A size-indexed binomial tree.+data Tree n a = Root a (Node n a)++-- | A binomial tree, indexed by its size.+data Node :: Nat -> * -> * where+        NilN :: Node 0 a+        (:<) :: {-# UNPACK #-} !(Tree n a)+             -> Node n a+             -> Node (1 + n) a++mergeTree :: Ord a => Tree n a -> Tree n a -> Tree (1 + n) a+mergeTree xr@(Root x xs) yr@(Root y ys)+  | x <= y    = Root x (yr :< xs)+  | otherwise = Root y (xr :< ys)+{-# INLINE mergeTree #-}++infixr 5 :-+-- | A size-indexed binomial heap.+--+-- The implementation is similar to:+--+-- * <http://www.cs.ox.ac.uk/ralf.hinze/publications/#J1 Hinze, Ralf. “Functional Pearls: Explaining Binomial Heaps.” Journal of Functional Programming 9, no. 1 (January 1999): 93–104. doi:10.1017/S0956796899003317.>+-- * <https://themonadreader.files.wordpress.com/2010/05/issue16.pdf Wasserman, Louis. “Playing with Priority Queues.” The Monad.Reader, May 12, 2010.>+--+-- However invariants are more aggressively maintained, using a+-- typechecker plugin. It is a list of binomial trees, equivalent to a+-- binary number (stored least-significant-bit first).+data Binomial :: Nat -> Nat -> * -> * where+        Nil  :: Binomial n 0 a+        (:-) :: {-# UNPACK #-} !(Tree z a)+             -> Binomial (1 + z) xs a+             -> Binomial z (1 + xs + xs) a+        Skip :: Binomial (1 + z) (1 + xs) a+             -> Binomial z (2 + xs + xs) a++instance Ord a => IndexedQueue (Binomial 0) a where+    empty = Nil+    minView xs = case minViewZip xs of+      Zipper x _ ys -> (x, ys)+    singleton x = Root x NilN :- Nil+    insert = merge . singleton+    minViewMay q b f = case q of+      Nil -> b+      _ :- _ -> uncurry f (minView q)+      Skip _ -> uncurry f (minView q)++instance Ord a => MeldableIndexedQueue (Binomial 0) a where+    merge = mergeB+    {-# INLINE merge #-}++mergeB+    :: Ord a+    => Binomial z xs a -> Binomial z ys a -> Binomial z (xs + ys) a+mergeB Nil ys              = ys+mergeB xs Nil              = xs+mergeB (Skip xs) (Skip ys) = Skip (mergeB xs ys)+mergeB (Skip xs) (y :- ys) = y :- mergeB xs ys+mergeB (x :- xs) (Skip ys) = x :- mergeB xs ys+mergeB (x :- xs) (y :- ys) = Skip (mergeCarry (mergeTree x y) xs ys)++mergeCarry+    :: Ord a+    => Tree z a+    -> Binomial z xs a+    -> Binomial z ys a+    -> Binomial z (1 + xs + ys) a+mergeCarry !t Nil ys              = carryLonger t ys+mergeCarry !t xs Nil              = carryLonger t xs+mergeCarry !t (Skip xs) (Skip ys) = t :- mergeB xs ys+mergeCarry !t (Skip xs) (y :- ys) = Skip (mergeCarry (mergeTree t y) xs ys)+mergeCarry !t (x :- xs) (Skip ys) = Skip (mergeCarry (mergeTree t x) xs ys)+mergeCarry !t (x :- xs) (y :- ys) = t :- mergeCarry (mergeTree x y) xs ys++carryLonger :: Ord a => Tree z a -> Binomial z xs a -> Binomial z (1 + xs) a+carryLonger !t Nil       = t :- Nil+carryLonger !t (Skip xs) = t :- xs+carryLonger !t (x :- xs) = Skip (carryLonger (mergeTree t x) xs)++data Zipper a n rk = Zipper !a (Node rk a) (Binomial rk n a)++skip :: Binomial (1 + z) xs a -> Binomial z (xs + xs) a+skip x = case x of+  Nil    -> Nil+  Skip _ -> Skip x+  _ :- _ -> Skip x++data MinViewZipper a n rk where+    Infty :: MinViewZipper a 0 rk+    Min :: {-# UNPACK #-} !(Zipper a n rk) -> MinViewZipper a (n+1) rk++slideLeft :: Zipper a n (1 + rk) -> Zipper a (1 + n + n) rk+slideLeft (Zipper m (t :< ts) hs)+  = Zipper m ts (t :- hs)++pushLeft :: Ord a => Tree rk a -> Zipper a n (1 + rk) -> Zipper a (2 + n + n) rk+pushLeft c (Zipper m (t :< ts) hs)+  = Zipper m ts (Skip (carryLonger (mergeTree c t) hs))++minViewZip :: Ord a => Binomial rk (1 + n) a -> Zipper a n rk+minViewZip (Skip xs) = slideLeft (minViewZip xs)+minViewZip (t@(Root x ts) :- f) = case minViewZipMay f of+  Min ex@(Zipper minKey _ _) | minKey < x -> pushLeft t ex+  _                          -> Zipper x ts (skip f)++minViewZipMay :: Ord a => Binomial rk n a -> MinViewZipper a n rk+minViewZipMay (Skip xs) = Min (slideLeft (minViewZip xs))+minViewZipMay Nil = Infty+minViewZipMay (t@(Root x ts) :- f) = Min $ case minViewZipMay f of+  Min ex@(Zipper minKey _ _) | minKey < x -> pushLeft t ex+  _                          -> Zipper x ts (skip f)++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------++instance NFData a => NFData (Binomial rk n a) where+    rnf Nil = ()+    rnf (Skip xs) = rnf xs `seq` ()+    rnf (x :- xs) = rnf x `seq` rnf xs `seq` ()++deriving instance Foldable (Binomial rk n)+deriving instance Functor (Binomial rk n)+deriving instance Traversable (Binomial rk n)+deriving instance Typeable a => Typeable (Binomial n a)++deriving instance Foldable (Tree rk)+deriving instance Functor (Tree rk)+deriving instance Traversable (Tree rk)+deriving instance Generic (Tree n a)+deriving instance Generic1 (Tree n)+deriving instance Typeable a => Typeable (Tree n a)++instance NFData a => NFData (Tree rk a) where+    rnf (Root x xs) = rnf x `seq` rnf xs `seq` ()++deriving instance Typeable a => Typeable (Node n a)+deriving instance Foldable (Node rk)+deriving instance Functor (Node rk)+deriving instance Traversable (Node rk)++instance NFData a => NFData (Node rk a) where+    rnf NilN = ()+    rnf (x :< xs) = rnf x `seq` rnf xs `seq` ()
+ src/Data/Queue/Indexed/Braun.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}++-- | Type-indexed Braun heaps.+module Data.Queue.Indexed.Braun+  (Braun(..)+  ,Offset(..))+  where++import           Data.Proxy+import           Data.Type.Equality+import           GHC.TypeLits++import           Data.Queue.Indexed.Class hiding (MeldableIndexedQueue (..))++import           Control.DeepSeq (NFData (rnf))++-- | A Braun heap. Somewhat based on+-- <https://github.com/coq/coq/blob/d8a07b44f5245f8e2f3a47095c70bb3cc85e3d99/lib/heap.ml this implementation>,+-- but with a different strategy for maintaining invariants.+--+-- A braun tree is one where every left branch has at most one more element+-- than the right branch.+data Braun n a where+        Leaf :: Braun 0 a+        Node ::+          !(Offset n m) -> a -> Braun n a -> Braun m a -> Braun (n + m + 1) a++-- | The "singleton" for whether or not the left branch is larger than the right.+data Offset n m where+        Even :: Offset n n+        Lean :: Offset (1 + n) n++instance Ord a => IndexedQueue Braun a where++  insert x Leaf = Node Even x Leaf Leaf+  insert x (Node o y l r)+    | x <= y    = Node n x (insert y r) l+    | otherwise = Node n y (insert x r) l+    where n = case o of+            Even -> Lean+            Lean -> Even++  empty = Leaf++  minView (Node o x l r) = (x, merge o l r)++  minViewMay Leaf b _           = b+  minViewMay (Node o x l r) _ f = f x (merge o l r)++  singleton x = Node Even x Leaf Leaf++extract :: Ord a => Braun (n + 1) a -> (a, Braun n a)+extract (Node Even y Leaf _) = (y, Leaf)+extract (Node Even y l@Node{} r) = (x, Node Lean y r l')+  where+    (x,l') = extract l+extract (Node Lean y l r) = (x, Node Even y r l')+  where+    (x,l') = extract l++replaceMax :: Ord a => a -> Braun (n + 1) a -> Braun (n + 1) a+replaceMax x (Node o _ Leaf r) = Node o x Leaf r+replaceMax x (Node o _ l@(Node _ lx _ _) Leaf)+  | x <= lx = Node o x l Leaf+replaceMax x (Node o _ l@(Node _ lx _ _) r@(Node _ rx _ _))+  | x <= lx, x <= rx = Node o x l r+replaceMax x (Node o _ l@(Node _ lx _ _) Leaf) =+    Node o lx (replaceMax x l) Leaf+replaceMax x (Node o _ l@(Node _ lx _ _) r@(Node _ rx _ _))+  | lx <= rx = Node o lx (replaceMax x l) r+replaceMax x (Node o _ l r@(Node _ rx _ _)) = Node o rx l (replaceMax x r)++merge :: Ord a => Offset n m -> Braun n a -> Braun m a -> Braun (n + m) a+merge Even = mergeEven+merge Lean = mergeLean++mergeEven :: Ord a => Braun n a -> Braun n a -> Braun (n + n) a+mergeEven Leaf _ = Leaf+mergeEven l@(Node lo lx ll lr) r@(Node _ ly _ _)+  | lx <= ly = Node Lean lx r (merge lo ll lr)+  | otherwise =+      let (x,l') = extract l+      in Node Lean ly (replaceMax x r) l'++mergeLean :: Ord a => Braun (n + 1) a -> Braun n a -> Braun (n + n + 1) a+mergeLean l@(Node lo lx (ll :: Braun n1 a) (lr :: Braun m a)) r@(Node _ ly _ _ :: Braun n a)+  | lx > ly =+      let (x,l') = extract l+      in Node Even ly (replaceMax x r) l'+  | otherwise =+      case prf (Proxy :: Proxy n) (Proxy :: Proxy n1) (Proxy :: Proxy m) Refl of+           Refl -> Node Even lx r (merge lo ll lr)+  where+    prf+        :: forall x y z p.+           p x -> p y -> p z -> (x + 1) :~: ((y + z) + 1) -> (y + z) :~: x+    prf _ _ _ Refl = Refl+mergeLean l Leaf = l++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData (Offset n m) where+    rnf Even = ()+    rnf Lean = ()++instance NFData a =>+         NFData (Braun n a) where+    rnf Leaf = ()+    rnf (Node o x l r) = rnf o `seq` rnf x `seq` rnf l `seq` rnf r `seq` ()
+ src/Data/Queue/Indexed/Class.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}++-- | Classes for common functions between the heaps.+module Data.Queue.Indexed.Class where++import           GHC.TypeLits++-- | A classed for indexed priority queues. Equivalent to 'Data.Heap.Queue'+-- except the queues are indexed by their sizes.+class IndexedQueue h a where++    {-# MINIMAL insert, empty, minViewMay, minView #-}++    -- | The empty queue+    empty+        :: h 0 a++    -- | Return the minimal element, and the rest of the queue.+    minView+        :: h (1 + n) a -> (a, h n a)++    -- | A queue with one element.+    singleton+        :: a -> h 1 a+    singleton = flip insert empty++    -- | Add an element to the queue.+    insert+        :: a -> h n a -> h (1 + n) a++    -- | Pattern match on the queue, and provide a proof that it+    -- is/isn't empty to the caller.+    minViewMay+       :: h n a+       -> (n ~ 0 => b)+       -> (forall m. (1 + m) ~ n => a -> h m a -> b)+       -> b++-- | Queues which can be merged. Conforming members should+-- form a monoid under 'merge' and 'empty'.+class IndexedQueue h a =>+      MeldableIndexedQueue h a where+    -- | Merge two heaps. This operation is associative, and has the+    -- identity of 'empty'.+    --+    -- @'merge' x ('merge' y z) = 'merge' ('merge' x y) z@+    --+    -- @'merge' x 'empty' = 'merge' 'empty' x = x@+    merge+        :: h n a -> h m a -> h (n + m) a
+ src/Data/Queue/Indexed/Erased.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE KindSignatures            #-}+{-# LANGUAGE BangPatterns              #-}+{-# LANGUAGE MultiParamTypeClasses     #-}+{-# LANGUAGE FlexibleInstances         #-}++-- | Erase the size parameter on a size-indexed heap, using existentials.+module Data.Queue.Indexed.Erased+  (ErasedSize(..))+  where++import           GHC.TypeLits++import           Data.Queue.Class+import           Data.Queue.Indexed.Class (IndexedQueue, MeldableIndexedQueue)+import qualified Data.Queue.Indexed.Class as Indexed++-- | This type contains a size-indexed heap, however the size index is+-- hidden. This allows it to act like a standard heap, while maintaining+-- the proven invariants of the size-indexed version.+data ErasedSize f a = forall (n :: Nat). ErasedSize+    { runErasedSize :: f n a+    }++instance IndexedQueue h a =>+         Queue (ErasedSize h) a where+    insert x (ErasedSize xs) = ErasedSize (Indexed.insert x xs)+    empty = ErasedSize Indexed.empty+    minView (ErasedSize xs) =+        Indexed.minViewMay+            xs+            Nothing+            (\y ys ->+                  Just (y, ErasedSize ys))+    fromList = go Indexed.empty+      where+        go+            :: forall h n a.+               (IndexedQueue h a)+            => h n a -> [a] -> ErasedSize h a+        go !h [] = ErasedSize h+        go !h (x:xs) = go (Indexed.insert x h) xs+++instance MeldableIndexedQueue h a => MeldableQueue (ErasedSize h) a where+    merge (ErasedSize xs) (ErasedSize ys) = ErasedSize (Indexed.merge xs ys)
+ src/Data/Queue/Indexed/Leftist.hs view
@@ -0,0 +1,95 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE RebindableSyntax      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-- | Statically verified, type-indexed, weight-biased leftist heaps.+module Data.Queue.Indexed.Leftist+  (Leftist(..))+  where++import           Data.Queue.Indexed.Class++import           Data.Type.Equality+import           Prelude+import           TypeLevel.Bool+import           TypeLevel.Singletons++import           Control.DeepSeq (NFData(rnf))++-- | A size-indexed weight-biased leftist heap. Somewhat based on+-- the implementation from+-- <https://github.com/jstolarek/dep-typed-wbl-heaps-hs here>.+--+-- Type-level natural numbers are used to maintain the invariants+-- in the size of the structure, but these are backed by+-- 'Numeric.Natural.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.+data Leftist n a where+        Leaf :: Leftist 0 a+        Node :: !(The Nat (n + m + 1))+             -> a+             -> Leftist n a+             -> Leftist m a+             -> !(m <= n)+             -> Leftist (n + m + 1) a++rank :: Leftist n s -> The Nat n+rank Leaf             = sing+rank (Node r _ _ _ _) = r+{-# INLINE rank #-}++instance Ord a => IndexedQueue Leftist a where++    minView (Node _ x l r _) = (x, merge l r)+    {-# INLINE minView #-}+++    singleton x = Node sing x Leaf Leaf Refl+    {-# INLINE singleton #-}++    empty = Leaf+    {-# INLINE empty #-}++    insert = merge . singleton+    {-# INLINE insert #-}++    minViewMay Leaf b _             = b+    minViewMay (Node _ x l r _) _ f = f x (merge l r)++instance Ord a =>+         MeldableIndexedQueue Leftist a where+    merge Leaf h2 = h2+    merge h1 Leaf = h1+    merge h1@(Node w1 p1 l1 r1 _) h2@(Node w2 p2 l2 r2 _)+      | p1 < p2 =+          if ll <=. lr+             then Node (w1 +. w2) p1 l1 (merge r1 h2)+             else Node (w1 +. w2) p1 (merge r1 h2) l1 . totalOrder ll lr+      | otherwise =+          if rl <=. rr+              then Node (w1 +. w2) p2 l2 (merge r2 h1)+              else Node (w1 +. w2) p2 (merge r2 h1) l2 . totalOrder rl rr+      where+        ll = rank r1 +. w2+        lr = rank l1+        rl = rank r2 +. w1+        rr = rank l2+    {-# INLINE merge #-}++instance NFData a =>+         NFData (Leftist n a) where+    rnf Leaf = ()+    rnf (Node n x l r Refl) = n `seq` rnf x `seq` rnf l `seq` rnf r `seq` ()
+ src/Data/Queue/Indexed/List.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}++{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}+++-- | This module exists to showcase some uses for indexed non-priority+-- queues.+module Data.Queue.Indexed.List+  (List(..)+  ,DiffList(..)+  ,reverseTraversable+  ,reverseTraversal)+  where++import           Data.Queue.Indexed.Class+import           TypeLevel.Singletons hiding (The(..))+import           Data.Traversable.Parts++-- | A simple length-indexed list.+infixr 5 :-+data List n a where+    Nil :: List 0 a+    (:-) :: a -> List n a -> List (1 + n) a++instance IndexedQueue List a where+    empty = Nil+    insert = (:-)+    minView (x :- xs) = (x,xs)+    minViewMay Nil b _ = b+    minViewMay (x :- xs) _ f = f x xs++instance MeldableIndexedQueue List a where+    merge Nil ys = ys+    merge (x :- xs) ys = x :- merge xs ys++-- | A list with efficient concatenation.+newtype DiffList n a = DiffList+    { runDiffList :: forall m. List m a -> List (n + m) a+    }++instance IndexedQueue DiffList a where+    empty = DiffList id+    insert x xs =+        DiffList+            (\ys ->+                  runDiffList xs (x :- ys))+    minView (DiffList xs) =+        case minView (xs Nil) of+            (y,ys) -> (y, DiffList (merge ys))+    minViewMay (DiffList xs) b f =+        minViewMay+            (xs Nil)+            b+            (\y ys ->+                  f y (DiffList (merge ys)))++-- | Performs merging in reverse order.+instance MeldableIndexedQueue DiffList a where+    merge (DiffList xs) (DiffList ys) = DiffList (ys . xs)++-- | Efficiently reverse any traversable, safely and totally.+--+-- >>> reverseTraversable [1,2,3]+-- [3,2,1]+--+-- prop> reverseTraversable xs == reverse (xs :: [Int])+reverseTraversable :: Traversable t => t a -> t a+reverseTraversable = transformTraversable (`runDiffList` Nil)++-- | Efficiently reverse any traversable, safely and totally.+--+-- >>> reverseTraversal (traverse.traverse) ('a',[1,2,3])+-- ('a',[3,2,1])+reverseTraversal+    :: ((a -> Parts DiffList List a a a) -> t -> Parts DiffList List a a t)+    -> t+    -> t+reverseTraversal = transformTraversal (`runDiffList` Nil)
+ src/Data/Queue/Indexed/Pairing.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations       #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-- | Size-indexed pairing heaps.+module Data.Queue.Indexed.Pairing+  (Pairing(..)+  ,HVec(..))+  where++import           Data.Queue.Indexed.Class+import           GHC.TypeLits++import Control.DeepSeq (NFData(rnf))++-- | A simple size-indexed pairing heap. In practice, this heap seems+-- to have the best performance.+--+-- Inspired by the implementation <https://github.com/treeowl/sort-traversable here>,+-- but uses type-level literals, rather than type-level Peano numbers.+data Pairing n a where+  E :: Pairing 0 a+  T :: a -> HVec n a -> Pairing (1 + n) a++type role Pairing nominal nominal++-- | A size-indexed vector of pairing heaps.+data HVec n a where+  HNil :: HVec 0 a+  HCons :: Pairing m a -> HVec n a -> HVec (m + n) a++instance Ord a => IndexedQueue Pairing a where+    minView (T x hs) = (x, mergePairs hs)+    {-# INLINABLE minView #-}+    singleton a = T a HNil+    empty = E+    insert = merge . singleton+    {-# INLINABLE insert #-}++    minViewMay E b _        = b+    minViewMay (T x hs) _ f = f x (mergePairs hs)++instance Ord a => MeldableIndexedQueue Pairing a where+    merge E ys = ys+    merge xs E = xs+    merge h1@(T x xs) h2@(T y ys)+      | x <= y = T x (HCons h2 xs)+      | otherwise = T y (HCons h1 ys)+    {-# INLINABLE merge #-}++mergePairs :: Ord a => HVec n a -> Pairing n a+mergePairs HNil = E+mergePairs (HCons h HNil) = h+mergePairs (HCons h1 (HCons h2 hs)) =+    merge (merge h1 h2) (mergePairs hs)+{-# INLINABLE mergePairs #-}++instance NFData a => NFData (Pairing n a) where+    rnf E = ()+    rnf (T x xs) = rnf x `seq` rnf xs `seq` ()++instance NFData a => NFData (HVec n a) where+    rnf HNil = ()+    rnf (HCons x xs) = rnf x `seq` rnf xs `seq` ()
+ src/Data/Queue/Indexed/Skew.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}++-- | Size-indexed skew heaps.+module Data.Queue.Indexed.Skew+  (Skew(..))+  where++import           Data.Queue.Indexed.Class++import           GHC.TypeLits++import           Control.DeepSeq (NFData(rnf))++-- | A size-indexed skew heap.+data Skew n a where+        Empty :: Skew 0 a+        Node :: a -> Skew n a -> Skew m a -> Skew (1 + n + m) a++instance Ord a => IndexedQueue Skew a where+    empty = Empty+    singleton x = Node x Empty Empty+    minView (Node x l r) = (x, merge l r)+    insert = merge . singleton+    minViewMay Empty b _        = b+    minViewMay (Node x l r) _ f = f x (merge l r)++instance Ord a => MeldableIndexedQueue Skew a where+    merge Empty ys = ys+    merge xs Empty = xs+    merge h1@(Node x lx rx) h2@(Node y ly ry)+      | x <= y = Node x (merge h2 rx) lx+      | otherwise = Node y (merge h1 ry) ly++instance NFData a =>+         NFData (Skew n a) where+    rnf Empty = ()+    rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r `seq` ()
+ src/Data/Queue/Leftist.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | Leftist heaps.+module Data.Queue.Leftist+  (Leftist(..)+  ,zygoLeftist)+  where++import           Data.Queue.Class++import           Control.DeepSeq (NFData (rnf))+import           Data.Data       (Data)+import           Data.Typeable   (Typeable)+import           GHC.Generics    (Generic, Generic1)+++-- | A simple, unchecked, weight-biased leftist heap. Based on+-- implementation from <https://github.com/jstolarek/dep-typed-wbl-heaps-hs here>.+data Leftist a+    = Leaf+    | Node {-# UNPACK #-} !Int+           a+           (Leftist a)+           (Leftist a)+    deriving (Functor,Foldable,Traversable,Data,Typeable,Generic,Generic1)++++rank :: Leftist s -> Int+rank Leaf           = 0+rank (Node r _ _ _) = r+{-# INLINE rank #-}++instance Ord a => Queue Leftist a where++    minView Leaf           = Nothing+    minView (Node _ x l r) = Just (x, merge l r)+    {-# INLINE minView #-}++    singleton x = Node 1 x Leaf Leaf+    {-# INLINE singleton #-}++    empty = Leaf+    {-# INLINE empty #-}++    insert = merge . singleton+    {-# INLINE insert #-}+++++instance Ord a =>+         MeldableQueue Leftist a where+    merge Leaf h2 = h2+    merge h1 Leaf = h1+    merge h1@(Node w1 p1 l1 r1) h2@(Node w2 p2 l2 r2)+      | p1 < p2 =+          if ll <= lr+              then Node (w1 + w2) p1 l1 (merge r1 h2)+              else Node (w1 + w2) p1 (merge r1 h2) l1+      | otherwise =+          if rl <= rr+              then Node (w1 + w2) p2 l2 (merge r2 h1)+              else Node (w1 + w2) p2 (merge r2 h1) l2+      where+        ll = rank r1 + w2+        lr = rank l1+        rl = rank r2 + w1+        rr = rank l2++instance Ord a => Monoid (Leftist a) where+    mempty = empty+    mappend = merge++-- | A zygomorphism over the heap. Useful for checking shape properties.+zygoLeftist+    :: b1+    -> (Int -> a -> b1 -> b1 -> b1)+    -> b+    -> (Int -> a -> b1 -> b -> b1 -> b -> b)+    -> Leftist a+    -> b+zygoLeftist b1 f1 b f = snd . go+  where+    go Leaf = (b1, b)+    go (Node n x l r) =+        let (lr1,lr) = go l+            (rr1,rr) = go r+        in (f1 n x lr1 rr1, f n x lr1 lr rr1 rr)+++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData a =>+         NFData (Leftist a) where+    rnf Leaf           = ()+    rnf (Node i x l r) = rnf i `seq` rnf x `seq` rnf l `seq` rnf r `seq` ()++instance Ord a => Eq (Leftist a) where+    (==) = eqQueue++instance Ord a => Ord (Leftist a) where+    compare = cmpQueue++instance (Show a, Ord a) => Show (Leftist a) where+    showsPrec = showsPrecQueue++instance (Read a, Ord a) => Read (Leftist a) where+    readsPrec = readPrecQueue
+ src/Data/Queue/Pairing.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | Pairing heaps.+module Data.Queue.Pairing+  (Pairing(..))+  where++import           Data.Queue.Class++import           Control.DeepSeq (NFData(rnf))+import           Data.Data       (Data)+import           Data.Typeable   (Typeable)+import           GHC.Generics    (Generic, Generic1)++-- | A simple, unchecked pairing heap.+data Pairing a+    = E+    | T a [Pairing a]+    deriving (Functor,Foldable,Traversable,Data,Typeable,Generic,Generic1)++instance Ord a => Monoid (Pairing a) where+    mempty = E+    mappend E ys = ys+    mappend xs E = xs+    mappend h1@(T x xs) h2@(T y ys)+      | x <= y = T x (h2 : xs)+      | otherwise = T y (h1 : ys)+    {-# INLINABLE mappend #-}++instance Ord a => Queue Pairing a where+    singleton a = T a []+    insert = mappend . singleton+    {-# INLINABLE insert #-}+    minView (T x hs) = Just (x, mergePairs hs)+    minView E        = Nothing+    {-# INLINABLE minView #-}+    empty = mempty+    {-# INLINE empty #-}++instance Ord a => MeldableQueue Pairing a where+    merge = mappend+    {-# INLINE merge #-}++mergePairs :: Ord a => [Pairing a] -> Pairing a+mergePairs [] = E+mergePairs [h] = h+mergePairs (h1 : h2 : hs) =+    mappend (mappend h1 h2) (mergePairs hs)+{-# INLINABLE mergePairs #-}++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData a =>+         NFData (Pairing a) where+    rnf E = ()+    rnf (T x xs) = rnf x `seq` rnf xs `seq` ()++instance Ord a => Eq (Pairing a) where+    (==) = eqQueue++instance Ord a => Ord (Pairing a) where+    compare = cmpQueue++instance (Show a, Ord a) => Show (Pairing a) where+    showsPrec = showsPrecQueue++instance (Read a, Ord a) => Read (Pairing a) where+    readsPrec = readPrecQueue
+ src/Data/Queue/Skew.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | Skew heaps.+module Data.Queue.Skew+  (Skew(..))+  where++import           Data.BinaryTree+import           Data.Queue.Class++import           Control.DeepSeq (NFData(rnf))+import           Data.Data       (Data)+import           Data.Typeable   (Typeable)+import           GHC.Generics    (Generic, Generic1)++-- | A simple, unchecked skew heap.+newtype Skew a = Skew+    { runSkew :: Tree a+    } deriving (Functor,Foldable,Traversable,Data,Typeable,Generic,Generic1)++instance Ord a => Monoid (Skew a) where+    mempty = Skew Leaf+    mappend (Skew xs) (Skew ys) = Skew (smerge xs ys)++smerge :: Ord a => Tree a -> Tree a -> Tree a+smerge Leaf ys = ys+smerge xs Leaf = xs+smerge h1@(Node x lx rx) h2@(Node y ly ry)+  | x <= y    = Node x (smerge h2 rx) lx+  | otherwise = Node y (smerge h1 ry) ly++instance Ord a => Queue Skew a where+    singleton x = Skew (Node x Leaf Leaf)+    minView (Skew Leaf)         = Nothing+    minView (Skew (Node x l r)) = Just (x, Skew (smerge l r))+    empty = mempty+    insert = merge . singleton++instance Ord a => MeldableQueue Skew a where+    merge = mappend++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData a =>+         NFData (Skew a) where+    rnf (Skew x) = rnf x `seq` ()++instance Ord a => Eq (Skew a) where+    (==) = eqQueue++instance Ord a => Ord (Skew a) where+    compare = cmpQueue++instance (Show a, Ord a) => Show (Skew a) where+    showsPrec = showsPrecQueue++instance (Read a, Ord a) => Read (Skew a) where+    readsPrec = readPrecQueue
+ src/Data/Queue/WithDict.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE DeriveDataTypeable    #-}++-- | Provides a wrapper for queues, allowing them to conform to 'Foldable'.+module Data.Queue.WithDict+  (WithDict(..))+  where++import           Data.Queue.Class+import           Data.Proxy++import           Control.DeepSeq (NFData(rnf))+import           Data.Data       (Data)+import           Data.Typeable   (Typeable)++-- | This stores the dictionary of methods for the+-- priority queue of @f@, allowing the entire type+-- to conform to 'Foldable'.+data WithDict f a where+    WithDict :: Queue f a => f a -> WithDict f a++instance Queue f a => Queue (WithDict f) a where+    minView (WithDict xs) = (fmap.fmap) WithDict (minView xs)+    insert x (WithDict xs) = WithDict (insert x xs)+    empty = WithDict empty+    singleton = WithDict . singleton+    toList (WithDict xs) = toList xs+    fromList = WithDict . fromList+    heapSort (_ :: p (WithDict h)) = heapSort (Proxy :: Proxy h)++instance MeldableQueue f a => MeldableQueue (WithDict f) a where+    merge (WithDict xs) (WithDict ys) = WithDict (merge xs ys)+    fromFoldable = WithDict . fromFoldable++instance Foldable (WithDict f) where+    foldr f b (WithDict xs) = go xs where+      go hs = case minView hs of+        Nothing     -> b+        Just (y,ys) -> f y (go ys)+    foldMap f (WithDict xs) = go xs where+      go hs = case minView hs of+        Nothing     -> mempty+        Just (y,ys) -> f y `mappend` go ys++--------------------------------------------------------------------------------+-- Instances+--------------------------------------------------------------------------------+instance NFData (f a) => NFData (WithDict f a) where+    rnf (WithDict x) = rnf x `seq` ()++deriving instance+         (Data a, Data (f a), Typeable f, Queue f a) => Data+         (WithDict f a)+deriving instance Typeable (WithDict f a)+++instance (Eq a, Queue f a) => Eq (WithDict f a) where+    (==) = eqQueue++instance (Ord a, Queue f a) => Ord (WithDict f a) where+    compare = cmpQueue++instance (Show a, Queue f a) => Show (WithDict f a) where+    showsPrec = showsPrecQueue++instance (Read a, Queue f a) => Read (WithDict f a) where+    readsPrec = readPrecQueue
+ src/Data/Traversable/Parts.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}++-- | Sort any traversable. Idea from <https://github.com/treeowl/sort-traversable here>,+-- but parameterized over the heap type.+--+-- Parts can be thought of as a safe version of @unsafePartsOf@ from lens.+module Data.Traversable.Parts+  (Parts(..)+  ,liftParts+  ,queueTraversable+  ,runParts+  ,queueTraversal+  ,runPartsWith+  ,transformTraversal+  ,transformTraversable)+  where++import           Data.Queue.Indexed.Class+import           GHC.TypeLits++-- | A queue with a certain number of elements, and a function which+-- extracts exactly that many elements from a larger queue.+-- You can transform the queue (i.e., reversing, etc.) before running+-- the function, effectively transforming the contents of a traversable+-- safely. If the underlying queue is a priority queue, then inserting+-- elements will sort them as you go.+data Parts f g a b r where+    Parts :: (forall n. g (m + n) b -> (g n b, r))+         -> !(f m a)+         -> Parts f g a b r++instance Functor (Parts f g a b) where+  fmap f (Parts g h) =+    Parts (\h' -> case g h' of (remn, r) -> (remn, f r)) h+  {-# INLINE fmap #-}++instance (IndexedQueue f x, MeldableIndexedQueue f x) =>+          Applicative (Parts f g x y) where+    pure x = Parts (\h -> (h, x)) empty+    {-# INLINE pure #-}++    (Parts f (xs :: f m x) :: Parts f g x y (a -> b)) <*> Parts g (ys :: f n x) =+      Parts h (merge xs ys)+      where+        h :: forall o . g ((m + n) + o) y -> (g o y, b)+        h v = case f v of { (v', a) ->+                  case g v' of { (v'', b) ->+                    (v'', a b)}}+    {-# INLINABLE (<*>) #-}++-- | Lift a value into the running queue.+liftParts :: (IndexedQueue g a, IndexedQueue f x) => x -> Parts f g x a a+liftParts a = Parts (\h -> case minView h of (x, h') -> (h', x)) (singleton a)+{-# INLINABLE liftParts #-}++-- | Run the built-up function on the stored queue.+runParts :: forall a b f. Parts f f b b a -> a+runParts (Parts (f :: f (m + 0) b -> (f 0 b, a)) xs) = snd $ f xs++-- | Perform a length-preserving transformation on the stored queue, and+-- run the built-up function on the transformed version.+runPartsWith :: forall a b c f g. (forall n. f n a -> g n b) -> Parts f g a b c -> c+runPartsWith f (Parts (g :: g (m + 0) b -> (g 0 b, c)) xs) = snd $ g (f xs)++-- | Enqueue every element of a traversable into a queue, and then+-- dequeue them back into the same traversable. This is useful if, for+-- instance, the queue is a priority queue: then this function will+-- perform a sort. If the queue is first-in last-out, this function will+-- perform a reversal.+queueTraversable :: (MeldableIndexedQueue f a, Traversable t) => p f -> t a -> t a+queueTraversable (_ :: p f) =+    runParts .+    traverse+        (liftParts :: (IndexedQueue g x, IndexedQueue f x) =>+                     x -> Parts f g x x x)+{-# INLINABLE queueTraversable #-}++-- | Apply a function which transforms a queue without changing its+-- size to an arbitrary traversable.+transformTraversable+    :: (MeldableIndexedQueue f a, IndexedQueue g b, Traversable t)+    => (forall n. f n a -> g n b) -> t a -> t b+transformTraversable f = runPartsWith f . traverse liftParts++-- | Perform an arbitrary length-preserving transformation+-- on a lens-style traversal.+transformTraversal+    :: (IndexedQueue g b, IndexedQueue f a)+    => (forall n. f n a -> g n b)+    -> ((a -> Parts f g a b b) -> t -> Parts f g a b t)+    -> t+    -> t+transformTraversal f trav = runPartsWith f . trav liftParts+++-- | Queues a traversal.+queueTraversal+    :: (IndexedQueue f b, IndexedQueue f a)+    => ((a -> Parts f f a b b) -> t -> Parts f f a a t) -> t -> t+queueTraversal trav = runParts . trav liftParts+{-# INLINABLE queueTraversal #-}+
+ src/Data/Tree/Replicate.hs view
@@ -0,0 +1,46 @@+-- | Functions for creating rose trees (from "Data.Tree") of a specified+-- size.+module Data.Tree.Replicate where++import           Control.Monad+import           Data.Tree++-- | @'replicateA' n x@ replicates the action @x@ @n@ times.+replicateA :: Applicative f => Int -> f a -> f (Tree a)+replicateA t x = go t+  where+    go n+      | n <= 1 = flip Node [] <$> x+    go n =+        let m =+                head+                    [ y+                    | y <- [1 ..]+                    , y * y >= (n - 1) ]+            lm = (n - 1) `div` m+        in if m * lm == (n - 1)+               then Node <$> x <*> replicateM lm (go m)+               else Node <$> x <*>+                    ((:) <$> go ((n - 1) - m * lm) <*> replicateM lm (go m))++-- | @'replicateTree' n a@ creates a tree of size @n@ filled with @a@.+--+-- >>> putStr (drawTree (replicateTree 4 "."))+-- .+-- |+-- +- .+-- |+-- `- .+--    |+--    `- .+--+-- prop> n > 0 ==> length (replicateTree n x) == n+replicateTree :: Int -> a -> Tree a+replicateTree t x = go t where+ go n | n <= 1 = Node x []+ go n =+   let m = head [ y | y <- [1..], y * y >= (n-1) ]+       lm = (n-1) `div` m+   in if m * lm == (n-1)+      then Node x (replicate lm (go m))+      else Node x (go ((n-1) - m * lm) : replicate lm (go m))
+ src/TypeLevel/Bool.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE PolyKinds        #-}+{-# LANGUAGE RankNTypes       #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE TypeFamilies     #-}+{-# LANGUAGE TypeOperators    #-}++-- | Rebinable syntax helper.+module TypeLevel.Bool where++import           Data.Type.Equality+import           TypeLevel.Singletons++import           Prelude++-- | For use with @-XRebindableSyntax@. This function can be used to+-- make Haskell look reasonably dependent:+--+-- @+-- depHask :: 'The' 'Bool' x -> 'IfThenElse' x 'Int' 'String'+-- depHask cond =+--     if cond+--         then \\'Refl' -> 1+--         else \\'Refl' -> "abc"+-- @+ifThenElse :: The Bool c -> (c :~: 'True -> a) -> (c :~: 'False -> a) -> a+ifThenElse Truey t _ = t Refl+ifThenElse Falsy _ f = f Refl++-- | Type-level if then else.+type family IfThenElse (c :: Bool) (true :: k) (false :: k) :: k+     where+        IfThenElse 'True true false = true+        IfThenElse 'False true false = false
+ src/TypeLevel/Nat.hs view
@@ -0,0 +1,210 @@+{-# LANGUAGE TypeFamilies       #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE TypeOperators      #-}+{-# LANGUAGE BangPatterns       #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE DeriveDataTypeable #-}++{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++-- | Type-level Peano arithmetic.+module TypeLevel.Nat where++import TypeLevel.Singletons hiding (type (+),Nat)+import Data.List (unfoldr)++import Control.DeepSeq (NFData(rnf))++import GHC.Generics (Generic)+import Data.Data (Data,Typeable)++-- $setup+-- >>> import Test.QuickCheck+-- >>> :{+-- instance Arbitrary Nat where+--     arbitrary = fmap (fromInteger . getNonNegative) arbitrary+-- :}++-- | Peano numbers. Care is taken to make operations as lazy as+-- possible:+--+-- >>> 1 > S (S undefined)+-- False+-- >>> Z > undefined+-- False+-- >>> 3 + (undefined :: Nat) >= 3+-- True+data Nat+    = Z+    | S Nat+    deriving (Eq,Generic,Data,Typeable)++-- | As lazy as possible+instance Ord Nat where+    compare Z Z = EQ+    compare (S n) (S m) = compare n m+    compare Z (S _) = LT+    compare (S _) Z = GT+    min Z _ = Z+    min (S n) (S m) = S (min n m)+    min _ Z = Z+    max Z m = m+    max (S n) (S m) = S (max n m)+    max n Z = n+    Z <= _ = True+    S n <= S m = n <= m+    S _ <= Z = False+    Z > _ = False+    S n > S m = n > m+    S _ > Z = True+    _ >= Z = True+    Z >= S _ = False+    S n >= S m = n >= m+    _ < Z = False+    S n < S m = n < m+    Z < S _ = True++-- | Singleton for type-level Peano numbers.+data instance The Nat n where+    Zy :: The Nat Z+    Sy :: The Nat n -> The Nat (S n)++-- | Add two type-level numbers.+infixl 6 ++type family (+) (n :: Nat) (m :: Nat) :: Nat where+    Z + m = m+    S n + m = S (n + m)++-- | Subtraction stops at zero.+--+-- prop> n >= m ==> m - n == Z+instance Num Nat where+    Z + m = m+    S n + m = S (n + m)+    Z * _ = Z+    S n * m = m + n * m+    abs = id+    signum Z = 0+    signum _ = 1+    fromInteger = go . abs+      where+        go 0 = Z+        go n+          | even n = r+          | otherwise = S r+          where+            r = S (S Z) * go (n `div` 2)+    S n - S m = n - m+    n - _ = n++-- | The maximum bound here is infinity.+--+-- prop> (maxBound :: Nat) > n+instance Bounded Nat where+    minBound = Z+    maxBound = S maxBound++-- | Uses custom 'enumFrom', 'enumFromThen', 'enumFromThenTo' to avoid+-- expensive conversions to and from 'Int'.+--+-- >>> [1..3] :: [Nat]+-- [1,2,3]+-- >>> [1..1] :: [Nat]+-- [1]+-- >>> [2..1] :: [Nat]+-- []+-- >>> take 3 [1,2..] :: [Nat]+-- [1,2,3]+-- >>> take 3 [5,4..] :: [Nat]+-- [5,4,3]+-- >>> [1,3..7] :: [Nat]+-- [1,3,5,7]+-- >>> [5,4..1] :: [Nat]+-- [5,4,3,2,1]+-- >>> [5,3..1] :: [Nat]+-- [5,3,1]+instance Enum Nat where+    succ = S+    pred (S n) = n+    pred Z = error "pred called on zero nat"+    fromEnum = go 0+      where+        go !n Z = n+        go !n (S m) = go (1 + n) m+    toEnum = go . abs+      where+        go 0 = Z+        go n+          | even n = r+          | otherwise = S r+          where+            r = S (S Z) * go (n `div` 2)+    enumFrom = iterate S+    enumFromTo n m = unfoldr f (n, S m - n)+      where+        f (_,Z) = Nothing+        f (e,S l) = Just (e, (S e, l))+    enumFromThen n m = iterate t n+      where+        ts Z mm = (+) mm+        ts (S nn) (S mm) = ts nn mm+        ts nn Z = subtract nn+        t = ts n m+    enumFromThenTo n m t =+        unfoldr+            f+            (n,either (const (S n - t)) (const (S t - n)) tt)+      where+        ts Z mm = Right mm+        ts (S nn) (S mm) = ts nn mm+        ts nn Z = Left nn+        tt = ts n m+        tf = either subtract (+) tt+        td = either subtract subtract tt+        f (_,Z) = Nothing+        f (e,l@(S _)) = Just (e, (tf e,td l))++-- | Reasonably expensive.+instance Real Nat where+    toRational = fromInteger . toInteger++-- | Not at all optimized.+--+-- >>> 5 `div` 2 :: Nat+-- 2+instance Integral Nat where+    toInteger = go 0+      where+        go !p Z = p+        go !p (S n) = go (p + 1) n+    quotRem _ Z = error "divide by zero"+    quotRem x (S y) = qr Z x (S y)+      where+        qr q n m = go n m+          where+            go nn Z = qr (S q) nn m+            go (S nn) (S mm) = go nn mm+            go Z (S _) = (q, n)+    div _ Z = error "divide by zero"+    div n m = go n where+      go = subt m where+        subt Z nn = S (go nn)+        subt (S mm) (S nn) = subt mm nn+        subt (S _) Z = Z+++-- | Shows integer representation.+instance Show Nat where+    showsPrec n = showsPrec n . toInteger++-- | Reads the integer representation.+instance Read Nat where+    readsPrec d r =+        [ (fromInteger n, xs)+        | (n,xs) <- readsPrec d r ]++-- | Will obviously diverge for values like `maxBound`.+instance NFData Nat where+    rnf Z = ()+    rnf (S n) = rnf n
+ src/TypeLevel/Nat/Proofs.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies  #-}+{-# LANGUAGE DataKinds     #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++-- | Some proofs on type-level Peano numbers.+module TypeLevel.Nat.Proofs where++import TypeLevel.Nat+import Data.Type.Equality+import Unsafe.Coerce++-- | Addition is associative.+plusAssoc :: The Nat x -> p y -> q z -> ((x + y) + z) :~: (x + (y + z))+plusAssoc Zy _ _ = Refl+plusAssoc (Sy x) y z = case plusAssoc x y z of+  Refl -> Refl+{-# NOINLINE plusAssoc #-}++-- | Zero is the identity of addition.+plusZeroNeutral :: The Nat n -> n + Z :~: n+plusZeroNeutral Zy = Refl+plusZeroNeutral (Sy n) = case plusZeroNeutral n of+  Refl -> Refl+{-# NOINLINE plusZeroNeutral #-}++-- | Successor distributes over addition+plusSuccDistrib :: The Nat n -> proxy m -> n + S m :~: S (n + m)+plusSuccDistrib Zy _ = Refl+plusSuccDistrib (Sy n) p = gcastWith (plusSuccDistrib n p) Refl+{-# NOINLINE plusSuccDistrib #-}+++{-# RULES+"plusAssoc" forall x y z. plusAssoc x y z = unsafeCoerce (Refl :: 'Z :~: 'Z)+"plusZeroNeutral" forall x. plusZeroNeutral x = unsafeCoerce (Refl :: 'Z :~: 'Z)+"plusSuccDistrib" forall x y. plusSuccDistrib x y = unsafeCoerce (Refl :: 'Z :~: 'Z)+ #-}
+ src/TypeLevel/Singletons.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances   #-}++-- | Provides singletons and general type-level utilities. singletons+-- are value-level representations of types.+--+-- <http://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf Eisenberg, Richard A., and Stephanie Weirich. “Dependently Typed Programming with Singletons.” In Proceedings of the 2012 Haskell Symposium, 117–130. Haskell ’12. New York, NY, USA: ACM, 2012. doi:10.1145/2364506.2364522.>+module TypeLevel.Singletons+  (The(Truey, Falsy, Nily, (:-))+  ,KnownSing(..)+  ,(*.)+  ,(+.)+  ,(^.)+  ,(-.)+  ,(<=.)+  ,totalOrder+  ,type (<=)+  ,type (Lit.+)+  ,type (Lit.*)+  ,type (Lit.^)+  ,Lit.Nat)+  where++import Data.Kind+import qualified GHC.TypeLits as Lit+import Data.Proxy+import Data.Type.Equality++import Data.Coerce+import Unsafe.Coerce++-- | A data family for singletons. The cute name allows code like this:+--+-- @addZeroZero :: The Nat n -> n + 0 :~: n@+--+data family The k :: k -> *++data instance The Bool x where+    Falsy :: The Bool 'False+    Truey :: The Bool 'True++infixr 5 :-+data instance The [k] xs where+    Nily :: The [k] '[]+    (:-) :: The k x -> The [k] xs -> The [k] (x ': xs)++-- | Class for singletons which can be generated.+class KnownSing (x :: k) where+    sing :: The k x++instance KnownSing 'True where+    sing = Truey++instance KnownSing 'False where+    sing = Falsy++instance KnownSing '[] where+    sing = Nily++instance (KnownSing xs, KnownSing x) =>+         KnownSing (x ': xs) where+    sing = sing :- sing++-- | This is just a newtype wrapper for 'Integer'. As such, it+-- is only valid if the programmer can't construct values where the+-- type index doesn't match the contained value. For that reason,+-- the constructor is not exported.+--+-- The reason for this setup is to allow properties and invariants to be proven+-- about the numbers involved, while actual computation can  be carried out+-- efficiently on the values at runtime.+--+-- See the implementation of "Data.Heap.Indexed.Leftist" for an example of+-- the uses of this type.+newtype instance The Lit.Nat n where+        NatSing :: Integer -> The Lit.Nat n++instance Lit.KnownNat n => KnownSing n where+    sing = NatSing $ Prelude.fromInteger $ Lit.natVal (Proxy :: Proxy n)++-- | Add two numbers, on both the value and type level.+infixl 6 +.+(+.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m)+(+.) =+    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.+ m))+        (Prelude.+)+{-# INLINE (+.) #-}++-- | Multiply two numbers, on both the value and type level.+infixl 7 *.+(*.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m)+(*.) =+    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.* m))+        (Prelude.*)+{-# INLINE (*.) #-}++-- | Raise a number to a power, on the type-level and value-level.+infixr 8 ^.+(^.) :: The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m)+(^.) =+    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.^ m))+        (Prelude.^)+{-# INLINE (^.) #-}++-- | Subtract two numbers, on the type-level and value-level, with a+-- proof that overflow can't occur.+infixl 6 -.+(-.) :: (m Lit.<= n) => The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m)+(-.) =+    (coerce :: (Integer -> Integer -> Integer) -> The Lit.Nat n -> The Lit.Nat m -> The Lit.Nat (n Lit.- m))+        (Prelude.-)+{-# INLINE (-.) #-}+++-- | Test order between two numbers, and provide a proof of that+-- order with the result.+infix 4 <=.+(<=.) :: The Lit.Nat n -> The Lit.Nat m -> The Bool (n Lit.<=? m)+(<=.) (NatSing x :: The Lit.Nat n) (NatSing y :: The Lit.Nat m)+  | x <= y = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'True) of+      Refl -> Truey+  | otherwise = case (unsafeCoerce (Refl :: 'True :~: 'True) :: (n Lit.<=? m) :~: 'False) of+      Refl -> Falsy+{-# INLINE (<=.) #-}++-- | A proof of a total order on the naturals.+totalOrder ::  p n -> q m -> (n Lit.<=? m) :~: 'False -> (m Lit.<=? n) :~: 'True+totalOrder (_ :: p n) (_ :: q m) Refl = unsafeCoerce Refl :: (m Lit.<=? n) :~: 'True++-- | A proof that x is less than or equal to y.+type x <= y = (x Lit.<=? y) :~: 'True
+ test/Spec.hs view
@@ -0,0 +1,342 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts    #-}++module Main (main) where++import           Test.DocTest+import           Test.QuickCheck+import           Test.Tasty+import           Test.Tasty.QuickCheck++import           Data.BinaryTree++import           Data.Queue.Binomial         hiding (Tree)+import qualified Data.Queue.Binomial         as Binomial+import           Data.Queue.Braun            (Braun (..))+import           Data.Queue.Leftist          (Leftist,zygoLeftist)+import           Data.Queue.Pairing          (Pairing(..))+import           Data.Queue.Skew++import qualified Data.Queue.Indexed.Binomial as Indexed+import qualified Data.Queue.Indexed.Braun    as Indexed+import           Data.Queue.Indexed.Erased+import qualified Data.Queue.Indexed.Leftist  as Indexed+import qualified Data.Queue.Indexed.Pairing  as Indexed+import qualified Data.Queue.Indexed.Skew     as Indexed++import           Data.Queue.Class+import           Data.Queue.Indexed.Class++import           TypeLevel.Nat++import           Data.List                  (sort)+import           Data.Monoid++import           Data.Proxy++import           Data.Functor.Classes++nat :: Gen Nat+nat = fmap (fromInteger . getNonNegative) arbitrary++binomial :: Ord a => Binomial 'Z a -> Bool+binomial = go 1 where+  go :: forall z a. Ord a => Int -> Binomial z a -> Bool+  go _ Nil       = True+  go n (Skip xs) = go (n * 2) xs+  go n (x :- xs) = length x == n && properTree x && go (n * 2) xs++  properTree :: forall z a. Ord a => Binomial.Tree z a -> Bool+  properTree (Root x xs) = isAbove x xs && properNode xs++  properNode :: forall z a. Ord a => Node z a -> Bool+  properNode (t :< ts) = properTree t && properNode ts+  properNode NilN      = True++pairing :: Ord a => Pairing a -> Bool+pairing E = True+pairing (T x xs) = all (\y -> isAbove x y && pairing y) xs++skew :: Ord a => Skew a -> Bool+skew (Skew xs) = isHeap xs++lengthAlg :: (Int, a -> Int -> Int -> Int)+lengthAlg = (0, const (+))++isAbove :: (Ord a, Foldable f) => a -> f a -> Bool+isAbove x = all (x<=)++propHeapSort :: (Queue h Int) => Proxy h -> TestTree+propHeapSort p =+    testProperty "sort" $+    \xs ->+         heapSort p (xs :: [Int]) === sort xs++braun :: Ord a => Braun a -> Bool+braun (Braun xs) = isHeap xs && uncurry zygoTree lengthAlg True go xs where+  go _ llen lproper rlen rproper =+    rlen <= llen &&+    llen <= rlen + 1 &&+    lproper && rproper++indexedSort :: IndexedQueue h Int => Proxy h -> TestTree+indexedSort (_ :: Proxy h) =+    testProperty+        "sort"+        (\xs ->+              heapSort (Proxy :: Proxy (ErasedSize h)) (xs :: [Int]) ===+              sort xs)++leftist :: Ord a => Leftist a -> Bool+leftist =+    zygoLeftist+        (Nothing, 0)+        (\_ x (_,ls) (_,rs) ->+              (Just x, succ (ls + rs)))+        True+        go+  where+    go i x (lval,ls) lproper (rval,rs) rproper =+        isAbove x lval &&+        isAbove x rval &&+        lproper && rproper && i == succ (ls + rs) && rs <= ls++intTree :: Gen (Tree Int)+intTree = sized (`replicateA` arbitrary)++reflexiveEq :: (Eq a, Show a) => Gen a -> Property+reflexiveEq xs = forAll xs (\x -> x === x)++eqProp :: (Eq a) => (a -> a -> Bool) -> Gen a -> Gen Property+eqProp f xs = do+    x <- xs+    y <- xs+    let e = x == y+    pure $ collect e $ e === f x y++symmetricEq :: (Eq a, Show a) => Gen a -> Gen Property+symmetricEq = eqProp (flip (==))++{-# ANN equalityProps "HLint: ignore Use ==" #-}+equalityProps :: (Eq a, Show a) => Gen a -> TestTree+equalityProps xs =+    testGroup+        "equality"+        [ testProperty "reflexive" (reflexiveEq xs)+        , testProperty "symmetric" (symmetricEq xs)+        , testProperty "correct /=" (eqProp (\x y -> not (x /= y)) xs)]++readShow :: (Eq a, Read a, Show a) => Gen a -> TestTree+readShow xs =+    testProperty "read . show" $+    forAll xs $+    \x ->+         (read . show) x === x++-- | Test that manual Read1 / Show1 classes are equivalent to derived read/show.+readShow1+    :: (Read1 f, Show1 f, Show (f a), Show a, Read a, Read (f a), Eq (f a))+    => Gen (f a) -> TestTree+readShow1 (xs :: Gen (f a)) =+    testGroup+        "readshow1"+        [ testProperty "show1" $+          forAll xs $+          \x ->+               manualShow x === show x+        , testProperty "read1 . show1" $+          do x <- xs+             n <- arbitrary+             pure $+                 (liftReadsPrec readsPrec readList n . manualShow) x ===+                 ((readsPrec n . show) x :: [(f a, String)])]+  where+    manualShow x = liftShowsPrec showsPrec showList 0 x ""++liftedEq :: (Eq1 f, Show (f a), Eq a, Eq (f a)) => Gen (f a) -> TestTree+liftedEq = testProperty "eq1" . eqProp (liftEq (==))++{-# ANN ordProps "HLint: ignore Use ==" #-}+ordProps :: (Ord a, Show a) => Gen a -> TestTree+ordProps xs =+    testGroup+        "ordering"+        [ testProperty "reflexive ord" $+          forAll xs $+          \x ->+               compare x x === EQ+        , testProperty "symmetric ord" $ cmpProp (\x y c -> inv (compare y x) === c) xs+        , testProperty "same as ==" $ eqProp (\x y -> (compare x y == EQ)) xs+        , testProperty "same as < " $ cmpProp (\x y c -> (c == LT) == (x < y)) xs+        , testProperty "same as <=" $ cmpProp (\x y c -> (c /= GT) == (x <= y)) xs+        , testProperty "same as > " $ cmpProp (\x y c -> (c == GT) == (x > y)) xs+        , testProperty "same as >=" $ cmpProp (\x y c -> (c /= LT) == (x >= y)) xs+        , testProperty "min is lte" $ do+              x <- xs+              y <- xs+              let m = min x y+              pure $ m <= x && m <= y+        , testProperty "max is gte" $ do+              x <- xs+              y <- xs+              let m = max x y+              pure $ m >= x && m >= y]+  where+    inv EQ = EQ+    inv LT = GT+    inv GT = LT++cmpProp :: (Ord a, Show a, Testable prop) => (a -> a -> Ordering -> prop) -> Gen a -> Gen Property+cmpProp f xs = do+    x <- xs+    y <- xs+    let c = compare x y+    pure $ collect c $ f x y c++monoidProps :: (Monoid a, Show a, Eq a) => Gen a -> TestTree+monoidProps xs =+    testGroup+        "monoid"+        [ testProperty "associativity" $+          do x <- xs+             y <- xs+             z <- xs+             pure $ (x <> y) <> z === x <> (y <> z)+        , testProperty "left identity" $+          do x <- xs+             pure $ x === mempty <> x+        , testProperty "right identity" $+          do x <- xs+             pure $ x === x <> mempty]++liftedOrd :: (Ord1 f, Show (f a), Ord a, Ord (f a)) => Gen (f a) -> TestTree+liftedOrd =+    testProperty "compare1" . cmpProp (\x y c -> liftCompare compare x y === c)++{-# ANN fmapLaw "HLint: ignore Functor law" #-}+fmapLaw+    :: (Functor f, Eq (f a), Show (f a))+    => Gen (f a) -> Property+fmapLaw xs = forAll xs $ \x -> fmap id x === x++{-# ANN fmapCompLaw "HLint: ignore Functor law" #-}+fmapCompLaw+    :: (Functor f, Eq (f c), Show (f c))+    => Blind (b -> c) -> Blind (a -> b) -> f a -> Property+fmapCompLaw (Blind f) (Blind g) xs =+ fmap (f . g) xs === (fmap f . fmap g) xs++functorLaws+    :: (Functor f+       ,Show (f a)+       ,Eq (f a)+       ,Eq (f c)+       ,Show (f c)+       ,CoArbitrary b+       ,Arbitrary c+       ,CoArbitrary a+       ,Arbitrary b)+    => p b -> q c -> Gen (f a) -> TestTree+functorLaws (_ :: p b) (_ :: q c) (xs :: Gen (f a)) =+    testGroup+        "functor laws"+        [ testProperty "identity" (fmapLaw xs)+        , testProperty+              "composition"+              (fmapCompLaw <$> (arbitrary :: Gen (Blind (b -> c))) <*>+               (arbitrary :: Gen (Blind (a -> b))) <*>+               xs)]++withGen :: Functor f => a -> f (a -> b) -> f b+withGen = fmap . flip ($)++proper :: Show a => (a -> Bool) -> Gen a -> TestTree+proper p xs = testProperty "proper" $ do+    x <- xs+    pure $ counterexample (show x) (p x)++main :: IO ()+main = do+    doctest ["-isrc", "src"]+    defaultMain $+        testGroup+            "Tests"+            [ let xs = fmap (fromList :: [Int] -> Binomial 'Z Int) arbitrary+              in testGroup+                     "Binomial"+                     [ proper binomial xs+                     , propHeapSort (Proxy :: Proxy (Binomial 'Z))+                     , readShow xs+                     , equalityProps xs+                     , ordProps xs+                     , monoidProps xs+                     , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int) xs]+            , let xs = fmap (fromList :: [Int] -> Braun Int) arbitrary+              in testGroup+                     "Braun"+                     [ proper braun xs+                     , propHeapSort (Proxy :: Proxy Braun)+                     , readShow xs+                     , equalityProps xs+                     , ordProps xs+                     , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int) xs]+            , testGroup "Leftist" $+              propHeapSort (Proxy :: Proxy Leftist) :+              withGen+                  (fmap (fromList :: [Int] -> Leftist Int) arbitrary)+                  [ proper leftist+                  , readShow+                  , equalityProps+                  , ordProps+                  , monoidProps+                  , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)]+            , testGroup "Pairing" $+              propHeapSort (Proxy :: Proxy Pairing) :+              withGen+                  (fmap (fromList :: [Int] -> Pairing Int) arbitrary)+                  [ proper pairing+                  , readShow+                  , equalityProps+                  , ordProps+                  , monoidProps+                  , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)]+            , testGroup "Skew" $+              propHeapSort (Proxy :: Proxy Skew) :+              withGen+                  (fmap (fromList :: [Int] -> Skew Int) arbitrary)+                  [ proper skew+                  , readShow+                  , equalityProps+                  , ordProps+                  , monoidProps+                  , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)]+            , testGroup+                  "Indexed Braun"+                  [indexedSort (Proxy :: Proxy Indexed.Braun)]+            , testGroup+                  "Indexed Binomial"+                  [indexedSort (Proxy :: Proxy (Indexed.Binomial 0))]+            , testGroup+                  "Indexed Leftist"+                  [indexedSort (Proxy :: Proxy Indexed.Leftist)]+            , testGroup+                  "Indexed Pairing"+                  [indexedSort (Proxy :: Proxy Indexed.Pairing)]+            , testGroup+                  "Indexed Skew"+                  [indexedSort (Proxy :: Proxy Indexed.Skew)]+            , testGroup "Binary Tree" $+              withGen+                  intTree+                  [ readShow+                  , readShow1+                  , equalityProps+                  , liftedEq+                  , ordProps+                  , liftedOrd+                  , monoidProps+                  , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)]+            , testGroup "Nat" $ withGen nat [readShow, equalityProps, ordProps]]
+ type-indexed-queues.cabal view
@@ -0,0 +1,169 @@+name:                type-indexed-queues+version:             0.1.0.0+synopsis:            Queues with verified and unverified versions.+description:+  This library provides implementations of five different queues+  (binomial, pairing, skew, leftist, and Braun), each in two+  flavours: one verified, and one not.+  .+  At the moment, only structural invariants are maintained.+  .+  = Comparisons of verified and unverified queues+  Both versions of each queue are provided for comparison: for+  instance, compare the standard leftist queue (in+  "Data.Queue.Leftist"):+  .+  > data Leftist a+  >   = Leaf+  >   | Node !Int+  >         a+  >         (Leftist a)+  >         (Leftist a)+  .+  To its size-indexed counterpart (in "Data.Queue.Indexed.Leftist"):+  .+  > data Leftist n a where+  >         Leaf :: Leftist 0 a+  >         Node :: !(The Nat (n + m + 1))+  >              -> a+  >              -> Leftist n a+  >              -> Leftist m a+  >              -> !(m <= n)+  >              -> Leftist (n + m + 1) a+  .+  The invariant here (that the size of the left queue must+  always be less than that of the right) is encoded in the+  proof @m '<=' n@.+  .+  With that in mind, compare the unverified and verified+  implementatons of @merge@:+  .+  > merge Leaf h2 = h2+  > merge h1 Leaf = h1+  > merge h1@(Node w1 p1 l1 r1) h2@(Node w2 p2 l2 r2)+  >   | p1 < p2 =+  >       if ll <= lr+  >           then Node (w1 + w2) p1 l1 (merge r1 h2)+  >           else Node (w1 + w2) p1 (merge r1 h2) l1+  >   | otherwise =+  >       if rl <= rr+  >           then Node (w1 + w2) p2 l2 (merge r2 h1)+  >           else Node (w1 + w2) p2 (merge r2 h1) l2+  >   where+  >     ll = rank r1 + w2+  >     lr = rank l1+  >     rl = rank r2 + w1+  >     rr = rank l2+  .+  Verified:+  .+  > merge Leaf h2 = h2+  > merge h1 Leaf = h1+  > merge h1@(Node w1 p1 l1 r1 _) h2@(Node w2 p2 l2 r2 _)+  >   | p1 < p2 =+  >       if ll <=. lr+  >         then Node (w1 +. w2) p1 l1 (merge r1 h2)+  >         else Node (w1 +. w2) p1 (merge r1 h2) l1 . totalOrder ll lr+  >   | otherwise =+  >       if rl <=. rr+  >           then Node (w1 +. w2) p2 l2 (merge r2 h1)+  >           else Node (w1 +. w2) p2 (merge r2 h1) l2 . totalOrder rl rr+  >   where+  >     ll = rank r1 +. w2+  >     lr = rank l1+  >     rl = rank r2 +. w1+  >     rr = rank l2+  .+  = Using type families and typechecker plugins to encode the invariants+  The similarity is accomplished through overloading, and some+  handy functions. For instance, the second if-then-else works+  on boolean /singletons/, and the @<=.@ function provides a+  proof of order along with its answer. The actual arithmetic+  is carried out at runtime on normal integers, rather than+  Peano numerals. These tricks are explained in more detail+  "TypeLevel.Singletons" and "TypeLevel.Bool".+  .+  A typechecker plugin does most of the heavy lifting, although+  there are some (small) manual proofs.+  .+  = Uses of verified queues+  The main interesting use of these sturctures is total traversable+  sorting (<https://github.com/treeowl/sort-traversable sort-traversable>).+  An implementation of this is provided in "Data.Traversable.Parts". I'm+  interested in finding out other uses for these kinds of structures.++homepage:            https://github.com/oisdk/type-indexed-queues+license:             MIT+license-file:        LICENSE+author:              Donnacha Oisín Kidney+maintainer:          mail@doisinkidney.com+copyright:           2017 Donnacha Oisín Kidney+category:            Data Structures+build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Data.Queue.Binomial+                     , Data.Queue.Pairing+                     , Data.Queue.Skew+                     , Data.Queue.Leftist+                     , Data.Queue.Braun+                     , Data.Queue.Class+                     , Data.Queue.WithDict+                     , Data.Queue.Indexed.Pairing+                     , Data.Queue.Indexed.Binomial+                     , Data.Queue.Indexed.Skew+                     , Data.Queue.Indexed.Leftist+                     , Data.Queue.Indexed.Braun+                     , Data.Queue.Indexed.Class+                     , Data.Queue.Indexed.Erased+                     , Data.Queue.Indexed.List+                     , Data.Traversable.Parts++                     , Data.Tree.Replicate++                     , TypeLevel.Nat+                     , Data.BinaryTree+                     , TypeLevel.Singletons+                     , TypeLevel.Nat.Proofs+                     , TypeLevel.Bool++  build-depends:       base >= 4.7 && < 5+                     , ghc-typelits-natnormalise >= 0.5+                     , deepseq >= 1.4+                     , containers >= 0.5+  default-language:    Haskell2010++benchmark bench+  default-language:    Haskell2010+  type:                exitcode-stdio-1.0+  hs-source-dirs:      bench+  main-is:             bench.hs+  ghc-options:         -O2 -rtsopts -threaded++  build-depends:       base >= 4.8+                     , type-indexed-queues+                     , criterion >= 0.6+                     , containers >= 0.5+                     , random >= 1.1+                     , pqueue >= 1.3++test-suite type-indexed-queues-test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             Spec.hs+  build-depends:       base+                     , type-indexed-queues+                     , QuickCheck >= 2.8+                     , doctest+                     , containers >= 0.5+                     , tasty >= 0.11+                     , tasty-quickcheck >= 0.8+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/oisdk/type-indexed-queues