Data.Map.Justified

Description

Have you ever known that a key could be found in a certain map? Were you tempted to reach for fromJust or error to handle the "impossible" case, when you knew that lookup should give Just v? (and did shifting requirements ever make the impossible become possible after all?)

Data.Map.Justified provides a zero-cost newtype wrapper around Data.Map's Map that enables you to separate the proof that a key is present from the operations using the key. Once you prove that a key is present, you can use it Maybe-free in any number of other operations -- sometimes even operations on other maps!

None of the functions in this module can cause a run-time error, and very few of the operations return a Maybe value.

See the Data.Map.Justified.Tutorial module for usage examples.

Example

 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

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

Output:

 Found key: Key 1
 Value for key: hello
 Value for key in updated map: howdy

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 ! when the key is absent)
2. Return a Maybe value (e.g. Data.Map's lookup)

The first option introduces partial functions, so is not very palatable. But what is wrong with the second option?

To understand the problem with returning a Maybe value, 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 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 have to handle the Nothing case?

In this situation, it is tempting to reach for the partial function fromJust, or a pattern match like Nothing -> error "The impossible happened!". But as parts of the program are changed over time, you may find the impossible has become possible after all (or perhaps 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 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, 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 Map and 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 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 member function. In 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, Member has the type

member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)

Instead of a boolean, 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.

Map and Key types

data Map ph k v

A 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".

Instances

Functor (Map ph k)

Methods

fmap :: (a -> b) -> Map ph k a -> Map ph k b

(<$) :: a -> Map ph k b -> Map ph k a

Foldable (Map ph k)

Methods

fold :: Monoid m => Map ph k m -> m

foldMap :: Monoid m => (a -> m) -> Map ph k a -> m

foldr :: (a -> b -> b) -> b -> Map ph k a -> b

foldr' :: (a -> b -> b) -> b -> Map ph k a -> b

foldl :: (b -> a -> b) -> b -> Map ph k a -> b

foldl' :: (b -> a -> b) -> b -> Map ph k a -> b

foldr1 :: (a -> a -> a) -> Map ph k a -> a

foldl1 :: (a -> a -> a) -> Map ph k a -> a

toList :: Map ph k a -> [a]

null :: Map ph k a -> Bool

length :: Map ph k a -> Int

elem :: Eq a => a -> Map ph k a -> Bool

maximum :: Ord a => Map ph k a -> a

minimum :: Ord a => Map ph k a -> a

sum :: Num a => Map ph k a -> a

product :: Num a => Map ph k a -> a

Traversable (Map ph k)

Methods

traverse :: Applicative f => (a -> f b) -> Map ph k a -> f (Map ph k b)

sequenceA :: Applicative f => Map ph k (f a) -> f (Map ph k a)

mapM :: Monad m => (a -> m b) -> Map ph k a -> m (Map ph k b)

sequence :: Monad m => Map ph k (m a) -> m (Map ph k a)

(Eq v, Eq k) => Eq (Map ph k v)

Methods

(==) :: Map ph k v -> Map ph k v -> Bool

(/=) :: Map ph k v -> Map ph k v -> Bool

(Ord v, Ord k) => Ord (Map ph k v)

Methods

compare :: Map ph k v -> Map ph k v -> Ordering

(<) :: Map ph k v -> Map ph k v -> Bool

(<=) :: Map ph k v -> Map ph k v -> Bool

(>) :: Map ph k v -> Map ph k v -> Bool

(>=) :: Map ph k v -> Map ph k v -> Bool

max :: Map ph k v -> Map ph k v -> Map ph k v

min :: Map ph k v -> Map ph k v -> Map ph k v

(Show v, Show k) => Show (Map ph k v)

Methods

showsPrec :: Int -> Map ph k v -> ShowS

show :: Map ph k v -> String

showList :: [Map ph k v] -> ShowS

data Key ph k

A key that knows it can be found in certain Maps.

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.

Instances

Eq k => Eq (Key ph k)

Methods

(==) :: Key ph k -> Key ph k -> Bool

(/=) :: Key ph k -> Key ph k -> Bool

Ord k => Ord (Key ph k)

Methods

compare :: Key ph k -> Key ph k -> Ordering

(<) :: Key ph k -> Key ph k -> Bool

(<=) :: Key ph k -> Key ph k -> Bool

(>) :: Key ph k -> Key ph k -> Bool

(>=) :: Key ph k -> Key ph k -> Bool

max :: Key ph k -> Key ph k -> Key ph k

min :: Key ph k -> Key ph k -> Key ph k

Show k => Show (Key ph k)

Methods

showsPrec :: Int -> Key ph k -> ShowS

show :: Key ph k -> String

showList :: [Key ph k] -> ShowS

data Index ph

An index that knows it is valid in certain Maps.

The evidence that the index is valid for a map is carried by the type system via the phantom type parameter ph. Indexing operations such as elemAt will only type-check if the Index and the Map have the same phantom type parameter.

Instances

Eq (Index ph)

Methods

(==) :: Index ph -> Index ph -> Bool

(/=) :: Index ph -> Index ph -> Bool

Ord (Index ph)

Methods

compare :: Index ph -> Index ph -> Ordering

(<) :: Index ph -> Index ph -> Bool

(<=) :: Index ph -> Index ph -> Bool

(>) :: Index ph -> Index ph -> Bool

(>=) :: Index ph -> Index ph -> Bool

max :: Index ph -> Index ph -> Index ph

min :: Index ph -> Index ph -> Index ph

Show (Index ph)

Methods

showsPrec :: Int -> Index ph -> ShowS

show :: Index ph -> String

showList :: [Index ph] -> ShowS

theMap :: Map ph k v -> Map k v

Get the underlying Data.Map Map out of a Map.

theKey :: Key ph k -> k

Get a bare key out of a key-plus-evidence by forgetting what map the key can be found in.

theIndex :: Index ph -> Int

Get a bare index out of an index-plus-evidence by forgetting what map the index is valid for.

Evaluation

withMap

Arguments

:: Map k v

The map to use as input

-> (forall ph. Map ph k v -> t)

The computation to apply

-> t

The resulting value

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

Like withMap, but begin with a singleton map taking k to v.

The continuation is passed a pair consisting of:

1. Evidence that k is in the map, and
2. The singleton map itself, of type Map ph k v.

withSingleton 1 'a' (uncurry lookup) == 'a'

data KeyInfo

Information about whether a key is present or missing. See withRecMap and Data.Map.Justified.Tutorial's example5.

Constructors

Present

Missing

Instances

Eq KeyInfo

Methods

(==) :: KeyInfo -> KeyInfo -> Bool

(/=) :: KeyInfo -> KeyInfo -> Bool

Ord KeyInfo

Methods

compare :: KeyInfo -> KeyInfo -> Ordering

(<) :: KeyInfo -> KeyInfo -> Bool

(<=) :: KeyInfo -> KeyInfo -> Bool

(>) :: KeyInfo -> KeyInfo -> Bool

(>=) :: KeyInfo -> KeyInfo -> Bool

max :: KeyInfo -> KeyInfo -> KeyInfo

min :: KeyInfo -> KeyInfo -> KeyInfo

Show KeyInfo

Methods

showsPrec :: Int -> KeyInfo -> ShowS

show :: KeyInfo -> String

showList :: [KeyInfo] -> ShowS

type MissingReference k f = (k, f (k, KeyInfo))

A description of what key/value-containing-keys pairs failed to be found. See withRecMap and Data.Map.Justified.Tutorial's example5.

withRecMap

Arguments

:: (Ord k, Traversable f, Representational f)

=> Map k (f k)

A map with key references

-> (forall ph. Map ph k (f (Key ph k)) -> t)

The checked continuation

-> Either [MissingReference k f] t

Resulting value, or failure report.

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 example5 for more usage examples.

Gathering evidence

member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)

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

keys :: Map ph k v -> [Key ph k]

A list of all of the keys in a map, along with proof that the keys exist within the map.

lookupMay :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

O(log n). Lookup the value at a key that is not already known to be in the map. Return Just the value and the key-with-evidence if the key was present, or Nothing otherwise.

lookupLT :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)

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)

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)

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)

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

Safe lookup

lookup :: Ord k => Key ph k -> Map ph k v -> v

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.

(!) :: Ord k => Map ph k v -> Key ph k -> v

O(log n). Find the value at a key. Unlike Data.Map's !, this function is total and can not fail at runtime.

Preserving key sets

Localized updates

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

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

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.

Mapping values

mapWithKey :: (Key ph k -> a -> b) -> Map ph k a -> Map ph k b

O(n). Map a function over all keys and values in the map.

traverseWithKey

Arguments

:: Applicative t

=> (Key ph k -> a -> t b)

traversal function

-> Map ph k a

the map to traverse

-> t (Map ph k b)

O(n). As in traverse: traverse the map, but give the traversing function access to the key associated with each value.

mapAccum :: (a -> b -> (a, c)) -> a -> Map ph k b -> (a, Map ph k c)

O(n). The function mapAccum 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)

O(n). The function mapAccumWithKey threads an accumulating argument through the map in ascending order of keys.

Zipping

zip :: Ord k => Map ph k a -> Map ph k b -> Map ph k (a, b)

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

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

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.

Enlarging key sets

Inserting new keys

inserting

Arguments

:: Ord k

=> k

key to insert at

-> v

value to insert

-> Map ph k v

initial map

-> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t)

continuation

-> t

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:

1. A proof that the inserted key exists in the new map,
2. 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
3. The updated Map, with a different phantom type.

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 example4 for more usage examples.

insertingWith

Arguments

:: Ord k

=> (v -> v -> v)

combining function for existing keys

-> k

key to insert at

-> v

value to insert

-> Map ph k v

initial map

-> (forall ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v) -> t)

continuation

-> t

O(log n). Insert with a function, combining new value and old value. insertingWith f key value mp cont will insert the pair (key, value) into mp 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):

1. A proof that the inserted key exists in the new map,
2. 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
3. The updated Map, with a different phantom type.

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

Unions

unioning

Arguments

:: Ord k

=> Map phL k v

left-hand map

-> Map phR k v

right-hand map

-> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)

continuation

-> t

Take the left-biased union of two Maps, as in Data.Map's union, evaluating the unioned map with the given continuation.

The continuation is given three things:

1. 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,
2. 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
3. The updated Map, with a different phantom type.

unioningWith

Arguments

:: Ord k

=> (v -> v -> v)

combining function for intersection

-> Map phL k v

left-hand map

-> Map phR k v

right-hand map

-> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)

continuation

-> t

unioningWith f is the same as unioning, except that f is used to combine values that correspond to keys found in both maps.

unioningWithKey

Arguments

:: Ord k

=> (Key phL k -> Key phR k -> v -> v -> v)

combining function for intersection, using key evidence

-> Map phL k v

left-hand map

-> Map phR k v

right-hand map

-> (forall ph'. (Key phL k -> Key ph' k, Key phR k -> Key ph' k, Map ph' k v) -> t)

continuation

-> t

unioningWithKey f is the same as unioningWith f, except that f also has access to the key and evidence that it is present in both maps.

Reducing key sets

Removing keys

deleting

Arguments

:: Ord k

=> k

key to remove

-> Map ph k v

initial map

-> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t)

continuation

-> t

O(log n). Delete a key and its value from the map.

The continuation is given two things:

1. A function that can be used to convert evidence that a key exists in the updated map, to evidence that the key exists in the original map. (contrast with inserting)
2. The updated map itself.

subtracting

Arguments

:: Ord k

=> Map phL k a

the left-hand map

-> Map phR k b

the right-hand map

-> (forall ph'. (Key ph' k -> Key phL k, Map ph' k a) -> t)

continuation

-> t

O(log n). Difference of two maps. Return elements of the first map not existing in the second map.

The continuation is given two things:

1. A function that can be used to convert evidence that a key exists in the difference, to evidence that the key exists in the original left-hand map.
2. The updated map itself.

Filtering

filtering

Arguments

:: (v -> Bool)

predicate on values

-> Map ph k v

original map

-> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t)

continuation

-> t

Keep only the keys and associated values in a map that satisfy the predicate.

The continuation is given two things:

1. A function that converts evidence that a key is present in the filtered map into evidence that the key is present in the original map, and
2. The filtered map itself, with a new phantom type parameter.

filteringWithKey

Arguments

:: (Key ph k -> v -> Bool)

predicate on keys and values

-> Map ph k v

original map

-> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t)

continuation

-> t

As filtering, except the filtering function also has access to the key and existence evidence.

Intersections

intersecting

Arguments

:: Ord k

=> Map phL k a

left-hand map

-> Map phR k b

right-hand map

-> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k a) -> t)

continuation

-> t

Take the left-biased intersections of two Maps, as in Data.Map's intersection, evaluating the intersection map with the given continuation.

The continuation is given two things:

1. A function that can be used to convert evidence that a key exists in the intersection to evidence that the key exists in each original map, and
2. The updated Map, with a different phantom type.

intersectingWith

Arguments

:: Ord k

=> (a -> b -> c)

combining function

-> Map phL k a

left-hand map

-> Map phR k b

right-hand map

-> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t)

continuation

-> t

As intersecting, but uses the combining function to merge mapped values on the intersection.

intersectingWithKey

Arguments

:: Ord k

=> (Key phL k -> Key phR k -> a -> b -> c)

combining function

-> Map phL k a

left-hand map

-> Map phR k b

right-hand map

-> (forall ph'. (Key ph' k -> (Key phL k, Key phR k), Map ph' k c) -> t)

continuation

-> t

As intersectingWith, but the combining function has access to the map keys.

Mapping key sets

mappingKeys

Arguments

:: Ord k2

=> (k1 -> k2)

key-mapping function

-> Map ph k1 v

initial map

-> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)

continuation

-> t

O(n*log n). mappingKeys evaluates a continuation with the map obtained by applying 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:

1. A function that converts evidence that a key belongs to the original map into evidence that a key belongs to the new map.
2. The new, possibly-smaller map.

mappingKnownKeys

Arguments

:: Ord k2

=> (Key ph k1 -> k2)

key-and-evidence-mapping function

-> Map ph k1 v

initial map

-> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)

continuation

-> t

O(n*log n). Same as mappingKeys, but the key-mapping function can make use of evidence that the input key belongs to the original map.

mappingKeysWith

Arguments

:: Ord k2

=> (v -> v -> v)

value-combining function

-> (k1 -> k2)

key-mapping function

-> Map ph k1 v

initial map

-> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)

continuation

-> t

O(n*log n). Same as mappingKeys, 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

Arguments

:: Ord k2

=> (v -> v -> v)

value-combining function

-> (Key ph k1 -> k2)

key-plus-evidence-mapping function

-> Map ph k1 v

initial map

-> (forall ph'. (Key ph k1 -> Key ph' k2, Map ph' k2 v) -> t)

continuation

-> t

O(n*log n). Same as mappingKnownKeys, 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.

Indexing

findIndex :: Ord k => Key ph k -> Map ph k a -> Index ph

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 findIndex, this function can not fail at runtime.

elemAt :: Index ph -> Map ph k v -> (Key ph k, v)

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 elemAt, this function can not fail at runtime.

Utilities

tie

Arguments

:: (Functor f, Ord k)

=> (f a -> a)

folding function

-> Map ph k (f (Key ph k))

map with recursive key references

-> Key ph k

-> a

Build a value by "tying the knot" according to the references in the map.