diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,7 @@ +# Change log + +`datafix` follows the [PVP][1]. +The change log is available [on GitHub][2]. + +[1]: https://pvp.haskell.org/ +[2]: https://github.com/sgraf812/datafix/releases diff --git a/datafix.cabal b/datafix.cabal --- a/datafix.cabal +++ b/datafix.cabal @@ -1,22 +1,29 @@ name: datafix -version: 0.0.0.1 +version: 0.0.0.2 synopsis: Fixing data-flow problems -description: Fixing data-flow problems in expression trees +description: 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](https://github.com/sgraf812/datafix/tree/master/examples). + license: ISC license-file: LICENSE author: Sebastian Graf maintainer: sgraf1337@gmail.com -copyright: © 2017 Sebastian Graf +copyright: © 2018 Sebastian Graf homepage: https://github.com/sgraf812/datafix bug-reports: https://github.com/sgraf812/datafix/issues category: Compiler build-type: Custom stability: alpha (experimental) -cabal-version: >=1.24 +cabal-version: 1.24 extra-source-files: + CHANGELOG.md README.md stack.yaml exprs/const.hs @@ -45,18 +52,23 @@ ghc-options: -Wall hs-source-dirs: src exposed-modules: Datafix - Datafix.Tutorial - Datafix.Description + Datafix.Common + Datafix.Denotational + Datafix.Explicit Datafix.MonoMap Datafix.NodeAllocator Datafix.ProblemBuilder + Datafix.Tutorial + Datafix.Utils.Constraints Datafix.Utils.TypeLevel Datafix.Worklist + Datafix.Worklist.Denotational Datafix.Worklist.Graph Datafix.Worklist.Graph.Dense Datafix.Worklist.Graph.Sparse Datafix.Worklist.Internal other-modules: + Datafix.Entailments Datafix.Utils.GrowableVector Datafix.IntArgsMonoMap Datafix.IntArgsMonoSet @@ -133,7 +145,7 @@ benchmark benchmarks type: exitcode-stdio-1.0 default-language: Haskell2010 - ghc-options: -Wall -O2 -threaded -rtsopts -with-rtsopts=-N + ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N hs-source-dirs: bench examples main-is: Main.hs other-modules: Sum diff --git a/examples/Analyses/AdHocStrAnal.hs b/examples/Analyses/AdHocStrAnal.hs --- a/examples/Analyses/AdHocStrAnal.hs +++ b/examples/Analyses/AdHocStrAnal.hs @@ -1,113 +1,113 @@ -module Analyses.AdHocStrAnal (analyse) where - -import Algebra.Lattice -import Analyses.StrAnal.Arity -import Analyses.StrAnal.Strictness - -import CoreSyn -import Id -import Var -import VarEnv - -analyse :: CoreExpr -> StrLattice -analyse e = analExpr emptyVarEnv e 0 - -applyWhen :: Bool -> (a -> a) -> a -> a -applyWhen True f = f -applyWhen False _ = id - -analExpr :: VarEnv StrType -> CoreExpr -> Arity -> StrLattice -analExpr env expr arity = - case expr of - Lit _ -> emptyStrLattice - Type _ -> emptyStrLattice - -- Coercions are irrelevant to Strictness Analysis: - -- 'emptyStrLattice' is already the 'top' element, - -- so it's a safe approximation. - Coercion _ -> emptyStrLattice - Tick _ e -> analExpr env e arity - Cast e _ -> analExpr env e arity - App f a -> - let - StrLattice (fTy, fAnns) = analExpr env f (arity + 1) - (argStr, fTy') = overArgs unconsArgStr fTy - argArity = - case argStr of - -- It's unfortunate that we don't have the type available to - -- trim this... But it doesn't hurt either. - HyperStrict -> Arity maxBound - Lazy -> 0 - Strict n -> n - StrLattice (aTy, aAnns) = analExpr env a argArity - in mkStrLattice (aTy `bothStrType` fTy') (fAnns \/ aAnns) - Var id_ - | isLocalId id_ -> - let - rhsType = case lookupVarEnv env id_ of - Just ty - -- 'ty' is a safe approximation for a call with 'idArity' at - -- minimum. - -- Note that 'Arity' is 'Op' ordered. - | arity <= Arity (idArity id_) -> ty - _ -> emptyStrType - in mkStrLattice (unitStrType id_ (Strict arity) `bothStrType` rhsType) emptyAnnotations - | otherwise -> emptyStrLattice - Lam id_ body - | isTyVar id_ -> analExpr env body arity - | otherwise -> - let - StrLattice (ty1, anns) = analExpr env body (0 /\ (arity-1)) - (argStr, ty2) = peelFV id_ ty1 - anns' = annotate id_ argStr anns - ty3 = modifyArgs (consArgStr argStr) ty2 - ty4 = applyWhen (arity == 0) lazifyStrType ty3 - in mkStrLattice ty4 anns' - Case scrut bndr _ alts -> - let - transferAlt (_, bndrs, alt) = - peelAndAnnotateFVs bndrs (analExpr env alt arity) - StrLattice (altTy, altAnns) = - peelAndAnnotateFV bndr . joins . map transferAlt $ alts - StrLattice (scrutTy, scrutAnns) = analExpr env scrut 0 - in mkStrLattice (scrutTy `bothStrType` altTy) (scrutAnns \/ altAnns) - Let bind body -> - let - -- we assume a single call with `idArity` for our approximation - (rhsAnns, env') = case bind of - NonRec id_ rhs - | StrLattice (ty, anns) <- analExpr env rhs (Arity (idArity id_)) - -> (anns, extendVarEnv env id_ ty) - Rec binds -> fixBinds env binds - bodyLatt = analExpr env' body arity - StrLattice (bodyTy, bodyAnns) = peelAndAnnotateFVs (bindersOf bind) bodyLatt - in mkStrLattice bodyTy (bodyAnns \/ rhsAnns) - -fixBinds :: VarEnv StrType -> [(Id, CoreExpr)] -> (Annotations, VarEnv StrType) -fixBinds env binds = mergeWithLatts stableLatts - where - mergeWithLatts :: [StrLattice] -> (Annotations, VarEnv StrType) - mergeWithLatts latts = foldr merger (emptyAnnotations, env) (zip binds latts) - - merger :: ((Id, CoreExpr), StrLattice) -> (Annotations, VarEnv StrType) -> (Annotations, VarEnv StrType) - merger ((id_, _), StrLattice (ty, anns)) (restAnns, env') = - (restAnns \/ anns, extendVarEnv env' id_ ty) - - latts0 :: [StrLattice] - latts0 = map (const bottom) binds - - approximations :: [[StrLattice]] - approximations = iterate (iter . snd . mergeWithLatts) latts0 - - stable :: ([StrLattice], [StrLattice]) -> Bool - stable (old, new) = map strType old == map strType new - - stableLatts :: [StrLattice] - stableLatts = snd . head . filter stable $ zip approximations (tail approximations) - - iter env' = snd (foldr iterBind (env', []) binds) - - iterBind (id_, rhs) (env', latts) = - let - latt = analExpr env' rhs (Arity (idArity id_)) - env'' = extendVarEnv env' id_ (strType latt) - in (env'', latt:latts) +module Analyses.AdHocStrAnal (analyse) where + +import Algebra.Lattice +import Analyses.StrAnal.Arity +import Analyses.StrAnal.Strictness + +import CoreSyn +import Id +import Var +import VarEnv + +analyse :: CoreExpr -> StrLattice +analyse e = analExpr emptyVarEnv e 0 + +applyWhen :: Bool -> (a -> a) -> a -> a +applyWhen True f = f +applyWhen False _ = id + +analExpr :: VarEnv StrType -> CoreExpr -> Arity -> StrLattice +analExpr env expr arity = + case expr of + Lit _ -> emptyStrLattice + Type _ -> emptyStrLattice + -- Coercions are irrelevant to Strictness Analysis: + -- 'emptyStrLattice' is already the 'top' element, + -- so it's a safe approximation. + Coercion _ -> emptyStrLattice + Tick _ e -> analExpr env e arity + Cast e _ -> analExpr env e arity + App f a -> + let + StrLattice (fTy, fAnns) = analExpr env f (arity + 1) + (argStr, fTy') = overArgs unconsArgStr fTy + argArity = + case argStr of + -- It's unfortunate that we don't have the type available to + -- trim this... But it doesn't hurt either. + HyperStrict -> Arity maxBound + Lazy -> 0 + Strict n -> n + StrLattice (aTy, aAnns) = analExpr env a argArity + in mkStrLattice (aTy `bothStrType` fTy') (fAnns \/ aAnns) + Var id_ + | isLocalId id_ -> + let + rhsType = case lookupVarEnv env id_ of + Just ty + -- 'ty' is a safe approximation for a call with 'idArity' at + -- minimum. + -- Note that 'Arity' is 'Op' ordered. + | arity <= Arity (idArity id_) -> ty + _ -> emptyStrType + in mkStrLattice (unitStrType id_ (Strict arity) `bothStrType` rhsType) emptyAnnotations + | otherwise -> emptyStrLattice + Lam id_ body + | isTyVar id_ -> analExpr env body arity + | otherwise -> + let + StrLattice (ty1, anns) = analExpr env body (0 /\ (arity-1)) + (argStr, ty2) = peelFV id_ ty1 + anns' = annotate id_ argStr anns + ty3 = modifyArgs (consArgStr argStr) ty2 + ty4 = applyWhen (arity == 0) lazifyStrType ty3 + in mkStrLattice ty4 anns' + Case scrut bndr _ alts -> + let + transferAlt (_, bndrs, alt) = + peelAndAnnotateFVs bndrs (analExpr env alt arity) + StrLattice (altTy, altAnns) = + peelAndAnnotateFV bndr . joins . map transferAlt $ alts + StrLattice (scrutTy, scrutAnns) = analExpr env scrut 0 + in mkStrLattice (scrutTy `bothStrType` altTy) (scrutAnns \/ altAnns) + Let bind body -> + let + -- we assume a single call with `idArity` for our approximation + (rhsAnns, env') = case bind of + NonRec id_ rhs + | StrLattice (ty, anns) <- analExpr env rhs (Arity (idArity id_)) + -> (anns, extendVarEnv env id_ ty) + Rec binds -> fixBinds env binds + bodyLatt = analExpr env' body arity + StrLattice (bodyTy, bodyAnns) = peelAndAnnotateFVs (bindersOf bind) bodyLatt + in mkStrLattice bodyTy (bodyAnns \/ rhsAnns) + +fixBinds :: VarEnv StrType -> [(Id, CoreExpr)] -> (Annotations, VarEnv StrType) +fixBinds env binds = mergeWithLatts stableLatts + where + mergeWithLatts :: [StrLattice] -> (Annotations, VarEnv StrType) + mergeWithLatts latts = foldr merger (emptyAnnotations, env) (zip binds latts) + + merger :: ((Id, CoreExpr), StrLattice) -> (Annotations, VarEnv StrType) -> (Annotations, VarEnv StrType) + merger ((id_, _), StrLattice (ty, anns)) (restAnns, env') = + (restAnns \/ anns, extendVarEnv env' id_ ty) + + latts0 :: [StrLattice] + latts0 = map (const bottom) binds + + approximations :: [[StrLattice]] + approximations = iterate (iter . snd . mergeWithLatts) latts0 + + stable :: ([StrLattice], [StrLattice]) -> Bool + stable (old, new) = map strType old == map strType new + + stableLatts :: [StrLattice] + stableLatts = snd . head . filter stable $ zip approximations (tail approximations) + + iter env' = snd (foldr iterBind (env', []) binds) + + iterBind (id_, rhs) (env', latts) = + let + latt = analExpr env' rhs (Arity (idArity id_)) + env'' = extendVarEnv env' id_ (strType latt) + in (env'', latt:latts) diff --git a/examples/Analyses/StrAnal/Analysis.hs b/examples/Analyses/StrAnal/Analysis.hs --- a/examples/Analyses/StrAnal/Analysis.hs +++ b/examples/Analyses/StrAnal/Analysis.hs @@ -24,7 +24,7 @@ import VarEnv analyse :: CoreExpr -> StrLattice -analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort 0 +analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort (0 :: Arity) applyWhen :: Bool -> (a -> a) -> a -> a applyWhen True f = f diff --git a/examples/Analyses/Templates/LetDn.hs b/examples/Analyses/Templates/LetDn.hs --- a/examples/Analyses/Templates/LetDn.hs +++ b/examples/Analyses/Templates/LetDn.hs @@ -76,20 +76,31 @@ -- lead to non-structural recursion, so termination isn't obvious and -- demands some confidence in domain theory by the programmer. buildDenotation - :: forall m - . MonadDependency m - => Eq (ReturnType (Domain m)) - => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool) - => TransferAlgebra (Domain m) + :: forall domain + . Eq (ReturnType domain) + => Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) + => TransferAlgebra domain -> CoreExpr - -> ProblemBuilder m (TF m) -buildDenotation alg' = buildExpr emptyVarEnv + -> Denotation domain +buildDenotation = buildDenotation' + +-- This brings in the scope the existentially quantified 'MonadDatafix'. Too +-- bad that we have no big lambda so that this is necessary. +buildDenotation' + :: forall m domain + . MonadDatafix m + => domain ~ Domain (DepM m) + => Eq (ReturnType domain) + => TransferAlgebra domain + -> CoreExpr + -> m (TF (DepM m)) +buildDenotation' alg' = buildExpr emptyVarEnv where - alg = alg' (Proxy :: Proxy m) (Proxy :: Proxy (Domain m)) + alg = alg' (Proxy :: Proxy (DepM m)) (Proxy :: Proxy domain) buildExpr - :: VarEnv (TF m) + :: VarEnv (TF (DepM m)) -> CoreExpr - -> ProblemBuilder m (TF m) + -> m (TF (DepM m)) buildExpr env expr = case expr of Lit lit -> pure (alg env (LitF lit)) diff --git a/src/Datafix.hs b/src/Datafix.hs --- a/src/Datafix.hs +++ b/src/Datafix.hs @@ -15,7 +15,9 @@ -- Look at "Datafix.Tutorial" for a tour guided by use cases. module Datafix - ( module Datafix.Description + ( module Datafix.Common + , module Datafix.Denotational + , module Datafix.Explicit , module Datafix.NodeAllocator , module Datafix.ProblemBuilder , Datafix.MonoMap.MonoMap @@ -23,7 +25,9 @@ , module Datafix.Worklist ) where -import Datafix.Description +import Datafix.Common +import Datafix.Denotational +import Datafix.Explicit import Datafix.MonoMap import Datafix.NodeAllocator import Datafix.ProblemBuilder diff --git a/src/Datafix/Common.hs b/src/Datafix/Common.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Common.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +-- | +-- Module : Datafix.Common +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- Common definitions for defining data-flow problems, defining infrastructure +-- around the notion of 'Domain'. + +module Datafix.Common + ( LiftedFunc + , ChangeDetector + , eqChangeDetector + , alwaysChangeDetector + , MonadDomain (..) + , Datafixable + ) where + +import Algebra.Lattice +import Datafix.MonoMap +import Datafix.Utils.Constraints +import Datafix.Utils.TypeLevel + +-- $setup +-- >>> :set -XTypeFamilies +-- >>> :set -XScopedTypeVariables +-- + +-- | Data-flow problems denote 'Node's 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 'LiftedFunc's of other 'Node's 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 +eqChangeDetector = + currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $ + const (/=) +{-# INLINE eqChangeDetector #-} + +-- | 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 +alwaysChangeDetector = + currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $ + \_ _ _ -> True +{-# INLINE alwaysChangeDetector #-} + +-- | 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 'Node's. + type 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](http://i.cs.hku.hk/~bruno/papers/hs2017.pdf) +-- instead of hackery from the [@constraints@ package](https://hackage.haskell.org/package/constraints-0.10/docs/Data-Constraint-Forall.html#t:ForallF), +-- @Datafixable@ is a specialized version of this: +-- +-- @ +-- type Datafixable domain = +-- ( forall r. Currying (ParamTypes domain) r +-- , MonoMapKey (Products (ParamTypes domain)) +-- , BoundedJoinSemiLattice (ReturnType domain) +-- ) +-- @ +-- +-- Now, let's assume a concrete @domain ~ String -> Bool -> Int@, so that +-- @'ParamTypes' (String -> Bool -> Int)@ expands to the type-level list @'[String, Bool]@ +-- and @'Products' '[String, Bool]@ reduces to @(String, Bool)@. +-- +-- Then this constraint makes sure we are able to +-- +-- 1. Curry the domain of @String -> Bool -> r@ for all @r@ to e.g. @(String, Bool) -> r@. +-- See 'Currying'. This constraint should always be discharged automatically by the +-- type-checker as soon as 'ParamTypes' and 'ReturnTypes' reduce for the 'Domain' argument, +-- which happens when the concrete @'MonadDependency' m@ is known. +-- +-- 2. We want to use a [monotone](https://en.wikipedia.org/wiki/Monotonic_function) +-- 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 'DataFlowProblem'. +-- +-- 3. For fixed-point iteration to work at all, the values which we iterate +-- naturally have to be instances of 'BoundedJoinSemiLattice'. +-- That type-class allows us to start iteration from a most-optimistic 'bottom' +-- value and successively iterate towards a conservative approximation using +-- the '(\/)' operator. +type Datafixable domain = + ( Forall (Currying (ParamTypes domain)) + , MonoMapKey (Products (ParamTypes domain)) + , BoundedJoinSemiLattice (ReturnType domain) + ) diff --git a/src/Datafix/Denotational.hs b/src/Datafix/Denotational.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Denotational.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +-- | +-- Module : Datafix.Denotational +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- 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 + ( MonadDatafix (..) + , datafixEq + , Denotation + ) where + +import Datafix.Common +import Datafix.Entailments +import Datafix.Utils.Constraints +import Datafix.Utils.TypeLevel + +-- | 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 +-- 'DataFlowProblem' 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 'ProblemBuilder'. + type 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 + -- @'Control.Monad.Fix.mfix' :: MonadFix m => (a -> m a) -> m a@. + datafix + :: 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 +datafixEq = datafix @m (eqChangeDetector @dom) \\ cdInst @dom + +-- | A denotation of some syntactic entity in a semantic @domain@, built in a +-- some 'MonadDatafix' context. +type Denotation dom + = forall m. (MonadDatafix m, dom ~ Domain (DepM m)) => m (LiftedFunc dom (DepM m)) diff --git a/src/Datafix/Description.hs b/src/Datafix/Description.hs deleted file mode 100644 --- a/src/Datafix/Description.hs +++ /dev/null @@ -1,248 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} - --- | --- Module : Datafix.Description --- Copyright : (c) Sebastian Graf 2018 --- License : ISC --- Maintainer : sgraf1337@gmail.com --- Portability : portable --- --- Primitives for describing a [data-flow problem](https://en.wikipedia.org/wiki/Data-flow_analysis) in a declarative manner. --- --- Import this module transitively through "Datafix" and get access to "Datafix.Worklist" for functions that compute solutions to your 'DataFlowProblem's. - -module Datafix.Description - ( Node (..) - , LiftedFunc - , ChangeDetector - , DataFlowProblem (..) - , MonadDependency (..) - , MonadDatafix (..) - , datafixEq - , eqChangeDetector - , alwaysChangeDetector - ) where - -import Datafix.Utils.TypeLevel - --- $setup --- >>> :set -XTypeFamilies --- >>> :set -XScopedTypeVariables --- >>> import Data.Proxy --- - --- | This is the type we use to index nodes in the data-flow graph. --- --- The connection between syntactic things (e.g. 'Id's) and 'Node's is --- made implicitly in code in analysis templates through an appropriate --- allocation mechanism as in 'NodeAllocator'. -newtype Node - = Node { unwrapNode :: Int } - deriving (Eq, Ord, Show) - --- | 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) - --- | Data-flow problems denote 'Node's 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 'LiftedFunc's of other 'Node's for the --- 'MonadDependency' case. -type LiftedFunc domain m - = Arrows (ParamTypes domain) (m (ReturnType domain)) - --- | 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 - { dfpTransfer :: !(Node -> LiftedFunc (Domain m) m) - -- ^ A transfer function per each 'Node' of the modeled data-flow problem. - , dfpDetectChange :: !(Node -> ChangeDetector (Domain m)) - -- ^ A 'ChangeDetector' for each 'Node' of the modeled data-flow problem. - -- In the simplest case, this just delegates to an 'Eq' instance. - } - --- | 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 'Node's. --- --- 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 @dependOn@s 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](https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem) --- 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 Domain m :: * - -- ^ The abstract domain in which 'Node's of the data-flow graph are denoted. - -- When this is a synonym for 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 'Node's. - dependOn :: Node -> LiftedFunc (Domain m) 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 'Data.Function.fix' to abstract over recursion. - --- | 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 where - -- | 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 - :: 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 -datafixEq = datafix @mdep @mdat (eqChangeDetector @(Domain mdep)) - --- | 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 -eqChangeDetector = - currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $ - const (/=) -{-# INLINE eqChangeDetector #-} - --- | 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 -alwaysChangeDetector = - currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $ - \_ _ _ -> True -{-# INLINE alwaysChangeDetector #-} diff --git a/src/Datafix/Entailments.hs b/src/Datafix/Entailments.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Entailments.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : Datafix.Entailments +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- A bunch of helpful auxiliary entailments for 'Currying' that are recurring +-- throughout the code base. + +module Datafix.Entailments + ( cdInst + , lfInst + , afInst + , idInst + ) where + +import Datafix.Utils.Constraints +import Datafix.Utils.TypeLevel + +-- | 'Currying' entailment for 'ChangeDetector's. +cdInst + :: Forall (Currying (ParamTypes domain)) + :- Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool) +cdInst = inst + +-- | 'Currying' entailment for 'LiftedFunc's. +lfInst + :: Forall (Currying (ParamTypes domain)) + :- Currying (ParamTypes domain) (m (ReturnType domain)) +lfInst = inst + +-- | 'Currying' entailment for abortion functions. +afInst + :: Forall (Currying (ParamTypes domain)) + :- Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain) +afInst = inst + +-- | 'Currying' entailment for pure functions. +idInst + :: Forall (Currying (ParamTypes domain)) + :- Currying (ParamTypes domain) (ReturnType domain) +idInst = inst diff --git a/src/Datafix/Explicit.hs b/src/Datafix/Explicit.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Explicit.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +-- | +-- Module : Datafix.Explicit +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- Primitives for describing a [data-flow problem](https://en.wikipedia.org/wiki/Data-flow_analysis) in a declarative manner. +-- This module requires you to manage assignment of 'Node's 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 +-- 'DataFlowProblem's. + +module Datafix.Explicit + ( Node (..) + , DataFlowProblem (..) + , MonadDependency (..) + ) where + +import Datafix.Common + +-- $setup +-- >>> :set -XTypeFamilies +-- >>> :set -XScopedTypeVariables +-- >>> import Data.Proxy +-- + +-- | This is the type we use to index nodes in the data-flow graph. +-- +-- The connection between syntactic things (e.g. 'Id's) and 'Node's is +-- made implicitly in code in analysis templates through an appropriate +-- allocation mechanism as in 'NodeAllocator'. +newtype Node + = Node { unwrapNode :: Int } + deriving (Eq, Ord, Show) + +-- | 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 + { dfpTransfer :: !(Node -> LiftedFunc (Domain m) m) + -- ^ A transfer function per each 'Node' of the modeled data-flow problem. + , dfpDetectChange :: !(Node -> ChangeDetector (Domain m)) + -- ^ A 'ChangeDetector' for each 'Node' of the modeled data-flow problem. + -- In the simplest case, this just delegates to an 'Eq' instance. + } + +-- | 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 'Node's. +-- +-- 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 @dependOn@s 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](https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem) +-- 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 where + dependOn :: Node -> LiftedFunc (Domain m) 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 'Data.Function.fix' to abstract over recursion. diff --git a/src/Datafix/NodeAllocator.hs b/src/Datafix/NodeAllocator.hs --- a/src/Datafix/NodeAllocator.hs +++ b/src/Datafix/NodeAllocator.hs @@ -22,7 +22,7 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Data.Primitive.Array -import Datafix.Description +import Datafix.Explicit import Datafix.Utils.GrowableVector (GrowableVector) import qualified Datafix.Utils.GrowableVector as GV import System.IO.Unsafe (unsafePerformIO) diff --git a/src/Datafix/ProblemBuilder.hs b/src/Datafix/ProblemBuilder.hs --- a/src/Datafix/ProblemBuilder.hs +++ b/src/Datafix/ProblemBuilder.hs @@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -13,7 +14,10 @@ -- Maintainer : sgraf1337@gmail.com -- Portability : portable -- --- Offers an instance for 'MonadDatafix' based on 'NodeAllocator'. +-- Builds a 'DataFlowProblem' for a 'Denotation'al 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.ProblemBuilder ( ProblemBuilder @@ -21,9 +25,12 @@ ) where import Data.Primitive.Array -import Datafix.Description +import Datafix.Common +import Datafix.Denotational +import Datafix.Entailments +import Datafix.Explicit import Datafix.NodeAllocator -import Datafix.Utils.TypeLevel +import Datafix.Utils.Constraints -- | Constructs a build plan for a 'DataFlowProblem' by tracking allocation of -- 'Node's mapping to 'ChangeDetector's and transfer functions. @@ -31,7 +38,8 @@ = ProblemBuilder { unwrapProblemBuilder :: NodeAllocator (ChangeDetector (Domain m), LiftedFunc (Domain m) m) a } deriving (Functor, Applicative, Monad) -instance MonadDependency m => MonadDatafix m (ProblemBuilder m) where +instance MonadDependency m => MonadDatafix (ProblemBuilder m) where + type DepM (ProblemBuilder m) = m datafix cd func = ProblemBuilder $ allocateNode $ \node -> do let deref = dependOn @m node (ret, transfer) <- unwrapProblemBuilder (func deref) @@ -45,12 +53,11 @@ buildProblem :: forall m . MonadDependency m - => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool) - => ProblemBuilder m (LiftedFunc (Domain m) m) + => Denotation (Domain m) -> (Node, Node, DataFlowProblem m) buildProblem buildDenotation = (root, Node (sizeofArray arr - 1), prob) where prob = DFP (snd . indexArray arr . unwrapNode) (fst . indexArray arr . unwrapNode) (root, arr) = runAllocator $ allocateNode $ \root_ -> do - denotation <- unwrapProblemBuilder buildDenotation - return (root_, (alwaysChangeDetector @(Domain m), denotation)) + denotation <- unwrapProblemBuilder (buildDenotation @(ProblemBuilder m)) + return (root_, (alwaysChangeDetector @(Domain m) \\ cdInst @(Domain m), denotation)) diff --git a/src/Datafix/Utils/Constraints.hs b/src/Datafix/Utils/Constraints.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Utils/Constraints.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +-- | +-- Module : Datafix.Utils.Constraints +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- Universally quantified constraints, until we have -XQuantifiedConstraints. + +module Datafix.Utils.Constraints + ( Dict (..) + , (:-) (..) + , (\\) + , Forall + , inst + ) where + +import Data.Kind +import Unsafe.Coerce (unsafeCoerce) + +data Dict :: Constraint -> Type where + Dict :: c => Dict c + +newtype a :- b = Sub (a => Dict b) + +infixl 1 \\ -- required comment + +-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@ +(\\) :: a => (b => r) -> (a :- b) -> r +r \\ Sub Dict = r + +-- The `Skolem` type family represents skolem variables; do not export! +-- If GHC supports it, these might be made closed with no instances. + +type family Skolem (p :: k -> Constraint) :: k + +-- The outer `Forall` type family prevents GHC from giving a spurious +-- superclass cycle error. +-- The inner `Forall_` class prevents the skolem from leaking to the user, +-- which would be disastrous. + +-- | A representation of the quantified constraint @forall a. p a@. +type family Forall (p :: k -> Constraint) :: Constraint +type instance Forall p = Forall_ p +class p (Skolem p) => Forall_ (p :: k -> Constraint) +instance p (Skolem p) => Forall_ (p :: k -> Constraint) + +inst :: forall p a . Forall p :- p a +inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p)) diff --git a/src/Datafix/Worklist.hs b/src/Datafix/Worklist.hs --- a/src/Datafix/Worklist.hs +++ b/src/Datafix/Worklist.hs @@ -7,14 +7,16 @@ -- -- This module provides the 'Impl.solveProblem' function, which solves the description of a -- 'Datafix.Description.DataFlowProblem' by employing a worklist algorithm. +-- There's also an interpreter for 'Denotation'al problems in the form of +-- 'Denotational.evalDenotation'. module Datafix.Worklist ( Impl.DependencyM - , Impl.Datafixable , Impl.Density (..) , Impl.IterationBound (..) , Impl.solveProblem - , Impl.evalDenotation + , Denotational.evalDenotation ) where -import qualified Datafix.Worklist.Internal as Impl +import qualified Datafix.Worklist.Denotational as Denotational +import qualified Datafix.Worklist.Internal as Impl diff --git a/src/Datafix/Worklist/Denotational.hs b/src/Datafix/Worklist/Denotational.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist/Denotational.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} + +-- | +-- Module : Datafix.Worklist.Denotational +-- Copyright : (c) Sebastian Graf 2018 +-- License : ISC +-- Maintainer : sgraf1337@gmail.com +-- Portability : portable +-- +-- Bridges the "Datafix.Worklist" solver for 'DataFlowProblem's ('solveProblem') +-- with the "Datafix.Denotational" approach, using 'MonadDatafix' to describe +-- a 'Denotation'. + +module Datafix.Worklist.Denotational + ( evalDenotation + ) where + +import Datafix.Common +import Datafix.Denotational +import Datafix.ProblemBuilder +import Datafix.Worklist.Internal + +-- | @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 + :: Datafixable domain + => Denotation domain + -- ^ A build plan for computing the denotation, possibly involving + -- fixed-point iteration factored through calls to 'datafix'. + -> IterationBound domain + -- ^ Whether the solution algorithm should respect a maximum bound on the + -- number of iterations per point. Pass 'NeverAbort' if you don't care. + -> domain +evalDenotation denot ib = solveProblem prob (Dense max_) ib root + where + (root, max_, prob) = buildProblem denot +{-# INLINE evalDenotation #-} diff --git a/src/Datafix/Worklist/Internal.hs b/src/Datafix/Worklist/Internal.hs --- a/src/Datafix/Worklist/Internal.hs +++ b/src/Datafix/Worklist/Internal.hs @@ -33,12 +33,14 @@ import Data.Maybe (fromMaybe, listToMaybe, mapMaybe) import Data.Type.Equality -import Datafix.Description hiding (dependOn) -import qualified Datafix.Description +import Datafix.Common +import Datafix.Entailments +import Datafix.Explicit hiding (dependOn) +import qualified Datafix.Explicit import Datafix.IntArgsMonoSet (IntArgsMonoSet) import qualified Datafix.IntArgsMonoSet as IntArgsMonoSet import Datafix.MonoMap (MonoMapKey) -import Datafix.ProblemBuilder +import Datafix.Utils.Constraints import Datafix.Utils.TypeLevel import Datafix.Worklist.Graph (GraphRef, PointInfo (..)) import qualified Datafix.Worklist.Graph as Graph @@ -58,9 +60,9 @@ -- -- 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)) -> ...@ + -- @(forall s. Datafixable 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)) -> ...@ + -- @(forall s r. (Datafixable 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 @@ -109,64 +111,13 @@ <*> newIORef unstable_ {-# INLINE initialEnv #-} --- | 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](http://i.cs.hku.hk/~bruno/papers/hs2017.pdf), --- @Datafixable@ is a specialized version of this: --- --- @ --- type Datafixable m = --- ( forall r. Currying (ParamTypes (Domain m)) r --- , MonoMapKey (Products (ParamTypes (Domain m))) --- , BoundedJoinSemiLattice (ReturnType (Domain m)) --- ) --- @ --- --- Now, let's assume a concrete @Domain m ~ String -> Bool -> Int@, so that --- @'ParamTypes' (String -> Bool -> Int)@ expands to the type-level list @'[String, Bool]@ --- and @'Products' '[String, Bool]@ reduces to @(String, Bool)@. --- --- Then this constraint makes sure we are able to --- --- 1. Curry the domain of @String -> Bool -> r@ for all @r@ to e.g. @(String, Bool) -> r@. --- See 'Currying'. This constraint should always be discharged automatically by the --- type-checker as soon as 'ParamTypes' and 'ReturnTypes' reduce for the 'Domain' argument, --- which happens when the concrete @'MonadDependency' m@ is known. --- --- (Actually, we do this for multiple concrete @r@ because of the missing --- support for quantified class constraints) --- --- 2. We want to use a [monotone](https://en.wikipedia.org/wiki/Monotonic_function) --- map of @(String, Bool)@ to @Int@ (the @ReturnType (Domain m)@). This is --- ensured by the @'MonoMapKey' (String, Bool)@ constraint. --- --- This constraint has to be discharged manually, but should amount to a --- single line of boiler-plate in most cases, see 'MonoMapKey'. --- --- Note that the monotonicity requirement means we have to pull non-monotone --- arguments in @Domain m@ into the 'Node' portion of the 'DataFlowProblem'. --- --- 3. For fixed-point iteration to work at all, the values which we iterate --- naturally have to be instances of 'BoundedJoinSemiLattice'. --- That type-class allows us to start iteration from a most-optimistic 'bottom' --- value and successively iterate towards a conservative approximation using --- the '(\/)' operator. -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)) - ) +-- | The 'Domain' is extracted from a type parameter. +instance Datafixable domain => MonadDomain (DependencyM graph domain) where + type Domain (DependencyM graph domain) = domain -- | This allows us to solve @MonadDependency m => DataFlowProblem m@ descriptions -- with 'solveProblem'. --- The 'Domain' is extracted from a type parameter. -instance (Datafixable (DependencyM graph domain), GraphRef graph) => MonadDependency (DependencyM graph domain) where - type Domain (DependencyM graph domain) = domain +instance (Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) where dependOn = dependOn @domain @graph {-# INLINE dependOn #-} @@ -282,7 +233,7 @@ {-# INLINE highestPriorityUnstableNode #-} withCall - :: Datafixable (DependencyM graph domain) + :: Datafixable domain => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO a @@ -314,13 +265,15 @@ => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph - => Datafixable depm + => Datafixable domain => Int -> Products dom -> ReaderT (Env graph domain) IO cod recompute node args = withCall node args $ do prob <- asks problem let node' = Node node let DM iterate' = uncurrys @dom @(depm cod) (dfpTransfer prob node') args + \\ lfInst @domain @depm let detectChange' = uncurrys @dom @(cod -> cod -> Bool) (dfpDetectChange prob node') args + \\ cdInst @domain -- We need to access the graph at three different points in time: -- -- 1. before the call to 'iterate', to access 'iterations', but only if abortion is required @@ -336,7 +289,7 @@ Just preInfo <- lift (withReaderT graph (Graph.lookup node args)) guard (iterations preInfo >= n) Just oldVal <- return (value preInfo) - return (uncurrys @dom @(cod -> cod) abort args oldVal) + return (uncurrys @dom @(cod -> cod) abort args oldVal \\ afInst @domain) -- For the 'Nothing' case, we proceed by iterating the transfer function. newVal <- maybe iterate' return maybeAbortedVal -- When abortion is required, 'iterate'' is not called and @@ -362,37 +315,40 @@ {-# INLINE recompute #-} dependOn - :: forall domain graph - . Datafixable (DependencyM graph domain) + :: forall domain graph depm + . depm ~ DependencyM graph domain + => Datafixable domain => GraphRef graph - => Node -> LiftedFunc domain (DependencyM graph domain) -dependOn (Node node) = currys @(ParamTypes domain) @(DependencyM graph domain (ReturnType domain)) impl - where - impl args = DM $ do - cycleDetected <- IntArgsMonoSet.member node args <$> asks callStack - isStable <- zoomUnstable $ - not . IntArgsMonoSet.member node args <$> get - maybePointInfo <- withReaderT graph (Graph.lookup node args) - zoomReferencedPoints (modify' (IntArgsMonoSet.insert node args)) - case maybePointInfo >>= value of - -- 'value' can only be 'Nothing' if there was a 'cycleDetected': - -- Otherwise, the node wasn't part of the call stack and thus will either - -- have a 'value' assigned or will not have been discovered at all. - Nothing | cycleDetected -> - -- Somewhere in an outer activation record we already compute this one. - -- We don't recurse again and just return an optimistic approximation, - -- such as 'bottom'. - -- Otherwise, 'recompute' will immediately add a 'PointInfo' before - -- any calls to 'dependOn' for a cycle to even be possible. - optimisticApproximation node args - Just val | isStable || cycleDetected -> - -- No brainer - return val - maybeVal -> - -- No cycle && (unstable || undiscovered). Apply one of the schemes - -- outlined in - -- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like - scheme2 maybeVal node args + => Node -> LiftedFunc domain depm +dependOn (Node node) = + currys @(ParamTypes domain) @(depm (ReturnType domain)) impl + \\ lfInst @domain @(DependencyM graph domain) + where + impl args = DM $ do + cycleDetected <- IntArgsMonoSet.member node args <$> asks callStack + isStable <- zoomUnstable $ + not . IntArgsMonoSet.member node args <$> get + maybePointInfo <- withReaderT graph (Graph.lookup node args) + zoomReferencedPoints (modify' (IntArgsMonoSet.insert node args)) + case maybePointInfo >>= value of + -- 'value' can only be 'Nothing' if there was a 'cycleDetected': + -- Otherwise, the node wasn't part of the call stack and thus will either + -- have a 'value' assigned or will not have been discovered at all. + Nothing | cycleDetected -> + -- Somewhere in an outer activation record we already compute this one. + -- We don't recurse again and just return an optimistic approximation, + -- such as 'bottom'. + -- Otherwise, 'recompute' will immediately add a 'PointInfo' before + -- any calls to 'dependOn' for a cycle to even be possible. + optimisticApproximation node args + Just val | isStable || cycleDetected -> + -- No brainer + return val + maybeVal -> + -- No cycle && (unstable || undiscovered). Apply one of the schemes + -- outlined in + -- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like + scheme2 maybeVal node args {-# INLINE dependOn #-} -- | Compute an optimistic approximation for a point of a given node that is @@ -404,7 +360,7 @@ -- that are lower bounds to the current point. optimisticApproximation :: GraphRef graph - => Datafixable (DependencyM graph domain) + => Datafixable domain => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain) optimisticApproximation node args = do points <- withReaderT graph (Graph.lookupLT node args) @@ -415,7 +371,7 @@ scheme1, scheme2 :: GraphRef graph - => Datafixable (DependencyM graph domain) + => Datafixable domain => Maybe (ReturnType domain) -> Int -> Products (ParamTypes domain) @@ -474,7 +430,7 @@ -- fixed-point has been reached. work :: GraphRef graph - => Datafixable (DependencyM graph domain) + => Datafixable domain => ReaderT (Env graph domain) IO () work = whileJust_ highestPriorityUnstableNode (uncurry recompute) {-# INLINE work #-} @@ -499,7 +455,7 @@ solveProblem :: forall domain graph . GraphRef graph - => Datafixable (DependencyM graph domain) + => Datafixable domain => DataFlowProblem (DependencyM graph domain) -- ^ The description of the @DataFlowProblem@ to solve. -> Density graph @@ -516,7 +472,7 @@ -- you specified via the @DataFlowProblem@. -> domain solveProblem prob density ib (Node node) = - castWith arrowsAxiom (currys @(ParamTypes domain) @(ReturnType domain) impl) + castWith arrowsAxiom (currys @(ParamTypes domain) @(ReturnType domain) impl \\ idInst @domain) where impl = fromMaybe (error "Broken invariant: The root node has no value") @@ -531,25 +487,3 @@ env <- initialEnv (IntArgsMonoSet.singleton node args) prob ib newGraphRef runReaderT (work >> withReaderT graph (Graph.lookup node args)) env {-# INLINE solveProblem #-} - --- | @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 DenseGraph.Ref domain) - => ProblemBuilder (DependencyM DenseGraph.Ref domain) (LiftedFunc domain (DependencyM DenseGraph.Ref domain)) - -- ^ A build plan for computing the denotation, possibly involving - -- fixed-point iteration factored through calls to 'datafix'. - -> IterationBound domain - -- ^ Whether the solution algorithm should respect a maximum bound on the - -- number of iterations per point. Pass 'NeverAbort' if you don't care. - -> domain -evalDenotation denot ib = solveProblem prob (Dense max_) ib root - where - (root, max_, prob) = buildProblem denot -{-# INLINE evalDenotation #-}