Copyright | (c) Matt Noonan 2017 |
---|---|

License | BSD-style |

Maintainer | matt.noonan@gmail.com |

Portability | portable |

Safe Haskell | None |

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 zero-cost `newtype`

wrapper around Data.Map's

that enables you
to separate the `Map`

*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

value.`Maybe`

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

`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's`Maybe`

)`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 v`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

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

v*know* that this key is in the map, why should I have to handle the

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

v*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,

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

ph k*any* value of type

.`Map`

ph k v

The

type is simply a `Key`

ph k`newtype`

wrapper around `k`

, but the phantom type `ph`

allows

to represent both `Key`

ph k*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

function. In Data.Map, `member`

has the type`member`

`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 type`Member`

`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, `Nothing`

*augmented with evidence that they key*
*is present*. This key-plus-evidence can then be used to do any number of

-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
- data Index ph
- theMap :: Map ph k v -> Map k v
- theKey :: Key ph k -> k
- theIndex :: Index ph -> Int
- 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 :: 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
- member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)
- keys :: Map ph k v -> [Key ph k]
- lookupMay :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
- 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
- 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)
- 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
- 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
- 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
- deleting :: Ord k => k -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t
- 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
- filtering :: (v -> Bool) -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t
- filteringWithKey :: (Key ph k -> v -> Bool) -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t
- 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
- 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
- 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
- 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
- findIndex :: Ord k => Key ph k -> Map ph k a -> Index ph
- elemAt :: Index ph -> 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.

theIndex :: Index ph -> Int Source #

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

# Evaluation

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

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

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.

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

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

# Safe lookup

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`

.

# Preserving key sets

## Localized updates

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.

## Mapping values

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.

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

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

# Enlarging key sets

## Inserting new keys

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

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

*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

for more usage examples.`example4`

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

will insert the pair (key, value) into `insertingWith`

f key value mp cont`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`

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

*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

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

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

*different phantom type*.

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

is the same as `unioningWith`

f

, except that `unioning`

`f`

is used to
combine values that correspond to keys found in both maps.

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

is the same as `unioningWithKey`

f

, except that `unioningWith`

f`f`

also
has access to the key and evidence that it is present in both maps.

# Reducing key sets

## Removing keys

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

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

) - The updated map itself.

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

- 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.
- The updated map itself.

## Filtering

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

- 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
- The filtered map itself, with a new phantom type parameter.

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

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

s, as in Data.Map's
`Map`

, evaluating the intersection map with the given continuation.`intersection`

The continuation is given two things:

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

, with a`Map`

*different phantom type*.

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

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

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

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

# Mapping key sets

:: 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)*.

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.

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

, but the key-mapping function can make use of
evidence that the input key belongs to the original map.`mappingKeys`

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

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

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

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

# Indexing

findIndex :: Ord k => Key ph k -> Map ph k a -> Index ph 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`