|
| 1 | +{-# language FunctionalDependencies, ScopedTypeVariables, FlexibleInstances, |
| 2 | + BangPatterns, UndecidableInstances #-} |
| 3 | + |
| 4 | +-- | An implementation of Okasaki's implicit queues holding elements of some |
| 5 | +-- semigroup. We track the sum of them all. |
| 6 | +module Data.AnnotatedQueue |
| 7 | + ( Queue |
| 8 | + , ViewL (..) |
| 9 | + , empty |
| 10 | + , viewl |
| 11 | + , drop1 |
| 12 | + , singleton |
| 13 | + , snoc |
| 14 | + , measure |
| 15 | + ) where |
| 16 | + |
| 17 | +import Data.Semigroup (Semigroup (..)) |
| 18 | + |
| 19 | +data FDigit a = FOne !a | FTwo !a !a |
| 20 | +data RDigit a = RZero | ROne !a |
| 21 | +data Node s a = Node !s !a !a |
| 22 | + |
| 23 | +newtype Queue s = Queue (Tree s (Elem s)) |
| 24 | +instance Semigroup s => Semigroup (Queue s) where |
| 25 | + (!t) <> u = case viewl u of |
| 26 | + EmptyL -> t |
| 27 | + ViewL x xs -> (t `snoc` x) <> xs |
| 28 | +instance Semigroup s => Monoid (Queue s) where |
| 29 | + mempty = empty |
| 30 | + mappend = (<>) |
| 31 | + |
| 32 | +newtype Elem a = Elem a |
| 33 | + |
| 34 | +-- Debit invariant (Okasaki): the middle tree of |
| 35 | +-- a Deep node is allowed |pr| - |sf| debits, where |
| 36 | +-- pr is the prefix and sf is the suffix. |
| 37 | +data Tree s a |
| 38 | + = Zero |
| 39 | + | One !a |
| 40 | + | Two !a !a |
| 41 | + | Deep !s !(FDigit a) (Tree s (Node s a)) !(RDigit a) |
| 42 | + |
| 43 | +empty :: Queue s |
| 44 | +empty = Queue Zero |
| 45 | + |
| 46 | +singleton :: s -> Queue s |
| 47 | +singleton = Queue . One . Elem |
| 48 | + |
| 49 | +snoc :: Semigroup s => Queue s -> s -> Queue s |
| 50 | +snoc (Queue t) s = Queue (snocTree t (Elem s)) |
| 51 | +{-# INLINABLE snoc #-} |
| 52 | + |
| 53 | +measure :: Semigroup s => Queue s -> Maybe s |
| 54 | +measure (Queue q) = case q of |
| 55 | + Zero -> Nothing |
| 56 | + One a -> Just (measure_ a) |
| 57 | + Two a b -> Just (measure_ a <> measure_ b) |
| 58 | + Deep s _ _ _ -> Just s |
| 59 | +{-# INLINABLE measure #-} |
| 60 | + |
| 61 | +class Measurable s a | a -> s where |
| 62 | + measure_ :: a -> s |
| 63 | +instance Measurable s (Elem s) where |
| 64 | + measure_ (Elem x) = x |
| 65 | +instance Measurable s (Node s a) where |
| 66 | + measure_ (Node s _ _) = s |
| 67 | +instance (Semigroup s, Measurable s a) => Measurable s (FDigit a) where |
| 68 | + measure_ (FOne a) = measure_ a |
| 69 | + measure_ (FTwo a b) = measure_ a <> measure_ b |
| 70 | +class SemiMeasurable s a | a -> s where |
| 71 | + semimeasure :: s -> a -> s |
| 72 | +instance (Semigroup s, Measurable s a) => SemiMeasurable s (RDigit a) where |
| 73 | + semimeasure s RZero = s |
| 74 | + semimeasure s (ROne a) = s <> measure_ a |
| 75 | +instance (Semigroup s, Measurable s a) |
| 76 | + => SemiMeasurable s (Tree s a) where |
| 77 | + semimeasure s Zero = s |
| 78 | + semimeasure s (One a) = s <> measure_ a |
| 79 | + semimeasure s (Two a b) = s <> measure_ a <> measure_ b |
| 80 | + semimeasure s (Deep t _ _ _) = s <> t |
| 81 | + |
| 82 | +node |
| 83 | + :: (Semigroup s, Measurable s a) |
| 84 | + => a -> a -> Node s a |
| 85 | +node a b = Node (measure_ a <> measure_ b) a b |
| 86 | +{-# INLINABLE node #-} |
| 87 | + |
| 88 | +deep :: (Semigroup s, Measurable s a) => FDigit a -> Tree s (Node s a) -> RDigit a -> Tree s a |
| 89 | +deep pr m sf = Deep (measure_ pr `semimeasure` m `semimeasure` sf) pr m sf |
| 90 | +{-# INLINABLE deep #-} |
| 91 | + |
| 92 | +snocTree :: (Measurable s a, Semigroup s) => Tree s a -> a -> Tree s a |
| 93 | +-- Note: in the last case we depart slightly from Okasaki. Following Hinze |
| 94 | +-- and Paterson, we force the *old* middle immediately to prevent a chain of |
| 95 | +-- thunks from accumulating in case of multiple sequential snocs. |
| 96 | +snocTree Zero a = One a |
| 97 | +snocTree (One a) b = Two a b |
| 98 | +snocTree (Two a b) c = Deep (measure_ a <> measure_ b <> measure_ c) (FTwo a b) Zero (ROne c) |
| 99 | +snocTree (Deep s pr m RZero) q = Deep (s <> measure_ q) pr m (ROne q) |
| 100 | +snocTree (Deep s pr !m (ROne p)) !q |
| 101 | + = Deep (s <> measure_ q) pr (snocTree m (node p q)) RZero |
| 102 | +{-# INLINABLE snocTree #-} |
| 103 | + |
| 104 | +{- |
| 105 | +Theorem: snocTree is O(1) and preserves the debit invariant. |
| 106 | +
|
| 107 | +Proof: |
| 108 | +
|
| 109 | +We show that snocTree costs at most 2 units of work. |
| 110 | +
|
| 111 | +Reminder: The debit invariant allows the middle tree of a Deep |
| 112 | +node |pr| - |sf| debits. |
| 113 | +
|
| 114 | +The first two cases are trivial as they don't involve any |
| 115 | +middle trees. |
| 116 | +
|
| 117 | +In the third case, the debit allowance on `m` |
| 118 | +drops by 1. We do 1 unit of unshared work and pay off one debit |
| 119 | +on `m`, for a total of 2 units of work. |
| 120 | +
|
| 121 | +In the last case, we have two possibilities, depending on the prefix: |
| 122 | +
|
| 123 | +1. The prefix has one element. Then the debit allowance on `m` is 0. We force `m` |
| 124 | +(for free). We do 1 unit of unshared work. We create a suspension for the |
| 125 | +recursive call and place 2 debits on it to pay for that. Since the debit |
| 126 | +allowance for the suspension only allows 1 debit, we pay one of them off now. |
| 127 | +So the amortized cost is 2. |
| 128 | +
|
| 129 | +2. The prefix has two elements. Then the debit allowance on `m` is 1. We pay off |
| 130 | +that debit and force `m`. We do 1 unit of unshared work. We create a suspension |
| 131 | +for the recursive call and place 2 debits on it. This is within the debit allowance |
| 132 | +for the result. So the amortized cost is 2. |
| 133 | +-} |
| 134 | + |
| 135 | +data ViewL s = EmptyL | ViewL !s (Queue s) |
| 136 | +data ViewLTree s a = EmptyLTree | ViewLTree !a (Tree s a) |
| 137 | + |
| 138 | +viewl :: Semigroup s => Queue s -> ViewL s |
| 139 | +viewl (Queue q) = case viewlTree q of |
| 140 | + EmptyLTree -> EmptyL |
| 141 | + ViewLTree (Elem s) q' -> ViewL s (Queue q') |
| 142 | +{-# INLINABLE viewl #-} |
| 143 | + |
| 144 | +viewlTree :: (Semigroup s, Measurable s a) => Tree s a -> ViewLTree s a |
| 145 | +viewlTree Zero = EmptyLTree |
| 146 | +viewlTree (One a) = ViewLTree a Zero |
| 147 | +viewlTree (Two a b) = ViewLTree a (One b) |
| 148 | +viewlTree (Deep _ (FTwo a b) m sf) = ViewLTree a (deep (FOne b) m sf) |
| 149 | +viewlTree (Deep _ (FOne a) m sf) = ViewLTree a $ case viewlTree m of |
| 150 | + EmptyLTree -> case sf of |
| 151 | + RZero -> Zero |
| 152 | + ROne b -> One b |
| 153 | + ViewLTree (Node p b c) m' -> Deep (p `semimeasure` m' `semimeasure` sf) (FTwo b c) m' sf |
| 154 | +{-# INLINABLE viewlTree #-} |
| 155 | + |
| 156 | +-- See Okasaki PFDS Theorem 11.1 for the proof that `viewlTree` takes O(1) |
| 157 | +-- amortized time. |
| 158 | + |
| 159 | +drop1 :: Semigroup s => Queue s -> Queue s |
| 160 | +drop1 q = case viewl q of |
| 161 | + EmptyL -> empty |
| 162 | + ViewL _ q' -> q' |
| 163 | +{- |
| 164 | +-- We could expand out the upper layer to avoid an unnecessary view allocation. |
| 165 | +-- Is that worth the extra code size? |
| 166 | +drop1 (Queue q) = Queue $ case q of |
| 167 | + Zero -> Zero |
| 168 | + One _ -> Zero |
| 169 | + Two _ b -> One b |
| 170 | + Deep _ (FTwo _ b) m sf -> deep (FOne b) m sf |
| 171 | + Deep _ (FOne _) m sf -> case viewlTree m of |
| 172 | + EmptyLTree -> case sf of |
| 173 | + RZero -> Zero |
| 174 | + ROne b -> One b |
| 175 | + ViewLTree (Node p b c) m' -> Deep (p `semimeasure` m' `semimeasure` sf) (FTwo b c) m' sf |
| 176 | +-} |
| 177 | +{-# INLINABLE drop1 #-} |
0 commit comments