Finite maps from k to v, with a way to quickly get from v to k for certain values of type v (those for which tag is defined).

Every value of this type must satisfy biMapInvariant.

Partial injections from a type to some tag type.

The idea is that tag should be injective on its domain: if tag x = tag y = Just i, then x = y. However, this property does not need to hold globally. The preconditions of the BiMap operations below specify for which sets of values tag must be injective.

\(\mathcal{O}(\log n)\). Is the value a source key?

\(\mathcal{O}(\log n)\). Is the value a target key?

\(\mathcal{O}(\log n)\). Look up a key.

\(\mathcal{O}(\log n)\). Inverse key lookup.

\(\mathcal{O}(1)\). Create a singleton map.

\(\mathcal{O}(\log n)\). Insert an element into a map. Overwrites existing values.

Precondition: See insertPrecondition.

Inserts a binding into the map. If a binding for the key already exists, then the value obtained by applying the function to the key, the new value and the old value is inserted, and the old value is returned.

Precondition: See insertLookupWithKeyPrecondition.

\(\mathcal{O}(\log n)\). Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed.

Precondition: See alterPrecondition.

(mathcal{O}(log n).) Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed.

The precondition for alterM f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

\(\mathcal{O}(\log n)\). Modifies the value at the given position, if any. If the function returns Nothing, then the value is removed.

Precondition: See updatePrecondition.

\(\mathcal{O}(\log n)\). Modifies the value at the given position, if any.

Precondition: See adjustPrecondition.

Left-biased union. For the time complexity, see union.

Precondition: See unionPrecondition.

\(\mathcal{O}(n \log n)\). Map a function over all values in the map.

Precondition: See mapWithKeyPrecondition.

\(\mathcal{O}(n)\). Changes all the values using the given function, which is also given access to keys.

Precondition: See mapWithKeyFixedTagsPrecondition. Note that tags must not change.

\(\mathcal{O}(n \log n)\). Conversion from lists of pairs. Later entries take precedence over earlier ones.

Precondition: See fromListPrecondition.

\(\mathcal{O}(n)\). Conversion from two lists that contain distinct keys/tags, with the keys/tags in ascending order.

Precondition: See fromDistinctAscendingListsPrecondition.

\(\mathcal{O}(n)\). Conversion to lists of pairs, with the keys in ascending order.

\(\mathcal{O}(n)\). Generates input suitable for fromDistinctAscendingLists.

\(\mathcal{O}(n)\). The keys, in ascending order.

\(\mathcal{O}(n)\). The values, ordered according to the corresponding keys.

Checks if the function tag is injective for the values in the given list for which the function is defined.

The invariant for BiMap.

The precondition for insert k v m: If v has a tag (tag v ≠ Nothing), then m must not contain any mapping k' ↦ v' for which k ≠ k' and tag v = tag v'.

The precondition for insertLookupWithKey f k v m is that, if the value v' is inserted into m, and tag v' is defined, then no key other than k may map to a value v'' for which tag v'' = tag v'.

The precondition for alter f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

The precondition for update f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

The precondition for adjust f k m is that, if the value v is inserted into m, and tag v is defined, then no key other than k may map to a value v' for which tag v' = tag v.

The precondition for mapWithKey f m: For any two distinct mappings k₁ ↦ v₁, k₂ ↦ v₂ in m for which the tags of f k₁ v₁ and f k₂ v₂ are defined the values of f must be distinct (f k₁ v₁ ≠ f k₂ v₂). Furthermore tag must be injective for { f k v | (k, v) ∈ m }.

The precondition for mapWithKeyFixedTags f m is that, if m maps k to v, then tag (f k v) == tag v.

The precondition for fromList kvs: For all pairs (k₁, v₁), (k₂, v₂) in kvs for which the tags of v₁ and v₂ are defined, if v₁ = v₂ then k₁ = k₂. Furthermore tag must be injective for the values in the list.

The precondition for fromDistinctAscendingLists (kvs, kks): The lists must contain distinct keys/tags, and must be sorted according to the keys/tags. Furthermore, for every pair (k, v) in the first list for which tag v = Just k' there must be a pair (k', k) in the second list, and there must not be any other pairs in that list. Finally tag must be injective for {v | (_, v) ∈ kvs }.