A simple Data.Map value used in several examples below.

 test_table = M.fromList [ (1, "hello"), (2, "world") ]

This example shows how the 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 withMap function is used to plumb a Data.Map Map into a function that expects a 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 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.

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 lookup; since we already proved that the key is present when we obtained a Key ph k value, 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

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

What if your set of keys can change over time?

If you were to insert a new key into a map, evidence that a key exists is in the old map is no longer equivalent to evidence that a key exists in the new map.

On the other hand, we know that if some key exists in the old map, then key must still exist in the new map. So there should be a way of "upgrading" evidence from the old map to the new. Furthermore, we know that the key we just added must be in the new map.

The inserting function inserts a value into a map and feeds the new map into a continuation, along with the "upgrade" and "new key" data.

 example4 = withMap test_table $ \table -> do
   inserting 3 NEW table $ \(newKey, upgrade, table') -> do
     forM_ (keys table) $ \key -> do
       putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
       putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
     putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)

Output:

 Key 1 maps to hello in the old table.
 Key 1 maps to hello in the new table.
 Key 2 maps to world in the old table.
 Key 2 maps to world in the new table.
 Also, the new table maps Key 3 to NEW

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, []) ]

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 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? withRecMap returns an Either value to represent failure; if a key is missing, then the result will be a value of the form Left problems, where problems is an explanation of where the missing keys are.

 example5 = 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