Passes using multiple types of facts (aka snooping)

[spacekitteh]

Imagine a pass which can use multiple types of facts - for example, a cache locality optimisation pass might want information about aliasing, branch selection frequency, and, optionally, the size of the code in a loop.

This might mean multiple types of fact, as well as the ability to OPTIONALLY use a fact type (i.e. if there is no provider of this type of fact, the pass is still valid, but probably not optimal).

It seems to me that the clearest way to handle this is with Effectful typing: each fact is represented with a separate effect type, and optional effects could be handled by a nondeterministic effect. Something like, e.g.:

myPassAnalysis :: (Member AliasFact r, Member BranchPredictionFact r, Member NonDetEff BlockSize r) => Eff r (Fact x f) -> n e x -> Fact x f

[spacekitteh]

One particularly interesting method is by using so-called "Logical lattices", outlined in Combining Abstract Interpreters. A logical lattice is one where the order is implication, with the base set being the set of finite conjunctions over some theory (cf #41). They further show a method to combine multiple lattices which results in an extremely precise lattice (more precise than the reduced product), assuming some suitable conditions (convexity, stably infinite input lattices, and disjoint theories (apart from equality)). The downside is that the join and existential operators, at least in their implementation, have O(n^2) complexity, but that looks like it can be countered by laziness.