Map

Map module: persistent hash-array-mapped-trie map.

Map(k, v) is an immutable, hash-indexed key-value store backed by a HAMT (Hash Array Mapped Trie). Lookup, insert, and delete are O(log₃₂ n) ≈ O(1) amortized. The HAMT provides excellent structural sharing under Perceus reference counting (path-copy only touches 1–7 nodes per update).

Operations that need key identity take an explicit comparator: cmp : k -> k -> Bool where cmp(a)(b) = true means a < b

Equality between keys is derived from the comparator: eq(a, b) = not cmp(a)(b) and not cmp(b)(a)

Standard comparators: fn a -> fn b -> a < b for Int or String keys (String: lexicographic) Map.int_cmp / Map.str_cmp the same, as named functions

Keys are located by hash, and the comparator only decides equality among keys whose hashes match, so it must agree with == (a comparator that treats two ==-different keys as equal, e.g. case-insensitively, does not merge them).

Element refinements: get, get_or, insert, remove, keys, values, map_values, merge and singleton are annotated with their generic types, so the refinement checker carries a refined map's key and value facts through them by PARAMETRICITY (checked, not assumed): Map.insert(m, k, v, cmp) with m : Map(String, {Int | _ > 0}) meets Map(String, {Int | _ > 0}) when v is positive. Their key-set contracts stay assumed, as below. See docs/refinement-types.md, "Map's own functions".

Iteration order is hash-traversal order (not sorted by key). Use to_list then sort externally if sorted order is needed.

Performance (n entries): Lookup / insert / delete O(log₃₂ n) ≈ O(1) size O(n) Traversals (fold / keys) O(n)

Types

ptypeMapMap(k, v) = HamtMap(HEntry(k, v))#

Map(k, v) wraps a Hamt.HEntry(k, v) trie node. We use HEntry directly as the Map type to avoid an extra wrapper allocation.

ptypeHEntryHEntry(k, v) =#

Re-export the HEntry constructors under Map-local names so pattern matching stays inside this module.

Functions

fncontains_keycontains_key(m, key, cmp) : {Bool | _ == member(key, keys(m))}#

Returns true if key is present in the map. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> Map.contains_key(Map.singleton(1, "a"), 1, fn a -> fn b -> a < b)
true
march> Map.contains_key(Map.empty(), 1, fn a -> fn b -> a < b)
false

fnemptyempty() : {Map(k, v) | keys(_) == empty}#

Returns an empty map.

Examples

march> Map.is_empty(Map.empty())
true
march> Map.size(Map.empty())
0

fnentriesentries(m)#

Returns all (key, value) pairs as a list (hash-traversal order). Same as to_list.

Examples

march> List.sort_by(Map.entries(Map.from_list([("b", 2), ("a", 1)], fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[("a", 1), ("b", 2)]

fnfilterfilter(m : Map(k, v), pred : k -> v -> Bool[p], cmp : k -> k -> Bool) : {Map(k[p], v[p]) | subset(keys(_), keys(m))}#

Returns a map containing only entries where pred(key)(value) is true. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b. pred : k -> v -> Bool (curried). Rebuilds the map by re-inserting the kept entries, O(n log n).

Examples

march> let m4 = Map.from_list([(1, 10), (2, 20), (3, 30)], fn a -> fn b -> a < b)
march> List.sort_by(Map.keys(Map.filter(m4, fn k -> fn v -> v > 15, fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[2, 3]

This contract is ASSUMED, not proved: the set of keys is a fact about the abstract map (keys) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the key type. See docs/refinement-types.md, "Set Refinements". The checker also assumes that every entry satisfies pred: a caller demanding Map(String, {Int | _ > 0}) of Map.filter(m, fn _k -> fn v -> v > 0, cmp) gets it (an abstract refinement of two arguments, k -> v -> Bool[p]).

fnfoldfold(m : Map(k, v), acc : b, f : b -> k -> v -> b) : b#

Left fold over all entries. Argument order: collection first, init second, callback last (uncurried-collection convention). The callback f is called uncurried as f(acc, key, val) = new_acc. Entries are visited in hash-traversal order, so f should not depend on the order. Generic in the accumulator b, so a refinement demanded of the result is checked as an invariant of acc (see docs/refinement-types.md, "Folds").

Examples

march> Map.fold(Map.from_list([(1, 10), (2, 20)], fn a -> fn b -> a < b), 0, fn (acc, k, v) -> acc + k + v)
33
march> Map.fold(Map.empty(), 7, fn (acc, k, v) -> acc + k + v)
7

fnfrom_listfrom_list(pairs, cmp)#

Builds a map from a list of (key, value) pairs. Later entries overwrite earlier ones for duplicate keys. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let m3 = Map.from_list([(1, "a"), (2, "b"), (1, "c")], fn a -> fn b -> a < b)
march> Map.get(m3, 1, fn a -> fn b -> a < b)
Some("c")
march> Map.is_empty(Map.from_list([], fn a -> fn b -> a < b))
true

fnfrom_list_intfrom_list_int(pairs)#

Build a Map(Int, v) from a list of pairs using the default Int comparator. Equivalent to Map.from_list(pairs, Map.int_cmp); later pairs overwrite earlier ones with the same key.

Examples

march> Map.size(Map.from_list_int([(1, "a"), (2, "b")]))
2

fnfrom_list_stringfrom_list_string(pairs)#

Build a Map(String, v) from a list of pairs using the default String comparator. Equivalent to Map.from_list(pairs, Map.str_cmp); later pairs overwrite earlier ones with the same key.

Examples

march> Map.get(Map.from_list_string([("a", 1), ("b", 2)]), "b", fn a -> fn b -> a < b)
Some(2)

fngetget(m : Map(k, v), key : k, cmp : k -> k -> Bool) : {Option(v) | is_Some(_) == member(key, keys(m))}#

Returns Some(value) if key is present, or None. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let m = Map.from_list([("a", 1), ("b", 2)], fn a -> fn b -> a < b)
march> Map.get(m, "b", fn a -> fn b -> a < b)
Some(2)
march> let m = Map.from_list([("a", 1), ("b", 2)], fn a -> fn b -> a < b)
march> Map.get(m, "z", fn a -> fn b -> a < b)
None

fnget_orget_or(m : Map(k, v), key : k, default : v, cmp : k -> k -> Bool) : v#

Returns the value for key, or default if the key is absent. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> Map.get_or(Map.singleton("a", 1), "a", 0, fn a -> fn b -> a < b)
1
march> Map.get_or(Map.singleton("a", 1), "z", 0, fn a -> fn b -> a < b)
0

fninsertinsert(m : Map(k, v), key : k, val : v, cmp : k -> k -> Bool) : {Map(k, v) | keys(_) == union(keys(m), singleton(key))}#

Inserts or updates a key-value pair. Returns the new map. If the key is already present its value is replaced. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let m1 = Map.insert(Map.singleton("a", 1), "a", 5, fn a -> fn b -> a < b)
march> Map.to_list(m1)
[("a", 5)]
march> let m1 = Map.insert(Map.singleton("a", 1), "a", 5, fn a -> fn b -> a < b)
march> Map.size(Map.insert(m1, "b", 2, fn a -> fn b -> a < b))
2

fnint_cmpint_cmp(a) do fn b -> a < b end#

Curried less-than comparator for Int keys: int_cmp(a)(b) is a < b. Pass to Map.* functions.

Examples

march> let lt1 = Map.int_cmp(1)
march> lt1(2)
true
march> let lt1 = Map.int_cmp(1)
march> lt1(1)
false

fnis_emptyis_empty(m) : {Bool | _ == (keys(m) == empty)}#

Returns true if the map contains no entries. O(1).

Examples

march> Map.is_empty(Map.singleton(1, "a"))
false
march> Map.is_empty(Map.remove(Map.singleton(1, "a"), 1, fn a -> fn b -> a < b))
true

fnkeyskeys(m : Map(k, v)) : {List(k) | elts(_) == keys(m)}#

Returns all keys as a list (hash-traversal order, not sorted).

Examples

march> List.sort_by(Map.keys(Map.from_list([("b", 2), ("a", 1)], fn a -> fn b -> a < b)), fn (x, y) -> x < y)
["a", "b"]

fnmap_valuesmap_values(m : Map(k, v), f : v -> w) : {Map(k, w) | keys(_) == keys(m)}#

Applies f to each value, returning a new map with the same keys. f takes the value only (not the key). Needs no comparator.

Examples

march> Map.to_list(Map.map_values(Map.singleton("a", 2), fn v -> v * 10))
[("a", 20)]

fnmergemerge(a : Map(k, v), b : Map(k, v), cmp : k -> k -> Bool) : {Map(k, v) | keys(_) == union(keys(a), keys(b))}#

Merges two maps. When a key appears in both maps, the value from b takes precedence. O(n log n) in the size of b. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let ma = Map.from_list([(1, "a"), (2, "b")], fn a -> fn b -> a < b)
march> let mb = Map.from_list([(2, "B"), (3, "C")], fn a -> fn b -> a < b)
march> List.sort_by(Map.to_list(Map.merge(ma, mb, fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[(1, "a"), (2, "B"), (3, "C")]

fnmerge_withmerge_with(a, b, f, cmp)#

Merges two maps with a combining function for conflicting keys. merge_with(a, b, f, cmp): when key exists in both, value: f(val_a)(val_b). Keys present in only one map keep their value. cmp : k -> k -> Bool; f : v -> v -> v (curried). O(n log n) in the size of b.

Examples

march> let ca = Map.from_list([("x", 1), ("y", 2)], fn a -> fn b -> a < b)
march> let cb = Map.from_list([("y", 10), ("z", 5)], fn a -> fn b -> a < b)
march> List.sort_by(Map.to_list(Map.merge_with(ca, cb, fn x -> fn y -> x + y, fn a -> fn b -> a < b)), fn (p, q) -> p < q)
[("x", 1), ("y", 12), ("z", 5)]

fnremoveremove(m : Map(k, v), key : k, cmp : k -> k -> Bool) : {Map(k, v) | keys(_) == diff(keys(m), singleton(key))}#

Removes a key from the map. Returns the map unchanged if the key is absent. cmp : k -> k -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let m2 = Map.from_list([(1, "a"), (2, "b")], fn a -> fn b -> a < b)
march> Map.to_list(Map.remove(m2, 1, fn a -> fn b -> a < b))
[(2, "b")]
march> let m2 = Map.from_list([(1, "a"), (2, "b")], fn a -> fn b -> a < b)
march> Map.size(Map.remove(m2, 9, fn a -> fn b -> a < b))
2

fnsingletonsingleton(key : k, val : v) : {Map(k, v) | keys(_) == singleton(key)}#

Returns a map containing exactly one key-value pair. Needs no comparator.

Examples

march> Map.to_list(Map.singleton("a", 1))
[("a", 1)]

fnsizesize(m) : {Int | _ == card(keys(m))}#

Returns the number of key-value pairs in the map. O(n): the count is not cached, every call walks the trie.

Examples

march> Map.size(Map.from_list([(1, "a"), (2, "b"), (1, "c")], fn a -> fn b -> a < b))
2

This contract is ASSUMED, not proved: the pair count is a fact about the abstract map (card(keys(m))) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the key type. See docs/refinement-types.md, "Set Refinements".

fnstr_cmpstr_cmp(a) do fn b -> a < b end#

Curried less-than comparator for String keys (lexicographic): str_cmp(a)(b) is a < b. Pass to Map.* functions.

Examples

march> let lt_b = Map.str_cmp("b")
march> lt_b("a")
false
march> let lt_b = Map.str_cmp("b")
march> lt_b("c")
true

fnto_listto_list(m)#

Converts a map to a list of (key, value) pairs (hash-traversal order, not sorted; sort the result if order matters).

Examples

march> Map.to_list(Map.empty())
[]
march> List.sort_by(Map.to_list(Map.from_list([(2, "b"), (1, "a")], fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[(1, "a"), (2, "b")]

fnvaluesvalues(m : Map(k, v)) : List(v)#

Returns all values as a list (hash-traversal order, the same order as keys).

Examples

march> List.sort_by(Map.values(Map.from_list([("b", 2), ("a", 1)], fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[1, 2]