datafix- Fixing data-flow problems

Copyright(c) Sebastian Graf 2017-2020
Safe HaskellNone



Common definitions for defining data-flow problems, defining infrastructure around the notion of Domain.



type LiftedFunc domain m = Arrows (ParamTypes domain) (m (ReturnType domain)) Source #

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.

type ChangeDetector domain = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) Source #

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
>>> cd 7 13

Now a (quite bogus) pointwise example:

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

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)

eqChangeDetector :: forall domain. Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) => Eq (ReturnType domain) => ChangeDetector domain Source #

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

alwaysChangeDetector :: forall domain. Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) => ChangeDetector domain Source #

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!

class (Monad m, Datafixable (Domain m)) => MonadDomain m Source #

A monad with an associated Domain. This class exists mostly to share the associated type-class between MonadDependency and MonadDatafix.

Also it implies that m satisfies Datafixable, which is common enough

Associated Types

type Domain m :: * Source #

The abstract domain in which nodes of the data-flow graph are denoted. When this reduces to a function, then all functions of this domain are assumed to be monotone wrt. the (at least) partial order of all occuring types!

If you can't guarantee monotonicity, try to pull non-monotone arguments into Nodes.

Datafixable domain => MonadDomain (DependencyM graph domain) Source #

The Domain is extracted from a type parameter.

Instance details

Defined in Datafix.Worklist.Internal

Associated Types

type Domain (DependencyM graph domain) :: Type Source #

type Datafixable domain = (Forall (Currying (ParamTypes domain)), MonoMapKey (Products (ParamTypes domain)), BoundedJoinSemiLattice (ReturnType domain)) Source #

A constraint synonym for constraints the domain has to suffice.

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

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

Now, let's assume a concrete domain ~ 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.
  2. We want to use a monotone map of (String, Bool) to Int (the ReturnType domain). 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 DataFlowFramework.

  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.

evalAt :: forall f arr. Currying (ParamTypes arr) (ReturnType arr) => Functor f => f arr -> Products (ParamTypes arr) -> f (ReturnType arr) Source #

(<!) :: forall f arr. Currying (ParamTypes arr) (ReturnType arr) => Functor f => f arr -> Products (ParamTypes arr) -> f (ReturnType arr) Source #