Parametric modular interpretation #659
Conversation
|
|
||
| source-repository-package | ||
| type: git | ||
| location: https://github.com/antitypical/fused-syntax.git | ||
| tag: 4a383d57c8fd7592f54a33f43eb9666314a6e80e |
There was a problem hiding this comment.
🔥
fused-syntax had been used for Core (along with a few other things), but it never worked the way I wanted and I don’t think it’s a good idea to try to continue maintaining it for the sake of this, so 🔥
| @@ -22,7 +22,6 @@ newtype EnvC m a = EnvC { runEnv :: m a } | |||
| instance Algebra sig m | |||
| => Algebra (Env Name :+: sig) (EnvC m) where | |||
| alg hdl sig ctx = case sig of | |||
| L (Alloc name) -> pure (name <$ ctx) | |||
There was a problem hiding this comment.
This should never have been here.
| runFail :: FailC m a -> m (Either (Reference, String) a) | ||
| runFail = runError . runFailC | ||
|
|
||
| newtype FailC m a = FailC { runFailC :: ErrorC (Reference, String) m a } | ||
| deriving (Alternative, Applicative, Functor, Monad) | ||
|
|
||
| instance Has (Reader Reference) sig m => MonadFail (FailC m) where | ||
| fail s = do | ||
| ref <- ask | ||
| FailC (throwError (ref :: Reference, s)) | ||
|
|
||
| instance Has (Reader Reference) sig m => Algebra (Fail :+: sig) (FailC m) where | ||
| alg _ (L (Fail s)) _ = fail s | ||
| alg hdl (R other) ctx = FailC (alg (runFailC . hdl) (R other) ctx) |
There was a problem hiding this comment.
This used to live elsewhere in the project. I’ve moved it here, and simplified it slightly by use of the Reference type (introduced in this PR, see below).
| {-# LANGUAGE MultiParamTypeClasses #-} | ||
| {-# LANGUAGE TypeOperators #-} | ||
| {-# LANGUAGE UndecidableInstances #-} | ||
| module Analysis.Carrier.Heap.Monovariant |
There was a problem hiding this comment.
Heapisn’t standard nomenclature when talking abstract interpretation;Storeis.- This was unnecessarily hard to use as defined. The
Storeeffect and carrier that replace it are more ergonomic.
| R other -> alg (runStoreC . hdl) other ctx | ||
|
|
||
|
|
||
| -- Env carrier |
There was a problem hiding this comment.
For convenience, I’ve placed both the Store and Env carriers in a single module. This makes it very slightly less convenient to mix-and-match, but that’s not something we expect to do in the short to medium term anyway.
| abstract :: Eq a => a -> Polytype a -> Polytype (Maybe a) | ||
| abstract n = fmap (\ a -> a <$ guard (a == n)) | ||
|
|
||
|
|
||
| forAll :: Eq a => a -> Polytype a -> Polytype a | ||
| forAll n body = PForAll (abstract n body) | ||
|
|
||
| forAlls :: (Eq a, Foldable t) => t a -> Polytype a -> Polytype a | ||
| forAlls ns body = foldr forAll body ns |
There was a problem hiding this comment.
This is the I Am Not a Number, I Am a Free Variable approach. It doesn’t give the fastest abstraction and substitution (relative to e.g. bound, but a) that doesn’t actually matter at all for our purposes, and b) the smarter next move would be HOAS anyway.
| data Constraint = Type :===: Type | ||
| deriving (Eq, Ord, Show) |
There was a problem hiding this comment.
This was, alas, too cute to live.
| Core.Parser | ||
| Core.Pretty |
| data Expr | ||
| = Var Name | ||
| | Abs Name Expr | ||
| | App Expr Expr | ||
| | Let Name Expr Expr | ||
| | Lit Int | ||
| | If Expr Expr Expr | ||
| | Die String | ||
| deriving (Eq, Ord, Show) |
There was a problem hiding this comment.
This is a minimalistic reference calculus that exercises the evaluation interfaces fully.
| and', or' :: Expr | ||
| and' = Abs "a" (Abs "b" (Var "a" $$ true $$ Var "b")) | ||
| or' = Abs "a" (Abs "b" (Var "a" $$ Var "b" $$ false)) |
There was a problem hiding this comment.
As seen on a blog post I wrote one time!
| | String Text | ||
| | Record Env | ||
| | Neutral Name (Snoc (Elim Concrete)) |
There was a problem hiding this comment.
Can we get a bit of documentation on this declaration? It’s different enough from its surroundings that some context would be welcome.
| -- This applies the Kleene fixed-point theorem to finitize a monotone action. cf https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem | ||
| convergeEither | ||
| :: Monad m | ||
| => (a -> m (Either b a)) -- ^ A monadic action to perform at each iteration, starting from the result of the previous iteration or from the seed value for the first iteration. Returns of 'Left' end iteration, while 'Right' begins another iteration. | ||
| -> a -- ^ An initial seed value to iterate from. | ||
| -> m b -- ^ A computation producing the least fixed point (the first value at which the actions converge). | ||
| convergeEither f = loop | ||
| where | ||
| loop = either pure loop <=< f |
This PR migrates
semantic-analysisover to the parametric modular abstract interpretation framework I’ve been building. It remains superficially similar, but has a better basis for the domain effect, better ergonomics via labelled effects for the store &c., and provides an operation analogous to linking, allowing out-of-order program analysis and (typically file-level) incremental updating.