justified-containers 0.1.1.1 → 0.1.2.0

raw patch · 3 files changed

+216/−80 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +27/−30
• justified-containers.cabal +1/−1
• src/Data/Map/Justified.hs +188/−49

@@ -8,38 +8,35 @@ `lookup` should give `Just v`? (and did shifting requirements ever make the impossible become possible after all?) -`Data.Map.Justified` provides a wrapper around `Data.Map`s `Data.Map.Map` that enables you-to separate the *proof that a key is present* from the *operations using the key*. Once-you prove that a key is present, you can use it `Maybe`-free in any number of other+`Data.Map.Justified` provides a zero-cost `newtype` wrapper around `Data.Map.Map`+that enables you to separate the *proof that a key is present* from the *operations using the key*.+Once you prove that a key is present, you can use it `Maybe`-free in any number of other operations -- sometimes even operations on other maps!  None of the functions in this module can cause a run-time error, and very few of the operations return a `Maybe` value. -See the `Data.Map.Justified.Tutorial` module for usage examples.+See the `Data.Map.Justified.Tutorial` module for usage examples, or browse the API of the+most recent release [on Hackage](https://hackage.haskell.org/package/justified-containers/docs/Data-Map-Justified.html). +### Example+ ```haskell     withMap test_table $ \table -> do            case member 1 table of     -        Nothing  -> putStrLn "Sorry, I couldnt prove that the key is present."+        Nothing  -> putStrLn "Sorry, I couldn't prove that the key is present."              Just key -> do-          -- In this do-block, 'key' represents the key 1, but carries type-level-          -- evidence that the key is present. Lookups and updates can now proceed-          -- without the possibility of error.-          putStrLn ("Found key: " ++ show key)-    -          -- lookup returns a value directly, not a 'Maybe'!+        +          -- We have proven that the key is present, and can now use it Maybe-free...+          putStrLn ("Found key: "     ++ show key)           putStrLn ("Value for key: " ++ lookup key table)-    -          -- If you update an already-mapped value, the set of valid keys does-          -- not change. So the evidence that 'key' could be found in 'table'-          -- is still sufficient to ensure that 'key' can be found in the updated-          -- table as well.-          let table = reinsert key "howdy" table-          putStrLn ("Value for key in updated map: " ++ lookup key table)++          -- ...even in certain other maps!+          let table' = reinsert key "howdy" table+          putStrLn ("Value for key in updated map: " ++ lookup key table') ```  Output:@@ -50,20 +47,20 @@  ## Motivation: `Data.Map` and `Maybe` values -Suppose you have a key-value mapping using `Data.Map`s type `Data.Map.Map k v`. Anybody making-use of `Data.Map.Map k v` to look up or modify a value must take into account the possibility+Suppose you have a key-value mapping using `Data.Map`'s type `Map k v`. Anybody making+use of `Map k v` to look up or modify a value must take into account the possibility that the given key is not present.  In `Data.Map`, there are two strategies for dealing with absent keys: -  1. Cause a runtime error (e.g. `Data.Map`s `Data.Map.!` when the key is absent)+  1. Cause a runtime error (e.g. `Data.Map`'s `(!)` when the key is absent) -  2. Return a `Maybe` value (e.g. `Data.Map`s `Data.Map.lookup`)+  2. Return a `Maybe` value (e.g. `Data.Map`'s `lookup`)  The first option introduces partial functions, so is not very palatable. But what is wrong with the second option? -To understand the problem with returning a `Maybe` value, lets ask what the  `Maybe v` in+To understand the problem with returning a `Maybe` value, let's ask what the  `Maybe v` in  ```haskell     lookup :: k -> Map k v -> Maybe v@@ -74,7 +71,7 @@ for the possibility that `key` cannot be found in `table`. I will ensure that you account for this possibility by forcing you to handle the `Nothing` case." In effect, `Data.Map` is requiring the user to prove they have handled the-possibility that a key is absent whenever they use the `Data.Map.lookup` function.+possibility that a key is absent whenever they use the `lookup` function.  ## Laziness (the bad kind) @@ -82,18 +79,18 @@ key is going to be present in a map. In this case, the `Maybe v` feels like a burden: I already *know* that this key is in the map, why should I have to handle the `Nothing` case? -In this situation, it is tempting to reach for the partial function `Data.Maybe.fromJust`,+In this situation, it is tempting to reach for the partial function `fromJust`, or a pattern match like `Nothing -> error "The impossible happened!"`. But as parts of the program are changed over time, you may find the impossible has become possible after all (or perhaps youll see the dreaded and unhelpful `*** Exception: Maybe.fromJust: Nothing`)  It is tempting to reach for partial functions or "impossible" runtime errors here, because the programmer has proven that the key is a member of the map in some other way. They-know that `Data.Map.lookup` should return a `Just v` --- but the *compiler* doesnt know this!+know that lookup` should return a `Just v` --- but the *compiler* doesnt know this!  The idea behind `Data.Map.Justified` is to encode the programmers knowledge that a key is present *within the type system*, where it can be checked at compile-time. Once a key-is known to be present, `Data.Map.Justified.lookup` will never fail. Your justification+is known to be present, `Data.Map.Justified`'s `lookup` will never fail. Your justification removes the `Just`!  # How it works@@ -108,7 +105,7 @@ *all maps of type `Map ph k v`*.  There are several ways to prove that a key belongs to a map, but the simplest is to just use-`Data.Map.Justified`s `Data.Map.Justified.member` function. In `Data.Map`, `Data.Map.member`+`Data.Map.Justified`'s `member` function. In `Data.Map`, `member` has the type  ```haskell@@ -116,13 +113,13 @@ ```  and reports whether or not the key can be found in the map. In `Data.Map.Justified`,-`Data.Map.Member` has the type+`member` has the type  ```haskell     member :: Ord k => k -> Map ph k v -> Maybe (Key ph k) ``` -Instead of a boolean, `Data.Map.Justified.member` either says `the key is not present`+Instead of a boolean, `Data.Map.Justified`'s `member` either says `the key is not present` (`Nothing`), or gives back the same key, *augmented with evidence that they key* *is present*. This key-plus-evidence can then be used to do any number of `Maybe`-free operations on the map.

@@ -1,5 +1,5 @@ name:                justified-containers-version:             0.1.1.1+version:             0.1.2.0 synopsis:            Keyed container types with type-checked proofs of key presence. description:         This package contains wrappers around standard container types,                      that provide guarantees about the presence of keys within the

@@ -13,7 +13,7 @@ -- @'lookup'@ should give @'Just' v@? (and did shifting requirements ever make the impossible -- become possible after all?) ----- "Data.Map.Justified" provides a wrapper around "Data.Map"'s @'Data.Map.Map'@ that enables you+-- "Data.Map.Justified" provides a zero-cost @newtype@ wrapper around "Data.Map"'s @'Data.Map.Map'@ that enables you -- to separate the /proof that a key is present/ from the /operations using the key/. Once -- you prove that a key is present, you can use it @Maybe@-free in any number of other -- operations -- sometimes even operations on other maps!@@ -23,28 +23,23 @@ -- -- See the 'Data.Map.Justified.Tutorial' module for usage examples. --+-- === Example -- @ --  withMap test_table $ \\table -> do --   --    case member 1 table of -----      Nothing  -> putStrLn "Sorry, I couldn't prove that the key is present."+--      Nothing  -> putStrLn "Sorry, I couldn\'t prove that the key is present." -- --      Just key -> do---        -- In this do-block, \'key\' represents the key 1, but carries type-level---        -- evidence that the key is present. Lookups and updates can now proceed---        -- without the possibility of error.+--+--        -- We have proven that the key is present, and can now use it Maybe-free... --        putStrLn ("Found key: " ++ show key)---  ---        -- lookup returns a value directly, not a \'Maybe\'! --        putStrLn ("Value for key: " ++ lookup key table) --  ---        -- If you update an already-mapped value, the set of valid keys does---        -- not change. So the evidence that \'key\' could be found in \'table\'---        -- is still sufficient to ensure that \'key\' can be found in the updated---        -- table as well.---        let table' = reinsert key "howdy" table---        putStrLn ("Value for key in updated map: " ++ lookup key table')+--        -- ...even in certain other maps!+--        let table\' = reinsert key "howdy" table+--        putStrLn ("Value for key in updated map: " ++ lookup key table\') -- @ -- Output: --@@ -151,36 +146,51 @@     , lookupGT     , lookupGE       -    -- * Lookup and update+    -- * Safe lookup     , lookup     , (!)++    -- * Preserving key sets+    -- ** Localized updates     , adjust     , adjustWithKey     , reinsert-    -- ** Inserting new keys-    , inserting-    , insertingWith-      -    -- * Mapping+    -- ** Mapping values     , mapWithKey     , traverseWithKey     , mapAccum     , mapAccumWithKey-    -- ** Mapping keys-    , mappingKeys-    , mappingKnownKeys-    , mappingKeysWith-    , mappingKnownKeysWith+    -- ** Zipping+    , zip+    , zipWith+    , zipWithKey       -    -- * Unions+    -- * Enlarging key sets  +    -- ** Inserting new keys+    , inserting+    , insertingWith+    -- ** Unions     , unioning     , unioningWith     , unioningWithKey -    -- * Zipping-    , zip-    , zipWith-    , zipWithKey+    -- * Reducing key sets+    -- ** Removing keys+    , deleting+    , subtracting+    -- ** Filtering+    , filtering+    , filteringWithKey+    -- ** Intersections+    , intersecting+    , intersectingWith+    , intersectingWithKey++    -- * Mapping key sets+    , mappingKeys+    , mappingKnownKeys+    , mappingKeysWith+    , mappingKnownKeysWith            -- * Indexing     , findIndex@@ -393,7 +403,7 @@ -- valid for the output map.  adjust :: Ord k => (v -> v) -> Key ph k -> Map ph k v -> Map ph k v-adjust f (Key k) (Map m) = Map (M.adjust f k m)+adjust f (Key k) = mmap (M.adjust f k)  -- | Adjust the valid at a key, known to be in the map, -- using the given function.@@ -403,7 +413,7 @@ -- valid for the output map.  adjustWithKey :: Ord k => (Key ph k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v-adjustWithKey f (Key k) (Map m) = Map (M.adjustWithKey f' k m)+adjustWithKey f (Key k) = mmap (M.adjustWithKey f' k)   where f' key = f (Key key)  -- | Replace the value at a key, known to be in the map.@@ -413,7 +423,7 @@ -- valid for the output map.  reinsert :: Ord k => Key ph k -> v -> Map ph k v -> Map ph k v-reinsert (Key k) v (Map m) = Map (M.insert k v m)+reinsert (Key k) v = mmap (M.insert k v)  -- | Insert a value for a key that is /not/ known to be in the map, -- evaluating the updated map with the given continuation.@@ -438,7 +448,7 @@           -> Map ph k v -- ^ initial map           -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t) -- ^ continuation           -> t-inserting k v (Map m) cont = cont (Key k, \(Key key) -> Key key, Map (M.insert k v m))+inserting k v m cont = cont (Key k, qed, mmap (M.insert k v) m)  -- | /O(log n)/. Insert with a function, combining new value and old value. -- @'insertingWith' f key value mp cont@@@ -465,8 +475,43 @@               -> Map ph k v -- ^ initial map               -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t) -- ^ continuation               -> t-insertingWith f k v (Map m) cont = cont (Key k, \(Key key) -> Key key, Map (M.insertWith f k v m))-                                         +insertingWith f k v m cont = cont (Key k, qed, mmap (M.insertWith f k v) m)++-- | /O(log n)/. Delete a key and its value from the map.+--+-- The continuation is given two things:+--+--   1. A function that can be used to convert evidence that a key+--      exists in the /updated/ map, to evidence that the key exists+--      in the /original/ map. (contrast with 'inserting')+--+--   2. The updated map itself.+--        +deleting :: Ord k+         => k  -- ^ key to remove+         -> Map ph k v -- ^ initial map+         -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -- ^ continuation+         -> t+deleting k m cont = cont (qed, mmap (M.delete k) m)++-- | /O(log n)/. Difference of two maps.+-- Return elements of the first map not existing in the second map.+--+-- The continuation is given two things:+--+--   1. A function that can be used to convert evidence that a key+--      exists in the difference, to evidence that the key exists+--      in the original left-hand map.+--+--   2. The updated map itself.+--        +subtracting :: Ord k+            => Map phL k a -- ^ the left-hand map+            -> Map phR k b -- ^ the right-hand map+            -> (forall ph'. (Key ph' k -> Key phL k, Map ph' k a) -> t) -- ^ continuation+            -> t+subtracting mapL mapR cont = cont (qed, mmap2 M.difference mapL mapR)+ {--------------------------------------------------------------------   Unions --------------------------------------------------------------------}@@ -489,9 +534,7 @@          -> Map phR k v -- ^ right-hand map          -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -- ^ continuation          -> t-unioning (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,-                                            \(Key key) -> Key key,-                                            Map (M.union mapL mapR))+unioning mapL mapR cont = cont (qed, qed, mmap2 M.union mapL mapR)  -- | @'unioningWith' f@ is the same as @'unioning'@, except that @f@ is used to -- combine values that correspond to keys found in both maps.@@ -501,9 +544,7 @@              -> Map phR k v -- ^ right-hand map              -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -- ^ continuation              -> t-unioningWith f (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,-                                                  \(Key key) -> Key key,-                                                  Map (M.unionWith f mapL mapR))+unioningWith f mapL mapR cont = cont (qed, qed, mmap2 (M.unionWith f) mapL mapR)  -- | @'unioningWithKey' f@ is the same as @'unioningWith' f@, except that @f@ also -- has access to the key and evidence that it is present in both maps.@@ -513,12 +554,39 @@                 -> Map phR k v -- ^ right-hand map                 -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -- ^ continuation                 -> t-unioningWithKey f (Map mapL) (Map mapR) cont = cont (\(Key key) -> Key key,-                                                     \(Key key) -> Key key,-                                                     Map (M.unionWithKey f' mapL mapR))+unioningWithKey f mapL mapR cont = cont (qed, qed, mmap2 (M.unionWithKey f') mapL mapR)   where f' k = f (Key k) (Key k)  {--------------------------------------------------------------------+  Filtering+--------------------------------------------------------------------}++-- | Keep only the keys and associated values in a map that satisfy+-- the predicate.+--+-- The continuation is given two things:+--+--    1. A function that converts evidence that a key is present in+--       the filtered map into evidence that the key is present in+--       the original map, and+--+--    2. The filtered map itself, with a new phantom type parameter.+--+filtering :: (v -> Bool) -- ^ predicate on values+          -> Map ph k v -- ^ original map+          -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -- ^ continuation+          -> t+filtering f m cont = cont (qed, mmap (M.filter f) m)++-- | As 'filtering', except the filtering function also has access to+-- the key and existence evidence.+filteringWithKey :: (Key ph k -> v -> Bool) -- ^ predicate on keys and values+                 -> Map ph k v -- ^ original map+                 -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -- ^ continuation+                 -> t+filteringWithKey f m cont = cont (qed, mmap (M.filterWithKey (f . Key)) m)+  +{--------------------------------------------------------------------   Mapping and traversing --------------------------------------------------------------------} @@ -527,7 +595,7 @@ mapWithKey :: (Key ph k -> a -> b)            -> Map ph k a            -> Map ph k b-mapWithKey f (Map m) = Map (M.mapWithKey f' m)+mapWithKey f = mmap (M.mapWithKey f')   where f' k = f (Key k)  -- | /O(n)/. As in @'Data.Map.traverse'@: traverse the map, but give the@@ -579,7 +647,7 @@             -> Map ph k1 v -- ^ initial map             -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -- ^ continuation             -> t-mappingKeys f (Map m) cont = cont (\(Key k) -> Key (f k), Map (M.mapKeys f m))+mappingKeys f m cont = cont (via f, mmap (M.mapKeys f) m)  -- | /O(n*log n)/. -- Same as @'mappingKeys'@, but the key-mapping function can make use of@@ -590,7 +658,7 @@             -> Map ph k1 v -- ^ initial map             -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -- ^ continuation             -> t-mappingKnownKeys f (Map m) cont = cont (Key . f, Map (M.mapKeys f' m))+mappingKnownKeys f m cont = cont (Key . f, mmap (M.mapKeys f') m)   where f' k = f (Key k)          -- | /O(n*log n)/.@@ -603,7 +671,7 @@                 -> Map ph k1 v -- ^ initial map                 -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -- ^ continuation                 -> t-mappingKeysWith op f (Map m) cont = cont (\(Key k) -> Key (f k), Map (M.mapKeysWith op f m))+mappingKeysWith op f m cont = cont (via f, mmap (M.mapKeysWith op f) m)  -- | /O(n*log n)/. -- Same as @'mappingKnownKeys'@, except a function is used to combine values when@@ -615,10 +683,50 @@                 -> Map ph k1 v -- ^ initial map                 -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -- ^ continuation                 -> t-mappingKnownKeysWith op f (Map m) cont = cont (Key . f, Map (M.mapKeysWith op f' m))+mappingKnownKeysWith op f m cont = cont (Key . f, mmap (M.mapKeysWith op f') m)   where f' k = f (Key k)          {--------------------------------------------------------------------+  Intersections+--------------------------------------------------------------------}++-- | Take the left-biased intersections of two @'Data.Map.Justified.Map'@s, as in "Data.Map"'s+-- @'Data.Map.intersection'@, evaluating the intersection map with the given continuation.+--+-- The continuation is given two things:+--+--   1. A function that can be used to convert evidence that a key exists in the intersection+--      to evidence that the key exists in each original map, and+--+--   2. The updated @'Data.Map.Justified.Map'@, with a /different phantom type/.+--+intersecting :: Ord k+             => Map phL k a -- ^ left-hand map+             -> Map phR k b -- ^ right-hand map+             -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k a) -> t) -- ^ continuation+             -> t+intersecting mapL mapR cont = cont (qed2, mmap2 M.intersection mapL mapR)++-- | As @'intersecting'@, but uses the combining function to merge mapped values on the intersection.+intersectingWith :: Ord k+                 => (a -> b -> c) -- ^ combining function+                 -> Map phL k a -- ^ left-hand map+                 -> Map phR k b -- ^ right-hand map+                 -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t) -- ^ continuation+                 -> t+intersectingWith f mapL mapR cont = cont (qed2, mmap2 (M.intersectionWith f) mapL mapR)++-- | As @'intersectingWith'@, but the combining function has access to the map keys.+intersectingWithKey :: Ord k+                    => (Key phL k -> Key phR k -> a -> b -> c) -- ^ combining function+                    -> Map phL k a -- ^ left-hand map+                    -> Map phR k b -- ^ right-hand map+                    -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t) -- ^ continuation+                    -> t+intersectingWithKey f mapL mapR cont = cont (qed2, mmap2 (M.intersectionWithKey f') mapL mapR)+  where f' k = f (Key k) (Key k)++{--------------------------------------------------------------------   Zipping --------------------------------------------------------------------} @@ -685,3 +793,34 @@   where     go = (`lookup` table)     table = fmap (phi . fmap go) m++{--------------------------------------------------------------------+  INTERNAL ONLY++  These functions are used to inform the type system about+  invariants of Data.Map. They cannot be available outside of+  this module.+--------------------------------------------------------------------}++-- | Coerce key-existence evidence+qed :: Key ph k -> Key ph' k+qed (Key k) = Key k++-- | Coerce key-existence evidence+qed2 :: Key ph k -> (Key phL k, Key phR k)+qed2 (Key k) = (Key k, Key k)++-- | Coerce key-existence evidence transported along a function+via :: (k1 -> k2) -> Key ph k1 -> Key ph' k2+via f (Key k) = Key (f k)++-- | Coerce one map type to another, using a function on "Data.Map"'s @'Data.Map.Map'@.+mmap :: (M.Map k1 v1 -> M.Map k2 v2) -> Map ph1 k1 v1 -> Map ph2 k2 v2+mmap f (Map m) = Map (f m)++-- | Coerce one map type to another, using a binary function on "Data.Map"'s @'Data.Map.Map'@.+mmap2 :: (M.Map k1 v1 -> M.Map k2 v2 -> M.Map k3 v3)+      -> Map ph1 k1 v1+      -> Map ph2 k2 v2+      -> Map ph3 k3 v3+mmap2 f (Map m1) (Map m2) = Map (f m1 m2)