March Docs

Set

Set module: persistent hash-array-mapped-trie set.

Set(a) is an immutable, hash-indexed collection backed by a HAMT via the Map module (Set(a) ≅ Map(a, Unit) internally). This gives O(log₃₂ n) ≈ O(1) amortized membership tests, insert, and delete.

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

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

Elements are located by hash; the comparator only decides equality among elements whose hashes match, so it must agree with ==.

Iteration order is hash-traversal order (not sorted). Use to_list then sort externally if sorted order is needed. For a set kept in sorted order, see SortedSet.

Types

ptypeSEntrySEntry(a) =#
ptypeSetSet(a) = HamtSet(Int, SEntry(a))#

Functions

fncontainscontains(s, elem, cmp) : {Bool | _ == member(elem, elts(s))}#

Returns true if the set contains elem. cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let s1 = Set.from_list(["a", "b"], fn a -> fn b -> a < b)
march> Set.contains(s1, "a", fn a -> fn b -> a < b)
true
march> let s1 = Set.from_list(["a", "b"], fn a -> fn b -> a < b)
march> Set.contains(s1, "z", fn a -> fn b -> a < b)
false

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fndifferencedifference(a, b, cmp) : {Set(a) | elts(_) == diff(elts(a), elts(b))}#

Returns elements in a that are not in b (set difference a \\ b). cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let da = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> List.sort_by(Set.to_list(Set.difference(da, Set.from_list([2, 9], fn a -> fn b -> a < b), fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[1, 3]

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnemptyempty() : {Set(a) | elts(_) == empty}#

Returns an empty set.

Examples

march> Set.size(Set.empty())
0

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fneqeq(a, b, cmp) : {Bool | _ == (elts(a) == elts(b))}#

Returns true if the two sets contain the same elements, regardless of the order they were inserted in. O(n) membership checks. cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> Set.eq(Set.from_list([1, 2], fn a -> fn b -> a < b), Set.from_list([2, 1], fn a -> fn b -> a < b), fn a -> fn b -> a < b)
true
march> Set.eq(Set.from_list([1, 2], fn a -> fn b -> a < b), Set.from_list([1], fn a -> fn b -> a < b), fn a -> fn b -> a < b)
false

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnfoldfold(s : Set(a), acc : b, f : b -> a -> b) : b#

Left fold over all elements. Argument order: collection first, init second, callback last (uncurried-collection convention). The callback f is called uncurried as f(acc, elem) = new_acc. Elements are visited in hash-traversal 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> Set.fold(Set.from_list([1, 2, 3], fn a -> fn b -> a < b), 0, fn (acc, x) -> acc + x)
6
fnfrom_listfrom_list(xs, cmp) : {Set(a) | elts(_) == elts(xs)}#

Builds a set from a list of elements; duplicates are kept once. cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> Set.size(Set.from_list([3, 1, 3, 2, 1], fn a -> fn b -> a < b))
3
march> Set.is_empty(Set.from_list([], fn a -> fn b -> a < b))
true

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fninsertinsert(s, elem, cmp) : {Set(a) | elts(_) == union(elts(s), singleton(elem))}#

Inserts elem into the set. Returns the set unchanged if elem is already present. cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let s2 = Set.insert(Set.singleton(1), 2, fn a -> fn b -> a < b)
march> Set.size(s2)
2
march> let s2 = Set.insert(Set.singleton(1), 2, fn a -> fn b -> a < b)
march> Set.size(Set.insert(s2, 1, fn a -> fn b -> a < b))
2

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnintersectionintersection(a, b, cmp) : {Set(a) | elts(_) == inter(elts(a), elts(b))}#

Returns the intersection of two sets (elements in both sets). cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let ia = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> List.sort_by(Set.to_list(Set.intersection(ia, Set.from_list([2, 3, 4], fn a -> fn b -> a < b), fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[2, 3]
march> let ia = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> Set.is_empty(Set.intersection(ia, Set.from_list([9], fn a -> fn b -> a < b), fn a -> fn b -> a < b))
true

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnis_emptyis_empty(s) : {Bool | _ == (elts(s) == empty)}#

Returns true if the set contains no elements.

Examples

march> Set.is_empty(Set.empty())
true
march> Set.is_empty(Set.from_list([1], fn a -> fn b -> a < b))
false

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnis_subsetis_subset(a, b, cmp) : {Bool | _ == subset(elts(a), elts(b))}#

Returns true if a is a subset of b (every element of a is in b). The empty set is a subset of every set. cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let sb = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> Set.is_subset(Set.from_list([1, 3], fn a -> fn b -> a < b), sb, fn a -> fn b -> a < b)
true
march> let sb = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> Set.is_subset(Set.from_list([1, 4], fn a -> fn b -> a < b), sb, fn a -> fn b -> a < b)
false
march> let sb = Set.from_list([1, 2, 3], fn a -> fn b -> a < b)
march> Set.is_subset(Set.empty(), sb, fn a -> fn b -> a < b)
true

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnremoveremove(s, elem, cmp) : {Set(a) | elts(_) == diff(elts(s), singleton(elem))}#

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

Examples

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

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnsingletonsingleton(x) : {Set(a) | elts(_) == singleton(x)}#

Returns a set containing exactly one element.

Examples

march> Set.to_list(Set.singleton("a"))
["a"]

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnsizesize(s) : {Int | _ == card(elts(s))}#

Returns the number of elements in the set. O(1): the count is cached.

Examples

march> Set.size(Set.from_list([1, 2, 2, 3], fn a -> fn b -> a < b))
3

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

fnto_listto_list(s) : {List(a) | elts(_) == elts(s)}#

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

Examples

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

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".

fnunionunion(a, b, cmp) : {Set(a) | elts(_) == union(elts(a), elts(b))}#

Returns the union of two sets (all elements in either set). Inserts each element of b into a: O(m) inserts for m = size(b). cmp : a -> a -> Bool where cmp(a)(b) = true means a < b.

Examples

march> let ua = Set.from_list([1, 2], fn a -> fn b -> a < b)
march> let ub = Set.from_list([2, 3], fn a -> fn b -> a < b)
march> List.sort_by(Set.to_list(Set.union(ua, ub, fn a -> fn b -> a < b)), fn (x, y) -> x < y)
[1, 2, 3]

This contract is ASSUMED, not proved: the set of elements is a fact about the abstract set (elts) the refinement checker takes on faith, and it holds only when cmp is a strict total order consistent with == on the element type. See docs/refinement-types.md, "Set Refinements".