-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Keyed container types with type-checked proofs of key presence.
--   
--   This package contains wrappers around standard container types, that
--   provide guarantees about the presence of keys within the container.
@package justified-containers
@version 0.3.0.0


-- | <h1>Description</h1>
--   
--   Have you ever <i>known</i> that a key could be found in a certain map?
--   Were you tempted to reach for <tt><tt>fromJust</tt></tt> or
--   <tt><a>error</a></tt> to handle the "impossible" case, when you knew
--   that <tt><a>lookup</a></tt> should give <tt><a>Just</a> v</tt>? (and
--   did shifting requirements ever make the impossible become possible
--   after all?)
--   
--   <a>Data.Map.Justified</a> provides a zero-cost <tt>newtype</tt>
--   wrapper around <a>Data.Map</a>'s <tt><a>Map</a></tt> that enables you
--   to separate the <i>proof that a key is present</i> from the
--   <i>operations using the key</i>. Once you prove that a key is present,
--   you can use it <tt>Maybe</tt>-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 <tt><a>Maybe</a></tt> value.
--   
--   See the <a>Data.Map.Justified.Tutorial</a> module for usage examples.
--   
--   <h3>Example</h3>
--   
--   <pre>
--   withMap test_table $ \table -&gt; do
--   
--     case member 1 table of
--   
--       Nothing  -&gt; putStrLn "Sorry, I couldn't prove that the key is present."
--   
--       Just key -&gt; do
--   
--         -- 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)
--   
--         -- ...even in certain other maps!
--         let table' = reinsert key "howdy" table
--         putStrLn ("Value for key in updated map: " ++ lookup key table')
--   </pre>
--   
--   Output:
--   
--   <pre>
--   Found key: Key 1
--   Value for key: hello
--   Value for key in updated map: howdy
--   </pre>
--   
--   <h2>Motivation: <a>Data.Map</a> and <tt><a>Maybe</a></tt> values</h2>
--   
--   Suppose you have a key-value mapping using <a>Data.Map</a>'s type
--   <tt><a>Map</a> k v</tt>. Anybody making use of <tt><a>Map</a> k v</tt>
--   to look up or modify a value must take into account the possibility
--   that the given key is not present.
--   
--   In <a>Data.Map</a>, there are two strategies for dealing with absent
--   keys:
--   
--   <ol>
--   <li>Cause a runtime error (e.g. <a>Data.Map</a>'s <tt><a>!</a></tt>
--   when the key is absent)</li>
--   <li>Return a <tt><a>Maybe</a></tt> value (e.g. <a>Data.Map</a>'s
--   <tt><a>lookup</a></tt>)</li>
--   </ol>
--   
--   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 <tt><a>Maybe</a></tt>
--   value, let's ask what returning <tt>Maybe v</tt> from
--   <tt><a>lookup</a> :: k -&gt; Map k v -&gt; Maybe v</tt> really does
--   for us. By returning a <tt>Maybe v</tt> value, <tt>lookup key
--   table</tt> is saying "Your program must account for the possibility
--   that <tt>key</tt> cannot be found in <tt>table</tt>. I will ensure
--   that you account for this possibility by forcing you to handle the
--   <tt><a>Nothing</a></tt> case." In effect, <a>Data.Map</a> is requiring
--   the user to prove they have handled the possibility that a key is
--   absent whenever they use the <tt><a>lookup</a></tt> function.
--   
--   <h2>Laziness (the bad kind)</h2>
--   
--   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
--   <tt><a>Maybe</a> v</tt> feels like a burden: I already <i>know</i>
--   that this key is in the map, why should I have to handle the
--   <tt><a>Nothing</a></tt> case?
--   
--   In this situation, it is tempting to reach for the partial function
--   <tt><a>fromJust</a></tt>, or a pattern match like <tt><a>Nothing</a>
--   -&gt; <a>error</a> "The impossible happened!"</tt>. 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 <tt>*** Exception: Maybe.fromJust: Nothing</tt>)
--   
--   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
--   <tt><a>lookup</a></tt> should return a <tt><a>Just</a> v</tt> --- but
--   the <i>compiler</i> doesn't know this!
--   
--   The idea behind <a>Data.Map.Justified</a> is to encode the
--   programmer's knowledge that a key is present <i>within the type
--   system</i>, where it can be checked at compile-time. Once a key is
--   known to be present, <tt><a>lookup</a></tt> will never fail. Your
--   justification removes the <tt><a>Just</a></tt>!
--   
--   <h2>How it works</h2>
--   
--   Evidence that a key can indeed be found in a map is carried by a
--   phantom type parameter <tt>ph</tt> shared by both the
--   <tt><a>Map</a></tt> and <tt><a>Key</a></tt> types. If you are able to
--   get your hands on a value of type <tt><a>Key</a> ph k</tt>, then you
--   must have already proven that the key is present in <i>any</i> value
--   of type <tt><a>Map</a> ph k v</tt>.
--   
--   The <tt><a>Key</a> ph k</tt> type is simply a <tt>newtype</tt> wrapper
--   around <tt>k</tt>, but the phantom type <tt>ph</tt> allows
--   <tt><a>Key</a> ph k</tt> to represent both <i>a key of type
--   <tt>k</tt></i> <b>and</b> <i>a proof that the key is present in</i>
--   <i>all maps of type <tt><a>Map</a> ph k v</tt></i>.
--   
--   There are several ways to prove that a key belongs to a map, but the
--   simplest is to just use <a>Data.Map.Justified</a>'s
--   <tt><a>member</a></tt> function. In <a>Data.Map</a>,
--   <tt><a>member</a></tt> has the type
--   
--   <pre>
--   <a>member</a> :: <a>Ord</a> k =&gt; k -&gt; <a>Map</a> k v -&gt; <a>Bool</a>
--   </pre>
--   
--   and reports whether or not the key can be found in the map. In
--   <a>Data.Map.Justified</a>, <tt><a>Member</a></tt> has the type
--   
--   <pre>
--   <a>member</a> :: <a>Ord</a> k =&gt; k -&gt; <a>Map</a> ph k v -&gt; <a>Maybe</a> (<a>Key</a> ph k)
--   </pre>
--   
--   Instead of a boolean, <tt><a>member</a></tt> either says "the key is
--   not present" (<tt><a>Nothing</a></tt>), or gives back the same key,
--   <i>augmented with evidence that they key</i> <i>is present</i>. This
--   key-plus-evidence can then be used to do any number of
--   <tt><a>Maybe</a></tt>-free operations on the map.
--   
--   <a>Data.Map.Justified</a> uses the same rank-2 polymorphism trick used
--   in the <tt><a>ST</a></tt> monad to ensure that the <tt>ph</tt> 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.
module Data.Map.Justified

-- | A <a>Data.Map</a> <tt><a>Map</a></tt> 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 <tt><a>Maybe</a></tt> layer.
--   
--   <tt><a>Map</a></tt> 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".
data Map ph k v

-- | A key that knows it can be found in certain <tt><a>Map</a></tt>s.
--   
--   The evidence that the key can be found in a map is carried by the type
--   system via the phantom type parameter <tt>ph</tt>. Certain operations
--   such as lookup will only type-check if the <tt><a>Key</a></tt> and the
--   <tt><a>Map</a></tt> have the same phantom type parameter.
data Key ph k

-- | An index that knows it is valid in certain <tt><a>Map</a></tt>s.
--   
--   The evidence that the index is valid for a map is carried by the type
--   system via the phantom type parameter <tt>ph</tt>. Indexing operations
--   such as <a>elemAt</a> will only type-check if the
--   <tt><a>Index</a></tt> and the <tt><a>Map</a></tt> have the same
--   phantom type parameter.
data Index ph

-- | Get the underlying <a>Data.Map</a> <tt><a>Map</a></tt> out of a
--   <tt><a>Map</a></tt>.
theMap :: Map ph k v -> Map k v

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

-- | Get a bare index out of an index-plus-evidence by forgetting what map
--   the index is valid for.
theIndex :: Index ph -> Int

-- | Evaluate an expression using justified key lookups into the given map.
--   
--   <pre>
--   import qualified Data.Map as M
--   
--   withMap (M.fromList [(1,"A"), (2,"B")]) $ \m -&gt; do
--   
--     -- prints "Found Key 1 with value A"
--     case member 1 m of
--       Nothing -&gt; putStrLn "Missing key 1."
--       Just k  -&gt; putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)
--   
--     -- prints "Missing key 3."
--     case member 3 m of
--       Nothing -&gt; putStrLn "Missing key 3."
--       Just k  -&gt; putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)
--   </pre>
withMap :: Map k v -> (forall ph. Map ph k v -> t) -> t

-- | Like <tt><a>withMap</a></tt>, but begin with a singleton map taking
--   <tt>k</tt> to <tt>v</tt>.
--   
--   The continuation is passed a pair consisting of:
--   
--   <ol>
--   <li>Evidence that <tt>k</tt> is in the map, and</li>
--   <li>The singleton map itself, of type <tt><a>Map</a> ph k v</tt>.</li>
--   </ol>
--   
--   <pre>
--   withSingleton 1 'a' (uncurry lookup) == 'a'
--   </pre>
withSingleton :: k -> v -> (forall ph. (Key ph k, Map ph k v) -> t) -> t

-- | Information about whether a key is present or missing. See
--   <tt><a>withRecMap</a></tt> and <a>Data.Map.Justified.Tutorial</a>'s
--   <tt><a>example5</a></tt>.
data KeyInfo
Present :: KeyInfo
Missing :: KeyInfo

-- | A description of what key/value-containing-keys pairs failed to be
--   found. See <tt><a>withRecMap</a></tt> and
--   <a>Data.Map.Justified.Tutorial</a>'s <tt><a>example5</a></tt>.
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.
--   
--   <pre>
--   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))]
--   </pre>
--   
--   See <tt><a>example5</a></tt> for more usage examples.
withRecMap :: forall k f t. (Ord k, Traversable f, Representational f) => Map k (f k) -> (forall ph. Map ph k (f (Key ph k)) -> t) -> Either [MissingReference k f] t

-- | <i>O(log n)</i>. Obtain evidence that the key is a member of the map.
--   
--   Where <a>Data.Map</a> generally requires evidence that a key exists in
--   a map at every use of some functions (e.g. <a>Data.Map</a>'s
--   <tt><a>lookup</a></tt>), <tt><a>Map</a></tt> requires the evidence
--   up-front. After it is known that a key can be found, there is no need
--   for <tt><a>Maybe</a></tt> types or run-time errors.
--   
--   The <tt>Maybe value</tt> that has to be checked at every lookup in
--   <a>Data.Map</a> is then shifted to a <tt>Maybe (Key ph k)</tt> 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.
--   
--   <pre>
--   withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 1) == False
--   withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 5) == True
--   </pre>
member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)

-- | 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]

-- | <i>O(log n)</i>. Lookup the value at a key that is <i>not</i> already
--   known to be in the map. Return <tt>Just</tt> the value <i>and</i> the
--   key-with-evidence if the key was present, or <tt>Nothing</tt>
--   otherwise.
lookupMay :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

-- | <i>O(log n)</i>. Find the largest key smaller than the given one and
--   return the corresponding (key,value) pair, with evidence for the key.
--   
--   <pre>
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupLT 3 table == Nothing
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupLT 4 table == Just (Key 3, 'a')
--   </pre>
lookupLT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

-- | <i>O(log n)</i>. Find the largest key smaller than or equal to the
--   given one and return the corresponding (key,value) pair, with evidence
--   for the key.
--   
--   <pre>
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupLE 2 table == Nothing
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupLE 4 table == Just (Key 3, 'a')
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupLE 5 table == Just (Key 5, 'b')
--   </pre>
lookupLE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

-- | <i>O(log n)</i>. Find the smallest key greater than the given one and
--   return the corresponding (key,value) pair, with evidence for the key.
--   
--   <pre>
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupGT 4 table == Just (Key 5, 'b')
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupGT 5 table == Nothing
--   </pre>
lookupGT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

-- | <i>O(log n)</i>. Find the smallest key greater than or equal to the
--   given one and return the corresponding (key,value) pair, with evidence
--   for the key.
--   
--   <pre>
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupGE 3 table == Just (Key 3, 'a')
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupGE 4 table == Just (Key 5, 'b')
--   withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -&gt; lookupGE 6 table == Nothing
--   </pre>
lookupGE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

-- | <i>O(log n)</i>. Lookup the value at a key, known to be in the map.
--   
--   The result is a <tt>v</tt> rather than a <tt>Maybe v</tt>, because the
--   proof obligation that the key is in the map must already have been
--   discharged to obtain a value of type <tt>Key ph k</tt>.
lookup :: Ord k => Key ph k -> Map ph k v -> v

-- | <i>O(log n)</i>. Find the value at a key. Unlike <a>Data.Map</a>'s
--   <tt><a>!</a></tt>, this function is total and can not fail at runtime.
(!) :: Ord k => Map ph k v -> Key ph k -> v

-- | 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 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 => (Key ph k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v

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

-- | <i>O(n)</i>. Map a function over all keys and values in the map.
mapWithKey :: (Key ph k -> a -> b) -> Map ph k a -> Map ph k b

-- | <i>O(n)</i>. As in <tt><a>traverse</a></tt>: traverse the map, but
--   give the traversing function access to the key associated with each
--   value.
traverseWithKey :: Applicative t => (Key ph k -> a -> t b) -> Map ph k a -> t (Map ph k b)

-- | <i>O(n)</i>. The function <tt><a>mapAccum</a></tt> threads an
--   accumulating argument through the map in ascending order of keys.
mapAccum :: (a -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c)

-- | <i>O(n)</i>. The function <tt><a>mapAccumWithKey</a></tt> threads an
--   accumulating argument through the map in ascending order of keys.
mapAccumWithKey :: (a -> Key ph k -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c)

-- | Zip the values in two maps together. The phantom type <tt>ph</tt>
--   ensures that the two maps have the same set of keys, so no elements
--   are left out.
zip :: Ord k => Map ph k a -> Map ph k b -> Map ph k (a, b)

-- | Combine the values in two maps together. The phantom type <tt>ph</tt>
--   ensures that the two maps have the same set of keys, so no elements
--   are left out.
zipWith :: Ord k => (a -> b -> c) -> Map ph k a -> Map ph k b -> Map ph k c

-- | Combine the values in two maps together, using the key and values. The
--   phantom type <tt>ph</tt> ensures that the two maps have the same set
--   of keys.
zipWithKey :: Ord k => (Key ph k -> a -> b -> c) -> Map ph k a -> Map ph k b -> Map ph k c

-- | Insert a value for a key that is <i>not</i> known to be in the map,
--   evaluating the updated map with the given continuation.
--   
--   The continuation is given three things:
--   
--   <ol>
--   <li>A proof that the inserted key exists in the new map,</li>
--   <li>A function that can be used to convert evidence that a key exists
--   in the original map, to evidence that the key exists in the updated
--   map, and</li>
--   <li>The updated <tt><a>Map</a></tt>, with a <i>different phantom
--   type</i>.</li>
--   </ol>
--   
--   <pre>
--   withMap (M.fromList [(5,'a'), (3,'b')]) (\table -&gt; inserting 5 'x' table $ \(_,_,table') -&gt; theMap table') == M.fromList [(3, 'b'), (5, 'x')]
--   withMap (M.fromList [(5,'a'), (3,'b')]) (\table -&gt; inserting 7 'x' table $ \(_,_,table') -&gt; theMap table') == M.fromList [(3, 'b'), (5, 'b'), (7, 'x')]
--   </pre>
--   
--   See <tt><a>example4</a></tt> for more usage examples.
inserting :: Ord k => k -> v -> Map ph k v -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t) -> t

-- | <i>O(log n)</i>. Insert with a function, combining new value and old
--   value. <tt><a>insertingWith</a> f key value mp cont</tt> will insert
--   the pair (key, value) into <tt>mp</tt> if key does not exist in the
--   map. If the key <i>does</i> exist, the function will insert the pair
--   <tt>(key, f new_value old_value)</tt>.
--   
--   The continuation is given three things (as in
--   <tt><a>inserting</a></tt>):
--   
--   <ol>
--   <li>A proof that the inserted key exists in the new map,</li>
--   <li>A function that can be used to convert evidence that a key exists
--   in the original map, to evidence that the key exists in the updated
--   map, and</li>
--   <li>The updated <tt><a>Map</a></tt>, with a <i>different phantom
--   type</i>.</li>
--   </ol>
--   
--   <pre>
--   withMap (M.fromList [(5,"a"), (3,"b")]) (theMap . insertingWith (++) 5) == M.fromList [(3,"b"), (5,"xxxa")]
--   withMap (M.fromList [(5,"a"), (3,"b")]) (theMap . insertingWith (++) 7) == M.fromList [(3,"b"), (5,"a"), (7,"xxx")]
--   </pre>
insertingWith :: Ord k => (v -> v -> v) -> k -> v -> Map ph k v -> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t) -> t

-- | Take the left-biased union of two <tt><a>Map</a></tt>s, as in
--   <a>Data.Map</a>'s <tt><a>union</a></tt>, evaluating the unioned map
--   with the given continuation.
--   
--   The continuation is given three things:
--   
--   <ol>
--   <li>A function that can be used to convert evidence that a key exists
--   in the left map to evidence that the key exists in the union,</li>
--   <li>A function that can be used to convert evidence that a key exists
--   in the right map to evidence that the key exists in the union,
--   and</li>
--   <li>The updated <tt><a>Map</a></tt>, with a <i>different phantom
--   type</i>.</li>
--   </ol>
unioning :: Ord k => Map phL k v -> Map phR k v -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -> t

-- | <tt><a>unioningWith</a> f</tt> is the same as
--   <tt><a>unioning</a></tt>, except that <tt>f</tt> is used to combine
--   values that correspond to keys found in both maps.
unioningWith :: Ord k => (v -> v -> v) -> Map phL k v -> Map phR k v -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -> t

-- | <tt><a>unioningWithKey</a> f</tt> is the same as
--   <tt><a>unioningWith</a> f</tt>, except that <tt>f</tt> also has access
--   to the key and evidence that it is present in both maps.
unioningWithKey :: Ord k => (Key phL k -> Key phR k -> v -> v -> v) -> Map phL k v -> Map phR k v -> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t) -> t

-- | <i>O(log n)</i>. Delete a key and its value from the map.
--   
--   The continuation is given two things:
--   
--   <ol>
--   <li>A function that can be used to convert evidence that a key exists
--   in the <i>updated</i> map, to evidence that the key exists in the
--   <i>original</i> map. (contrast with <a>inserting</a>)</li>
--   <li>The updated map itself.</li>
--   </ol>
deleting :: Ord k => k -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t

-- | <i>O(log n)</i>. Difference of two maps. Return elements of the first
--   map not existing in the second map.
--   
--   The continuation is given two things:
--   
--   <ol>
--   <li>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.</li>
--   <li>The updated map itself.</li>
--   </ol>
subtracting :: Ord k => Map phL k a -> Map phR k b -> (forall ph'. (Key ph' k -> Key phL k, Map ph' k a) -> t) -> t

-- | Keep only the keys and associated values in a map that satisfy the
--   predicate.
--   
--   The continuation is given two things:
--   
--   <ol>
--   <li>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</li>
--   <li>The filtered map itself, with a new phantom type parameter.</li>
--   </ol>
filtering :: (v -> Bool) -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t

-- | As <a>filtering</a>, except the filtering function also has access to
--   the key and existence evidence.
filteringWithKey :: (Key ph k -> v -> Bool) -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t

-- | Take the left-biased intersections of two <tt><a>Map</a></tt>s, as in
--   <a>Data.Map</a>'s <tt><a>intersection</a></tt>, evaluating the
--   intersection map with the given continuation.
--   
--   The continuation is given two things:
--   
--   <ol>
--   <li>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</li>
--   <li>The updated <tt><a>Map</a></tt>, with a <i>different phantom
--   type</i>.</li>
--   </ol>
intersecting :: Ord k => Map phL k a -> Map phR k b -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k a) -> t) -> t

-- | As <tt><a>intersecting</a></tt>, but uses the combining function to
--   merge mapped values on the intersection.
intersectingWith :: Ord k => (a -> b -> c) -> Map phL k a -> Map phR k b -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t) -> t

-- | As <tt><a>intersectingWith</a></tt>, but the combining function has
--   access to the map keys.
intersectingWithKey :: Ord k => (Key phL k -> Key phR k -> a -> b -> c) -> Map phL k a -> Map phR k b -> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t) -> t

-- | <i>O(n*log n)</i>. <tt><a>mappingKeys</a></tt> evaluates a
--   continuation with the map obtained by applying <tt>f</tt> to each key
--   of <tt>s</tt>.
--   
--   The size of the resulting map may be smaller if <tt>f</tt> maps two or
--   more distinct keys to the same new key. In this case the value at the
--   greatest of the original keys is retained.
--   
--   The continuation is passed two things:
--   
--   <ol>
--   <li>A function that converts evidence that a key belongs to the
--   original map into evidence that a key belongs to the new map.</li>
--   <li>The new, possibly-smaller map.</li>
--   </ol>
mappingKeys :: Ord k2 => (k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t

-- | <i>O(n*log n)</i>. Same as <tt><a>mappingKeys</a></tt>, but the
--   key-mapping function can make use of evidence that the input key
--   belongs to the original map.
mappingKnownKeys :: Ord k2 => (Key ph k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t

-- | <i>O(n*log n)</i>. Same as <tt><a>mappingKeys</a></tt>, except a
--   function is used to combine values when two or more keys from the
--   original map correspond to the same key in the final map.
mappingKeysWith :: Ord k2 => (v -> v -> v) -> (k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t

-- | <i>O(n*log n)</i>. Same as <tt><a>mappingKnownKeys</a></tt>, except a
--   function is used to combine values when two or more keys from the
--   original map correspond to the same key in the final map.
mappingKnownKeysWith :: Ord k2 => (v -> v -> v) -> (Key ph k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t

-- | <i>O(log n)</i>. Return the <i>index</i> of a key, which is its
--   zero-based index in the sequence sorted by keys. The index is a number
--   from <i>0</i> up to, but not including, the size of the map. The index
--   also carries a proof that it is valid for the map.
--   
--   Unlike <a>Data.Map</a>'s <tt><a>findIndex</a></tt>, this function can
--   not fail at runtime.
findIndex :: Ord k => Key ph k -> Map ph k a -> Index ph

-- | <i>O(log n)</i>. Retrieve an element by its <i>index</i>, i.e. by its
--   zero-based index in the sequence sorted by keys.
--   
--   Unlike <a>Data.Map</a>'s <tt><a>elemAt</a></tt>, this function can not
--   fail at runtime.
elemAt :: Index ph -> Map ph k v -> (Key ph k, v)

-- | 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
instance GHC.Classes.Ord Data.Map.Justified.KeyInfo
instance GHC.Classes.Eq Data.Map.Justified.KeyInfo
instance GHC.Show.Show Data.Map.Justified.KeyInfo
instance GHC.Show.Show (Data.Map.Justified.Index ph)
instance GHC.Classes.Ord (Data.Map.Justified.Index ph)
instance GHC.Classes.Eq (Data.Map.Justified.Index ph)
instance GHC.Show.Show k => GHC.Show.Show (Data.Map.Justified.Key ph k)
instance GHC.Classes.Ord k => GHC.Classes.Ord (Data.Map.Justified.Key ph k)
instance GHC.Classes.Eq k => GHC.Classes.Eq (Data.Map.Justified.Key ph k)
instance Data.Traversable.Traversable (Data.Map.Justified.Map ph k)
instance Data.Foldable.Foldable (Data.Map.Justified.Map ph k)
instance GHC.Base.Functor (Data.Map.Justified.Map ph k)
instance (GHC.Show.Show k, GHC.Show.Show v) => GHC.Show.Show (Data.Map.Justified.Map ph k v)
instance (GHC.Classes.Ord k, GHC.Classes.Ord v) => GHC.Classes.Ord (Data.Map.Justified.Map ph k v)
instance (GHC.Classes.Eq k, GHC.Classes.Eq v) => GHC.Classes.Eq (Data.Map.Justified.Map ph k v)


-- | <h1>Description</h1>
--   
--   The examples below demonstrate how to use the types and functions in
--   <a>Data.Map.Justified</a>.
--   
--   You should be able to simply load this module in <tt>ghci</tt> to play
--   along. The import list is:
--   
--   <pre>
--   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_)
--   </pre>
module Data.Map.Justified.Tutorial

-- | A simple <a>Data.Map</a> value used in several examples below.
--   
--   <pre>
--   test_table = M.fromList [ (1, "hello"), (2, "world") ]
--   </pre>
test_table :: Map Int String

-- | This example shows how the <tt><a>member</a></tt> 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 <a>Data.Map</a> may use a <tt><a>Maybe</a></tt> type to ensure
--   that the user handles missing keys when performing a lookup, here we
--   use the <tt><a>Maybe</a></tt> type to either tell the user that a key
--   is missing (by returning <tt><a>Nothing</a></tt>), or actually give
--   back evidence of the key's presence (by returning <tt>Just
--   known_key</tt>)
--   
--   The <tt><a>withMap</a></tt> function is used to plumb a
--   <a>Data.Map</a> <tt><a>Map</a></tt> into a function that expects a
--   <a>Data.Map.Justified</a> <tt><a>Map</a></tt>. In the code below, you
--   can think of <tt>table</tt> as <tt>test_table</tt>, enhanced with the
--   ability to use verified keys.
--   
--   You can get from <tt>table</tt> back to <tt>test_table</tt> using the
--   function <tt><a>theMap</a></tt>.
--   
--   <pre>
--   example1 = withMap test_table $ \table -&gt; do
--   
--     putStrLn "Is 1 a valid key?"
--     case member 1 table of
--       Nothing  -&gt; putStrLn "  No, it was not found."
--       Just key -&gt; putStrLn $ "  Yes, found key: " ++ show key
--   
--     putStrLn "Is 5 a valid key?"
--     case member 5 table of
--       Nothing  -&gt; putStrLn "  No, it was not found."
--       Just key -&gt; putStrLn $ "  Yes, found key: " ++ show key
--   </pre>
--   
--   Output:
--   
--   <pre>
--   Is 1 a valid key?
--     Yes, found key: Key 1
--   Is 5 a valid key?
--     No, it was not found.
--   </pre>
example1 :: IO ()

-- | Once you have obtained a verified key, how do you use it?
--   
--   <a>Data.Map.Justified</a> has several functions that are similar to
--   ones found in <a>Data.Map</a> that operate over verified keys. In this
--   example, notice that we can extract values directly from the map using
--   <tt><a>lookup</a></tt>; since we already proved that the key is
--   present when we obtained a <tt>Key ph k</tt> value,
--   <tt><a>lookup</a></tt> does not need to return a <tt><a>Maybe</a></tt>
--   value.
--   
--   <pre>
--   example2 = withMap test_table $ \table -&gt; do
--   
--     case member 1 table of
--       Nothing  -&gt; putStrLn "Sorry, I couldn't prove that the key is present."
--       Just key -&gt; 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')
--   </pre>
--   
--   Output:
--   
--   <pre>
--   Found key: Key 1
--   Value for key: hello
--   Value for key in updated map: howdy
--   </pre>
example2 :: IO ()

-- | It is a bit surprising to realize that a key of type <tt>Key ph k</tt>
--   can be used to safely look up values in <i>any</i> map of type <tt>Map
--   ph k v</tt>, 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 <i>different</i> (but related) tables, using the same
--   key evidence.
--   
--   <pre>
--   example3 = withMap test_table $ \table -&gt; do
--   
--     let uppercase = map toUpper
--         updated_table = fmap (reverse . uppercase) table
--     
--     for (keys table) $ \key -&gt; 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 ()
--   </pre>
--   
--   Output:
--   
--   <pre>
--   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
--   </pre>
example3 :: IO ()

-- | 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 <tt>key</tt> exists in the old
--   map, then <tt>key</tt> 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 <tt><a>inserting</a></tt> function inserts a value into a map and
--   feeds the new map into a continuation, along with the "upgrade" and
--   "new key" data.
--   
--   <pre>
--   example4 = withMap test_table $ \table -&gt; do
--     inserting 3 <a>NEW</a> table $ \(newKey, upgrade, table') -&gt; do
--       forM_ (keys table) $ \key -&gt; 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)
--   </pre>
--   
--   Output:
--   
--   <pre>
--   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
--   </pre>
example4 :: IO ()

-- | The next example uses a directed graph, defined by this adjacency
--   list.
--   
--   <pre>
--   adjacencies = M.fromList [ (1, [2,3]), (2, [1,5,3]), (3, [4]), (4, [3, 1]), (5, []) ]
--   </pre>
adjacencies :: Map Int [Int]

-- | 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
--   
--   <pre>
--   type Digraphy node = M.Map node [node]
--   </pre>
--   
--   If you want to do a computation with a <tt>Digraphy node</tt>, you
--   probably want each of the neighbor nodes to have keys in the
--   <tt>Digraphy node</tt> map. That is, you may really want
--   
--   <pre>
--   type Digraph ph node = Map ph node [Key ph node]
--                              /\           /\
--                              |            |
--                              +-----+------+
--                                    |
--    (each neighbor should carry a proof that they are also in the map)
--   </pre>
--   
--   You can do this via <tt><a>withRecMap</a></tt>, which converts each
--   key reference of type <tt>k</tt> in your map to a verified key of type
--   <tt><a>Key</a> ph k</tt>.
--   
--   But what if a referenced key really is missing from the map?
--   <tt><a>withRecMap</a></tt> returns an <tt><a>Either</a></tt> value to
--   represent failure; if a key is missing, then the result will be a
--   value of the form <tt><a>Left</a> problems</tt>, where
--   <tt>problems</tt> is an explanation of where the missing keys are.
--   
--   <pre>
--   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) -&gt; [ (src,tgt) | (tgt, Missing) &lt;- tgts ]) problems
--         forM_ badPairs $ \(src,tgt) -&gt; putStrLn ("    " ++ show src ++ " -&gt; " ++ show tgt)
--   </pre>
--   
--   Output:
--   
--   <pre>
--   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 -&gt; 6
--   </pre>
example5 :: IO ()
