diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/bench/bench.hs b/bench/bench.hs new file mode 100644 --- /dev/null +++ b/bench/bench.hs @@ -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] diff --git a/src/Data/BinaryTree.hs b/src/Data/BinaryTree.hs new file mode 100644 --- /dev/null +++ b/src/Data/BinaryTree.hs @@ -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 +-- . +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)] diff --git a/src/Data/Queue/Binomial.hs b/src/Data/Queue/Binomial.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Binomial.hs @@ -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: +-- +-- * +-- * +-- +-- 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 diff --git a/src/Data/Queue/Braun.hs b/src/Data/Queue/Braun.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Braun.hs @@ -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 +-- . +-- +-- 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 diff --git a/src/Data/Queue/Class.hs b/src/Data/Queue/Class.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Class.hs @@ -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 (:) [] diff --git a/src/Data/Queue/Indexed/Binomial.hs b/src/Data/Queue/Indexed/Binomial.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Binomial.hs @@ -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: +-- +-- * +-- * +-- +-- 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` () diff --git a/src/Data/Queue/Indexed/Braun.hs b/src/Data/Queue/Indexed/Braun.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Braun.hs @@ -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 +-- , +-- 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` () diff --git a/src/Data/Queue/Indexed/Class.hs b/src/Data/Queue/Indexed/Class.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Class.hs @@ -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 diff --git a/src/Data/Queue/Indexed/Erased.hs b/src/Data/Queue/Indexed/Erased.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Erased.hs @@ -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) diff --git a/src/Data/Queue/Indexed/Leftist.hs b/src/Data/Queue/Indexed/Leftist.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Leftist.hs @@ -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 +-- . +-- +-- 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` () diff --git a/src/Data/Queue/Indexed/List.hs b/src/Data/Queue/Indexed/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/List.hs @@ -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) diff --git a/src/Data/Queue/Indexed/Pairing.hs b/src/Data/Queue/Indexed/Pairing.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Pairing.hs @@ -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 , +-- 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` () diff --git a/src/Data/Queue/Indexed/Skew.hs b/src/Data/Queue/Indexed/Skew.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Skew.hs @@ -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` () diff --git a/src/Data/Queue/Leftist.hs b/src/Data/Queue/Leftist.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Leftist.hs @@ -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 . +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 diff --git a/src/Data/Queue/Pairing.hs b/src/Data/Queue/Pairing.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Pairing.hs @@ -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 diff --git a/src/Data/Queue/Skew.hs b/src/Data/Queue/Skew.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Skew.hs @@ -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 diff --git a/src/Data/Queue/WithDict.hs b/src/Data/Queue/WithDict.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/WithDict.hs @@ -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 diff --git a/src/Data/Traversable/Parts.hs b/src/Data/Traversable/Parts.hs new file mode 100644 --- /dev/null +++ b/src/Data/Traversable/Parts.hs @@ -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 , +-- 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 #-} + diff --git a/src/Data/Tree/Replicate.hs b/src/Data/Tree/Replicate.hs new file mode 100644 --- /dev/null +++ b/src/Data/Tree/Replicate.hs @@ -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)) diff --git a/src/TypeLevel/Bool.hs b/src/TypeLevel/Bool.hs new file mode 100644 --- /dev/null +++ b/src/TypeLevel/Bool.hs @@ -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 diff --git a/src/TypeLevel/Nat.hs b/src/TypeLevel/Nat.hs new file mode 100644 --- /dev/null +++ b/src/TypeLevel/Nat.hs @@ -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 diff --git a/src/TypeLevel/Nat/Proofs.hs b/src/TypeLevel/Nat/Proofs.hs new file mode 100644 --- /dev/null +++ b/src/TypeLevel/Nat/Proofs.hs @@ -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) + #-} diff --git a/src/TypeLevel/Singletons.hs b/src/TypeLevel/Singletons.hs new file mode 100644 --- /dev/null +++ b/src/TypeLevel/Singletons.hs @@ -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. +-- +-- +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 diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -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]] diff --git a/type-indexed-queues.cabal b/type-indexed-queues.cabal new file mode 100644 --- /dev/null +++ b/type-indexed-queues.cabal @@ -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 (). + 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