Sequence values in the abstract domain #204
Conversation
| , string :: Text -> m value | ||
| , asString :: value -> m Text | ||
| , record :: [(User, value)] -> m value | ||
| , (...) :: address -> User -> m (Maybe address) |
There was a problem hiding this comment.
Whitespace-only changes to this block.
| deriving (Foldable, Functor, Generic1, Traversable) | ||
|
|
||
| -- FIXME: Union the effects/annotations on the operands. | ||
| deriving via (Last (Term Monotype a)) instance Semigroup (Term Monotype a) |
There was a problem hiding this comment.
I was legit surprised that this instance isn’t orphaned, but it’s due to Monotype being defined in this module.
| | String Text | ||
| | Record Env | ||
| deriving (Eq, Ord, Show) | ||
| deriving Semigroup via Last Concrete |
There was a problem hiding this comment.
This instance makes me so happy!
| v <- bind n addr (eval (instantiate1 (pure n) b)) | ||
| v <$ assign addr v | ||
| a :>> b -> eval a >> eval b | ||
| a :>> b -> (<>) <$> eval a <*> eval b |
There was a problem hiding this comment.
Combining the results of evaluations together with <> enables us to model effects compositionally. E.g. given a program like:
def f
a
b
endThen a domain modelling the type-and-effect of f will define <> to combine the effects incurred by both a and b while taking the type of only b, whereas a domain modelling the import graph would union together any imports performed by either a or b. On the other hand, the concrete domain implements <> to simply discard a, since it isn’t attempting to instrument the effects, only perform them.
There was a problem hiding this comment.
It’s also worth asking: why a semigroup, when so much of the abstract interpretation literature focuses on (semi)lattices? In short, our lattice structure is provided by the sets of computations performed under the nondeterminism effect; paraphrasing Darais et al, concretization maps values in the abstract domain to finite sets of observations in the concrete domain. So in short, the lattice’s least upper bound operation is a) provided by NonDet, and b) semantically distinct from the use of <> to combine sequenced abstracted values.
There was a problem hiding this comment.
Finally, we could eventually consider strengthening the Semigroup constraint to Monoid to allow us to represent divergent/exceptional computation with mempty; or further strengthening it to some sort of unital semiring structure to combine the two kinds of combination, with addition for the least upper bound, zero for the bottom, multiplication for sequencing, and unit for its, well, unit. (I haven’t actually checked to see if this would actually be a lawful semiring; the distributive laws seem like they’d be pretty interesting.)
There was a problem hiding this comment.
This all makes total sense to me, and is a huge win for clarity. Can we move the relevant sections of the above comments (which are wonderful!) to comments on the deriving instances for Concrete and Term Monotype a?
| v <- bind n addr (eval (instantiate1 (pure n) b)) | ||
| v <$ assign addr v | ||
| a :>> b -> eval a >> eval b | ||
| a :>> b -> (<>) <$> eval a <*> eval b |
There was a problem hiding this comment.
This all makes total sense to me, and is a huge win for clarity. Can we move the relevant sections of the above comments (which are wonderful!) to comments on the deriving instances for Concrete and Term Monotype a?
This PR uses a
Semigroupinstance on the abstract domain in order to combine sequenced values together. This in turn allows us to compute import/scope graphs for imperative sequences of code using an abstract domain (i.e. by returning graphs as values) instead of requiring out-of-band instrumentation (e.g. aWritereffect accumulating a graph).