Data.Lattice

Join-semilattices: carriers ordered by a least upper bound.

The order-theoretic half of the fixpoint substrate, on its own so a program can talk about joins without pulling in a solver: Data.Fixpoint imports this module and iterates over its carriers, and a static analysis, a CRDT merge, or a permissions meet is the same vocabulary with no worklist near it. Opt-in: not in Base.

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.

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.

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.

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 given Data.Lattice.Semilattice(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 given Data.Lattice.Semilattice(a)

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