justified-containers (empty) → 0.1.0.0

raw patch · 6 files changed

+682/−0 lines, 6 filesdep +basedep +containerssetup-changed

Dependencies added: base, containers

Files

LICENSE +25/−0
README.md +2/−0
Setup.hs +2/−0
justified-containers.cabal +29/−0
src/Data/Map/Justified.hs +331/−0
src/Data/Map/Justified/Tutorial.hs +293/−0

+ LICENSE view

@@ -0,0 +1,25 @@+BSD 2-Clause License++Copyright (c) 2017, Matt Noonan+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++* Redistributions of source code must retain the above copyright notice, this+  list of conditions and the following disclaimer.++* Redistributions in binary form must reproduce the above copyright notice,+  this list of conditions and the following disclaimer in the documentation+  and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,2 @@+# justified-containers+Standard containers, with keys that carry evidence of their own presence.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ justified-containers.cabal view

@@ -0,0 +1,29 @@+name:                justified-containers+version:             0.1.0.0+synopsis:            Keyed container types with verified keys.+description:         This package contains wrappers around standard container types,+                     that provide guarantees about the presence of keys within the+                     container.+homepage:            https://github.com/matt-noonan/justified-containers+license:             BSD2+license-file:        LICENSE+author:              Matt Noonan+maintainer:          matt.noonan@gmail.com+copyright:           2017 Matt Noonan+category:            Data Structures+build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Data.Map.Justified+                     , Data.Map.Justified.Tutorial+  ghc-options:         -O2 -Wall+  build-depends:       base >= 4.7 && < 5+                     , containers                     +  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/matt-noonan/justified-containers

+ src/Data/Map/Justified.hs view

@@ -0,0 +1,331 @@+{-# LANGUAGE RankNTypes, DeriveTraversable #-}+-- |+-- Module      :  Data.Map.Justified+-- Copyright   :  (c) Matt Noonan 2017+-- License     :  BSD-style+-- Maintainer  :  matt.noonan@gmail.com+-- Portability :  portable+--+-- = Description+--+-- A wrapper around "Data.Map"'s 'Data.Map.Map' for shifting the burden of proof that a key+-- exists in a map from "lookup time" to "key creation time".+--+-- == Motivation: "Data.Map" and 'Maybe' values+--+-- 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)+--+--   2. Return a 'Maybe' value (e.g. "Data.Map"'s 'Data.Map.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, let's ask what returning+-- @Maybe v@ from @lookup :: k -> Map k v -> Maybe v@ really does for us. By returning+-- a @Maybe v@ value, @lookup key table@ is saying "Your program must account+-- 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.+--+-- == Laziness (the bad kind)+--+-- Every programmer has probably had the experience of knowing, somehow, that a certain+-- 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 handle the 'Nothing' case?+--+-- In this situation, it is tempting to reach for the partial function 'Data.Maybe.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 you'll 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/ doesn't know this!+--+-- The idea behind "Data.Map.Justified" is to encode the programmer's 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+-- removes the 'Just'!+--+-- == How it works+--+-- Evidence that a key can indeed be found in a map is carried by a phantom type parameter @ph@+-- shared by both the 'Data.Map.Justified.Map' and 'Data.Map.Justified.Key' types. If you are+-- able to get your hands on a value of type @Key ph k@, then you must have already proven that+-- the key is present in /any/ value of type @Map ph k v@.+--+-- The @Key ph k@ type is simply a @newtype@ wrapper around @k@, but the phantom type @ph@ allows+-- @Key ph k@ to represent both /a key of type @k@/ __and__ /a proof that the key is present in+-- 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'+-- has the type+--+-- @member :: Ord k => k -> Map k v -> Bool@+--+-- and reports whether or not the key can be found in the map. In "Data.Map.Justified",+-- 'Data.Map.Member' has the type+--+-- @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"+-- ('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.+--+-- "Data.Map.Justified" uses the same rank-2 polymorphism trick used in the 'ST' monad to+-- ensure that the @ph@ phantom type can not be extracted; in effect, the proof that a key is+-- present can't leak to contexts where the proof would no longer be valid.+--+-- == Tutorial+--+-- See "Data.Map.Justified.Tutorial" for usage examples and FAQs.++module Data.Map.Justified (+    -- * Map and Key types+      Map+    , Key+    , theKey+    , theMap++    -- * Evaluation+    , withMap+    , KeyInfo(..)+    , MissingReference+    , withRecMap++    -- * Gathering evidence+    , member+    , keys++    -- * Lookup and update+    , lookup+    , (!)+    , adjust+    , adjustWithKey+    , reinsert++    -- * Indexing+    , findIndex+    , elemAt++    -- * Utilities+    , tie++    ) where++import Prelude hiding (lookup)+import qualified Data.Map as M+import Data.List (partition)+import Control.Arrow ((&&&))++{--------------------------------------------------------------------+  Map and Key types+--------------------------------------------------------------------}+-- | A "Data.Map" 'Data.Map.Map' wrapper that allows direct lookup of keys that+-- are known to exist in the map.+--+-- Here, "direct lookup" means that once a key has been proven+-- to exist in the map, it can be used to extract a value directly+-- from the map, rather than requiring a 'Maybe' layer.+--+-- 'Map' allows you to shift the burden of proof that a key exists+-- in a map from "prove at every lookup" to "prove once per key".+newtype Map ph k v = Map (M.Map k v) deriving (Eq, Ord, Show, Functor, Foldable, Traversable)++-- | A key that knows it can be found in certain 'Map's.+-- +-- The evidence that the key can be found in a map is carried by+-- the type system via the phantom type parameter @ph@. Certain+-- operations such as lookup will only type-check if the 'Key'+-- and the 'Map' have the same phantom type parameter.+newtype Key ph k = Key k deriving (Eq, Ord, Show)++-- | Get a bare key out of a key-plus-evidence by forgetting+-- what map the key can be found in.+theKey :: Key ph k -> k+theKey (Key k) = k++-- | Get the underlying "Data.Map" 'Data.Map' out of a 'Map'.+theMap :: Map ph k v -> M.Map k v+theMap (Map m) = m++{--------------------------------------------------------------------+  Evaluation+--------------------------------------------------------------------}+-- | Evaluate an expression using justified key lookups into the given map.+--+-- > import qualified Data.Map as M+-- >+-- > withMap (M.fromList [(1,"A"), (2,"B")]) $ \m -> do+-- >+-- >   -- prints "Found Key 1 with value A"+-- >   case member 1 m of+-- >     Nothing -> putStrLn "Missing key 1."+-- >     Just k  -> putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)+-- >+-- >   -- prints "Missing key 3."+-- >   case member 3 m of+-- >     Nothing -> putStrLn "Missing key 3."+-- >     Just k  -> putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)++withMap :: M.Map k v -> (forall ph. Map ph k v -> t) -> t+withMap m f = f (Map m)++-- | Information about whether a key is present or missing.+-- See 'Data.Map.Justified.withRecMap' and "Data.Map.Justified.Tutorial"'s+-- 'Data.Map.Justified.Tutorial.example4'.+data KeyInfo = Present | Missing deriving (Show, Eq, Ord)++-- | A description of what key/value-containing-keys pairs failed to be found.+-- See 'Data.Map.Justified.withRecMap' and "Data.Map.Justified.Tutorial"'s+-- 'Data.Map.Justified.Tutorial.example4'.+type MissingReference k f = (k, f (k, KeyInfo))++-- | Evaluate an expression using justified key lookups into the given map,+-- when the values can contain references back to keys in the map.+--+-- Each referenced key is checked to ensure that it can be found in the map.+-- If all referenced keys are found, they are augmented with evidence and the+-- given function is applied.+-- If some referenced keys are missing, information about the missing references+-- is generated instead.+--+-- > import qualified Data.Map as M+-- >+-- > data Cell ptr = Nil | Cons ptr ptr deriving (Functor, Foldable, Traversable)+-- >+-- > memory1 = M.fromList [(1, Cons 2 1), (2, Nil)]+-- > withRecMap memory1 (const ()) -- Right ()+-- >+-- > memory2 = M.fromList [(1, Cons 2 3), (2, Nil)]+-- > withRecMap memory2 (const ()) -- Left [(1, Cons (2,Present) (3,Missing))]++withRecMap :: (Ord k, Traversable f)+           => M.Map k (f k)+           -> (forall ph. Map ph k (f (Key ph k)) -> t)+           -> Either [MissingReference k f] t+withRecMap m f =+  case bad of+    [] -> Right $ f (Map $ M.map (fmap Key) $ M.fromList ok)+    _  -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bad)+  where+    (ok, bad) = partition (all ((== Present) . locate) . snd) (M.toList m)+    locate k = if M.member k m then Present else Missing++{--------------------------------------------------------------------+  Gathering evidence+--------------------------------------------------------------------}+-- | /O(log n)/. Obtain evidence that the key is a member of the map.+--+-- Where "Data.Map" generally requires evidence that a key exists in a map+-- at every use of some functions (e.g. "Data.Map"'s 'Data.Map.lookup'),+-- 'Map' requires the evidence up-front. After it is known that a key can be+-- found, there is no need for 'Maybe' types or run-time errors.+--+-- The @Maybe value@ that has to be checked at every lookup in "Data.Map"+-- is then shifted to a @Maybe (Key ph k)@ that has to be checked in order+-- to obtain evidence that a key is in the map.+--+-- Note that the "evidence" only exists at the type level, during compilation;+-- there is no runtime distinction between keys and keys-plus-evidence.+--+-- > withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 1) == False+-- > withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 5) == True+member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)+member k (Map m) = fmap (const $ Key k) (M.lookup k m)++-- | A list of all of the keys in a map, along with proof+-- that the keys exist within the map.+keys :: Map ph k v -> [Key ph k]+keys (Map m) = map Key (M.keys m)+++{--------------------------------------------------------------------+  Lookup and update+--------------------------------------------------------------------}+-- | /O(log n)/. Find the value at a key. Unlike+-- "Data.Map"'s 'Data.Map.!', this function is total and can not fail at runtime.+(!) :: Ord k => Map ph k v -> Key ph k -> v+(!) = flip lookup++-- | /O(log n)/. Lookup the value at a key, known to be in the map.+--+-- The result is a @v@ rather than a @Maybe v@, because the+-- proof obligation that the key is in the map must already+-- have been discharged to obtain a value of type @Key ph k@.+--+lookup :: Ord k => Key ph k -> Map ph k v -> v+lookup (Key k) (Map m) = case M.lookup k m of+  Just value -> value+  Nothing    -> error "Data.Map.Justified has been subverted!"++-- | Adjust the valid at a key, known to be in the map,+-- using the given function.+--+-- Since the set of valid keys in the input map and output map+-- are the same, keys that were valid for the input map remain+-- 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 the valid at a key, known to be in the map,+-- using the given function.+--+-- Since the set of valid keys in the input map and output map+-- are the same, keys that were valid for the input map remain+-- valid for the output map.++adjustWithKey :: Ord k => (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)++-- | Replace the value at a key, known to be in the map.+--+-- Since the set of valid keys in the input map and output map+-- are the same, keys that were valid for the input map remain+-- 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)+++{--------------------------------------------------------------------+  Indexing+--------------------------------------------------------------------}+-- | /O(log n)/. Return the /index/ of a key, which is its zero-based index in+-- the sequence sorted by keys. The index is a number from /0/ up to, but not+-- including, the 'size' of the map. The index also carries a proof that it is+-- valid for the map.+--+-- Unlike "Data.Map"'s 'Data.Map.findIndex', this function can not fail at runtime.++findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int+findIndex (Key k) (Map m) = Key (M.findIndex k m)++-- | /O(log n)/. Retrieve an element by its /index/, i.e. by its zero-based+-- index in the sequence sorted by keys.+--+-- Unlike "Data.Map"'s 'Data.Map.elemAt', this function can not fail at runtime.++elemAt :: Key ph Int -> Map ph k v -> (Key ph k, v)+elemAt (Key n) (Map m) = let (k,v) = M.elemAt n m in (Key k, v)++{--------------------------------------------------------------------+  Utilities+--------------------------------------------------------------------}++-- | Build a value by "tying the knot" according to the references in the map.+tie :: (Functor f, Ord k) => (f a -> a) ->  Map ph k (f (Key ph k)) -> Key ph k -> a+tie phi m = go+  where+    go = (`lookup` table)+    table = fmap (phi . fmap go) m

+ src/Data/Map/Justified/Tutorial.hs view

@@ -0,0 +1,293 @@+{-# LANGUAGE RankNTypes, DeriveTraversable #-}+-- |+-- Module      :  Data.Map.Justified.Tutorial+-- Copyright   :  (c) Matt Noonan 2017+-- License     :  BSD-style+-- Maintainer  :  matt.noonan@gmail.com+-- Portability :  portable+--+-- = Description+--+-- The examples below demonstrate how to use the types and functions in "Data.Map.Justified".+--+-- You should be able to simply load this module in @ghci@ to play along.+-- The import list is:+--+-- @+--  import Prelude hiding (lookup)+--  +--  import Data.Map.Justified+--  +--  import qualified Data.Map as M+--  +--  import Data.Traversable (for)+--  import Data.Char (toUpper)+--  import Control.Monad (forM_)+-- @++module Data.Map.Justified.Tutorial where++import Prelude hiding (lookup)++import Data.Map.Justified++import qualified Data.Map as M++import Data.Char (toUpper)+import Control.Monad (forM_)++-- | A simple "Data.Map" value used in several examples below.+--+-- @+--  test_table = M.fromList [ (1, "hello"), (2, "world") ]+-- @+test_table :: M.Map Int String+test_table = M.fromList [ (1, "hello"), (2, "world") ]++-- | This example shows how the 'Data.Map.Justified.member'+-- function can be used to obtain a key whose type has been+-- augmented by a proof that the key is present in maps of a+-- certain type.+--+-- Where "Data.Map" may use a 'Maybe' type to ensure that+-- the user handles missing keys when performing a lookup,+-- here we use the 'Maybe' type to either tell the user+-- that a key is missing (by returning 'Nothing'), or+-- actually give back evidence of the key's presence+-- (by returning @Just known_key@)+--+-- The 'Data.Map.Justified.withMap' function is used to+-- plumb a "Data.Map" 'Data.Map.Map' into a function that+-- expects a "Data.Map.Justified" 'Data.Map.Justified.Map'.+-- In the code below, you can think of @table@ as @test_table@,+-- enhanced with the ability to use verified keys.+--+-- You can get from @table@ back to @test_table@ using the+-- function 'Data.Map.Justified.theMap'.+--+-- @+--  example1 = withMap test_table $ \\table -> do+--+--    putStrLn "Is 1 a valid key?"+--    case member 1 table of+--      Nothing  -> putStrLn "  No, it was not found."+--      Just key -> putStrLn $ "  Yes, found key: " ++ show key+--+--    putStrLn "Is 5 a valid key?"+--    case member 5 table of+--      Nothing  -> putStrLn "  No, it was not found."+--      Just key -> putStrLn $ "  Yes, found key: " ++ show key+-- @+-- Output:+--+-- @+--  Is 1 a valid key?+--    Yes, found key: Key 1+--  Is 5 a valid key?+--    No, it was not found.+-- @+example1 :: IO ()+example1 = withMap test_table $ \table -> do++    putStrLn "Is 1 a valid key?"+    case member 1 table of+      Nothing  -> putStrLn "  No, it was not found."+      Just key -> putStrLn $ "  Yes, found key: " ++ show key++    putStrLn "Is 5 a valid key?"+    case member 5 table of+      Nothing  -> putStrLn "  No, it was not found."+      Just key -> putStrLn $ "  Yes, found key: " ++ show key++-- | Once you have obtained a verified key, how do you use it?+--+-- "Data.Map.Justified" has several functions that are similar+-- to ones found in "Data.Map" that operate over verified keys.+-- In this example, notice that we can extract values directly+-- from the map using 'Data.Map.Justified.lookup'; since we already+-- proved that the key is present when we obtained a @Key ph k@+-- value, 'Data.Map.Justified.lookup' does not need to return a+-- 'Maybe' value.+--+-- @+--  example2 = withMap test_table $ \\table -> do+--  +--    case member 1 table of+--      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)+--  +--        -- Note that 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')+-- @+-- Output:+--+-- @+--  Found key: Key 1+--  Value for key: hello+--  Value for key in updated map: howdy+-- @+example2 :: IO ()+example2 = withMap test_table $ \table -> do++  case member 1 table of+    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)++      -- Note that 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')++-- | It is a bit surprising to realize that a key of type @Key ph k@ can+-- be used to safely look up values in /any/ map of type @Map ph k v@,+-- not only the map that they key was originally found in!+--+-- This example makes use of that property to look up corresponding+-- elements of two /different/ (but related) tables, using the same+-- key evidence.+--+-- @+--  example3 = withMap test_table $ \\table -> do+--  +--    let uppercase = map toUpper+--        updated_table = fmap (reverse . uppercase) table+--    +--    for (keys table) $ \\key -> do+--      -- Although we are iterating over keys from the original table, they+--      -- can also be used to safely lookup values in the fmapped table.+--      -- Unlike (!) from Data.Map, Data.Map.Justified's (!) can not fail at runtime.+--      putStrLn ("In original table, " ++ show key ++ " maps to " ++ table ! key)+--      putStrLn ("In updated table,  " ++ show key ++ " maps to " ++ updated_table ! key)+--  +--    return ()+-- @+-- Output:+--+-- @+--  In original table, Key 1 maps to hello+--  In updated table,  Key 1 maps to OLLEH+--  In original table, Key 2 maps to world+--  In updated table,  Key 2 maps to DLROW+-- @+example3 :: IO ()+example3 = withMap test_table $ \table -> do++  let uppercase = map toUpper+      updated_table = fmap (reverse . uppercase) table+  +  forM_ (keys table) $ \key -> do+    -- Although we are iterating over keys from the original table, they+    -- can also be used to safely lookup values in the fmapped table.+    -- Unlike (!) from Data.Map, Data.Map.Justified's (!) can not fail at runtime.+    putStrLn ("In original table, " ++ show key ++ " maps to " ++ table ! key)+    putStrLn ("In updated table,  " ++ show key ++ " maps to " ++ updated_table ! key)++  return ()++-- | The next example uses a directed graph, defined by this adjacency list.+--+-- @+--  adjacencies = M.fromList [ (1, [2,3]), (2, [1,5,3]), (3, [4]), (4, [3, 1]), (5, []) ]+-- @+adjacencies :: M.Map Int [Int]+adjacencies = M.fromList [ (1, [2,3]), (2, [1,5,3]), (3, [4]), (4, [3, 1]), (5, []) ]++-- | Sometimes, the values in a map may include references back to keys+-- in the map. A canonical example of this is the adjacency map representation of+-- a directed graph, where each node maps to its list of immediate successors.+-- The type would look something like+--+-- @+--  type Digraphy node = M.Map node [node]+-- @+--+-- If you want to do a computation with a @Digraphy node@, you probably want each+-- of the neighbor nodes to have keys in the @Digraphy node@ map. That is, you+-- may really want+--+-- @+--  type Digraph ph node = Map ph node [Key ph node]+--                             \/\\           \/\\+--                             |            |+--                             +-----+------++--                                   |+--   (each neighbor should carry a proof that they are also in the map)+-- @+-- You can do this via 'Data.Map.Justified.withRecMap', which converts each+-- key reference of type @k@ in your map to a verified key of type @Key ph k@.+--+-- But what if a referenced key really is missing from the map? 'Data.Map.Justified.withRecMap'+-- returns an 'Either' value to represent failure; if a key is missing, then the+-- result will be a value of the form @Left problem@, where @problem@ is an explanation+-- of where the missing keys are.+--+-- @+--  example4 = do+--     -- Print out the nodes in a graph +--     putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)+--     trial adjacencies+--  +--     -- Now add the (non-present) node 6 as a target of an edge from node 4 and try again:+--     let adjacencies' = M.adjust (6:) 4 adjacencies+--     putStrLn ("Finding nodes in the directed graph " ++ show adjacencies')+--     trial adjacencies'+--     +--    where+--      trial adj = either showComplaint showNodes (withRecMap adj (map theKey . keys))+--      +--      showNodes nodes = putStrLn ("  Nodes: " ++ show nodes)+--  +--      showComplaint problems = do+--        putStrLn "  The following edges are missing targets:"+--        let badPairs = concatMap (\\(src, tgts) -> [ (src,tgt) | (tgt, Missing) <- tgts ]) problems+--        forM_ badPairs $ \\(src,tgt) -> putStrLn ("    " ++ show src ++ " -> " ++ show tgt)+-- @+-- Output:+--+-- @+--  Finding nodes in the directed graph fromList [(1,[2,3]),(2,[1,5,3]),(3,[4]),(4,[3,1]),(5,[])]+--    Nodes: [1,2,3,4,5]+--  Finding nodes in the directed graph fromList [(1,[2,3]),(2,[1,5,3]),(3,[4]),(4,[6,3,1]),(5,[])]+--    The following edges are missing targets:+--      4 -> 6+-- @+example4 :: IO ()+example4 = do+   -- Print out the nodes in a graph +   putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)+   trial adjacencies++   -- Now add the (non-present) node 6 as a target of an edge from node 4 and try again:+   let adjacencies' = M.adjust (6:) 4 adjacencies+   putStrLn ("Finding nodes in the directed graph " ++ show adjacencies')+   trial adjacencies'+   +  where+    trial adj = either showComplaint showNodes (withRecMap adj (map theKey . keys))+    +    showNodes nodes = putStrLn ("  Nodes: " ++ show nodes)++    showComplaint problems = do+      putStrLn "  The following edges are missing targets:"+      let badPairs = concatMap (\(src, tgts) -> [ (src,tgt) | (tgt, Missing) <- tgts ]) problems+      forM_ badPairs $ \(src,tgt) -> putStrLn ("    " ++ show src ++ " -> " ++ show tgt)