Merge remote-tracking branch 'origin/typescript-exports' into import-language-tour

2024-12-29 01:42:43 +03:00 · 2018-03-12 15:40:22 -07:00 · 2018-03-12 15:40:22 -07:00 · af66a0c229
commit af66a0c229
parent 296fc5d4b5 cc4fd12428
28 changed files with 561 additions and 564 deletions
--- a/semantic.cabal
+++ b/semantic.cabal
@ -19,7 +19,7 @@ library
                     -- , Analysis.Abstract.Collecting
                     , Analysis.Abstract.Dead
                     , Analysis.Abstract.Evaluating
-                     -- , Analysis.Abstract.Tracing
+                     , Analysis.Abstract.Tracing
                     , Analysis.ConstructorName
                     , Analysis.CyclomaticComplexity
                     , Analysis.Decorator
@ -40,7 +40,6 @@ library
                     , Control.Monad.Effect.Fresh
                     -- , Control.Monad.Effect.GC
                     , Control.Monad.Effect.NonDet
-                     -- , Control.Monad.Effect.Trace
                     -- Datatypes for abstract interpretation
                     , Data.Abstract.Address
                     , Data.Abstract.Cache
@ -64,6 +63,7 @@ library
                     , Data.Functor.Classes.Generic
                     , Data.JSON.Fields
                     , Data.Language
+                     , Data.Map.Monoidal
                     , Data.Mergeable
                     , Data.Output
                     , Data.Patch
@ -158,8 +158,8 @@ library
                     , optparse-applicative
                     , parallel
                     , parsers
-                     , pointed
                     , recursion-schemes
+                     , reducers
                     , scientific
                     , split
                     , stm-chans
--- a/src/Analysis/Abstract/Caching.hs
+++ b/src/Analysis/Abstract/Caching.hs
@ -1,124 +1,110 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Analysis.Abstract.Caching
-  ( evaluateCache )
-  where
+( type Caching
+) where

-import Prologue
-import Data.Monoid (Alt(..))
-import Control.Abstract.Evaluator
-import Control.Effect
-import Control.Monad.Effect.Fail
-import Control.Monad.Effect.Fresh
-import Control.Monad.Effect.NonDet
-import Control.Monad.Effect.Reader
-import Control.Monad.Effect.State
-import Data.Abstract.Address
+import Control.Abstract.Analysis
 import Data.Abstract.Cache
 import Data.Abstract.Configuration
-import Data.Abstract.Environment
-import Data.Abstract.Evaluatable
-import Data.Abstract.ModuleTable
-import Data.Abstract.Live
 import Data.Abstract.Store
 import Data.Abstract.Value
-import qualified Data.Set as Set
+import Data.Monoid (Alt (..))
+import Prologue

 -- | The effects necessary for caching analyses.
-type CachingEffects t v
-  = '[ Fresh                                  -- For 'MonadFresh'.
-     , Reader (Live (LocationFor v) v)        -- For 'MonadGC'.
-     , Reader (Environment (LocationFor v) v) -- For 'MonadEnv'.
-     , State (Environment (LocationFor v) v)  -- For 'MonadEvaluator'.
-     , State (Map Name (Name, Maybe (Address (LocationFor v) v)))      -- For 'MonadEvaluator'.
-     , Fail                                   -- For 'MonadFail'.
-     , NonDetEff                              -- For 'Alternative' & 'MonadNonDet'.
-     , State (Store (LocationFor v) v)        -- For 'MonadStore'.
-     , Reader (Cache (LocationFor v) t v)     -- For reading memoized values.
-     , State (Cache (LocationFor v) t v)      -- For writing said values.
-     , Reader (ModuleTable t)                 -- Cache of unevaluated modules
-     , State (ModuleTable (EnvironmentFor v)) -- Cache of evaluated modules
-     ]
+type CachingEffects term value effects
+  = Fresh                        -- For 'MonadFresh'.
+ ': NonDetEff                    -- For 'Alternative' and 'MonadNonDet'.
+ ': Reader (CacheFor term value) -- The in-cache used as an oracle while converging on a result.
+ ': State  (CacheFor term value) -- The out-cache used to record results in each iteration of convergence.
+ ': effects

-newtype CachingAnalysis term value a = CachingAnalysis { runCachingAnalysis :: Evaluator (CachingEffects term value) term value a }
-  deriving (Alternative, Applicative, Functor, Monad, MonadFail, MonadFresh, MonadNonDet)
+-- | The cache for term and abstract value types.
+type CacheFor term value = Cache (LocationFor value) term value

-deriving instance MonadEvaluator term value (CachingAnalysis term value)
+-- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
+newtype Caching m term value (effects :: [* -> *]) a = Caching (m term value effects a)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

-- TODO: reabstract these later on
+deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Caching m term value effects)

-askCache :: CachingAnalysis t v (Cache (LocationFor v) t v)
-askCache = CachingAnalysis (Evaluator ask)
+-- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
+class MonadEvaluator term value m => MonadCaching term value m where
+  -- | Look up the set of values for a given configuration in the in-cache.
+  consultOracle :: ConfigurationFor term value -> m (Set (value, StoreFor value))
+  -- | Run an action with the given in-cache.
+  withOracle :: CacheFor term value -> m a -> m a

-localCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v a -> CachingAnalysis t v a
-localCache f (CachingAnalysis (Evaluator a)) = CachingAnalysis (Evaluator (local f a))
+  -- | Look up the set of values for a given configuration in the out-cache.
+  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, StoreFor value)))
+  -- | Run an action, caching its result and 'Store' under the given configuration.
+  caching :: ConfigurationFor term value -> Set (value, StoreFor value) -> m value -> m value

-asksCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a
-asksCache f = f <$> askCache
+  -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
+  isolateCache :: m a -> m (CacheFor term value)

-getsCache :: (Cache (LocationFor v) t v -> a) -> CachingAnalysis t v a
-getsCache f = f <$> getCache
+instance ( Effectful (m term value)
+         , Members (CachingEffects term value '[]) effects
+         , MonadEvaluator term value (m term value effects)
+         , Ord (CellFor value)
+         , Ord (LocationFor value)
+         , Ord term
+         , Ord value
+         )
+         => MonadCaching term value (Caching m term value effects) where
+  consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
+  withOracle cache = raise . local (const cache) . lower

-getCache :: CachingAnalysis t v (Cache (LocationFor v) t v)
-getCache = CachingAnalysis (Evaluator get)
+  lookupCache configuration = raise (cacheLookup configuration <$> get)
+  caching configuration values action = do
+    raise (modify (cacheSet configuration values))
+    result <- (,) <$> action <*> getStore
+    raise (modify (cacheInsert configuration result))
+    pure (fst result)

-putCache :: Cache (LocationFor v) t v -> CachingAnalysis t v ()
-putCache v = CachingAnalysis (Evaluator (put v))
-
-modifyCache :: (Cache (LocationFor v) t v -> Cache (LocationFor v) t v) -> CachingAnalysis t v ()
-modifyCache f = fmap f getCache >>= putCache
+  isolateCache action = raise (put (mempty :: CacheFor term value)) *> action *> raise get

 -- | This instance coinductively iterates the analysis of a term until the results converge.
-instance ( Corecursive t
-         , Ord t
-         , Ord v
-         , Ord (Cell (LocationFor v) v)
-         , Evaluatable (Base t)
-         , Foldable (Cell (LocationFor v))
-         , FreeVariables t
-         , MonadAddressable (LocationFor v) v (CachingAnalysis t v)
-         , MonadValue t v (CachingAnalysis t v)
-         , Recursive t
-         , Semigroup (Cell (LocationFor v) v)
+instance ( Corecursive term
+         , Effectful (m term value)
+         , MonadAnalysis term value (m term value effects)
+         , MonadFresh (m term value effects)
+         , MonadNonDet (m term value effects)
+         , Members (CachingEffects term value '[]) effects
+         , Ord (CellFor value)
+         , Ord (LocationFor value)
+         , Ord term
+         , Ord value
         )
-         => MonadAnalysis t v (CachingAnalysis t v) where
+         => MonadAnalysis term value (Caching m term value effects) where
+  -- We require the 'CachingEffects' in addition to the underlying analysis’ 'RequiredEffects'.
+  type RequiredEffects term value (Caching m term value effects) = CachingEffects term value (RequiredEffects term value (m term value effects))
+
+  -- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
  analyzeTerm e = do
    c <- getConfiguration (embedSubterm e)
+    cached <- lookupCache c
+    case cached of
+      Just pairs -> scatter pairs
+      Nothing -> do
+        pairs <- consultOracle c
+        caching c pairs (liftAnalyze analyzeTerm e)
+
+  evaluateModule e = do
+    c <- getConfiguration e
    -- Convergence here is predicated upon an Eq instance, not α-equivalence
-    cache <- converge (\ prevCache -> do
-      putCache (mempty :: Cache (LocationFor v) t v)
+    cache <- converge (\ prevCache -> isolateCache $ do
      putStore (configurationStore c)
      -- We need to reset fresh generation so that this invocation converges.
      reset 0
      -- This is subtle: though the calling context supports nondeterminism, we want
      -- to corral all the nondeterminism that happens in this @eval@ invocation, so
-      -- that it doesn't "leak" to the calling context and diverge
-      -- (otherwise this would never complete).
-      _ <- localCache (const prevCache) (gather Set.singleton (memoizeEval e))
-      getCache) mempty
+      -- that it doesn't "leak" to the calling context and diverge (otherwise this
+      -- would never complete). We don’t need to use the values, so we 'gather' the
+      -- nondeterministic values into @()@.
+      withOracle prevCache (gather (const ()) (Caching (evaluateModule e)))) mempty
    maybe empty scatter (cacheLookup c cache)

-
-- | Coinductively-cached evaluation.
-evaluateCache :: forall v term
-              . ( Ord v
-                , Ord term
-                , Ord (LocationFor v)
-                , Ord (Cell (LocationFor v) v)
-                , Corecursive term
-                , Evaluatable (Base term)
-                , FreeVariables term
-                , Foldable (Cell (LocationFor v))
-                , Functor (Base term)
-                , Recursive term
-                , MonadAddressable (LocationFor v) v (CachingAnalysis term v)
-                , MonadValue term v (CachingAnalysis term v)
-                , Semigroup (Cell (LocationFor v) v)
-                , ValueRoots (LocationFor v) v
-                )
-              => term
-              -> Final (CachingEffects term v) v
-evaluateCache = run @(CachingEffects term v) . runEvaluator . runCachingAnalysis . evaluateTerm
-
 -- | Iterate a monadic action starting from some initial seed until the results converge.
 --
 --   This applies the Kleene fixed-point theorem to finitize a monotone action. cf https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem
@ -134,40 +120,6 @@ converge f = loop
          else
            loop x'

-- | Get the current 'Configuration' with a passed-in term.
-getConfiguration :: Ord (LocationFor v) => t -> CachingAnalysis t v (Configuration (LocationFor v) t v)
-getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getStore
-
 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator term v m) => t (a, Store (LocationFor v) v) -> m a
+scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Store (LocationFor value) value) -> m a
 scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value))
-
-- | Evaluation of a single iteration of an analysis, given a 'MonadCacheIn' instance as an oracle for results and a 'MonadCacheOut' instance to record computed results in.
-memoizeEval :: forall v term
-            . ( Ord v
-              , Ord term
-              , Ord (LocationFor v)
-              , Ord (Cell (LocationFor v) v)
-              , Corecursive term
-              , Evaluatable (Base term)
-              , FreeVariables term
-              , Foldable (Cell (LocationFor v))
-              , Functor (Base term)
-              , Recursive term
-              , MonadAddressable (LocationFor v) v (CachingAnalysis term v)
-              , MonadValue term v (CachingAnalysis term v)
-              , Semigroup (Cell (LocationFor v) v)
-              )
-            => SubtermAlgebra (Base term) term (CachingAnalysis term v v)
-memoizeEval e = do
-  c <- getConfiguration (embedSubterm e)
-  cached <- getsCache (cacheLookup c)
-  case cached of
-    Just pairs -> scatter pairs
-    Nothing -> do
-      pairs <- asksCache (fromMaybe mempty . cacheLookup c)
-      modifyCache (cacheSet c pairs)
-      v <- eval e
-      store' <- getStore
-      modifyCache (cacheInsert c (v, store'))
-      pure v
--- a/src/Analysis/Abstract/Dead.hs
+++ b/src/Analysis/Abstract/Dead.hs
@ -1,85 +1,52 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, UndecidableInstances #-}
-module Analysis.Abstract.Dead where
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, TypeFamilies, TypeOperators #-}
+module Analysis.Abstract.Dead
+( type DeadCode
+) where

-import Control.Abstract.Addressable
-import Control.Abstract.Evaluator
-import Control.Effect
-import Control.Monad.Effect.Fail
-import Control.Monad.Effect.Reader
-import Control.Monad.Effect.State
-import Data.Abstract.Address
-import Data.Abstract.Evaluatable
-import Data.Abstract.ModuleTable
-import Data.Abstract.Store
-import Data.Abstract.Value
+import Control.Abstract.Analysis
+import Data.Semigroup.Reducer as Reducer
 import Data.Set (delete)
 import Prologue

-- | The effects necessary for dead code analysis.
-type DeadCodeEffects t v
-  = '[ State (Dead t)                                             -- The set of dead terms
-     , Fail                                                       -- Failure with an error message
-     , State (Store (LocationFor v) v)                            -- The heap
-     , State (Map Name (Name, Maybe (Address (LocationFor v) v))) -- Set of exports
-     , State (EnvironmentFor v)                                   -- Global (imperative) environment
-     , Reader (EnvironmentFor v)                                  -- Local environment (e.g. binding over a closure)
-     , Reader (ModuleTable t)                                     -- Cache of unevaluated modules
-     , State (ModuleTable (EnvironmentFor v))                     -- Cache of evaluated modules
-     ]
-
-
-- | Run a dead code analysis of the given program.
-evaluateDead :: forall term value
-             .  ( Corecursive term
-                , Evaluatable (Base term)
-                , Foldable (Base term)
-                , FreeVariables term
-                , MonadAddressable (LocationFor value) value (DeadCodeAnalysis term value)
-                , MonadValue term value (DeadCodeAnalysis term value)
-                , Ord (LocationFor value)
-                , Ord term
-                , Recursive term
-                , Semigroup (Cell (LocationFor value) value)
-                )
-             => term
-             -> Final (DeadCodeEffects term value) value
-evaluateDead term = run @(DeadCodeEffects term value) . runEvaluator . runDeadCodeAnalysis $ do
-  killAll (subterms term)
-  evaluateTerm term
-  where subterms :: (Ord a, Recursive a, Foldable (Base a)) => a -> Dead a
-        subterms term = para (foldMap (uncurry ((<>) . point))) term <> point term
-
-
-- | A newtype wrapping 'Evaluator' which performs a dead code analysis on evaluation.
-newtype DeadCodeAnalysis term value a = DeadCodeAnalysis { runDeadCodeAnalysis :: Evaluator (DeadCodeEffects term value) term value a }
-  deriving (Applicative, Functor, Monad, MonadFail)
-
-deriving instance MonadEvaluator term value (DeadCodeAnalysis term value)
+-- | An analysis tracking dead (unreachable) code.
+newtype DeadCode m term value (effects :: [* -> *]) a = DeadCode (m term value effects a)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

+deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (DeadCode m term value effects)

 -- | A set of “dead” (unreachable) terms.
-newtype Dead a = Dead { unDead :: Set a }
-  deriving (Eq, Foldable, Semigroup, Monoid, Ord, Pointed, Show)
+newtype Dead term = Dead { unDead :: Set term }
+  deriving (Eq, Foldable, Semigroup, Monoid, Ord, Show)
+
+deriving instance Ord term => Reducer term (Dead term)

 -- | Update the current 'Dead' set.
-killAll :: Dead t -> DeadCodeAnalysis t v ()
-killAll = DeadCodeAnalysis . Evaluator . put
+killAll :: (Effectful (m term value), Member (State (Dead term)) effects) => Dead term -> DeadCode m term value effects ()
+killAll = raise . put

 -- | Revive a single term, removing it from the current 'Dead' set.
-revive :: Ord t => t -> DeadCodeAnalysis t v ()
-revive t = DeadCodeAnalysis (Evaluator (modify (Dead . delete t . unDead)))
+revive :: (Effectful (m term value), Member (State (Dead term)) effects) => Ord term => term -> DeadCode m term value effects ()
+revive t = raise (modify (Dead . delete t . unDead))
+
+-- | Compute the set of all subterms recursively.
+subterms :: (Ord term, Recursive term, Foldable (Base term)) => term -> Dead term
+subterms term = term `cons` para (foldMap (uncurry cons)) term


-instance ( Corecursive t
-         , Evaluatable (Base t)
-         , FreeVariables t
-         , MonadAddressable (LocationFor v) v (DeadCodeAnalysis t v)
-         , MonadValue t v (DeadCodeAnalysis t v)
-         , Ord t
-         , Recursive t
-         , Semigroup (Cell (LocationFor v) v)
+instance ( Corecursive term
+         , Effectful (m term value)
+         , Foldable (Base term)
+         , Member (State (Dead term)) effects
+         , MonadAnalysis term value (m term value effects)
+         , Ord term
         )
-         => MonadAnalysis t v (DeadCodeAnalysis t v) where
+         => MonadAnalysis term value (DeadCode m term value effects) where
+  type RequiredEffects term value (DeadCode m term value effects) = State (Dead term) ': RequiredEffects term value (m term value effects)
+
  analyzeTerm term = do
    revive (embedSubterm term)
-    eval term
+    liftAnalyze analyzeTerm term
+
+  evaluateModule term = do
+    killAll (subterms term)
+    DeadCode (evaluateModule term)
--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@ -1,67 +1,57 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableInstances #-}
-module Analysis.Abstract.Evaluating where
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
+module Analysis.Abstract.Evaluating
+( type Evaluating
+, evaluate
+, evaluates
+) where

 import Control.Abstract.Evaluator
-import Control.Effect
+import Control.Monad.Effect hiding (run)
 import Control.Monad.Effect.Fail
+import Control.Monad.Effect.Fresh
+import Control.Monad.Effect.NonDet
 import Control.Monad.Effect.Reader
 import Control.Monad.Effect.State
 import Data.Abstract.Address
 import Data.Abstract.Evaluatable
 import Data.Abstract.ModuleTable
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Data.Blob
 import Data.Language
 import Data.List.Split (splitWhen)
+import Prelude hiding (fail)
 import Prologue
 import qualified Data.ByteString.Char8 as BC
 import qualified Data.Map as Map
 import System.FilePath.Posix

-
-- | The effects necessary for concrete interpretation.
-type EvaluationEffects t v
-  = '[ Fail                                                       -- Failure with an error message
-     , State (Store (LocationFor v) v)                            -- The heap
-     , State (Map Name (Name, Maybe (Address (LocationFor v) v))) -- Set of exports
-     , State (EnvironmentFor v)                                   -- Global (imperative) environment
-     , Reader (EnvironmentFor v)                                  -- Local environment (e.g. binding over a closure)
-     , Reader (ModuleTable t)                                     -- Cache of unevaluated modules
-     , State (ModuleTable (EnvironmentFor v))                     -- Cache of evaluated modules
-     ]
-
 -- | Evaluate a term to a value.
-evaluate :: forall v term
+evaluate :: forall value term
         .  ( Evaluatable (Base term)
            , FreeVariables term
-            , MonadAddressable (LocationFor v) v (Evaluation term v)
-            , MonadValue term v (Evaluation term v)
-            , Ord (LocationFor v)
+            , MonadAddressable (LocationFor value) value (Evaluating term value (EvaluatingEffects term value))
+            , MonadValue term value (Evaluating term value (EvaluatingEffects term value))
            , Recursive term
-            , Semigroup (Cell (LocationFor v) v)
            )
         => term
-         -> Final (EvaluationEffects term v) v
-evaluate = run @(EvaluationEffects term v) . runEvaluator . runEvaluation . evaluateTerm
+         -> Final (EvaluatingEffects term value) value
+evaluate = runAnalysis @(Evaluating term value) . evaluateModule

 -- | Evaluate terms and an entry point to a value.
-evaluates :: forall v term
+evaluates :: forall value term
          .  ( Evaluatable (Base term)
             , FreeVariables term
-             , MonadAddressable (LocationFor v) v (Evaluation term v)
-             , MonadValue term v (Evaluation term v)
-             , Ord (LocationFor v)
+             , MonadAddressable (LocationFor value) value (Evaluating term value (EvaluatingEffects term value))
+             , MonadValue term value (Evaluating term value (EvaluatingEffects term value))
             , Recursive term
-             , Semigroup (Cell (LocationFor v) v)
             )
          => [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
          -> (Blob, term)   -- Entrypoint
-          -> Final (EvaluationEffects term v) v
-evaluates pairs (b, t) = run @(EvaluationEffects term v) (runEvaluator (runEvaluation (withModules b pairs (evaluateTerm t))))
+          -> Final (EvaluatingEffects term value) value
+evaluates pairs (b, t) = runAnalysis @(Evaluating term value) (withModules b pairs (evaluateModule t))

 -- | Run an action with the passed ('Blob', @term@) pairs available for imports.
-withModules :: (MonadAnalysis term value m, MonadEvaluator term value m) => Blob -> [(Blob, term)] -> m a -> m a
+withModules :: MonadAnalysis term value m => Blob -> [(Blob, term)] -> m a -> m a
 withModules Blob{..} pairs = localModuleTable (const moduleTable)
  where
    moduleTable = ModuleTable (Map.fromList (map (first moduleName) pairs))
@ -73,18 +63,57 @@ withModules Blob{..} pairs = localModuleTable (const moduleTable)
      _ ->  toName path
    toName str = qualifiedName (fmap BC.pack (splitWhen (== pathSeparator) str))

-- | An analysis performing concrete evaluation of @term@s to @value@s.
-newtype Evaluation term value a = Evaluation { runEvaluation :: Evaluator (EvaluationEffects term value) term value a }
-  deriving (Applicative, Functor, Monad, MonadFail)
+-- | An analysis evaluating @term@s to @value@s with a list of @effects@ using 'Evaluatable', and producing incremental results of type @a@.
+newtype Evaluating term value effects a = Evaluating (Eff effects a)
+  deriving (Applicative, Functor, Effectful, Monad)

-deriving instance MonadEvaluator term value (Evaluation term value)

-instance ( Evaluatable (Base t)
-         , FreeVariables t
-         , MonadAddressable (LocationFor v) v (Evaluation t v)
-         , MonadValue t v (Evaluation t v)
-         , Recursive t
-         , Semigroup (Cell (LocationFor v) v)
+deriving instance Member Fail      effects => MonadFail   (Evaluating term value effects)
+deriving instance Member Fresh     effects => MonadFresh  (Evaluating term value effects)
+deriving instance Member NonDetEff effects => Alternative (Evaluating term value effects)
+deriving instance Member NonDetEff effects => MonadNonDet (Evaluating term value effects)
+
+-- | Effects necessary for evaluating (whether concrete or abstract).
+type EvaluatingEffects term value
+  = '[ Fail                                        -- Failure with an error message
+     , Reader (EnvironmentFor value)               -- Local environment (e.g. binding over a closure)
+     , State  (EnvironmentFor value)               -- Global (imperative) environment
+     , State  (StoreFor value)                     -- The heap
+     , Reader (ModuleTable term)                   -- Cache of unevaluated modules
+     , State  (ModuleTable (EnvironmentFor value)) -- Cache of evaluated modules
+
+     , State (Map Name (Name, Maybe (Address (LocationFor value) value))) -- Set of exports
+     ]
+
+instance Members (EvaluatingEffects term value) effects => MonadEvaluator term value (Evaluating term value effects) where
+  getGlobalEnv = raise get
+  putGlobalEnv = raise . put
+  withGlobalEnv s = raise . localState s . lower
+
+  addExport key = raise . modify . Map.insert key
+  getExports = raise get
+  withExports s = raise . localState s . lower
+
+  askLocalEnv = raise ask
+  localEnv f a = raise (local f (lower a))
+
+  getStore = raise get
+  putStore = raise . put
+
+  getModuleTable = raise get
+  modifyModuleTable f = raise (modify f)
+
+  askModuleTable = raise ask
+  localModuleTable f a = raise (local f (lower a))
+
+instance ( Evaluatable (Base term)
+         , FreeVariables term
+         , Members (EvaluatingEffects term value) effects
+         , MonadAddressable (LocationFor value) value (Evaluating term value effects)
+         , MonadValue term value (Evaluating term value effects)
+         , Recursive term
         )
-         => MonadAnalysis t v (Evaluation t v) where
+         => MonadAnalysis term value (Evaluating term value effects) where
+  type RequiredEffects term value (Evaluating term value effects) = EvaluatingEffects term value
+
  analyzeTerm = eval
--- a/src/Analysis/Abstract/Tracing.hs
+++ b/src/Analysis/Abstract/Tracing.hs
@ -1,73 +1,43 @@
-{-# LANGUAGE AllowAmbiguousTypes, DataKinds, ScopedTypeVariables, TypeApplications, TypeFamilies #-}
-module Analysis.Abstract.Tracing where
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
+module Analysis.Abstract.Tracing
+( type Tracing
+) where

-import Prologue
-import Control.Effect
-import Control.Monad.Effect hiding (run)
-import Control.Monad.Effect.Addressable
-import Control.Monad.Effect.Env
-import Control.Monad.Effect.Fail
-import Control.Monad.Effect.Reader
-import Control.Monad.Effect.State
-import Control.Monad.Effect.Trace
+import Control.Abstract.Analysis
 import Control.Monad.Effect.Writer
-import Data.Abstract.Address
 import Data.Abstract.Configuration
-import Data.Abstract.Environment
-import Data.Abstract.Eval
-import Data.Abstract.Store
 import Data.Abstract.Value
+import Data.Semigroup.Reducer as Reducer
+import Data.Union
+import Prologue hiding (trace)

-- | The effects necessary for tracing analyses.
-type Tracing g t v
-  = '[ Writer (g (Configuration (LocationFor v) t v)) -- For 'MonadTrace'.
-     , Fail                                           -- For 'MonadFail'.
-     , State (Store (LocationFor v) v)                -- For 'MonadStore'.
-     , Reader (Environment (LocationFor v) v)         -- For 'MonadEnv'.
-     ]
+-- | Trace analysis.
+--
+--   Instantiating @trace@ to @[]@ yields a linear trace analysis, while @Set@ yields a reachable state analysis.
+newtype Tracing (trace :: * -> *) m term value (effects :: [* -> *]) a = Tracing (m term value effects a)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)

-- | Linear trace analysis.
-evalTrace :: forall v term
-          . ( Ord v, Ord term, Ord (Cell (LocationFor v) v)
-            , Functor (Base term)
-            , Recursive term
-            , Addressable (LocationFor v) (Eff (Tracing [] term v))
-            , MonadGC v (Eff (Tracing [] term v))
-            , Semigroup (Cell (LocationFor v) v)
-            , Eval term v (Eff (Tracing [] term v)) (Base term)
-            )
-          => term -> Final (Tracing [] term v) v
-evalTrace = run @(Tracing [] term v) . fix (evTell @[] (\ recur yield -> eval recur yield . project)) pure
+deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Tracing trace m term value effects)

-- | Reachable configuration analysis.
-evalReach :: forall v term
-          . ( Ord v, Ord term, Ord (LocationFor v), Ord (Cell (LocationFor v) v)
-            , Functor (Base term)
-            , Recursive term
-            , Addressable (LocationFor v) (Eff (Tracing Set term v))
-            , MonadGC v (Eff (Tracing Set term v))
-            , Semigroup (Cell (LocationFor v) v)
-            , Eval term v (Eff (Tracing Set term v)) (Base term)
-            )
-          => term -> Final (Tracing Set term v) v
-evalReach = run @(Tracing Set term v) . fix (evTell @Set (\ recur yield -> eval recur yield . project)) pure
-
-
-- | Small-step evaluation which records every visited configuration.
-evTell :: forall g t m v
-       . ( Monoid (g (Configuration (LocationFor v) t v))
-         , Pointed g
-         , MonadTrace t v g m
-         , MonadEnv v m
-         , MonadStore v m
-         , MonadGC v m
+instance ( Corecursive term
+         , Effectful (m term value)
+         , Member (Writer (trace (ConfigurationFor term value))) effects
+         , MonadAnalysis term value (m term value effects)
+         , Ord (LocationFor value)
+         , Reducer (ConfigurationFor term value) (trace (ConfigurationFor term value))
         )
-       => (((v -> m v) -> t -> m v) -> (v -> m v) -> t -> m v)
-       -> ((v -> m v) -> t -> m v)
-       -> (v -> m v) -> t -> m v
-evTell ev0 ev' yield e = do
-  env <- askEnv
-  store <- getStore
-  roots <- askRoots
-  trace (point (Configuration e roots env store) :: g (Configuration (LocationFor v) t v))
-  ev0 ev' yield e
+         => MonadAnalysis term value (Tracing trace m term value effects) where
+  type RequiredEffects term value (Tracing trace m term value effects) = Writer (trace (ConfigurationFor term value)) ': RequiredEffects term value (m term value effects)
+
+  analyzeTerm term = do
+    config <- getConfiguration (embedSubterm term)
+    trace (Reducer.unit config)
+    liftAnalyze analyzeTerm term
+
+-- | Log the given trace of configurations.
+trace :: ( Effectful (m term value)
+         , Member (Writer (trace (ConfigurationFor term value))) effects
+         )
+      => trace (ConfigurationFor term value)
+      -> Tracing trace m term value effects ()
+trace = raise . tell
--- a/src/Control/Abstract/Addressable.hs
+++ b/src/Control/Abstract/Addressable.hs
@ -1,65 +1,61 @@
-{-# LANGUAGE FunctionalDependencies, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Addressable where

-import Control.Abstract.Evaluator
+import Control.Abstract.Analysis
 import Control.Applicative
 import Control.Monad ((<=<))
-import Control.Monad.Effect.Fail
 import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
 import Data.Abstract.Store
 import Data.Abstract.Value
 import Data.Foldable (asum, toList)
-import Data.Pointed
 import Data.Semigroup
+import Data.Semigroup.Reducer
 import Prelude hiding (fail)

 -- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
-class (Monad m, Ord l, Pointed (Cell l), l ~ LocationFor a) => MonadAddressable l a m | m -> a where
-  deref :: Address l a
-        -> m a
+class (Monad m, Ord l, l ~ LocationFor value, Reducer value (Cell l value)) => MonadAddressable l value m where
+  deref :: Address l value -> m value

-  alloc :: Name
-        -> m (Address l a)
+  alloc :: Name -> m (Address l value)

 -- | Look up or allocate an address for a 'Name' free in a given term & assign it a given value, returning the 'Name' paired with the address.
 --
 --   The term is expected to contain one and only one free 'Name', meaning that care should be taken to apply this only to e.g. identifiers.
-lookupOrAlloc :: ( FreeVariables t
-                 , MonadAddressable (LocationFor a) a m
-                 , MonadEvaluator t a m
-                 , Semigroup (Cell (LocationFor a) a)
+lookupOrAlloc :: ( FreeVariables term
+                 , MonadAddressable (LocationFor value) value m
+                 , MonadEvaluator term value m
+                 , Semigroup (CellFor value)
                 )
-                 => t
-                 -> a
-                 -> Environment (LocationFor a) a
-                 -> m (Name, Address (LocationFor a) a)
+                 => term
+                 -> value
+                 -> Environment (LocationFor value) value
+                 -> m (Name, Address (LocationFor value) value)
 lookupOrAlloc term = let [name] = toList (freeVariables term) in
                         lookupOrAlloc' name

 -- | Look up or allocate an address for a 'Name' & assign it a given value, returning the 'Name' paired with the address.
-lookupOrAlloc' :: ( Semigroup (Cell (LocationFor a) a)
-                  , MonadAddressable (LocationFor a) a m
-                  , MonadEvaluator t a m
+lookupOrAlloc' :: ( Semigroup (CellFor value)
+                  , MonadAddressable (LocationFor value) value m
+                  , MonadEvaluator term value m
                  )
                  => Name
-                  -> a
-                  -> Environment (LocationFor a) a
-                  -> m (Name, Address (LocationFor a) a)
+                  -> value
+                  -> Environment (LocationFor value) value
+                  -> m (Name, Address (LocationFor value) value)
 lookupOrAlloc' name v env = do
  a <- maybe (alloc name) pure (envLookup name env)
  assign a v
  pure (name, a)

 -- | Write a value to the given 'Address' in the 'Store'.
-assign :: ( Ord (LocationFor a)
-          , MonadEvaluator t a m
-          , Pointed (Cell (LocationFor a))
-          , Semigroup (Cell (LocationFor a) a)
+assign :: ( Ord (LocationFor value)
+          , MonadEvaluator term value m
+          , Reducer value (CellFor value)
          )
-          => Address (LocationFor a) a
-          -> a
+          => Address (LocationFor value) value
+          -> value
          -> m ()
 assign address = modifyStore . storeInsert address

@ -67,7 +63,7 @@ assign address = modifyStore . storeInsert address
 -- Instances

 -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
-instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddressable Precise v m where
+instance (Monad m, LocationFor value ~ Precise, MonadEvaluator term value m) => MonadAddressable Precise value m where
  deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
    where
      -- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
@ -78,7 +74,7 @@ instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddres


 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, LocationFor v ~ Monovariant, Monad m, MonadEvaluator t v m) => MonadAddressable Monovariant v m where
+instance (Alternative m, Monad m, LocationFor value ~ Monovariant, MonadEvaluator term value m, Ord value) => MonadAddressable Monovariant value m where
  deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup

  alloc = pure . Address . Monovariant
--- a/src/Control/Abstract/Analysis.hs
+++ b/src/Control/Abstract/Analysis.hs
@ -1,18 +1,64 @@
-{-# LANGUAGE DefaultSignatures, FunctionalDependencies #-}
-module Control.Abstract.Analysis where
+{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies #-}
+module Control.Abstract.Analysis
+( MonadAnalysis(..)
+, evaluateTerm
+, liftAnalyze
+, runAnalysis
+, module X
+, Subterm(..)
+, SubtermAlgebra
+) where

+import Control.Abstract.Evaluator as X
+import Control.Effect as X
+import qualified Control.Monad.Effect as Effect
+import Control.Monad.Effect.Fail as X
+import Control.Monad.Effect.Fresh as X
+import Control.Monad.Effect.NonDet as X
+import Control.Monad.Effect.Reader as X
+import Control.Monad.Effect.State as X
+import Data.Coerce
 import Prologue

 -- | A 'Monad' in which one can evaluate some specific term type to some specific value type.
 --
 --   This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
-class Monad m => MonadAnalysis term value m | m -> term, m -> value where
+class (MonadEvaluator term value m, Recursive term) => MonadAnalysis term value m where
+  -- | The effects necessary to run the analysis. Analyses which are composed on top of (wrap) other analyses should include the inner analyses 'RequiredEffects' in their own list.
+  type family RequiredEffects term value m :: [* -> *]
+
  -- | Analyze a term using the semantics of the current analysis. This should generally only be called by definitions of 'evaluateTerm' and 'analyzeTerm' in this or other instances.
  analyzeTerm :: SubtermAlgebra (Base term) term (m value)

-  -- | Evaluate a term to a value using the semantics of the current analysis.
-  --
-  --   This should always be called instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves.
-  evaluateTerm :: MonadAnalysis term value m => term -> m value
-  default evaluateTerm :: (MonadAnalysis term value m, Recursive term) => term -> m value
-  evaluateTerm = foldSubterms analyzeTerm
+  -- | Evaluate a (root-level) term to a value using the semantics of the current analysis. This should be used to evaluate single-term programs as well as each module in multi-term programs.
+  evaluateModule :: term -> m value
+  evaluateModule = evaluateTerm
+
+-- | Evaluate a term to a value using the semantics of the current analysis.
+--
+--   This should always be called when e.g. evaluating the bodies of closures instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves. On the other hand, top-level evaluation should be performed using 'evaluateModule'.
+evaluateTerm :: MonadAnalysis term value m => term -> m value
+evaluateTerm = foldSubterms analyzeTerm
+
+
+-- | Lift a 'SubtermAlgebra' for an underlying analysis into a containing analysis. Use this when defining an analysis which can be composed onto other analyses to ensure that a call to 'analyzeTerm' occurs in the inner analysis and not the outer one.
+liftAnalyze :: ( Coercible (  m term value (effects :: [* -> *]) value) (t m term value effects value)
+               , Coercible (t m term value effects value) (  m term value effects value)
+               , Functor (Base term)
+               )
+            => SubtermAlgebra (Base term) term (  m term value effects value)
+            -> SubtermAlgebra (Base term) term (t m term value effects value)
+liftAnalyze analyze term = coerce (analyze (second coerce <$> term))
+
+
+-- | Run an analysis, performing its effects and returning the result alongside any state.
+--
+--   This enables us to refer to the analysis type as e.g. @Analysis1 (Analysis2 Evaluating) Term Value@ without explicitly mentioning its effects (which are inferred to be simply its 'RequiredEffects').
+runAnalysis :: ( Effectful m
+               , RunEffects effects a
+               , RequiredEffects term value (m effects) ~ effects
+               , MonadAnalysis term value (m effects)
+               )
+            => m effects a
+            -> Final effects a
+runAnalysis = Effect.run . runEffects . lower
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@ -1,19 +1,14 @@
-{-# LANGUAGE DataKinds, FunctionalDependencies, GeneralizedNewtypeDeriving, RankNTypes, StandaloneDeriving, UndecidableInstances, TypeApplications, ScopedTypeVariables #-}
+{-# LANGUAGE ConstrainedClassMethods, FunctionalDependencies #-}
 module Control.Abstract.Evaluator where

-import Prologue
-import Control.Monad.Effect
-import Control.Monad.Effect.Fail
-import Control.Monad.Effect.Fresh
-import Control.Monad.Effect.NonDet
-import Control.Monad.Effect.Reader
-import Control.Monad.Effect.State
 import Data.Abstract.Address
-import Data.Abstract.FreeVariables (Name)
-import Data.Map as Map
+import Data.Abstract.Configuration
+import Data.Abstract.FreeVariables
+import Data.Abstract.Live
 import Data.Abstract.ModuleTable
 import Data.Abstract.Value
 import Prelude hiding (fail)
+import Prologue

 -- | A 'Monad' providing the basic essentials for evaluation.
 --
@ -26,20 +21,14 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
  getGlobalEnv :: m (EnvironmentFor value)
  -- | Set the global environment
  putGlobalEnv :: EnvironmentFor value -> m ()
-  -- | Update the global environment.
-  modifyGlobalEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m ()
-
  withGlobalEnv :: EnvironmentFor value -> m a -> m a

  -- | Add an export to the global export state.
  addExport :: Name -> (Name, Maybe (Address (LocationFor value) value)) -> m ()
-
  -- | Get the global export state.
  getExports :: m (Map Name (Name, Maybe (Address (LocationFor value) value)))
-  -- | Get the global export state.
-
  -- | Sets the exports state to the given map for the lifetime of the given action.
-  withExports :: (Map Name (Name, Maybe (Address (LocationFor value) value))) -> m a -> m a
+  withExports :: Map Name (Name, Maybe (Address (LocationFor value) value)) -> m a -> m a

  -- | Retrieve the local environment.
  askLocalEnv :: m (EnvironmentFor value)
@ -48,8 +37,8 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where

  -- | Retrieve the heap.
  getStore :: m (StoreFor value)
-  -- | Update the heap.
-  modifyStore :: (StoreFor value -> StoreFor value) -> m ()
+  -- | Set the heap.
+  putStore :: StoreFor value -> m ()

  -- | Retrieve the table of evaluated modules.
  getModuleTable :: m (ModuleTable (EnvironmentFor value))
@ -61,44 +50,18 @@ class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
  -- | Run an action with a locally-modified table of unevaluated modules.
  localModuleTable :: (ModuleTable term -> ModuleTable term) -> m a -> m a

-instance Members '[ Fail
-                  , Reader (EnvironmentFor value)
-                  , State  (Map Name (Name, Maybe (Address (LocationFor value) value)))
-                  , State  (EnvironmentFor value)
-                  , State  (StoreFor value)
-                  , Reader (ModuleTable term)
-                  , State  (ModuleTable (EnvironmentFor value))
-                  ] effects
-         => MonadEvaluator term value (Evaluator effects term value) where
-  getGlobalEnv = Evaluator get
-  putGlobalEnv = Evaluator . put
-  modifyGlobalEnv f = Evaluator (modify f)
-  withGlobalEnv s = Evaluator . localState s . runEvaluator
+  -- | Retrieve the current root set.
+  askRoots :: Ord (LocationFor value) => m (Live (LocationFor value) value)
+  askRoots = pure mempty

-  addExport key = Evaluator . modify . Map.insert key
-  getExports = Evaluator get
-  withExports s = Evaluator . localState s . runEvaluator
+  -- | Get the current 'Configuration' with a passed-in term.
+  getConfiguration :: Ord (LocationFor value) => term -> m (Configuration (LocationFor value) term value)
+  getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getStore

-  askLocalEnv = Evaluator ask
-  localEnv f a = Evaluator (local f (runEvaluator a))
+-- | Update the global environment.
+modifyGlobalEnv :: MonadEvaluator term value m => (EnvironmentFor value -> EnvironmentFor value) -> m  ()
+modifyGlobalEnv f = getGlobalEnv >>= putGlobalEnv . f

-  getStore = Evaluator get
-  modifyStore f = Evaluator (modify f)
-
-  getModuleTable = Evaluator get
-  modifyModuleTable f = Evaluator (modify f)
-
-  askModuleTable = Evaluator ask
-  localModuleTable f a = Evaluator (local f (runEvaluator a))
-
-putStore :: MonadEvaluator t value m => StoreFor value -> m ()
-putStore = modifyStore . const
-
-- | An evaluator of @term@s to @value@s, producing incremental results of type @a@ using a list of @effects@.
-newtype Evaluator effects term value a = Evaluator { runEvaluator :: Eff effects a }
-  deriving (Applicative, Functor, Monad)
-
-deriving instance Member Fail effects => MonadFail (Evaluator effects term value)
-deriving instance Member NonDetEff effects => Alternative (Evaluator effects term value)
-deriving instance Member NonDetEff effects => MonadNonDet (Evaluator effects term value)
-deriving instance Member Fresh effects => MonadFresh (Evaluator effects term value)
+-- | Update the heap.
+modifyStore :: MonadEvaluator term value m => (StoreFor value -> StoreFor value) -> m ()
+modifyStore f = getStore >>= putStore . f
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@ -3,66 +3,68 @@ module Control.Abstract.Value where

 import Control.Abstract.Addressable
 import Control.Abstract.Analysis
-import Control.Abstract.Evaluator
-import Control.Monad.Effect.Fresh
-import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
-import Data.Abstract.Value as Value
 import Data.Abstract.Type as Type
+import Data.Abstract.Value as Value
 import Data.Scientific (Scientific)
-import Prologue
 import qualified Data.Map as Map
 import Prelude hiding (fail)
+import Prologue

 -- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
 --
 --   This allows us to abstract the choice of whether to evaluate under binders for different value types.
-class (MonadEvaluator t v m) => MonadValue t v m where
+class (MonadAnalysis term value m, Show value) => MonadValue term value m where
  -- | Construct an abstract unit value.
-  unit :: m v
+  --   TODO: This might be the same as the empty tuple for some value types
+  unit :: m value

  -- | Construct an abstract integral value.
-  integer :: Prelude.Integer -> m v
+  integer :: Prelude.Integer -> m value

  -- | Construct an abstract boolean value.
-  boolean :: Bool -> m v
+  boolean :: Bool -> m value

  -- | Construct an abstract string value.
-  string :: ByteString -> m v
+  string :: ByteString -> m value

  -- | Construct a floating-point value.
-  float :: Scientific -> m v
+  float :: Scientific -> m value
+
+  -- | Construct an N-ary tuple of multiple (possibly-disjoint) values
+  multiple :: [value] -> m value

  -- | Construct an abstract interface value.
-  interface :: v -> m v
+  interface :: value -> m value

  -- | Eliminate boolean values. TODO: s/boolean/truthy
-  ifthenelse :: v -> m v -> m v -> m v
+  ifthenelse :: value -> m value -> m value -> m value

  -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  abstract :: [Name] -> Subterm t (m v) -> m v
+  abstract :: [Name] -> Subterm term (m value) -> m value
  -- | Evaluate an application (like a function call).
-  apply :: v -> [Subterm t (m v)] -> m v
+  apply :: value -> [Subterm term (m value)] -> m value

  -- | Extract the environment from an interface value.
-  environment :: v -> m (EnvironmentFor v)
+  environment :: value -> m (EnvironmentFor value)

 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance ( FreeVariables t
-         , MonadAddressable location (Value location t) m
-         , MonadAnalysis t (Value location t) m
-         , MonadEvaluator t (Value location t) m
-         , Recursive t
-         , Semigroup (Cell location (Value location t))
+instance ( MonadAddressable location (Value location term) m
+         , MonadAnalysis term (Value location term) m
+         , Show location
+         , Show term
         )
-         => MonadValue t (Value location t) m where
+         => MonadValue term (Value location term) m where
+
+  unit    = pure . injValue $ Value.Unit
+  integer = pure . injValue . Integer
+  boolean = pure . injValue . Boolean
+  string  = pure . injValue . Value.String
+  float   = pure . injValue . Value.Float
+  multiple vals =
+    pure . injValue $ Value.Tuple vals

-  unit    = pure $ inj Value.Unit
-  integer = pure . inj . Integer
-  boolean = pure . inj . Boolean
-  string  = pure . inj . Value.String
-  float   = pure . inj . Value.Float
  interface v = do
    -- TODO: If the set of exports is empty because no exports have been
    -- defined, do we export all terms, or no terms? This behavior varies across
@ -70,16 +72,16 @@ instance ( FreeVariables t
    env <- getGlobalEnv
    exports <- getExports
    let env' = if Map.null exports then env else bindExports exports env
-    pure (inj (Value.Interface v env'))
+    pure (injValue (Value.Interface v env'))

  ifthenelse cond if' else'
-    | Just (Boolean b) <- prj cond = if b then if' else else'
-    | otherwise = fail "not defined for non-boolean conditions"
+    | Just (Boolean b) <- prjValue cond = if b then if' else else'
+    | otherwise = fail ("not defined for non-boolean conditions: " <> show cond)

-  abstract names (Subterm body _) = inj . Closure names body <$> askLocalEnv
+  abstract names (Subterm body _) = injValue . Closure names body <$> askLocalEnv

  apply op params = do
-    Closure names body env <- maybe (fail "expected a closure") pure (prj op)
+    Closure names body env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
    bindings <- foldr (\ (name, param) rest -> do
      v <- subtermValue param
      a <- alloc name
@ -88,11 +90,11 @@ instance ( FreeVariables t
    localEnv (mappend bindings) (evaluateTerm body)

  environment v
-    | Just (Interface _ env) <- prj v = pure env
-    | otherwise                       = pure mempty
+    | Just (Interface _ env) <- prjValue v = pure env
+    | otherwise                            = pure mempty

 -- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadValue t Type m where
+instance (Alternative m, MonadAnalysis term Type m, MonadFresh m) => MonadValue term Type m where
  abstract names (Subterm _ body) = do
    (env, tvars) <- foldr (\ name rest -> do
      a <- alloc name
@ -108,6 +110,7 @@ instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadValue t
  boolean _ = pure Bool
  string _  = pure Type.String
  float _   = pure Type.Float
+  multiple  = pure . Type.Product
  -- TODO
  interface = undefined

--- a/src/Control/Effect.hs
+++ b/src/Control/Effect.hs
@ -1,7 +1,6 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, MultiParamTypeClasses, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Control.Effect where

-import Prologue
 import qualified Control.Monad.Effect as Effect
 import Control.Monad.Effect.Fail
 import Control.Monad.Effect.Internal hiding (run)
@ -9,10 +8,12 @@ import Control.Monad.Effect.NonDetEff
 import Control.Monad.Effect.Reader
 import Control.Monad.Effect.State
 import Control.Monad.Effect.Writer
+import Data.Semigroup.Reducer
+import Prologue

-- | Run a computation in 'Eff' to completion, interpreting each effect with some sensible defaults, and return the 'Final' result.
-run :: RunEffects fs a => Eff fs a -> Final fs a
-run = Effect.run . runEffects
+-- | Run an 'Effectful' computation to completion, interpreting each effect with some sensible defaults, and return the 'Final' result.
+run :: (Effectful m, RunEffects effects a) => m effects a -> Final effects a
+run = Effect.run . runEffects . lower

 -- | A typeclass to run a computation to completion, interpreting each effect with some sensible defaults.
 class RunEffects fs a where
@ -60,6 +61,20 @@ instance Monoid w => RunEffect (Writer w) a where
 -- | 'NonDetEff' effects are interpreted into a nondeterministic set of result values.
 instance Ord a => RunEffect NonDetEff a where
  type Result NonDetEff a = Set a
-  runEffect = relay (pure . point) (\ m k -> case m of
+  runEffect = relay (pure . unit) (\ m k -> case m of
    MZero -> pure mempty
    MPlus -> mappend <$> k True <*> k False)
+
+
+-- | Types wrapping 'Eff' actions.
+--
+--   Most instances of 'Effectful' will be derived using @-XGeneralizedNewtypeDeriving@, with these ultimately bottoming out on the instance for 'Eff' (for which 'raise' and 'lower' are simply the identity). Because of this, types can be nested arbitrarily deeply and still call 'raise'/'lower' just once to get at the (ultimately) underlying 'Eff'.
+class Effectful (m :: [* -> *] -> * -> *) where
+  -- | Raise an action in 'Eff' into an action in @m@.
+  raise :: Eff effects a -> m effects a
+  -- | Lower an action in @m@ into an action in 'Eff'.
+  lower :: m effects a -> Eff effects a
+
+instance Effectful Eff where
+  raise = id
+  lower = id
--- a/src/Control/Monad/Effect/NonDet.hs
+++ b/src/Control/Monad/Effect/NonDet.hs
@ -4,15 +4,15 @@ module Control.Monad.Effect.NonDet
 , NonDetEff
 ) where

-import Prologue
 import Control.Monad.Effect.Internal
 import Control.Monad.Effect.NonDetEff
+import Prologue

 -- | 'Monad's offering local isolation of nondeterminism effects.
 class (Alternative m, Monad m) => MonadNonDet m where
  -- | Run a computation, gathering any nondeterministically produced results into a single 'Monoid'al value.
  gather :: Monoid b
-         => (a -> b) -- ^ A function constructing a 'Monoid'al value from a single computed result. This might typically be @point@ (for @Pointed@ functors), 'pure' (for 'Applicative's), or some similar singleton constructor.
+         => (a -> b) -- ^ A function constructing a 'Monoid'al value from a single computed result. This might typically be @unit@ (for @Reducer@s), 'pure' (for 'Applicative's), or some similar singleton constructor.
         -> m a      -- ^ The computation to run locally-nondeterministically.
         -> m b      -- ^ A _deterministic_ computation producing the 'Monoid'al accumulation of the _locally-nondeterministic_ result values.

--- a/src/Control/Monad/Effect/Trace.hs
+++ b/src/Control/Monad/Effect/Trace.hs
@ -1,17 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, TypeOperators, UndecidableInstances #-}
-module Control.Monad.Effect.Trace where
-
-import Control.Monad.Effect
-import Control.Monad.Effect.Writer
-import Data.Abstract.Configuration
-import Data.Abstract.Value
-
-- | 'Monad's offering a writable trace of configurations.
--
--   @t@ is the type of terms, @v@ the type of values, @g@ the type of the collection represented by the log (e.g. '[]' for regular traces, or @Set@ for the trace of reachable states).
-class Monad m => MonadTrace t v g m where
-  -- | Log the given collection of configurations.
-  trace :: g (Configuration (LocationFor v) t v) -> m ()
-
-instance (Writer (g (Configuration (LocationFor v) t v)) :< fs) => MonadTrace t v g (Eff fs) where
-  trace = tell
--- a/src/Data/Abstract/Address.hs
+++ b/src/Data/Abstract/Address.hs
@ -1,8 +1,9 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, TypeFamilyDependencies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeFamilies, TypeFamilyDependencies #-}
 module Data.Abstract.Address where

-import Prologue
 import Data.Abstract.FreeVariables
+import Data.Semigroup.Reducer
+import Prologue

 -- | An abstract address with a location of @l@ pointing to a variable of type @a@.
 newtype Address l a = Address { unAddress :: l }
@ -33,10 +34,12 @@ newtype Latest a = Latest { unLatest :: a }
  deriving (Eq, Foldable, Functor, Generic1, Ord, Show, Traversable)

 instance Semigroup (Latest a) where
-  (<>) = flip const
+  _ <> a = a

-instance Pointed Latest where
-  point = Latest
+instance Reducer a (Latest a) where
+  unit = Latest
+  cons _ = id
+  snoc _ = unit

 instance Eq1 Latest where liftEq = genericLiftEq
 instance Ord1 Latest where liftCompare = genericLiftCompare
--- a/src/Data/Abstract/Cache.hs
+++ b/src/Data/Abstract/Cache.hs
@ -1,32 +1,33 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
 module Data.Abstract.Cache where

-import Prologue
 import Data.Abstract.Address
 import Data.Abstract.Configuration
 import Data.Abstract.Store
-import Data.Map as Map
+import Data.Map.Monoidal as Monoidal
+import Prologue

 -- | A map of 'Configuration's to 'Set's of resulting values & 'Store's.
-newtype Cache l t v = Cache { unCache :: Map.Map (Configuration l t v) (Set (v, Store l v)) }
+newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Store l v)) }

 deriving instance (Eq l, Eq t, Eq v, Eq (Cell l v)) => Eq (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Ord (Cache l t v)
 deriving instance (Show l, Show t, Show v, Show (Cell l v)) => Show (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Semigroup (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Monoid (Cache l t v)
+deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Store l v)) (Cache l t v)

 -- | Look up the resulting value & 'Store' for a given 'Configuration'.
 cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Store l v))
-cacheLookup key = Map.lookup key . unCache
+cacheLookup key = Monoidal.lookup key . unCache

 -- | Set the resulting value & 'Store' for a given 'Configuration', overwriting any previous entry.
 cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Store l v) -> Cache l t v -> Cache l t v
-cacheSet key value = Cache . Map.insert key value . unCache
+cacheSet key value = Cache . Monoidal.insert key value . unCache

 -- | Insert the resulting value & 'Store' for a given 'Configuration', appending onto any previous entry.
 cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Store l v) -> Cache l t v -> Cache l t v
-cacheInsert key value = Cache . Map.insertWith (<>) key (point value) . unCache
+cacheInsert = curry cons


 instance (Eq l, Eq t, Eq1 (Cell l)) => Eq1 (Cache l t) where
--- a/src/Data/Abstract/Configuration.hs
+++ b/src/Data/Abstract/Configuration.hs
@ -6,6 +6,10 @@ import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.Live
 import Data.Abstract.Store
+import Data.Abstract.Value
+
+-- | The configuration for term and abstract value types.
+type ConfigurationFor term value = Configuration (LocationFor value) term value

 -- | A single point in a program’s execution.
 data Configuration l t v
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@ -1,4 +1,4 @@
-{-# LANGUAGE DefaultSignatures, FunctionalDependencies, UndecidableInstances #-}
+{-# LANGUAGE DefaultSignatures, MultiParamTypeClasses, UndecidableInstances #-}
 module Data.Abstract.Evaluatable
 ( Evaluatable(..)
 , module Addressable
@ -12,15 +12,11 @@ module Data.Abstract.Evaluatable

 import Control.Abstract.Addressable as Addressable
 import Control.Abstract.Analysis as Analysis
-import Control.Abstract.Evaluator
 import Control.Abstract.Value as Value
-import Control.Monad.Effect.Fail
-import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables as FreeVariables
 import Data.Abstract.ModuleTable
 import Data.Abstract.Value
-import Data.Algebra
 import Data.Functor.Classes
 import Data.Proxy
 import Data.Semigroup
@ -34,10 +30,7 @@ class Evaluatable constr where
  eval :: ( FreeVariables term
          , MonadAddressable (LocationFor value) value m
          , MonadAnalysis term value m
-          , MonadEvaluator term value m
          , MonadValue term value m
-          , Ord (LocationFor value)
-          , Semigroup (Cell (LocationFor value) value)
          )
       => SubtermAlgebra constr term (m value)
  default eval :: (MonadFail m, Show1 constr) => SubtermAlgebra constr term (m value)
@ -77,27 +70,25 @@ instance Evaluatable [] where
 -- | Require/import another term/file and return an Effect.
 --
 -- Looks up the term's name in the cache of evaluated modules first, returns a value if found, otherwise loads/evaluates the module.
-require :: ( MonadAnalysis term v m
-           , MonadEvaluator term v m
-           , MonadValue term v m
+require :: ( MonadAnalysis term value m
+           , MonadValue term value m
           )
        => ModuleName
-        -> m (EnvironmentFor v)
+        -> m (EnvironmentFor value)
 require name = getModuleTable >>= maybe (load name) pure . moduleTableLookup name

 -- | Load another term/file and return an Effect.
 --
 -- Always loads/evaluates.
-load :: ( MonadAnalysis term v m
-        , MonadEvaluator term v m
-        , MonadValue term v m
+load :: ( MonadAnalysis term value m
+        , MonadValue term value m
        )
     => ModuleName
-     -> m (EnvironmentFor v)
+     -> m (EnvironmentFor value)
 load name = askModuleTable >>= maybe notFound evalAndCache . moduleTableLookup name
  where notFound = fail ("cannot load module: " <> show name)
        evalAndCache e = do
-          v <- evaluateTerm e
+          v <- evaluateModule e
          env <- environment v
          modifyModuleTable (moduleTableInsert name env)
          pure env
--- a/src/Data/Abstract/Store.hs
+++ b/src/Data/Abstract/Store.hs
@ -1,14 +1,15 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
 module Data.Abstract.Store where

-import Prologue
 import Data.Abstract.Address
 import Data.Abstract.Live
-import qualified Data.Map as Map
+import qualified Data.Map.Monoidal as Monoidal
+import Data.Semigroup.Reducer
+import Prologue

 -- | A map of addresses onto cells holding their values.
-newtype Store l a = Store { unStore :: Map.Map l (Cell l a) }
-  deriving (Generic1, Monoid, Semigroup)
+newtype Store l a = Store { unStore :: Monoidal.Map l (Cell l a) }
+  deriving (Generic1)

 deriving instance (Eq l, Eq (Cell l a)) => Eq (Store l a)
 deriving instance (Ord l, Ord (Cell l a)) => Ord (Store l a)
@ -19,23 +20,26 @@ instance (Show l, Show1 (Cell l)) => Show1 (Store l) where liftShowsPrec = gener
 deriving instance Foldable (Cell l) => Foldable (Store l)
 deriving instance Functor (Cell l) => Functor (Store l)
 deriving instance Traversable (Cell l) => Traversable (Store l)
+deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Store l a)
+deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Store l a)
+deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Store l a)

 -- | Look up the cell of values for an 'Address' in a 'Store', if any.
 storeLookup :: Ord l => Address l a -> Store l a -> Maybe (Cell l a)
-storeLookup (Address address) = Map.lookup address . unStore
+storeLookup (Address address) = Monoidal.lookup address . unStore

 -- | Look up the list of values stored for a given address, if any.
 storeLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Store l a -> Maybe [a]
 storeLookupAll address = fmap toList . storeLookup address

 -- | Append a value onto the cell for a given address, inserting a new cell if none existed.
-storeInsert :: (Ord l, Semigroup (Cell l a), Pointed (Cell l)) => Address l a -> a -> Store l a -> Store l a
-storeInsert (Address address) value = Store . Map.insertWith (<>) address (point value) . unStore
+storeInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Store l a -> Store l a
+storeInsert (Address address) value = flip snoc (address, value)

 -- | The number of addresses extant in a 'Store'.
 storeSize :: Store l a -> Int
-storeSize = Map.size . unStore
+storeSize = Monoidal.size . unStore

 -- | Restrict a 'Store' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
 storeRestrict :: Ord l => Store l a -> Live l a -> Store l a
-storeRestrict (Store m) roots = Store (Map.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
+storeRestrict (Store m) roots = Store (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@ -1,4 +1,4 @@
-{-# LANGUAGE ConstraintKinds, DataKinds, FunctionalDependencies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE ConstraintKinds, DataKinds, FunctionalDependencies, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
 module Data.Abstract.Value where

 import Data.Abstract.Address
@ -10,32 +10,42 @@ import qualified Data.Abstract.Type as Type
 import qualified Data.Set as Set
 import Data.Scientific (Scientific)
 import Prologue
-import Prelude hiding (Float, Integer, String, fail)
+import Prelude hiding (Float, Integer, String)
 import qualified Prelude

-type ValueConstructors location
-  = '[Closure location
+type ValueConstructors location term
+  = '[Closure location term
    , Interface location
    , Unit
    , Boolean
    , Float
    , Integer
    , String
+    , Tuple
    ]

 -- | Open union of primitive values that terms can be evaluated to.
-type Value location = Union (ValueConstructors location)
+--   Fix by another name.
+newtype Value location term = Value { deValue :: Union (ValueConstructors location term) (Value location term) }
+  deriving (Eq, Show, Ord)
+
+-- | Identical to 'inj', but wraps the resulting sub-entity in a 'Value'.
+injValue :: (f :< ValueConstructors location term) => f (Value location term) -> Value location term
+injValue = Value . inj
+
+-- | Identical to 'prj', but unwraps the argument out of its 'Value' wrapper.
+prjValue :: (f :< ValueConstructors location term) => Value location term -> Maybe (f (Value location term))
+prjValue = prj . deValue

 -- TODO: Parameterize Value by the set of constructors s.t. each language can have a distinct value union.
-- TODO: Wrap the Value union in a newtype to differentiate from (eventual) à la carte Types.

 -- | A function value consisting of a list of parameters, the body of the function, and an environment of bindings captured by the body.
-data Closure location term = Closure [Name] term (Environment location (Value location term))
+data Closure location term value = Closure [Name] term (Environment location value)
  deriving (Eq, Generic1, Ord, Show)

-instance (Eq location) => Eq1 (Closure location) where liftEq = genericLiftEq
-instance (Ord location) => Ord1 (Closure location) where liftCompare = genericLiftCompare
-instance (Show location) => Show1 (Closure location) where liftShowsPrec = genericLiftShowsPrec
+instance (Eq location, Eq term) => Eq1 (Closure location term) where liftEq = genericLiftEq
+instance (Ord location, Ord term) => Ord1 (Closure location term) where liftCompare = genericLiftCompare
+instance (Show location, Show term) => Show1 (Closure location term) where liftShowsPrec = genericLiftShowsPrec

 -- | A program value consisting of the value of the program and its environment of bindings.
 --   The @Value@ stored herein is the last value evaluated within a given @Program@,
@ -43,7 +53,7 @@ instance (Show location) => Show1 (Closure location) where liftShowsPrec = gener
 --   compilation unit. If you want to get at the bindings of an interface (which
 --   is probably what you want), look them up in the provided environment, not
 --   in the value.
-data Interface location term = Interface (Value location term) (Environment location (Value location term))
+data Interface location value = Interface value (Environment location value)
  deriving (Eq, Generic1, Ord, Show)

 instance (Eq location) => Eq1 (Interface location) where liftEq = genericLiftEq
@ -51,7 +61,7 @@ instance (Ord location) => Ord1 (Interface location) where liftCompare = generic
 instance (Show location) => Show1 (Interface location) where liftShowsPrec = genericLiftShowsPrec

 -- | The unit value. Typically used to represent the result of imperative statements.
-data Unit term = Unit
+data Unit value = Unit
  deriving (Eq, Generic1, Ord, Show)

 instance Eq1 Unit where liftEq = genericLiftEq
@ -59,7 +69,7 @@ instance Ord1 Unit where liftCompare = genericLiftCompare
 instance Show1 Unit where liftShowsPrec = genericLiftShowsPrec

 -- | Boolean values.
-newtype Boolean term = Boolean Prelude.Bool
+newtype Boolean value = Boolean Prelude.Bool
  deriving (Eq, Generic1, Ord, Show)

 instance Eq1 Boolean where liftEq = genericLiftEq
@ -67,7 +77,7 @@ instance Ord1 Boolean where liftCompare = genericLiftCompare
 instance Show1 Boolean where liftShowsPrec = genericLiftShowsPrec

 -- | Arbitrary-width integral values.
-newtype Integer term = Integer Prelude.Integer
+newtype Integer value = Integer Prelude.Integer
  deriving (Eq, Generic1, Ord, Show)

 instance Eq1 Integer where liftEq = genericLiftEq
@ -75,7 +85,7 @@ instance Ord1 Integer where liftCompare = genericLiftCompare
 instance Show1 Integer where liftShowsPrec = genericLiftShowsPrec

 -- | String values.
-newtype String term = String ByteString
+newtype String value = String ByteString
  deriving (Eq, Generic1, Ord, Show)

 instance Eq1 String where liftEq = genericLiftEq
@ -83,19 +93,33 @@ instance Ord1 String where liftCompare = genericLiftCompare
 instance Show1 String where liftShowsPrec = genericLiftShowsPrec

 -- | Float values.
-newtype Float term = Float Scientific
+newtype Float value = Float Scientific
  deriving (Eq, Generic1, Ord, Show)

 instance Eq1 Float where liftEq = genericLiftEq
 instance Ord1 Float where liftCompare = genericLiftCompare
 instance Show1 Float where liftShowsPrec = genericLiftShowsPrec

+-- Zero or more values.
+-- TODO: Investigate whether we should use Vector for this.
+-- TODO: Should we have a Some type over a nonemmpty list? Or does this merit one?
+
+newtype Tuple value = Tuple [value]
+  deriving (Eq, Generic1, Ord, Show)
+
+instance Eq1 Tuple where liftEq = genericLiftEq
+instance Ord1 Tuple where liftCompare = genericLiftCompare
+instance Show1 Tuple where liftShowsPrec = genericLiftShowsPrec
+
 -- | The environment for an abstract value type.
 type EnvironmentFor v = Environment (LocationFor v) v

 -- | The store for an abstract value type.
 type StoreFor v = Store (LocationFor v) v

+-- | The cell for an abstract value type.
+type CellFor value = Cell (LocationFor value) value
+
 -- | The location type (the body of 'Address'es) which should be used for an abstract value type.
 type family LocationFor value :: * where
  LocationFor (Value location term) = location
@ -108,8 +132,8 @@ class ValueRoots l v | v -> l where

 instance (FreeVariables term, Ord location) => ValueRoots location (Value location term) where
  valueRoots v
-    | Just (Closure names body env) <- prj v = envRoots env (foldr Set.delete (freeVariables body) names)
-    | otherwise                              = mempty
+    | Just (Closure names body env) <- prjValue v = envRoots env (foldr Set.delete (freeVariables (body :: term)) names)
+    | otherwise                                   = mempty

 instance ValueRoots Monovariant Type.Type where
  valueRoots _ = mempty
--- a/src/Data/Algebra.hs
+++ b/src/Data/Algebra.hs
@ -14,6 +14,7 @@ module Data.Algebra
 , openFToOpenR
 ) where

+import Data.Bifunctor
 import Data.Functor.Foldable ( Base
                             , Corecursive(embed)
                             , Recursive(project)
@ -45,7 +46,10 @@ type OpenRAlgebra f t a = forall b . (b -> (t, a)) -> f b -> a

 -- | A subterm and its computed value, used in 'SubtermAlgebra'.
 data Subterm t a = Subterm { subterm :: !t, subtermValue :: !a }
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
+
+instance Bifunctor Subterm where
+  bimap f g (Subterm a b) = Subterm (f a) (g b)

 -- | Like an R-algebra, but using 'Subterm' to label the fields instead of an anonymous pair.
 type SubtermAlgebra f t a = f (Subterm t a) -> a
--- a/src/Data/Diff.hs
+++ b/src/Data/Diff.hs
@ -82,11 +82,6 @@ merging :: Functor syntax => Term syntax ann -> Diff syntax ann ann
 merging = cata (\ (In ann syntax) -> mergeF (In (ann, ann) syntax))


-diffPatch :: Diff syntax ann1 ann2 -> Maybe (Patch (TermF syntax ann1 (Diff syntax ann1 ann2)) (TermF syntax ann2 (Diff syntax ann1 ann2)))
-diffPatch diff = case unDiff diff of
-  Patch patch -> Just patch
-  _ -> Nothing
-
 diffPatches :: (Foldable syntax, Functor syntax) => Diff syntax ann1 ann2 -> [Patch (TermF syntax ann1 (Diff syntax ann1 ann2)) (TermF syntax ann2 (Diff syntax ann1 ann2))]
 diffPatches = para $ \ diff -> case diff of
  Patch patch -> bimap (fmap fst) (fmap fst) patch : bifoldMap (foldMap snd) (foldMap snd) patch
--- a/src/Data/Map/Monoidal.hs
+++ b/src/Data/Map/Monoidal.hs
@ -0,0 +1,44 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses #-}
+-- | This module defines a 'Map' type whose 'Monoid' and 'Reducer' instances merge values using the 'Semigroup' instance for the underlying type.
+module Data.Map.Monoidal
+( Map
+, lookup
+, size
+, insert
+, filterWithKey
+, module Reducer
+) where
+
+import qualified Data.Map as Map
+import Data.Semigroup.Reducer as Reducer
+import Prelude hiding (lookup)
+import Prologue hiding (Map)
+
+newtype Map key value = Map { unMap :: Map.Map key value }
+  deriving (Eq, Eq1, Eq2, Foldable, Functor, Ord, Ord1, Ord2, Show, Show1, Show2, Traversable)
+
+
+lookup :: Ord key => key -> Map key value -> Maybe value
+lookup key = Map.lookup key . unMap
+
+size :: Map key value -> Int
+size = Map.size . unMap
+
+insert :: Ord key => key -> value -> Map key value -> Map key value
+insert key value = Map . Map.insert key value . unMap
+
+filterWithKey :: (key -> value -> Bool) -> Map key value -> Map key value
+filterWithKey f = Map . Map.filterWithKey f . unMap
+
+
+instance (Ord key, Semigroup value) => Semigroup (Map key value) where
+  Map a <> Map b = Map (Map.unionWith (<>) a b)
+
+instance (Ord key, Semigroup value) => Monoid (Map key value) where
+  mempty = Map Map.empty
+  mappend = (<>)
+
+instance (Ord key, Reducer a value) => Reducer (key, a) (Map key value) where
+  unit (key, a) = Map (Map.singleton key (unit a))
+  cons (key, a) (Map m) = Map (Map.insertWith (<>) key (unit a) m)
+  snoc (Map m) (key, a) = Map (Map.insertWith (flip (<>)) key (unit a) m)
--- a/src/Data/Syntax.hs
+++ b/src/Data/Syntax.hs
@ -7,6 +7,7 @@ import Data.Abstract.Evaluatable
 import Data.AST
 import Data.Range
 import Data.Record
+import qualified Data.Set as Set
 import Data.Span
 import Data.Term
 import Diffing.Algorithm hiding (Empty)
@ -112,7 +113,7 @@ instance Evaluatable Identifier where
    maybe (fail ("free variable: " <> show name)) deref (envLookup name env)

 instance FreeVariables1 Identifier where
-  liftFreeVariables _ (Identifier x) = point x
+  liftFreeVariables _ (Identifier x) = Set.singleton x


 newtype Program a = Program [a]
--- a/src/Data/Syntax/Declaration.hs
+++ b/src/Data/Syntax/Declaration.hs
@ -1,13 +1,11 @@
 {-# LANGUAGE DeriveAnyClass, MultiParamTypeClasses, ScopedTypeVariables, UndecidableInstances #-}
 module Data.Syntax.Declaration where

-import Prologue
 import Data.Abstract.Environment
 import Data.Abstract.Evaluatable
 import Diffing.Algorithm
 import qualified Data.Map as Map
-import Data.ByteString as B
-import qualified Data.List.NonEmpty as NonEmpty
+import Prologue

 data Function a = Function { functionContext :: ![a], functionName :: !a, functionParameters :: ![a], functionBody :: !a }
  deriving (Eq, Foldable, Functor, GAlign, Generic1, Mergeable, Ord, Show, Traversable, FreeVariables1)
@ -90,7 +88,7 @@ instance Evaluatable OptionalParameter

 -- TODO: Should we replace this with Function and differentiate by context?
 -- TODO: How should we distinguish class/instance methods?
-
+-- TODO: It would be really nice to have a more meaningful type contained in here than [a]
 -- | A declaration of possibly many variables such as var foo = 5, bar = 6 in JavaScript.
 newtype VariableDeclaration a = VariableDeclaration { variableDeclarations :: [a] }
  deriving (Diffable, Eq, Foldable, Functor, GAlign, Generic1, Mergeable, Ord, Show, Traversable, FreeVariables1)
@ -99,9 +97,9 @@ instance Eq1 VariableDeclaration where liftEq = genericLiftEq
 instance Ord1 VariableDeclaration where liftCompare = genericLiftCompare
 instance Show1 VariableDeclaration where liftShowsPrec = genericLiftShowsPrec

-- TODO: Implement Eval instance for VariableDeclaration
-instance Evaluatable VariableDeclaration
-
+instance Evaluatable VariableDeclaration where
+  eval (VariableDeclaration [])   = unit
+  eval (VariableDeclaration decs) = multiple =<< traverse subtermValue decs

 -- | A TypeScript/Java style interface declaration to implement.
 data InterfaceDeclaration a = InterfaceDeclaration { interfaceDeclarationContext :: ![a], interfaceDeclarationIdentifier :: !a, interfaceDeclarationBody :: !a }
--- a/src/Data/Syntax/Literal.hs
+++ b/src/Data/Syntax/Literal.hs
@ -236,9 +236,8 @@ instance Eq1 Tuple where liftEq = genericLiftEq
 instance Ord1 Tuple where liftCompare = genericLiftCompare
 instance Show1 Tuple where liftShowsPrec = genericLiftShowsPrec

-- TODO: Implement Eval instance for Tuple
-instance Evaluatable Tuple
-
+instance Evaluatable Tuple where
+  eval (Tuple cs) = multiple =<< traverse subtermValue cs

 newtype Set a = Set { setElements :: [a] }
  deriving (Diffable, Eq, Foldable, Functor, GAlign, Generic1, Mergeable, Ord, Show, Traversable, FreeVariables1)
--- a/src/Language/TypeScript/Assignment.hs
+++ b/src/Language/TypeScript/Assignment.hs
@ -13,8 +13,6 @@ import Data.Syntax (emptyTerm, handleError, parseError, infixContext, makeTerm,
 import Language.TypeScript.Grammar as Grammar
 import Prologue
 import qualified Data.ByteString.Char8 as BC
-import qualified Data.ByteString as B
-import Data.Char (ord)
 import qualified Assigning.Assignment as Assignment
 import qualified Data.Syntax as Syntax
 import qualified Data.Syntax.Comment as Comment
--- a/src/Language/TypeScript/Syntax.hs
+++ b/src/Language/TypeScript/Syntax.hs
@ -77,6 +77,8 @@ newtype Tuple a = Tuple { _tupleElements :: [a] }
 instance Eq1 Tuple where liftEq = genericLiftEq
 instance Ord1 Tuple where liftCompare = genericLiftCompare
 instance Show1 Tuple where liftShowsPrec = genericLiftShowsPrec
+
+-- This is a tuple type, not a tuple value, so we can't lean on the shared Tuple value
 instance Evaluatable Tuple

 data Constructor a = Constructor { _constructorTypeParameters :: !a, _constructorFormalParameters :: ![a], _constructorType :: !a }
--- a/src/Prologue.hs
+++ b/src/Prologue.hs
@ -53,7 +53,6 @@ import Data.Functor.Classes.Generic as X
 import Data.Functor.Foldable as X (Base, Recursive(..), Corecursive(..))
 import Data.Mergeable as X (Mergeable)
 import Data.Monoid as X (Monoid(..), First(..), Last(..))
-import Data.Pointed as X
 import Data.Proxy as X (Proxy(..))
 import Data.Semigroup as X (Semigroup(..))
 import Data.Traversable as X
--- a/src/Semantic/Util.hs
+++ b/src/Semantic/Util.hs
@ -1,11 +1,13 @@
 -- MonoLocalBinds is to silence a warning about a simplifiable constraint.
-{-# LANGUAGE DataKinds, MonoLocalBinds, TypeOperators, TypeApplications #-}
+{-# LANGUAGE DataKinds, MonoLocalBinds, TypeApplications, TypeOperators #-}
 module Semantic.Util where

-import Prologue
 import Analysis.Abstract.Caching
+import Analysis.Abstract.Dead
 import Analysis.Abstract.Evaluating
+import Analysis.Abstract.Tracing
 import Analysis.Declaration
+import Control.Abstract.Analysis
 import Control.Monad.IO.Class
 import Data.Abstract.Address
 import Data.Abstract.Type
@ -20,13 +22,14 @@ import Data.Term
 import Diffing.Algorithm
 import Diffing.Interpreter
 import Parsing.Parser
+import Prologue
 import Semantic
 import Semantic.IO as IO
 import Semantic.Task

 import qualified Language.Go.Assignment as Go
-import qualified Language.Ruby.Assignment as Ruby
 import qualified Language.Python.Assignment as Python
+import qualified Language.Ruby.Assignment as Ruby
 import qualified Language.TypeScript.Assignment as TypeScript

 type Language a = Value Precise (Term (Union a) (Record Location))
@ -40,20 +43,18 @@ file :: MonadIO m => FilePath -> m Blob
 file path = fromJust <$> IO.readFile path (languageForFilePath path)

 -- Ruby
-evaluateRubyFile path = Prelude.fst . evaluate @RubyValue <$>
-  (file path >>= runTask . parse rubyParser)
+evaluateRubyFile path = fst . evaluate @RubyValue . snd <$> parseFile rubyParser path

 evaluateRubyFiles paths = do
-  blobs@(b:bs) <- traverse file paths
-  (t:ts) <- runTask $ traverse (parse rubyParser) blobs
-  pure $ evaluates @RubyValue (zip bs ts) (b, t)
+  first:rest <- traverse (parseFile rubyParser) paths
+  pure $ evaluates @RubyValue rest first

 -- Go
-typecheckGoFile path = evaluateCache @Type <$>
-  (file path >>= runTask . parse goParser)
+typecheckGoFile path = runAnalysis @(Caching Evaluating Go.Term Type) . evaluateModule . snd <$>
+  parseFile goParser path

-evaluateGoFile path = evaluateCache @GoValue <$>
-  (file path >>= runTask . parse goParser)
+evaluateGoFile path = runAnalysis @(Evaluating Go.Term GoValue) . evaluateModule . snd <$>
+  parseFile goParser path

 evaluateGoFiles paths = do
  blobs@(b:bs) <- traverse file paths
@ -61,25 +62,30 @@ evaluateGoFiles paths = do
  pure $ evaluates @GoValue (zip bs ts) (b, t)

 -- Python
-typecheckPythonFile path = evaluateCache @Type <$>
-  (file path >>= runTask . parse pythonParser)
+typecheckPythonFile path = runAnalysis @(Caching Evaluating Python.Term Type) . evaluateModule . snd <$> parseFile pythonParser path

-evaluatePythonFile path = evaluate @PythonValue <$>
-  (file path >>= runTask . parse pythonParser)
+tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
+
+evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
+
+evaluatePythonFile path = evaluate @PythonValue . snd <$> parseFile pythonParser path

 evaluatePythonFiles paths = do
-  blobs@(b:bs) <- traverse file paths
-  (t:ts) <- runTask $ traverse (parse pythonParser) blobs
-  pure $ evaluates @PythonValue (zip bs ts) (b, t)
+  first:rest <- traverse (parseFile pythonParser) paths
+  pure $ evaluates @PythonValue rest first

 -- TypeScript
-evaluateTypeScriptFile path = Prelude.fst . evaluate @TypeScriptValue <$>
-  (file path >>= runTask . parse typescriptParser)
+evaluateTypeScriptFile path = fst . evaluate @TypeScriptValue . snd <$> parseFile typescriptParser path

 evaluateTypeScriptFiles paths = do
-  blobs@(b:bs) <- traverse file paths
-  (t:ts) <- runTask $ traverse (parse typescriptParser) blobs
-  pure $ evaluates @TypeScriptValue (zip bs ts) (b, t)
+  first:rest <- traverse (parseFile typescriptParser) paths
+  pure $ evaluates @TypeScriptValue rest first
+
+
+parseFile :: Parser term -> FilePath -> IO (Blob, term)
+parseFile parser path = runTask $ do
+  blob <- file path
+  (,) blob <$> parse parser blob


 -- Diff helpers