Data.UnionFind.Payload

A persistent union-find whose canonical roots carry a descriptor payload.

The payload-free forest in Data.UnionFind answers only equivalence; this module is the opt-in layer for solvers that also attach a fact to each class (a metavariable’s solution, a binding level, a rank). One descriptor lives at each canonical root, and ufp_union_with combines exactly the two descriptors whose classes are joined, exactly once per join.

Absence is explicit where the payload-free forest is implicit: a key that was never inserted has no descriptor, so it is not a silent singleton; ufp_find answers None and the writing operations answer UfAbsent. Duplicate insertion is UfDuplicate, never a silent overwrite.

Determinism is part of the public contract, not a courtesy: ufp_union_with keeps the smaller root by Ord, passes the kept root’s descriptor to combine first and the absorbed root’s second, and deletes the losing descriptor, so a class’s representative and payload are a pure function of the insertions and unions performed, never of the order finds ran in. The representation (parent links) is private; render a forest through ufp_roots, which describes the logical partition. There is no path compression: a query-history-dependent representation would leak into any structural comparison, the wrong trade before a serialization boundary is pinned. Opt-in: not in Base.

Types

UnionFind

type UnionFind(k, a) = Ufp { parents: Map(k, k), payloads: Map(k, a) }

A payload-carrying forest over ordered keys. The constructor is the module’s private representation; go through the ufp_ functions.

UfError

type UfError = UfDuplicate | UfAbsent deriving (Eq, Show)

Why a forest operation refused.

Functions and Values

ufp_empty

ufp_empty : forall a b. Data.UnionFind.Payload.UnionFind(a, b)

The empty forest: no keys, no classes.

ufp_insert

ufp_insert : forall a b. (Data.UnionFind.Payload.UnionFind(a, b), a, b) -> Result(Data.UnionFind.Payload.UnionFind(a, b), Data.UnionFind.Payload.UfError) given Ord(a)

Insert x as a fresh singleton class with descriptor a. Inserting a key that is already a member (root or not) is UfDuplicate.

ufp_find(result_or(ufp_empty, ufp_insert(ufp_empty, 1, "one")), 1)

Some((1, one))

ufp_find

ufp_find : forall a b. (Data.UnionFind.Payload.UnionFind(a, b), a) -> Option((a, b)) given Ord(a)

The canonical root of x’s class and the class descriptor, or None when x was never inserted.

ufp_find(result_or(ufp_empty, ufp_insert(ufp_empty, 1, "one")), 9)

None

ufp_set

ufp_set : forall a b. (Data.UnionFind.Payload.UnionFind(a, b), a, b) -> Result(Data.UnionFind.Payload.UnionFind(a, b), Data.UnionFind.Payload.UfError) given Ord(a)

Replace the descriptor of x’s class, or UfAbsent when x was never inserted. The class and its root are unchanged.

ufp_union_with

ufp_union_with : forall e0 a b. ((a, a) -> a ! {e0}, Data.UnionFind.Payload.UnionFind(b, a), b, b) -> Result(Data.UnionFind.Payload.UnionFind(b, a), Data.UnionFind.Payload.UfError) ! {e0} given Ord(b)

Join the classes of x and y. The smaller root by Ord stays the root; combine receives the kept root’s descriptor first and the absorbed root’s second, runs exactly once per join that changes the partition, and its result becomes the joined class’s descriptor. Joining a class with itself is a no-op that never calls combine; either key absent is UfAbsent.

let uf1 = result_or(ufp_empty, ufp_insert(ufp_empty, 2, "b"))
let uf2 = result_or(ufp_empty, ufp_insert(uf1, 1, "a"))
ufp_find(result_or(ufp_empty, ufp_union_with(concat, uf2, 2, 1)), 2)

Some((1, ab))

ufp_roots

ufp_roots : forall a b. (Data.UnionFind.Payload.UnionFind(a, b)) -> List((a, b)) given Ord(a)

The logical partition: every canonical root paired with its class descriptor, in ascending key order. This is the rendering to compare or serialize; it is independent of the parent paths any sequence of joins happened to build.

let uf1 = result_or(ufp_empty, ufp_insert(ufp_empty, 2, "b"))
let uf2 = result_or(ufp_empty, ufp_insert(uf1, 1, "a"))
ufp_roots(result_or(ufp_empty, ufp_union_with(concat, uf2, 1, 2)))

[(1, ab)]

ufp_equiv

ufp_equiv : forall a b. (Data.UnionFind.Payload.UnionFind(a, b), a, a) -> Option(Bool) given Ord(a)

Whether x and y are members of the same class; None when either was never inserted.