Documentation

This is the type we use to index nodes in the data-flow graph.

The connection between syntactic things (e.g. Ids) and Nodes is made implicitly in code in analysis templates through an appropriate allocation mechanism as in NodeAllocator.

Data-flow problems denote Nodes in the data-flow graph by monotone transfer functions.

This type alias alone carries no semantic meaning. However, it is instructive to see some examples of how this alias reduces to a normal form:

  LiftedFunc Int m ~ m Int
  LiftedFunc (Bool -> Int) m ~ Bool -> m Int
  LiftedFunc (a -> b -> Int) m ~ a -> b -> m Int
  LiftedFunc (a -> b -> c -> Int) m ~ a -> b -> c -> m Int

m will generally be an instance of MonadDependency and the type alias effectively wraps m around domain's return type. The result is a function that produces its return value while potentially triggering side-effects in m, which amounts to depending on LiftedFuncs of other Nodes for the MonadDependency case.

A function that checks points of some function with type domain for changes. If this returns True, the point of the function is assumed to have changed.

An example is worth a thousand words, especially because of the type-level hackery:

>>> cd = (\a b -> even a /= even b) :: ChangeDetector Int

This checks the parity for changes in the abstract domain of integers. Integers of the same parity are considered unchanged.

>>> cd 4 5
True
>>> cd 7 13
False

Now a (quite bogus) pointwise example:

>>> cd = (\x fx gx -> x + abs fx /= x + abs gx) :: ChangeDetector (Int -> Int)
>>> cd 1 (-1) 1
False
>>> cd 15 1 2
True
>>> cd 13 35 (-35)
False

This would consider functions id and negate unchanged, so the sequence iterate negate :: Int -> Int would be regarded immediately as convergent:

>>> f x = iterate negate x !! 0
>>> let g x = iterate negate x !! 1
>>> cd 123 (f 123) (g 123)
False

Models a data-flow problem, where each Node is mapped to its denoting LiftedFunc and a means to detect when the iterated transfer function reached a fixed-point through a ChangeDetector.

A monad with a single impure primitive dependOn that expresses a dependency on a Node of a data-flow graph.

The associated Domain type is the abstract domain in which we denote Nodes.

Think of it like memoization on steroids. You can represent dynamic programs with this quite easily:

>>> :{
  transferFib :: forall m . (MonadDependency m, Domain m ~ Int) => Node -> LiftedFunc Int m
  transferFib (Node 0) = return 0
  transferFib (Node 1) = return 1
  transferFib (Node n) = (+) <$> dependOn @m (Node (n-1)) <*> dependOn @m (Node (n-2))
  -- sparing the negative n error case
:}

We can construct a description of a DataFlowProblem with this transferFib function:

>>> :{
  dataFlowProblem :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m
  dataFlowProblem = DFP transferFib (const (eqChangeDetector @(Domain m)))
:}

We regard the ordinary fib function a solution to the recurrence modeled by transferFib:

>>> :{
  fib :: Int -> Int
  fib 0 = 0
  fib 1 = 1
  fib n = fib (n-1) + fib (n - 2)
:}

E.g., under the assumption of fib being total (which is true on the domain of natural numbers), it computes the same results as the least fixed-point of the series of iterations of the transfer function transferFib.

Ostensibly, the nth iteration of transferFib substitutes each dependOn with transferFib repeatedly for n times and finally substitutes all remaining dependOns with a call to error.

Computing a solution by fixed-point iteration in a declarative manner is the purpose of this library. There potentially are different approaches to computing a solution, but in Datafix.Worklist we offer an approach based on a worklist algorithm, trying to find a smart order in which nodes in the data-flow graph are reiterated.

The concrete MonadDependency depends on the solution algorithm, which is in fact the reason why there is no satisfying data type in this module: We are only concerned with declaring data-flow problems here.

The distinguishing feature of data-flow graphs is that they are not necessarily acyclic (data-flow graphs of dynamic programs always are!), but under certain conditions even have solutions when there are cycles.

Cycles occur commonly in data-flow problems of static analyses for programming languages, introduced through loops or recursive functions. Thus, this library mostly aims at making the life of compiler writers easier.

Builds on MonadDependency by providing a way to track dependencies without explicit Node management. Essentially, this allows to specify a build plan for a DataFlowProblem through calls to datafix in analogy to fix or mfix.

Shorthand that partially applies datafix to an eqChangeDetector.

A ChangeDetector that delegates to the Eq instance of the node values.

A ChangeDetector that always returns True.

Use this when recomputing a node is cheaper than actually testing for the change. Beware of cycles in the resulting dependency graph, though!