diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/justified-containers.cabal b/justified-containers.cabal --- a/justified-containers.cabal +++ b/justified-containers.cabal @@ -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 diff --git a/src/Data/Map/Justified.hs b/src/Data/Map/Justified.hs --- a/src/Data/Map/Justified.hs +++ b/src/Data/Map/Justified.hs @@ -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)