Merge pull request #204 from github/sequence-values-in-the-abstract-domain

Sequence values in the abstract domain

Author: robrix

semantic-core/src/Analysis/Concrete.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
 module Analysis.Concrete
 ( Concrete(..)
 , concrete
@@ -28,6 +28,7 @@ import qualified Data.IntSet as IntSet
 import           Data.Loc
 import qualified Data.Map as Map
 import           Data.Name
+import           Data.Semigroup (Last (..))
 import qualified Data.Set as Set
 import           Data.Term
 import           Data.Text (Text, pack)
@@ -47,6 +48,8 @@ data Concrete
   | String Text
   | Record Env
   deriving (Eq, Ord, Show)
+  -- NB: We derive the 'Semigroup' instance for 'Concrete' to take the second argument. This is equivalent to stating that the return value of an imperative sequence of statements is the value of its final statement.
+  deriving Semigroup via Last Concrete
 
 recordFrame :: Concrete -> Maybe Env
 recordFrame (Record frame) = Just frame

semantic-core/src/Analysis/Eval.hs

@@ -30,6 +30,7 @@ import Prelude hiding (fail)
 eval :: ( Carrier sig m
         , Member (Reader Loc) sig
         , MonadFail m
+        , Semigroup value
         )
      => Analysis address value m
      -> (Term Core User -> m value)
@@ -41,12 +42,15 @@ eval Analysis{..} eval = \case
       addr <- alloc n
       v <- bind n addr (eval (instantiate1 (pure n) b))
       v <$ assign addr v
-    a :>> b -> eval a >> eval b
+    -- NB: Combining the results of the evaluations allows us to model effects in abstract domains. This in turn means that we can define an abstract domain modelling the types-and-effects of computations by means of a 'Semigroup' instance which takes the type of its second operand and the union of both operands’ effects.
+    --
+    -- It’s also worth noting that we use a semigroup instead of a semilattice because the lattice structure of our abstract domains is instead modelled by nondeterminism effects used by some of them.
+    a :>> b -> (<>) <$> eval a <*> eval b
     Named (Ignored n) a :>>= b -> do
       a' <- eval a
       addr <- alloc n
       assign addr a'
-      bind n addr (eval (instantiate1 (pure n) b))
+      bind n addr ((a' <>) <$> eval (instantiate1 (pure n) b))
     Lam (Named (Ignored n) b) -> abstract eval n (instantiate1 (pure n) b)
     f :$ a -> do
       f' <- eval f
@@ -210,18 +214,18 @@ ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' stateme
 
 
 data Analysis address value m = Analysis
-  { alloc       :: User -> m address
-  , bind        :: forall a . User -> address -> m a -> m a
-  , lookupEnv   :: User -> m (Maybe address)
-  , deref       :: address -> m (Maybe value)
-  , assign      :: address -> value -> m ()
-  , abstract    :: (Term Core User -> m value) -> User -> Term Core User -> m value
-  , apply       :: (Term Core User -> m value) -> value -> value -> m value
-  , unit        :: m value
-  , bool        :: Bool -> m value
-  , asBool      :: value -> m Bool
-  , string      :: Text -> m value
-  , asString    :: value -> m Text
-  , record      :: [(User, value)] -> m value
-  , (...)       :: address -> User -> m (Maybe address)
+  { alloc     :: User -> m address
+  , bind      :: forall a . User -> address -> m a -> m a
+  , lookupEnv :: User -> m (Maybe address)
+  , deref     :: address -> m (Maybe value)
+  , assign    :: address -> value -> m ()
+  , abstract  :: (Term Core User -> m value) -> User -> Term Core User -> m value
+  , apply     :: (Term Core User -> m value) -> value -> value -> m value
+  , unit      :: m value
+  , bool      :: Bool -> m value
+  , asBool    :: value -> m Bool
+  , string    :: Text -> m value
+  , asString  :: value -> m Text
+  , record    :: [(User, value)] -> m value
+  , (...)     :: address -> User -> m (Maybe address)
   }

semantic-core/src/Analysis/Typecheck.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-}
+{-# LANGUAGE DeriveGeneric, DeriveTraversable, DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-}
 module Analysis.Typecheck
 ( Monotype (..)
 , Meta
@@ -30,6 +30,7 @@ import qualified Data.Map as Map
 import           Data.Maybe (fromJust, fromMaybe)
 import           Data.Name as Name
 import           Data.Scope
+import           Data.Semigroup (Last (..))
 import qualified Data.Set as Set
 import           Data.Term
 import           Data.Void
@@ -44,6 +45,11 @@ data Monotype f a
   | Record (Map.Map User (f a))
   deriving (Foldable, Functor, Generic1, Traversable)
 
+-- FIXME: Union the effects/annotations on the operands.
+
+-- | We derive the 'Semigroup' instance for types to take the second argument. This is equivalent to stating that the type of an imperative sequence of statements is the type of its final statement.
+deriving via (Last (Term Monotype a)) instance Semigroup (Term Monotype a)
+
 deriving instance (Eq   a, forall a . Eq   a => Eq   (f a), Monad f) => Eq   (Monotype f a)
 deriving instance (Ord  a, forall a . Eq   a => Eq   (f a)
                          , forall a . Ord  a => Ord  (f a), Monad f) => Ord  (Monotype f a)