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. 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.

Type Classes

Semilattice

class Semilattice(a)
  lat_bottom : () -> a
  lat_join : (a, a) -> a
  lat_leq : (a, a) -> Bool

A carrier ordered by a least upper bound, with a least element: everything a fixpoint needs to know about the values it is solving for.

lat_join is the least upper bound, lat_bottom its identity, and lat_leq the partial order the join induces. The laws, for all x, y, z:

• associative: lat_join(x, lat_join(y, z)) and lat_join(lat_join(x, y), z) - commutative: lat_join(x, y) and lat_join(y, x) - idempotent: lat_join(x, x) and x - identity: lat_join(lat_bottom(), x) and x - order: lat_leq(x, y) is true exactly when lat_join(x, y) and y agree

The equality every law is stated up to is lat_equiv, the equivalence the order induces, rather than structural equality: Map and Option carriers have no Eq instance to state it with, and two values at the same point of the order are interchangeable to every consumer here.

Instance resolution keys on the head type constructor, so a carrier admits exactly one instance: there is no second, set-specific Map instance beside the one below, and none is needed, because that one already is set union at Map(k, Unit), which is how Data.Set spells a set. The same rule is why Int and List have no instance: max on Int is a join with no identity (Int has no least element), and a list admits several defensible joins (union, pointwise, concatenation) with nothing in the type to choose between them. A program that wants one declares it on its own type.

Instances

latUnit

instance latUnit : Semilattice(Unit)

The one-point lattice. Trivial on its own; it is the payload that turns the map instance into set union, since there a key’s presence is the information and its value carries none.

latBool

instance latBool : Semilattice(Bool)

Disjunction, ordered false below true: the carrier a reachability or “is this ever called” pass accumulates in.

latOption

instance latOption : Semilattice(Option(a))

The lifted lattice: None strictly below every Some, and two Somes joined under the payload’s own order. None is genuinely below Some of bottom, so “absent” and “present and empty” stay distinguishable, which is what a “has this node been reached at all” question needs.

latPair

instance latPair : Semilattice((a, b))

The product lattice: componentwise join, componentwise order. Two analyses run as one pass by pairing their carriers.

latMap

instance latMap : Semilattice(Map(k, v, ord))

The partial-map lattice: the empty map is bottom, an absent key is strictly below any present one, and two present keys join under the payload’s order. At Unit that is exactly set union over Data.Set (presence is the only information a key carries); at a nested map it is the map of sets the compiler’s own fixpoint is specialized to.

Functions and Values

lat_joins

lat_joins : forall a. (List(a)) -> a

The join of a list, bottom-first. The combining step a transfer function takes over its dependencies’ values.

lat_joins([false, true, false])

true

lat_equiv

lat_equiv : forall a. (a, a) -> Bool

Whether two values sit at the same point of the order. This is the equality the laws are stated up to, and the only one available on a carrier with no Eq instance.

lat_equiv(map_insert(1, (), map_empty), map_insert(1, (), map_empty))

true

fix_at

fix_at : forall a b c. (Map(b, c, a), b) -> 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}

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}

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}

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]]