Data.UnionFind

A persistent union-find (disjoint-set) over an ordered key type.

A set is named by its canonical root, and uf_union always keeps the smaller key (by Ord) as the root, so a set’s representative is a pure function of its members, never of the order unions ran in. There is no path compression (that needs mutation); uf_find walks parent links to the root on each call. A key absent from the map is its own singleton root, so uf_empty needs no pre-population. The occurs check an HM unifier layers on top is type-specific and lives with the unifier, not here. Opt-in: not in Base.

Functions and Values

uf_empty

uf_empty : forall a b. Map(a, a, b)

The empty forest: every key is its own singleton root.

uf_find

uf_find : forall a b. (Map(b, b, a), b) -> b

The canonical root of x’s set.

uf_find(uf_union(uf_union(uf_empty, 3, 2), 2, 1), 3)

1

uf_union

uf_union : forall a b. (Map(b, b, a), b, b) -> Map(b, b, a)

Merge the sets of x and y, keeping the smaller root; a no-op when they are already joined.

uf_equiv(uf_union(uf_union(uf_empty, 1, 2), 2, 3), 1, 3)

true

uf_equiv

uf_equiv : forall a b. (Map(b, b, a), b, b) -> Bool

True when x and y belong to the same set.