Exception tracking #666
Exception tracking #666
Conversation
This is almost certainly wrong overall, but it's a start.
| @@ -0,0 +1,40 @@ | |||
| -- GHCI settings, collected by running cabal repl -v and checking out the flags cabal passes to ghc. | |||
There was a problem hiding this comment.
This and several other files exist solely to make local development of just semantic-analysis more convenient.
| data Snoc a = Nil | Snoc a :> a | ||
| deriving (Foldable, Functor, Traversable) | ||
|
|
||
|
|
There was a problem hiding this comment.
It looked like it would be important for Snoc to be accessible elsewhere. It turned out not to be, but there's no reason it shouldn't have its own home.
| dif :: Has (Dom val) sig m => val -> m a -> m a -> m a | ||
| dif :: Has (Dom val) sig m => val -> m val -> m val -> m val |
There was a problem hiding this comment.
This is necessary for us to collect the results from both branches of a conditional in exception tracking. a would always be val during abstract interpretation anyway, so it doesn't hurt us any.
| DAbs _ b -> runExcC (hdl (b mempty <$ ctx)) | ||
| DApp f a -> pure $ f <> a <$ ctx |
There was a problem hiding this comment.
We dive into abstractions eagerly, like a typechecker would. Then in applications we can simply union up the results.
This is wrong: it means we'll charge exceptions thrown within a lambda to the lambda, not to call sites, as tho the exceptions were thrown when constructing the lambda, rather than when calling it. Wrong, but convenient: it means we don't have to construct closures (or any model thereof) and then have to deal with partiality on application.
| DBool _ -> pure nil | ||
| DIf c t e -> fmap (mappend c) <$> runExcC (hdl (t <$ ctx) <|> hdl (e <$ ctx)) | ||
| DString _ -> pure nil | ||
| DDie e -> pure $ e <> fromExceptions [Exception n | n <- Set.toList (freeVariables e)] <$ ctx |
There was a problem hiding this comment.
This is the only really interesting case. We return all the free variables and exceptions in the argument, as well as making exceptions from the former.
That means raise IOError is going to (correctly) throw IOError, while raise "foo" won't return anything (underapproximation), and raise Foo(bar) will throw both Foo and bar (overapproximation).
🎩 @patrickt for an excellent observation.
This PR copies exception tracking from membrane into semantic-analysis, transposing as necessary to reflect the differing domain abstractions. (This was intended to have been done at the same time as #659, but got overlooked.)
Note that some details necessarily differ slightly; our
Domabstraction is a fair bit different, and in particular theirddie(which throws an exception) takes aString, while ours takes aval(as of #664), making ours more expressive, but more subtle as well.I'm likely to push the modular abstract interpretation stuff to a future PR.