-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Fixing data-flow problems
--
-- Fixing data-flow problems in expression trees
@package datafix
@version 0.0.0.1
-- | A uniform interface for ordered maps that can be used to model
-- monotone functions.
module Datafix.MonoMap
-- | Chooses an appropriate MonoMap for a given key type.
--
-- MonoMaps should all be ordered maps, which feature efficient
-- variants of the lookupLT and lookupMin combinators. This
-- unifies Data.Maybe, Data.IntMap.Strict,
-- Data.Map.Strict and Data.POMap.Strict under a common
-- type class, for which instances can delegate to the most efficient
-- variant available.
--
-- Because of lookupLT, this class lends itself well to
-- approximating monotone functions.
--
-- The default implementation delegates to POMap, so when there is
-- no specially crafted map data-structure for your key type, all you
-- need to do is to make sure it satisfies PartialOrd. Then you
-- can do
--
--
-- >>> import Data.IntSet
--
-- >>> instance MonoMapKey IntSet
--
--
-- to make use of the default implementation.
class Foldable (MonoMap k) => MonoMapKey k where {
type family MonoMap k = (r :: * -> *) | r -> k;
type MonoMap k = POMap k;
}
empty :: MonoMapKey k => MonoMap k v
empty :: (MonoMapKey k, (MonoMap k v ~ POMap k v)) => MonoMap k v
singleton :: MonoMapKey k => k -> v -> MonoMap k v
singleton :: (MonoMapKey k, (MonoMap k v ~ POMap k v)) => k -> v -> MonoMap k v
insert :: MonoMapKey k => k -> v -> MonoMap k v -> MonoMap k v
insert :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => k -> v -> MonoMap k v -> MonoMap k v
delete :: MonoMapKey k => k -> MonoMap k v -> MonoMap k v
delete :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> MonoMap k v
lookup :: MonoMapKey k => k -> MonoMap k v -> Maybe v
lookup :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> Maybe v
-- | Key point of this interface! Note that it returns a list of lower
-- bounds, to account for the PartialOrd case.
lookupLT :: MonoMapKey k => k -> MonoMap k v -> [(k, v)]
-- | Key point of this interface! Note that it returns a list of lower
-- bounds, to account for the PartialOrd case.
lookupLT :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> [(k, v)]
lookupMin :: MonoMapKey k => MonoMap k v -> [(k, v)]
lookupMin :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => MonoMap k v -> [(k, v)]
difference :: MonoMapKey k => MonoMap k a -> MonoMap k b -> MonoMap k a
difference :: (MonoMapKey k, MonoMap k a ~ POMap k a, MonoMap k b ~ POMap k b, PartialOrd k) => MonoMap k a -> MonoMap k b -> MonoMap k a
keys :: MonoMapKey k => MonoMap k a -> [k]
keys :: (MonoMapKey k, MonoMap k v ~ POMap k v) => MonoMap k v -> [k]
insertWith :: MonoMapKey k => (v -> v -> v) -> k -> v -> MonoMap k v -> MonoMap k v
insertWith :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => (v -> v -> v) -> k -> v -> MonoMap k v -> MonoMap k v
insertLookupWithKey :: MonoMapKey k => (k -> v -> v -> v) -> k -> v -> MonoMap k v -> (Maybe v, MonoMap k v)
insertLookupWithKey :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => (k -> v -> v -> v) -> k -> v -> MonoMap k v -> (Maybe v, MonoMap k v)
updateLookupWithKey :: MonoMapKey k => (k -> v -> Maybe v) -> k -> MonoMap k v -> (Maybe v, MonoMap k v)
updateLookupWithKey :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => (k -> v -> Maybe v) -> k -> MonoMap k v -> (Maybe v, MonoMap k v)
alter :: MonoMapKey k => (Maybe v -> Maybe v) -> k -> MonoMap k v -> MonoMap k v
alter :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => (Maybe v -> Maybe v) -> k -> MonoMap k v -> MonoMap k v
adjust :: MonoMapKey k => (v -> v) -> k -> MonoMap k v -> MonoMap k v
adjust :: (MonoMapKey k, MonoMap k v ~ POMap k v, PartialOrd k) => (v -> v) -> k -> MonoMap k v -> MonoMap k v
-- | Delegates to Maybe.
-- | Delegates to IntMap.
instance Datafix.MonoMap.MonoMapKey ()
instance Datafix.MonoMap.MonoMapKey GHC.Types.Int
-- | Some type-level helpers for 'curry'/'uncurry'ing arbitrary function
-- types.
module Datafix.Utils.TypeLevel
-- | All p as ensures that the constraint p is satisfied
-- by all the types in as. (Types is between
-- scare-quotes here because the code is actually kind polymorphic)
-- | On Booleans
-- | On Lists
-- | Version of Foldr taking a defunctionalised argument so that
-- we can use partially applied functions.
data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
-- | Arrows [a1,..,an] r corresponds to a1 -> .. -> an
-- -> r
type Arrows (as :: [*]) (r :: *) = Foldr (->) r as
arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func
-- | Products [] corresponds to (), Products [a]
-- corresponds to a, Products [a1,..,an] corresponds to
-- (a1, (..,( an)..)).
--
-- So, not quite a right fold, because we want to optimize for the empty,
-- singleton and pair case.
-- | IsBase t is 'True whenever t is *not* a
-- function space.
-- | Using IsBase we can define notions of ParamTypes and
-- ReturnTypes which *reduce* under positive information
-- IsBase t ~ 'True even though the shape of t is not
-- formally exposed
-- | Currying as b witnesses the isomorphism between Arrows as
-- b and Products as -> b. It is defined as a type class
-- rather than by recursion on a singleton for as so all of that
-- these conversions are inlined at compile time for concrete arguments.
class Currying as b
uncurrys :: Currying as b => Arrows as b -> Products as -> b
currys :: Currying as b => (Products as -> b) -> Arrows as b
data Function :: * -> * -> *
data Constant0 :: Function a (Function b a -> *) -> *
data Constant1 :: * -> Function b a -> *
instance Datafix.Utils.TypeLevel.Currying '[] b
instance Datafix.Utils.TypeLevel.Currying '[a] b
instance Datafix.Utils.TypeLevel.Currying (a2 : as) b => Datafix.Utils.TypeLevel.Currying (a1 : a2 : as) b
-- | Primitives for describing a data-flow problem in a declarative
-- manner.
--
-- Import this module transitively through Datafix and get access
-- to Datafix.Worklist for functions that compute solutions to
-- your DataFlowProblems.
module Datafix.Description
-- | 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.
newtype Node
Node :: Int -> Node
[unwrapNode] :: Node -> Int
-- | 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 LiftedFunc domain m = Arrows (ParamTypes domain) (m (ReturnType domain))
-- | 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
--
type ChangeDetector domain = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)
-- | 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.
data DataFlowProblem m
DFP :: !(Node -> LiftedFunc (Domain m) m) -> !(Node -> ChangeDetector (Domain m)) -> DataFlowProblem m
-- | A transfer function per each Node of the modeled data-flow
-- problem.
[dfpTransfer] :: DataFlowProblem m -> !(Node -> LiftedFunc (Domain m) m)
-- | A ChangeDetector for each Node of the modeled data-flow
-- problem. In the simplest case, this just delegates to an Eq
-- instance.
[dfpDetectChange] :: DataFlowProblem m -> !(Node -> ChangeDetector (Domain m))
-- | 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.
class Monad m => MonadDependency m where {
type family Domain m :: *;
}
-- | Expresses a dependency on a node of the data-flow graph, thus
-- introducing a way of trackable recursion. That's similar to how you
-- would use fix to abstract over recursion.
dependOn :: MonadDependency m => Node -> LiftedFunc (Domain m) m
-- | 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.
class (MonadDependency mdep, Monad mdat) => MonadDatafix mdep mdat | mdat -> mdep
-- | This is the closest we can get to an actual fixed-point combinator.
--
-- We need to provide a ChangeDetector for detecting the
-- fixed-point as well as a function to be iterated. In addition to
-- returning a better approximation of itself in terms of itself, it can
-- return an arbitrary value of type a. Because the iterated
-- function might want to datafix additional times (think of
-- nested let bindings), the return values are wrapped in mdat.
--
-- Finally, the arbitrary a value is returned, in analogy to
-- a in mfix :: MonadFix m => (a -> m a) -> m
-- a.
datafix :: MonadDatafix mdep mdat => ChangeDetector (Domain mdep) -> (LiftedFunc (Domain mdep) mdep -> mdat (a, LiftedFunc (Domain mdep) mdep)) -> mdat a
-- | Shorthand that partially applies datafix to an
-- eqChangeDetector.
datafixEq :: forall mdep mdat a. MonadDatafix mdep mdat => Currying (ParamTypes (Domain mdep)) (ReturnType (Domain mdep) -> ReturnType (Domain mdep) -> Bool) => Eq (ReturnType (Domain mdep)) => (LiftedFunc (Domain mdep) mdep -> mdat (a, LiftedFunc (Domain mdep) mdep)) -> mdat a
-- | A ChangeDetector that delegates to the Eq instance of
-- the node values.
eqChangeDetector :: forall domain. Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) => Eq (ReturnType domain) => ChangeDetector domain
-- | 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!
alwaysChangeDetector :: forall domain. Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) => ChangeDetector domain
instance GHC.Show.Show Datafix.Description.Node
instance GHC.Classes.Ord Datafix.Description.Node
instance GHC.Classes.Eq Datafix.Description.Node
-- | Helpers for allocating Nodes in an ergonomic manner, e.g.
-- taking care to get mfix right under the hood for allocation in
-- recursive bindings groups through the key primitive
-- allocateNode.
module Datafix.NodeAllocator
-- | A state monad wrapping a mapping from Node to some v
-- which we will instantiate to appropriate LiftedFuncs.
data NodeAllocator v a
-- | Allocates the next Node, which is greater than any nodes
-- requested before.
--
-- The value stored at that node is the result of a NodeAllocator
-- computation which may already access the Node associated with
-- that value. This is important for the case of recursive let, where the
-- denotation of an expression depends on itself.
allocateNode :: (Node -> NodeAllocator v (a, v)) -> NodeAllocator v a
-- | Runs the allocator, beginning with an empty mapping.
runAllocator :: NodeAllocator v a -> (a, Array v)
instance GHC.Base.Monad (Datafix.NodeAllocator.NodeAllocator v)
instance GHC.Base.Applicative (Datafix.NodeAllocator.NodeAllocator v)
instance GHC.Base.Functor (Datafix.NodeAllocator.NodeAllocator v)
-- | Offers an instance for MonadDatafix based on
-- NodeAllocator.
module Datafix.ProblemBuilder
-- | Constructs a build plan for a DataFlowProblem by tracking
-- allocation of Nodes mapping to ChangeDetectors and
-- transfer functions.
data ProblemBuilder m a
-- | (root, max, dfp) = buildProblem builder executes the build
-- plan specified by builder and returns the resulting
-- DataFlowProblem dfp, as well as the root
-- Node denoting the transfer function returned by the
-- ProblemBuilder action and the maximum node of the
-- problem as a proof for its denseness.
buildProblem :: forall m. MonadDependency m => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool) => ProblemBuilder m (LiftedFunc (Domain m) m) -> (Node, Node, DataFlowProblem m)
instance GHC.Base.Monad (Datafix.ProblemBuilder.ProblemBuilder m)
instance GHC.Base.Applicative (Datafix.ProblemBuilder.ProblemBuilder m)
instance GHC.Base.Functor (Datafix.ProblemBuilder.ProblemBuilder m)
instance Datafix.Description.MonadDependency m => Datafix.Description.MonadDatafix m (Datafix.ProblemBuilder.ProblemBuilder m)
-- | Abstracts over the representation of the data-flow graph.
--
-- The contents of this module are more or less internal to the
-- Datafix.Worklist implementation.
module Datafix.Worklist.Graph
-- | The data associated with each point in the transfer function of a
-- data-flow Node.
data PointInfo domain
PointInfo :: !(Maybe (ReturnType domain)) -> !(IntArgsMonoSet (Products (ParamTypes domain))) -> !(IntArgsMonoSet (Products (ParamTypes domain))) -> !Int -> PointInfo domain
-- | The value at this point. Can be Nothing only when a loop was
-- detected.
[value] :: PointInfo domain -> !(Maybe (ReturnType domain))
-- | Points this point of the transfer function depends on.
[references] :: PointInfo domain -> !(IntArgsMonoSet (Products (ParamTypes domain)))
-- | Points depending on this point.
[referrers] :: PointInfo domain -> !(IntArgsMonoSet (Products (ParamTypes domain)))
-- | The number of times this point has been updated through calls to
-- updateNodeValue.
[iterations] :: PointInfo domain -> !Int
-- | The default PointInfo.
emptyPointInfo :: PointInfo domain
-- | Diff between two IntArgsMonoSets.
data Diff a
Diff :: !(IntArgsMonoSet a) -> !(IntArgsMonoSet a) -> Diff a
[added] :: Diff a -> !(IntArgsMonoSet a)
[removed] :: Diff a -> !(IntArgsMonoSet a)
-- | Computes the diff between two IntArgsMonoSets.
computeDiff :: MonoMapKey k => IntArgsMonoSet k -> IntArgsMonoSet k -> Diff k
-- | Abstracts over the concrete representation of the data-flow graph.
--
-- There are two instances: The default Ref for sparse graphs
-- based on an IntMap and Ref for the dense case, storing
-- the Node mapping in a IOVector.
class GraphRef (ref :: * -> *)
updatePoint :: (GraphRef ref, MonoMapKey (Products (ParamTypes domain))) => Int -> Products (ParamTypes domain) -> ReturnType domain -> IntArgsMonoSet (Products (ParamTypes domain)) -> ReaderT (ref domain) IO (PointInfo domain)
lookup :: (GraphRef ref, MonoMapKey (Products (ParamTypes domain))) => Int -> Products (ParamTypes domain) -> ReaderT (ref domain) IO (Maybe (PointInfo domain))
lookupLT :: (GraphRef ref, MonoMapKey (Products (ParamTypes domain))) => Int -> Products (ParamTypes domain) -> ReaderT (ref domain) IO [(Products (ParamTypes domain), PointInfo domain)]
instance (GHC.Classes.Eq (Datafix.Utils.TypeLevel.ReturnType domain), GHC.Classes.Eq (Datafix.IntArgsMonoSet.IntArgsMonoSet (Datafix.Utils.TypeLevel.Products (Datafix.Utils.TypeLevel.ParamTypes domain)))) => GHC.Classes.Eq (Datafix.Worklist.Graph.PointInfo domain)
instance (GHC.Show.Show (Datafix.Utils.TypeLevel.ReturnType domain), GHC.Show.Show (Datafix.IntArgsMonoSet.IntArgsMonoSet (Datafix.Utils.TypeLevel.Products (Datafix.Utils.TypeLevel.ParamTypes domain)))) => GHC.Show.Show (Datafix.Worklist.Graph.PointInfo domain)
-- | Dense data-flow graph representation based on IOVector.
module Datafix.Worklist.Graph.Dense
-- | Reference to a dense data-flow graph representation.
data Ref domain
-- | Allocates a new dense graph Ref.
newRef :: MonoMapKey (Products (ParamTypes domain)) => Int -> IO (Ref domain)
instance Datafix.Worklist.Graph.GraphRef Datafix.Worklist.Graph.Dense.Ref
-- | Sparse data-flow graph representation based on IntMap.
module Datafix.Worklist.Graph.Sparse
-- | Reference to a sparse data-flow graph representation.
data Ref domain
-- | Allocates a new sparse graph Ref.
newRef :: IO (Ref domain)
instance Datafix.Worklist.Graph.GraphRef Datafix.Worklist.Graph.Sparse.Ref
-- | Internal module, does not follow the PVP. Breaking changes may happen
-- at any minor version.
module Datafix.Worklist.Internal
-- | 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.
newtype DependencyM graph domain a
-- | Why does this use IO? Actually, we only need ST here,
-- but that means we have to carry around the state thread in type
-- signatures.
--
-- This ultimately leaks badly into the exported interface in
-- solveProblem: Since we can't have universally quantified
-- instance contexts (yet!), we can' write (forall s. Datafixable
-- (DependencyM s graph domain)) => (forall s. DataFlowProblem
-- (DependencyM s graph domain)) -> ... and have to instead have
-- the isomorphic (forall s r. (Datafixable (DependencyM s graph
-- domain) => r) -> r) -> (forall s. DataFlowProblem
-- (DependencyM s graph domain)) -> ... and urge all call sites
-- to pass a meaningless id parameter.
--
-- Also, this means more explicit type signatures as we have to make
-- clear to the type-checker that s is universally quantified in
-- everything that touches it, e.g.
-- Analyses.StrAnal.LetDn.buildProblem from the test suite.
--
-- So, bottom line: We resort to IO and unsafePerformIO and
-- promise not to launch missiles. In particular, we don't export
-- DM and also there must never be an instance of MonadIO
-- for this.
DM :: (ReaderT (Env graph domain) IO a) -> DependencyM graph domain a
-- | The iteration state of 'DependencyM'/'solveProblem'.
data Env graph domain
Env :: !(DataFlowProblem (DependencyM graph domain)) -> !(IterationBound domain) -> !(IntArgsMonoSet (Products (ParamTypes domain))) -> !(graph domain) -> !(IORef (IntArgsMonoSet (Products (ParamTypes domain)))) -> !(IORef (IntArgsMonoSet (Products (ParamTypes domain)))) -> Env graph domain
-- | Constant. The specification of the data-flow problem we ought to
-- solve.
[problem] :: Env graph domain -> !(DataFlowProblem (DependencyM graph domain))
-- | Constant. Whether to abort after a number of iterations or not.
[iterationBound] :: Env graph domain -> !(IterationBound domain)
-- | Contextual state. The set of points in the domain of
-- Nodes currently in the call stack.
[callStack] :: Env graph domain -> !(IntArgsMonoSet (Products (ParamTypes domain)))
-- | Constant ref to stateful graph. The data-flow graph, modeling
-- dependencies between data-flow Nodes, or rather specific points
-- in the domain of each Node.
[graph] :: Env graph domain -> !(graph domain)
-- | Constant (but the the wrapped set is stateful). The set of points the
-- currently recomputed node references so far.
[referencedPoints] :: Env graph domain -> !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
-- | Constant (but the the wrapped queue is stateful). Unstable nodes that
-- will be recomputed by the worklist algorithm.
[unstable] :: Env graph domain -> !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) -> DataFlowProblem (DependencyM graph domain) -> IterationBound domain -> IO (graph domain) -> IO (Env graph domain)
-- | 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
--
--
-- - 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)
-- - 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.
-- - 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.
--
type Datafixable m = (Currying (ParamTypes (Domain m)) (ReturnType (Domain m)), Currying (ParamTypes (Domain m)) (m (ReturnType (Domain m))), Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool), Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m)), MonoMapKey (Products (ParamTypes (Domain m))), BoundedJoinSemiLattice (ReturnType (Domain m)))
-- | This allows us to solve MonadDependency m => DataFlowProblem
-- m descriptions with solveProblem. The Domain is
-- extracted from a type parameter.
-- | 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.
data Density graph
[Sparse] :: Density Ref
[Dense] :: Node -> Density Ref
-- | A function that computes a sufficiently conservative approximation of
-- a point in the abstract domain for when the solution algorithm decides
-- to have iterated the node often enough.
--
-- When domain is a 'BoundedMeetSemilattice'/'BoundedLattice',
-- the simplest abortion function would be to constantly return
-- top.
--
-- As is the case for LiftedFunc and ChangeDetector, this
-- carries little semantic meaning if viewed in isolation, so here are a
-- few examples for how the synonym expands:
--
--
-- AbortionFunction Int ~ Int -> Int
-- AbortionFunction (String -> Int) ~ String -> Int -> Int
-- AbortionFunction (a -> b -> c -> PowerSet) ~ a -> b -> c -> PowerSet -> PowerSet
--
--
-- E.g., the current value of the point is passed in (the tuple (a,
-- b, c, PowerSet)) and the function returns an appropriate
-- conservative approximation in that point.
type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain)
-- | Aborts iteration of a value by constantly returning the
-- top element of the assumed BoundedMeetSemiLattice of the
-- ReturnType.
abortWithTop :: forall domain. Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain) => BoundedMeetSemiLattice (ReturnType domain) => AbortionFunction domain
-- | Expresses that iteration should or shouldn't stop after a point has
-- been iterated a finite number of times.
data IterationBound domain
-- | Will keep on iterating until a precise, yet conservative approximation
-- has been reached. Make sure that your domain satisfies the
-- ascending chain condition, e.g. that fixed-point iteration
-- always comes to a halt!
NeverAbort :: IterationBound domain
-- | For when your domain doesn't satisfy the ascending chain
-- condition or when you are sensitive about solution performance.
--
-- The Integer determines the maximum number of iterations of a
-- single point of a Node (with which an entire function with many
-- points may be associated) before iteration aborts in that point by
-- calling the supplied AbortionFunction. The responsibility of
-- the AbortionFunction is to find a sufficiently conservative
-- approximation for the current value at that point.
--
-- When your ReturnType is an instance of
-- BoundedMeetSemiLattice, abortWithTop might be a
-- worthwhile option. A more sophisticated solution would trim the
-- current value to a certain cut-off depth, depending on the first
-- parameter, instead.
AbortAfter :: Int -> (AbortionFunction domain) -> IterationBound domain
zoomIORef :: State s a -> ReaderT (IORef s) IO a
zoomReferencedPoints :: State (IntArgsMonoSet (Products (ParamTypes domain))) a -> ReaderT (Env graph domain) IO a
zoomUnstable :: State (IntArgsMonoSet (Products (ParamTypes domain))) a -> ReaderT (Env graph domain) IO a
enqueueUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int -> k -> ReaderT (Env graph domain) IO ()
deleteUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int -> k -> ReaderT (Env graph domain) IO ()
highestPriorityUnstableNode :: k ~ Products (ParamTypes domain) => MonoMapKey k => ReaderT (Env graph domain) IO (Maybe (Int, k))
withCall :: Datafixable (DependencyM graph domain) => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO a -> ReaderT (Env graph domain) IO a
-- | The first of the two major functions of this module.
--
-- recompute node args iterates the value of the passed
-- node at the point args by invoking its transfer
-- function. It does so in a way that respects the IterationBound.
--
-- This function is not exported, and is only called by work and
-- dependOn, for when the iteration strategy decides that the
-- node needs to be (and can be) re-iterated. It performs
-- tracking of which Nodes the transfer function depended on, do
-- that the worklist algorithm can do its magic.
recompute :: forall domain graph dom cod depm. dom ~ ParamTypes domain => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph => Datafixable depm => Int -> Products dom -> ReaderT (Env graph domain) IO cod
dependOn :: forall domain graph. Datafixable (DependencyM graph domain) => GraphRef graph => Node -> LiftedFunc domain (DependencyM graph domain)
-- | Compute an optimistic approximation for a point of a given node that
-- is as precise as possible, given the other points of that node we
-- already computed.
--
-- E.g., it is always valid to return bottom from this, but in
-- many cases we can be more precise since we possibly have computed
-- points for the node that are lower bounds to the current point.
optimisticApproximation :: GraphRef graph => Datafixable (DependencyM graph domain) => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain)
-- | scheme 1 (see
-- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).
--
-- Let the worklist algorithm figure things out.
scheme1 :: GraphRef graph => Datafixable (DependencyM graph domain) => Maybe (ReturnType domain) -> Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain)
-- | scheme 2 (see
-- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).
--
-- Descend into <math> nodes when there is no cycle to discover the
-- set of reachable nodes as quick as possible. Do *not* descend into
-- unstable, non-(bot) nodes.
scheme2 :: GraphRef graph => Datafixable (DependencyM graph domain) => Maybe (ReturnType domain) -> Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain)
-- | As long as the supplied Maybe expression returns "Just _", the
-- loop body will be called and passed the value contained in the
-- Just. Results are discarded.
--
-- Taken from whileJust_.
whileJust_ :: Monad m => m (Maybe a) -> (a -> m b) -> m ()
-- | Defined as 'work = whileJust_ highestPriorityUnstableNode (uncurry
-- recompute)'.
--
-- Tries to dequeue the highestPriorityUnstableNode and
-- recomputes the value of one of its unstable points,
-- until the worklist is empty, indicating that a fixed-point has been
-- reached.
work :: GraphRef graph => Datafixable (DependencyM graph domain) => ReaderT (Env graph domain) IO ()
-- | 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.
solveProblem :: forall domain graph. GraphRef graph => Datafixable (DependencyM graph domain) => DataFlowProblem (DependencyM graph domain) -> Density graph -> IterationBound domain -> Node -> domain
-- | 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.
evalDenotation :: forall domain. Datafixable (DependencyM Ref domain) => ProblemBuilder (DependencyM Ref domain) (LiftedFunc domain (DependencyM Ref domain)) -> IterationBound domain -> domain
instance GHC.Base.Monad (Datafix.Worklist.Internal.DependencyM graph domain)
instance GHC.Base.Applicative (Datafix.Worklist.Internal.DependencyM graph domain)
instance GHC.Base.Functor (Datafix.Worklist.Internal.DependencyM graph domain)
instance (Datafix.Worklist.Internal.Datafixable (Datafix.Worklist.Internal.DependencyM graph domain), Datafix.Worklist.Graph.GraphRef graph) => Datafix.Description.MonadDependency (Datafix.Worklist.Internal.DependencyM graph domain)
-- | This module provides the solveProblem function, which solves
-- the description of a DataFlowProblem by employing a worklist
-- algorithm.
module Datafix.Worklist
-- | 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.
data DependencyM graph domain a
-- | 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
--
--
-- - 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)
-- - 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.
-- - 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.
--
type Datafixable m = (Currying (ParamTypes (Domain m)) (ReturnType (Domain m)), Currying (ParamTypes (Domain m)) (m (ReturnType (Domain m))), Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool), Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m)), MonoMapKey (Products (ParamTypes (Domain m))), BoundedJoinSemiLattice (ReturnType (Domain m)))
-- | 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.
data Density graph
[Sparse] :: Density Ref
[Dense] :: Node -> Density Ref
-- | Expresses that iteration should or shouldn't stop after a point has
-- been iterated a finite number of times.
data IterationBound domain
-- | Will keep on iterating until a precise, yet conservative approximation
-- has been reached. Make sure that your domain satisfies the
-- ascending chain condition, e.g. that fixed-point iteration
-- always comes to a halt!
NeverAbort :: IterationBound domain
-- | For when your domain doesn't satisfy the ascending chain
-- condition or when you are sensitive about solution performance.
--
-- The Integer determines the maximum number of iterations of a
-- single point of a Node (with which an entire function with many
-- points may be associated) before iteration aborts in that point by
-- calling the supplied AbortionFunction. The responsibility of
-- the AbortionFunction is to find a sufficiently conservative
-- approximation for the current value at that point.
--
-- When your ReturnType is an instance of
-- BoundedMeetSemiLattice, abortWithTop might be a
-- worthwhile option. A more sophisticated solution would trim the
-- current value to a certain cut-off depth, depending on the first
-- parameter, instead.
AbortAfter :: Int -> (AbortionFunction domain) -> IterationBound domain
-- | 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.
solveProblem :: forall domain graph. GraphRef graph => Datafixable (DependencyM graph domain) => DataFlowProblem (DependencyM graph domain) -> Density graph -> IterationBound domain -> Node -> domain
-- | 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.
evalDenotation :: forall domain. Datafixable (DependencyM Ref domain) => ProblemBuilder (DependencyM Ref domain) (LiftedFunc domain (DependencyM Ref domain)) -> IterationBound domain -> domain
-- | This is the top-level, import-all, kitchen sink module.
--
-- Look at Datafix.Tutorial for a tour guided by use cases.
module Datafix
-- | What is This?
--
-- The purpose of datafix is to separate declaring data-flow
-- problems from computing their solutions by fixed-point
-- iteration.
--
-- The need for this library arose when I was combining two analyses
-- within GHC for my master's thesis. I recently held a talk on
-- that topic, feel free to click through if you want to know the
-- details.
--
-- You can think of data-flow problems as problems that are solvable by
-- dynamic programming or memoization, except that the
-- dependency graph of data-flow problems doesn't need to be acyclic.
--
-- Data-flow problems are declared with the primitives in
-- Datafix.Description and solved by
-- Datafix.Worklist.solveProblem.
--
-- With that out of the way, let's set in place the GHCi environment of
-- our examples:
--
--
-- >>> :set -XScopedTypeVariables
--
-- >>> :set -XTypeApplications
--
-- >>> :set -XTypeFamilies
--
-- >>> import Datafix
--
-- >>> import Data.Proxy (Proxy (..))
--
-- >>> import Algebra.Lattice (JoinSemiLattice (..), BoundedJoinSemiLattice (..))
--
-- >>> import Numeric.Natural
--
--
-- Use Case: Solving Recurrences
--
-- Let's start out by computing the fibonacci series:
--
--
-- >>> :{
-- fib :: Natural -> Natural
-- fib 0 = 0
-- fib 1 = 1
-- fib n = fib (n-1) + fib (n-2)
-- :}
--
--
--
-- >>> fib 3
-- 2
--
-- >>> fib 10
-- 55
--
--
-- Bring your rabbits to the vet while you can still count them...
--
-- Anyway, the fibonacci series is a typical problem exhibiting
-- overlapping subproblems. As a result, our fib function
-- from above scales badly in the size of its input argument n.
-- Because we repeatedly recompute solutions, the time complexity of our
-- above function is in <math>!
--
-- We can do better by using dynamic programming or
-- memoization to keep a cache of already computed sub-problems,
-- which helps computing the <math>th item in <math> time and
-- space:
--
--
-- >>> :{
-- fib2 :: Natural -> Natural
-- fib2 n = fibs !! fromIntegral n
-- where
-- fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
-- :}
--
--
--
-- >>> fib2 3
-- 2
--
-- >>> fib2 10
-- 55
--
--
-- That's one of Haskell's pet issues: Expressing dynamic programs as
-- lists through laziness.
--
-- As promised in the previous section, we can do the same using
-- datafix. First, we need to declare a transfer function
-- that makes the data dependencies for the recursive case explicit, as
-- if we were using fix to eliminate the recursion:
--
--
-- >>> :{
-- transferFib
-- :: forall m
-- . (MonadDependency m, Domain m ~ Natural)
-- => Node
-- -> LiftedFunc Natural m
-- transferFib (Node 0) = return 0
-- transferFib (Node 1) = return 1
-- transferFib (Node n) = do
-- a <- dependOn @m (Node (n-1))
-- b <- dependOn @m (Node (n-2))
-- return (a + b)
-- :}
--
--
-- MonadDependency contains a single primitive dependOn for
-- that purpose.
--
-- Every point of the fibonacci series is modeled as a seperate
-- Node of the data-flow graph. By looking at the definition of
-- LiftedFunc, we can see that LiftedFunc Natural m ~ m
-- Natural, so for our simple Natural Domain, the
-- transfer function is specified directly in MonadDependency.
--
-- Note that indeed we eliminated explicit recursion in
-- transferFib. This allows the solution algorithm to track and
-- discover dependencies of the transfer function as it is executed!
--
-- With our transfer function (which denotes data-flow nodes in the
-- semantics of Naturals) in place, we can construct a
-- DataFlowProblem:
--
--
-- >>> :{
-- fibDfp :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m
-- fibDfp = DFP transferFib (const (eqChangeDetector @(Domain m)))
-- :}
--
--
-- The eqChangeDetector is important for cyclic dependency graphs
-- and makes sure we detect when a fixed-point has been reached.
--
-- That's it for describing the data-flow problem of fibonacci numbers.
-- We can ask Datafix.Worklist.solveProblem for a
-- solution in a minute.
--
-- The solveProblem solver demands an instance of
-- BoundedJoinSemiLattice on the Domain for when the
-- data-flow graph is cyclic. We conveniently delegate to the total
-- Ord instance for Natural, knowing that its semantic
-- interpretation is irrelevant to us:
--
--
-- >>> instance JoinSemiLattice Natural where (\/) = max
--
-- >>> instance BoundedJoinSemiLattice Natural where bottom = 0
--
--
-- And now the final incantation of the solver:
--
--
-- >>> solveProblem fibDfp Sparse NeverAbort (Node 10)
-- 55
--
--
-- This will also execute in <math> space and time, all without
-- worrying about a smart solution strategy involving how to tie knots or
-- allocate vectors. Granted, this doesn't really pay off for simple
-- problems like computing fibonacci numbers because of the boilerplate
-- involved and the somewhat devious type-level story, but the intended
-- use case is that of static analysis of programming languages.
--
-- Before I delegate you to a blog post about strictness analysis, we
-- will look at a more devious reccurence relation with actual cycles in
-- the resulting data-flow graph.
--
-- Use Case: Solving Cyclic Recurrences
--
-- The recurrence relation describing fibonacci numbers admits a clear
-- plan of how to compute a solution, because the dependency graph is
-- obviously acyclic: To compute the next new value of the sequence, only
-- the prior two values are needed.
--
-- This is not true of the following reccurence relation:
--
-- <math>
--
-- The identity function is the only solution to this, but it is unclear
-- how we could arrive at that conclusion just by translating that
-- relation into Haskell:
--
--
-- >>> :{
-- f n
-- | even n = 2 * f (n `div` 2)
-- | odd n = f (n + 1) - 1
-- :}
--
--
-- Imagine a call f 1: This will call f 2 recursively,
-- which again will call f 1. We hit a cyclic dependency!
--
-- Fortunately, we can use datafix to compute the solution by
-- fixed-point iteration (which assumes monotonicity of the function to
-- approximate):
--
--
-- >>> :{
-- transferF
-- :: forall m
-- . (MonadDependency m, Domain m ~ Int)
-- => Node
-- -> LiftedFunc Int m
-- transferF (Node n)
-- | even n = (* 2) <$> dependOn @m (Node (n `div` 2))
-- | odd n = (subtract 1) <$> dependOn @m (Node (n + 1))
-- :}
--
--
--
-- >>> :{
-- fDfp :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m
-- fDfp = DFP transferF (const (eqChangeDetector @(Domain m)))
-- :}
--
--
-- Specification of the data-flow problem works the same as for the
-- fib function.
--
-- As for Natural, we need an instance of
-- BoundedJoinSemiLattice for Int to compute a solution:
--
--
-- >>> instance JoinSemiLattice Int where (\/) = max
--
-- >>> instance BoundedJoinSemiLattice Int where bottom = minBound
--
--
-- Now it's just a matter of calling solveProblem with the right
-- parameters:
--
--
-- >>> solveProblem fDfp Sparse NeverAbort (Node 0)
-- 0
--
-- >>> solveProblem fDfp Sparse NeverAbort (Node 5)
-- 5
--
-- >>> solveProblem fDfp Sparse NeverAbort (Node 42)
-- 42
--
-- >>> solveProblem fDfp Sparse NeverAbort (Node (-10))
-- -10
--
--
-- Note how the specification of the data-flow problem was as
-- unexciting as it was for the fibonacci sequence (modulo boilerplate),
-- yet the recurrence we solved was pretty complicated already.
--
-- Of course, encoding the identity function this way is inefficient. But
-- keep in mind that in general, we don't know the solution to a
-- particular recurrence! It's always possible to solve the recurrence by
-- hand upfront, but that's trading precious developer time for what
-- might be a throw-away problem anyway.
--
-- Which brings us to the prime and final use case...
--
-- Use Case: Static Analysis
--
-- Recurrence equations occur all the time in denotational
-- semantics and static data-flow analysis.
--
-- For every invocation of the compiler, for every module, for every
-- analysis within the compiler, a recurrence relation representing
-- program semantics is to be solved. Naturally, we can't task a human
-- with solving a bunch of complicated recurrences everytime we hit
-- compile.
--
-- In the imperative world, it's common-place to have some kind of
-- fixed-point iteration framework carry out the iteration of the
-- data-flow graph, but I could not find a similar abstraction for
-- functional programming languages yet. Analyses for functional
-- languages are typically carried out as iterated traversals of the
-- syntax tree, but that is unsatisfying for a number of reasons:
--
--
-- - Solution logic of the data-flow problem is intertwined with its
-- specification.
-- - Solution logic is duplicated among multiple analyses, violating
-- DRY.
-- - A consequence of the last two points is that performance tweaks
-- have to be adapted for every analysis separately. In the case of GHC's
-- Demand Analyser, going from chaotic iteration (which corresponds to
-- naive iterated tree traversals) to an iteration scheme that caches
-- results of inner let-bindings, annotations to the syntax tree are
-- suddenly used like State threads, which makes the analysis
-- logic even more complex than it already was.
--
--
-- So, I can only encourage any compiler dev who wants to integrate
-- static analyses into their compiler to properly specify the data-flow
-- problems in terms of datafix and leave the intricacies of
-- finding a good iteration order to this library :)
module Datafix.Tutorial