Copyright | (c) Matt Noonan 2017 |
---|---|
License | BSD-style |
Maintainer | matt.noonan@gmail.com |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Description
Have you ever known that a key could be found in a certain map? Were you tempted to
reach for
or fromJust
to handle the "impossible" case, when you knew that
error
should give lookup
? (and did shifting requirements ever make the impossible
become possible after all?)Just
v
Data.Map.Justified provides a wrapper around Data.Map's
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 Map
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
value.Maybe
See the Tutorial
module for usage examples.
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) -- 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
Motivation: Data.Map and Maybe
values
Maybe
Suppose you have a key-value mapping using Data.Map's type
. 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.Map
k v
In Data.Map, there are two strategies for dealing with absent keys:
- Cause a runtime error (e.g. Data.Map's
when the key is absent)!
- Return a
value (e.g. Data.Map'sMaybe
)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
value, let's ask what returning
Maybe
Maybe v
from
really does for us. By returning
a lookup
:: k -> Map k v -> Maybe vMaybe 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
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 Nothing
function.lookup
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
feels like a burden:
I already know that this key is in the map, why should I have to handle the Maybe
v
case?Nothing
In this situation, it is tempting to reach for the partial function
,
or a pattern match like fromJust
. 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 Nothing
-> error
"The impossible happened!"*** 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
should return a lookup
--- but the compiler doesn't know this!Just
v
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,
will never fail. Your justification
removes the lookup
!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
and Map
types. If you are
able to get your hands on a value of type Key
, then you must have already proven that
the key is present in any value of type Key
ph k
.Map
ph k v
The
type is simply a Key
ph knewtype
wrapper around k
, but the phantom type ph
allows
to represent both a key of type Key
ph kk
and a proof that the key is present in
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
function. In Data.Map, member
has the typemember
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,
has the typeMember
member
::Ord
k => k ->Map
ph k v ->Maybe
(Key
ph k)
Instead of a boolean,
either says "the key is not present"
(member
), 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 Nothing
-free
operations on the map.Maybe
Data.Map.Justified uses the same rank-2 polymorphism trick used in the
monad to
ensure that the ST
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.
- data Map ph k v
- data Key ph k
- theKey :: Key ph k -> k
- theMap :: Map ph k v -> Map k v
- withMap :: Map k v -> (forall ph. Map ph k v -> t) -> t
- withSingleton :: k -> v -> (forall ph. (Key ph k, Map ph k v) -> t) -> t
- data KeyInfo
- type MissingReference k f = (k, f (k, KeyInfo))
- withRecMap :: (Ord k, Traversable f) => Map k (f k) -> (forall ph. Map ph k (f (Key ph k)) -> t) -> Either [MissingReference k f] t
- member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)
- keys :: Map ph k v -> [Key ph k]
- lookupLT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
- lookupLE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
- lookupGT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
- lookupGE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
- lookup :: Ord k => Key ph k -> Map ph k v -> v
- (!) :: Ord k => Map ph k v -> Key ph k -> v
- adjust :: Ord k => (v -> v) -> Key ph k -> Map ph k v -> Map ph k v
- adjustWithKey :: Ord k => (Key ph k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v
- reinsert :: Ord k => Key ph k -> v -> Map ph k v -> Map ph k v
- 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
- 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
- mapWithKey :: (Key ph k -> a -> b) -> Map ph k a -> Map ph k b
- traverseWithKey :: Applicative t => (Key ph k -> a -> t b) -> Map ph k a -> t (Map ph k b)
- mapAccum :: (a -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c)
- mapAccumWithKey :: (a -> Key ph k -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c)
- mappingKeys :: Ord k2 => (k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t
- 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
- 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
- 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
- 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
- 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
- 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
- zip :: Ord k => Map ph k a -> Map ph k b -> Map ph k (a, b)
- zipWith :: Ord k => (a -> b -> c) -> Map ph k a -> Map ph k b -> Map ph k c
- zipWithKey :: Ord k => (Key ph k -> a -> b -> c) -> Map ph k a -> Map ph k b -> Map ph k c
- findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int
- elemAt :: Key ph Int -> Map ph k v -> (Key ph k, v)
- tie :: (Functor f, Ord k) => (f a -> a) -> Map ph k (f (Key ph k)) -> Key ph k -> a
Map and Key types
A Data.Map
wrapper that allows direct lookup of keys that
are known to exist in the map.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
layer.Maybe
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".Map
theKey :: Key ph k -> k Source #
Get a bare key out of a key-plus-evidence by forgetting what map the key can be found in.
Evaluation
withMap :: Map k v -> (forall ph. Map ph k v -> t) -> t Source #
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)
withSingleton :: k -> v -> (forall ph. (Key ph k, Map ph k v) -> t) -> t Source #
Information about whether a key is present or missing.
See
and Data.Map.Justified.Tutorial's withRecMap
.example5
type MissingReference k f = (k, f (k, KeyInfo)) Source #
A description of what key/value-containing-keys pairs failed to be found.
See
and Data.Map.Justified.Tutorial's withRecMap
.example5
withRecMap :: (Ord k, Traversable f) => Map k (f k) -> (forall ph. Map ph k (f (Key ph k)) -> t) -> Either [MissingReference k f] t Source #
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))]
See
for more usage examples.example5
Gathering evidence
member :: Ord k => k -> Map ph k v -> Maybe (Key ph k) Source #
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
),
lookup
requires the evidence up-front. After it is known that a key can be
found, there is no need for Map
types or run-time errors.Maybe
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
keys :: Map ph k v -> [Key ph k] Source #
A list of all of the keys in a map, along with proof that the keys exist within the map.
lookupLT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v) Source #
O(log n). Find the largest key smaller than the given one and return the corresponding (key,value) pair, with evidence for the key.
withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLT 3 table == Nothing withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLT 4 table == Just (Key 3, 'a')
lookupLE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v) Source #
O(log n). Find the largest key smaller than or equal to the given one and return the corresponding (key,value) pair, with evidence for the key.
withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 2 table == Nothing withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 4 table == Just (Key 3, 'a') withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupLE 5 table == Just (Key 5, 'b')
lookupGT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v) Source #
O(log n). Find the smallest key greater than the given one and return the corresponding (key,value) pair, with evidence for the key.
withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGT 4 table == Just (Key 5, 'b') withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGT 5 table == Nothing
lookupGE :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v) Source #
O(log n). Find the smallest key greater than or equal to the given one and return the corresponding (key,value) pair, with evidence for the key.
withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 3 table == Just (Key 3, 'a') withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 4 table == Just (Key 5, 'b') withMap (M.fromList [(3,'a'), (5,'b')]) $ \table -> lookupGE 6 table == Nothing
Lookup and update
lookup :: Ord k => Key ph k -> Map ph k v -> v Source #
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
.
adjust :: Ord k => (v -> v) -> Key ph k -> Map ph k v -> Map ph k v Source #
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 Source #
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.
reinsert :: Ord k => Key ph k -> v -> Map ph k v -> Map ph k v Source #
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.
Inserting new keys
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 Source #
Insert a value for a key that is not known to be in the map, evaluating the updated map with the given continuation.
The continuation is given three things:
- A proof that the inserted key exists in the new map,
- 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
- The updated
, with a different phantom type.Map
withMap (M.fromList [(5,'a'), (3,'b')]) (\table -> inserting 5 'x' table $ \(_,_,table') -> theMap table') == M.fromList [(3, 'b'), (5, 'x')] withMap (M.fromList [(5,'a'), (3,'b')]) (\table -> inserting 7 'x' table $ \(_,_,table') -> theMap table') == M.fromList [(3, 'b'), (5, 'b'), (7, 'x')]
See
for more usage examples.example4
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 Source #
O(log n). Insert with a function, combining new value and old value.
will insert the pair (key, value) into insertingWith
f key value mp contmp
if key does
not exist in the map. If the key does exist, the function will
insert the pair (key, f new_value old_value)
.
The continuation is given three things (as in
):inserting
- A proof that the inserted key exists in the new map,
- 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
- The updated
, with a different phantom type.Map
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")]
Mapping
mapWithKey :: (Key ph k -> a -> b) -> Map ph k a -> Map ph k b Source #
O(n). Map a function over all keys and values in the map.
traverseWithKey :: Applicative t => (Key ph k -> a -> t b) -> Map ph k a -> t (Map ph k b) Source #
O(n). As in
: traverse the map, but give the
traversing function access to the key associated with each value.traverse
mapAccum :: (a -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c) Source #
O(n). The function
threads an accumulating
argument through the map in ascending order of keys.mapAccum
mapAccumWithKey :: (a -> Key ph k -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c) Source #
O(n). The function
threads an accumulating
argument through the map in ascending order of keys.mapAccumWithKey
Mapping keys
mappingKeys :: Ord k2 => (k1 -> k2) -> Map ph k1 v -> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t) -> t Source #
O(n*log n).
evaluates a continuation with the map obtained by applying
mappingKeys
f
to each key of s
.
The size of the resulting map may be smaller if f
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:
- A function that converts evidence that a key belongs to the original map into evidence that a key belongs to the new map.
- The new, possibly-smaller 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 Source #
O(n*log n).
Same as
, but the key-mapping function can make use of
evidence that the input key belongs to the original map.mappingKeys
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 Source #
O(n*log n).
Same as
, 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.mappingKeys
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 Source #
O(n*log n).
Same as
, 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.mappingKnownKeys
Unions
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 Source #
Take the left-biased union of two
s, as in Data.Map's
Map
, evaluating the unioned map with the given continuation.union
The continuation is given three things:
- 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,
- 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
- The updated
, with a different phantom type.Map
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 Source #
is the same as unioningWith
f
, except that unioning
f
is used to
combine values that correspond to keys found 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 Source #
is the same as unioningWithKey
f
, except that unioningWith
ff
also
has access to the key and evidence that it is present in both maps.
Zipping
zip :: Ord k => Map ph k a -> Map ph k b -> Map ph k (a, b) Source #
Zip the values in two maps together. The phantom type ph
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 Source #
Combine the values in two maps together. The phantom type ph
ensures
that the two maps have the same set of keys, so no elements are left out.
zipWithKey :: Ord k => (Key ph k -> a -> b -> c) -> Map ph k a -> Map ph k b -> Map ph k c Source #
Combine the values in two maps together, using the key and values.
The phantom type ph
ensures that the two maps have the same set of
keys.
Indexing
findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int Source #
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
, this function can not fail at runtime.findIndex