-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Fixing data-flow problems
--
-- Fixing data-flow problems in expression trees. This should be useful
-- if you want to write optimizations for your favorite programming
-- language. See the Tutorial module for an introduction. After that, you
-- might want to take a look at the `examples/` folder in the
-- repository.
@package datafix
@version 0.0.1.0
-- | 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 {
-- | The particular ordered map implementation to use for the key type
-- k.
--
-- The default implementation delegates to POMap.
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
instance Datafix.MonoMap.MonoMapKey ()
instance Datafix.MonoMap.MonoMapKey GHC.Types.Int
-- | Universally quantified constraints, until we have
-- -XQuantifiedConstraints.
module Datafix.Utils.Constraints
data Dict :: Constraint -> Type
[Dict] :: c => Dict c
newtype a :- b
Sub :: (a => Dict b) -> (:-) a b
-- | Given that a :- b, derive something that needs a context
-- b, using the context a
(\\) :: a => (b => r) -> (a :- b) -> r
infixl 1 \\
-- | A representation of the quantified constraint forall a. p a.
type family Forall (p :: k -> Constraint) :: Constraint
inst :: forall p a. Forall p :- p a
instance forall k (p :: k -> GHC.Types.Constraint). p (Datafix.Utils.Constraints.Skolem p) => Datafix.Utils.Constraints.Forall_ p
-- | 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)
type family All (p :: k -> Constraint) (as :: [k]) :: Constraint
-- | On Booleans
type family If (b :: Bool) (l :: k) (r :: k) :: k
-- | On Lists
type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l
-- | Version of Foldr taking a defunctionalised argument so that
-- we can use partially applied functions.
type family Foldr' (c :: Function k (Function l l -> *) -> *) (n :: l) (as :: [k]) :: l
type family Map (f :: Function k l -> *) (as :: [k]) :: [l]
data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
type family Constant (b :: l) (as :: [k]) :: [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.
type family Products (as :: [*])
-- | IsBase t is 'True whenever t is *not* a
-- function space.
type family IsBase (t :: *) :: Bool
-- | 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
type family ParamTypes (t :: *) :: [*]
type family ParamTypes' (t :: *) :: [*]
type family ReturnType (t :: *) :: *
type family ReturnType' (t :: *) :: *
-- | 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 -> *
type family Apply (t :: Function k l -> *) (u :: k) :: l
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
-- | Common definitions for defining data-flow problems, defining
-- infrastructure around the notion of Domain.
module Datafix.Common
-- | 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)
-- | 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
-- | 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
class (Monad m, Datafixable (Domain m)) => MonadDomain m where {
-- | 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.
type family Domain m :: *;
}
-- | 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
--
--
-- - 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.
-- - 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.
-- - 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 domain = (Forall (Currying (ParamTypes domain)), MonoMapKey (Products (ParamTypes domain)), BoundedJoinSemiLattice (ReturnType domain))
evalAt :: forall f arr. Currying (ParamTypes arr) (ReturnType arr) => Functor f => f arr -> Products (ParamTypes arr) -> f (ReturnType arr)
( Functor f => f arr -> Products (ParamTypes arr) -> f (ReturnType arr)
-- | Primitives for describing a data-flow problem in a declarative
-- manner. This module requires you to manage assignment of Nodes
-- in the data-flow graph to denotations by hand. If you're looking for a
-- safer approach suited for static analysis, have a look at
-- Datafix.Denotational.
--
-- Import this module transitively through Datafix and get access
-- to Datafix.Worklist for functions that compute solutions to
-- your DataFlowFrameworks.
module Datafix.Explicit
-- | 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
-- | 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 DataFlowFramework m
DFF :: !Node -> LiftedFunc (Domain m) m -> !Node -> ChangeDetector (Domain m) -> DataFlowFramework m
-- | A transfer function per each Node of the modeled data-flow
-- problem.
[dffTransfer] :: DataFlowFramework 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.
[dffDetectChange] :: DataFlowFramework 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 DataFlowFramework with this
-- transferFib function:
--
--
-- >>> :{
-- dataFlowFramework :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowFramework m
-- dataFlowFramework = DFF 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 MonadDomain m => MonadDependency 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
instance GHC.Show.Show Datafix.Explicit.Node
instance GHC.Classes.Ord Datafix.Explicit.Node
instance GHC.Classes.Eq Datafix.Explicit.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)
-- | Provides an alternative method (to
-- MonadDependency/Datafix.Explicit) of formulating
-- data-flow problems as a Denotation built in the context of
-- MonadDatafix. This offers better usability for defining static
-- analyses, as the problem of allocating nodes in the data-flow graph is
-- abstracted from the user.
module Datafix.Denotational
-- | Builds on an associated DepM that is a MonadDomain (like
-- any MonadDependency) by providing a way to track dependencies
-- without explicit Node management. Essentially, this allows to
-- specify a build plan for a DataFlowFramework through calls to
-- datafix in analogy to fix or mfix.
class (Monad m, MonadDomain (DepM m)) => MonadDatafix m where {
-- | The monad in which data dependencies are expressed. Can and will be
-- instantiated to some MonadDependency, if you choose to go
-- through FrameworkBuilder.
type family DepM m :: * -> *;
}
-- | 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 m.
--
-- Finally, the arbitrary a value is returned, in analogy to
-- a in mfix :: MonadFix m => (a -> m a) ->
-- m a.
datafix :: (MonadDatafix m, dom ~ Domain (DepM m)) => ChangeDetector dom -> (LiftedFunc dom (DepM m) -> m (a, LiftedFunc dom (DepM m))) -> m a
-- | Shorthand that partially applies datafix to an
-- eqChangeDetector.
datafixEq :: forall m dom a. MonadDatafix m => dom ~ Domain (DepM m) => Eq (ReturnType dom) => (LiftedFunc dom (DepM m) -> m (a, LiftedFunc dom (DepM m))) -> m a
-- | A denotation of some syntactic entity in a semantic domain,
-- built in a some MonadDatafix context.
type Denotation domain func = forall m. (MonadDatafix m, domain ~ Domain (DepM m)) => m (LiftedFunc func (DepM m))
-- | Builds a DataFlowFramework for a Denotational
-- formulation in terms of MonadDatafix. Effectively reduces
-- descriptions from Datafix.Denotational to ones from
-- Datafix.Explicit, so that solvers such as
-- Datafix.Worklist only have to provide an interpreter for
-- MonadDependency.
module Datafix.FrameworkBuilder
-- | Constructs a build plan for a DataFlowFramework by tracking
-- allocation of Nodes mapping to ChangeDetectors and
-- transfer functions.
data FrameworkBuilder m a
-- | (root, max, dff) = buildFramework builder executes the build
-- plan specified by builder and returns the resulting
-- DataFlowFramework dff, as well as the root
-- Node denoting the transfer function returned by the
-- FrameworkBuilder action and the maximum node of the
-- problem as a proof for its denseness.
buildFramework :: forall m a. MonadDependency m => (forall md. (MonadDatafix md, DepM md ~ m) => md a) -> (a, Node, DataFlowFramework m)
instance GHC.Base.Monad (Datafix.FrameworkBuilder.FrameworkBuilder m)
instance GHC.Base.Applicative (Datafix.FrameworkBuilder.FrameworkBuilder m)
instance GHC.Base.Functor (Datafix.FrameworkBuilder.FrameworkBuilder m)
instance Datafix.Explicit.MonadDependency m => Datafix.Denotational.MonadDatafix (Datafix.FrameworkBuilder.FrameworkBuilder 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 DataFlowFramework 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
-- domain => (forall s. DataFlowFramework (DependencyM s graph
-- domain)) -> ... and have to instead have the isomorphic
-- (forall s r. (Datafixable domain => r) -> r) -> (forall
-- s. DataFlowFramework (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.buildDenotation 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 :: !DataFlowFramework (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 -> !DataFlowFramework (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)) -> DataFlowFramework (DependencyM graph domain) -> IterationBound domain -> IO (graph domain) -> IO (Env graph domain)
-- | 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 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 domain => Int -> Products dom -> ReaderT (Env graph domain) IO cod
dependOn :: forall domain graph depm. depm ~ DependencyM graph domain => Datafixable domain => GraphRef graph => Node -> LiftedFunc domain depm
-- | 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 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 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 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 domain => ReaderT (Env graph domain) IO ()
-- | Computes the (pure) solution of the DependencyM action
-- act specified in the last parameter. act may
-- reference (via dependOn) Nodes of the
-- DataFlowFramework dff's fixed-point, specified as the
-- first parameter.
--
-- dff's fixed-point is determined by its transfer functions,
-- and solveProblem will make sure that all (relevant)
-- Nodes will have reached their fixed-point according to their
-- transfer function before computing the solution for act.
--
-- We try to be smart in saving unnecessary iterations of transfer
-- functions by employing a worklist algorithm. For function domains,
-- where each Node denotes a monotone function, each point's
-- dependencies' will be tracked individually.
--
-- Apart from dff and act, the Density of the
-- data-flow graph and the IterationBound can be specified. Pass
-- Sparse and NeverAbort when in doubt.
--
-- If your problem only has finitely many different Nodes ,
-- consider using the FrameworkBuilder 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.
--
-- See Datafix.Tutorial and the examples/ subfolder for
-- examples.
solveProblem :: forall domain graph a. GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) -> Density graph -> IterationBound domain -> DependencyM graph domain a -> a
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.Common.Datafixable domain => Datafix.Common.MonadDomain (Datafix.Worklist.Internal.DependencyM graph domain)
instance (Datafix.Common.Datafixable domain, Datafix.Worklist.Graph.GraphRef graph) => Datafix.Explicit.MonadDependency (Datafix.Worklist.Internal.DependencyM graph domain)
-- | Bridges the Datafix.Worklist solver for
-- DataFlowFrameworks (solveProblem) with the
-- Datafix.Denotational approach, using MonadDatafix to
-- describe a Denotation.
module Datafix.Worklist.Denotational
-- | evalDenotation denot ib returns a value in domain
-- that is described by the denotation denot.
--
-- It does so by building up the DataFlowFramework 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, domain ~ Domain (DepM m) is for.
evalDenotation :: forall domain func. Datafixable domain => Forall (Currying (ParamTypes func)) => Denotation domain func -> IterationBound domain -> func
-- | This module provides the solveProblem function, which solves
-- the description of a DataFlowFramework by employing a worklist
-- algorithm. There's also an interpreter for Denotational
-- problems in the form of evalDenotation.
module Datafix.Worklist
-- | The concrete MonadDependency for this worklist-based solver.
--
-- This essentially tracks the current approximation of the solution to
-- the DataFlowFramework as mutable state while
-- solveProblem makes sure we will eventually halt with a
-- conservative approximation.
data DependencyM graph domain a
-- | 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 the (pure) solution of the DependencyM action
-- act specified in the last parameter. act may
-- reference (via dependOn) Nodes of the
-- DataFlowFramework dff's fixed-point, specified as the
-- first parameter.
--
-- dff's fixed-point is determined by its transfer functions,
-- and solveProblem will make sure that all (relevant)
-- Nodes will have reached their fixed-point according to their
-- transfer function before computing the solution for act.
--
-- We try to be smart in saving unnecessary iterations of transfer
-- functions by employing a worklist algorithm. For function domains,
-- where each Node denotes a monotone function, each point's
-- dependencies' will be tracked individually.
--
-- Apart from dff and act, the Density of the
-- data-flow graph and the IterationBound can be specified. Pass
-- Sparse and NeverAbort when in doubt.
--
-- If your problem only has finitely many different Nodes ,
-- consider using the FrameworkBuilder 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.
--
-- See Datafix.Tutorial and the examples/ subfolder for
-- examples.
solveProblem :: forall domain graph a. GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) -> Density graph -> IterationBound domain -> DependencyM graph domain a -> a
-- | evalDenotation denot ib returns a value in domain
-- that is described by the denotation denot.
--
-- It does so by building up the DataFlowFramework 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, domain ~ Domain (DepM m) is for.
evalDenotation :: forall domain func. Datafixable domain => Forall (Currying (ParamTypes func)) => Denotation domain func -> IterationBound domain -> func
-- | This is the top-level, import-all, kitchen sink module.
--
-- Look at Datafix.Tutorial for a tour guided by use cases.
module Datafix
-- | The particular ordered map implementation to use for the key type
-- k.
--
-- The default implementation delegates to POMap.
type family MonoMap k = (r :: * -> *) | r -> k
type family Apply (t :: Function k l -> *) (u :: k) :: l
data Constant1 :: * -> Function b a -> *
data Constant0 :: Function a (Function b a -> *) -> *
data Function :: * -> * -> *
-- | 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
type family ReturnType' (t :: *) :: *
type family ReturnType (t :: *) :: *
type family ParamTypes' (t :: *) :: [*]
-- | 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
type family ParamTypes (t :: *) :: [*]
-- | IsBase t is 'True whenever t is *not* a
-- function space.
type family IsBase (t :: *) :: Bool
-- | 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.
type family Products (as :: [*])
-- | Arrows [a1,..,an] r corresponds to a1 -> .. -> an
-- -> r
type Arrows (as :: [*]) (r :: *) = Foldr (->) r as
type family Constant (b :: l) (as :: [k]) :: [l]
data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
-- | Version of Foldr taking a defunctionalised argument so that
-- we can use partially applied functions.
type family Foldr' (c :: Function k (Function l l -> *) -> *) (n :: l) (as :: [k]) :: l
-- | On Lists
type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l
-- | On Booleans
type family If (b :: Bool) (l :: k) (r :: k) :: k
-- | 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)
type family All (p :: k -> Constraint) (as :: [k]) :: Constraint
arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func
-- | 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 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
-- DataFlowFramework:
--
--
-- >>> :{
-- fibDff :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m
-- fibDff = DFF 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 fibDff Sparse NeverAbort (dependOn @(DependencyM _ Natural) (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))
-- :}
--
--
--
-- >>> :{
-- fDff :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowFramework m
-- fDff = DFF 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 fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 0))
-- 0
--
-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 5))
-- 5
--
-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 42))
-- 42
--
-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (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 :)
--
-- Comparison to Datalog/Soufflé
--
-- In its most declarative form, datafix is an embedded DSL for
-- specifying static analyses. In that regard, it is really similar to
-- Soufflé, only that Soufflé uses an external DSL (a Datalog
-- dialect) to specify the analysis. The resulting compiled executable
-- needs to run in a separate process and gets the facts of the input
-- program encoded in datalog facts. datafix analyses, on the
-- other hand, will be compiled into the host program and don't need an
-- additional communication layer.
module Datafix.Tutorial