Data.Fixpoint

Least fixed points over a join-semilattice, solved by worklist.

This is the iteration half of the substrate the compiler analyzes itself with, mirrored into Prism the way Data.Graph mirrors the components half. The compiler’s own fixpoint solves for the least x above a seed and closed under a step, over a finite map of sets, by recomputing every key each round until no key grows. The same shape is here, driven by a worklist instead of rounds, and generalized from “a set” to any carrier with a Semilattice instance (the class and its carriers live in Data.Lattice; this module is only the iteration). A pass that propagates latent effects along a call graph, an occurrence count, or a liveness set is the same program three times: a per-node contribution, a join, and a dependency relation saying who must be recomputed when a node moves.

Determinism. The node set is the seed’s key set, taken in ascending Ord(k) order; the dependency relation is reversed once through Data.Graph, whose successor lists are ascending and duplicate-free; and a node is appended to the queue only when it is not already waiting. The queue is therefore a pure function of the two input maps, and a map is a pure function of its bindings, never of insertion order. Two callers who build the same relation from differently ordered lists run the same iteration, not merely reach the same answer.

Termination. Every update joins into the previous value (fix_least never replaces, it accumulates), so a node’s value only ever ascends, and a node is re-queued only when its value strictly ascended. On a carrier of finite height the chain stabilizes, no node is re-queued, and the queue drains. Two things break that argument, and neither is checkable here: a carrier of unbounded height (a Map that gains a fresh key every visit), and a lat_join/lat_leq pair that disagree, which reports a change forever. So the loop is bounded: it consumes one unit of budget per visit and calls fail() when the budget runs out, rather than spinning. fix_budget is the default, and fix_least_within takes the budget explicitly for a carrier taller than that default assumes. Opt-in: not in Base.

Functions and Values

fix_at

fix_at : forall a b c. (Map(b, c, a), b) -> c given Ord(b), Data.Lattice.Semilattice(c)

The value assigned to key, or bottom when the assignment says nothing about it. A transfer function reads its dependencies through this rather than matching on map_lookup, so an unmentioned node reads as the least element instead of an Option the caller has to decide about.

(
  fix_at(map_from_list([("seen", true)]), "seen"),
  fix_at(map_from_list([("other", false)]), "missing"),
)

(true, false)

fix_budget

fix_budget : forall a b c d. (Map(c, d, a), Map(c, List(c), b)) -> Int

The default visit budget: (n + 1) * (n + e + 1) for n nodes and e dependency edges. It bounds the visits a solve over a carrier of height at most n can take, which covers the archetypal carrier (a set drawn from the node set itself) with room to spare. A taller carrier belongs in fix_least_within with a budget the caller can justify.

fix_budget(
  map_from_list([("a", false), ("b", false)]),
  map_from_list([("a", ["b"])]),
)

12

fix_least

fix_least : forall e0 a b c d. (Map(c, d, a), Map(c, List(c), b), (c, Map(c, d, a)) -> d ! {Fail, e0}) -> Map(c, d, a) ! {Fail, e0} given Ord(c), Data.Lattice.Semilattice(d)

The least assignment above seed closed under step, by worklist.

seed’s keys are the node set, and the solution has exactly those keys. uses is the dependency relation, mapping a node to the nodes it reads; step(key, current) is the transfer function, returning key’s contribution under the current assignment. The result at a node is the join of its seed value and every contribution step made for it.

Two conditions are the caller’s to keep, and the solver reports neither. step(key, current) may read current only at key itself and at the nodes uses lists for key, since those are the only changes that re-queue it; a transfer function that reads further gets an assignment that is closed with respect to the relation it declared and no other. And step must be monotone in current, or the result is merely some post-fixpoint rather than the least one. Neither slip can spin the solver, because the update accumulates; the budget is what covers the two failures that can.

fix_least(
    map_from_list([("a", false), ("b", true)]),
    map_from_list([("a", ["b"])]),
    \(_key, cur) -> fix_at(cur, "b"),
  ).map_to_list()

[(a, true), (b, true)]

fix_least_within

fix_least_within : forall e0 a b c d. (Int, Map(c, d, a), Map(c, List(c), b), (c, Map(c, d, a)) -> d ! {Fail, e0}) -> Map(c, d, a) ! {Fail, e0} given Ord(c), Data.Lattice.Semilattice(d)

fix_least with an explicit visit budget. fail() when the budget is exhausted: the solve is abandoned rather than reported at whatever assignment it had reached, since a partial answer to a least-fixpoint question is a wrong answer, not an approximate one.

succeeds(\() ->
  fix_least_within(
    0,
    map_from_list([("a", false)]),
    map_empty,
    \(_key, _cur) -> true,
  ),
)

false

fix_propagate

fix_propagate : forall a b c d e. (Map(d, e, a), Map(d, List(d), b)) -> Map(d, e, c) ! {Fail} given Ord(d), Data.Lattice.Semilattice(e)

The transitive closure of a per-node contribution along a dependency relation: the least x with x[k] the join of own[k] and every x[j] for j in uses[k].

This is what the compiler’s own fixpoint is called for every time, with own the operations a function performs itself and uses its callees, and it is the reduction an occurrence or liveness pass makes: contribution, join, relation. The node set is every key of own together with every node the relation mentions, so a callee that contributes nothing itself still gets an answer.

map(
    set_to_list,
    map_values(
        fix_propagate(
            map_from_list([("f", set_from_list(["A"])), ("g", set_from_list(["B"]))]),
            map_from_list([("f", ["g"]), ("g", ["f"])]),
          ),
      ),
  )

[[A, B], [A, B]]