Documentation

The concrete MonadDependency for this worklist-based solver.

This essentially tracks the current approximation of the solution to the DataFlowProblem as mutable state while solveProblem makes sure we will eventually halt with a conservative approximation.

A constraint synonym for the constraints m and its associated Domain have to suffice.

This is actually a lot less scary than you might think. Assuming we got quantified class constraints, Datafixable is a specialized version of this:

type Datafixable m =
  ( forall r. Currying (ParamTypes (Domain m)) r
  , MonoMapKey (Products (ParamTypes (Domain m)))
  , BoundedJoinSemiLattice (ReturnType (Domain m))
  )

Now, let's assume a concrete Domain m ~ String -> Bool -> Int, so that ParamTypes (String -> Bool -> Int) expands to the type-level list '[String, Bool] and Products '[String, Bool] reduces to (String, Bool).

Then this constraint makes sure we are able to

1. Curry the domain of String -> Bool -> r for all r to e.g. (String, Bool) -> r. See Currying. This constraint should always be discharged automatically by the type-checker as soon as ParamTypes and ReturnTypes reduce for the Domain argument, which happens when the concrete MonadDependency m is known.

   (Actually, we do this for multiple concrete r because of the missing support for quantified class constraints)

2. We want to use a monotone map of (String, Bool) to Int (the ReturnType (Domain m)). This is ensured by the MonoMapKey (String, Bool) constraint.

   This constraint has to be discharged manually, but should amount to a single line of boiler-plate in most cases, see MonoMapKey.

   Note that the monotonicity requirement means we have to pull non-monotone arguments in Domain m into the Node portion of the DataFlowProblem.

3. For fixed-point iteration to work at all, the values which we iterate naturally have to be instances of BoundedJoinSemiLattice. That type-class allows us to start iteration from a most-optimistic bottom value and successively iterate towards a conservative approximation using the '(/)' operator.

Specifies the density of the problem, e.g. whether the domain of Nodes can be confined to a finite range, in which case solveProblem tries to use a Data.Vector based graph representation rather than one based on Data.IntMap.

Expresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.

Computes a solution to the described DataFlowProblem by iterating transfer functions until a fixed-point is reached.

It does do by employing a worklist algorithm, iterating unstable Nodes only. Nodes become unstable when the point of another Node their transfer function dependOned changed.

The sole initially unstable Node is the last parameter, and if your domain is function-valued (so the returned Arrows expands to a function), then any further parameters specify the exact point in the Nodes transfer function you are interested in.

If your problem only has finitely many different Nodes , consider using the ProblemBuilder API (e.g. datafix + evalDenotation) for a higher-level API that let's you forget about Nodes and instead let's you focus on building more complex data-flow frameworks.

evalDenotation denot ib returns a value in domain that is described by the denotation denot.

It does so by building up the DataFlowProblem corresponding to denot and solving the resulting problem with solveProblem, the documentation of which describes in detail how to arrive at a stable denotation and what the IterationBound ib is for.