search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Understand and explore whether we really need that many monads in `SymEval` #112

Open VictorCMiraldo opened 2 years ago

VictorCMiraldo commented 2 years ago

In #110 we started using a pure and parallel solve function; which meant we could remove IO from the symbolic engine altogether! :tada:

Yet, the SymEval monad now looks like:

newtype SymEval lang a = SymEval
  { symEval ::
      ReaderT
        (PrtOrderedDefs lang)
        (ReaderT (SymEvalSolvers lang) (StateT (SymEvalSt lang) WeightedList))
        a
  }

And, in particular, the StateT is the one that hurts our ability to parallelize the symbolic engine even further: every call to mapM can't be replaced by a parMap because of the state being threaded through.

This issue aims at document an exploration of the design space: now that we have no more IO to deal with, we might be able to afford ourselves better types and an even cleaner implementation.

One particular point where it might be interesting to attempt to parallelize is the Monad instance for WeigthedList.

VictorCMiraldo commented 2 years ago

For the record, I think we can drastically simplify WeigthedT and make it a plain monad, no need to be a transformer at this point. Also, no need to use a "list" structure either; WeigthedT could well be a tree: there's no more need to worry about synchronizing different monadic effects inside! :)

VictorCMiraldo commented 2 years ago

Another piece of information to use: https://github.com/tweag/pirouette/pull/110#discussion_r899946371

serras commented 2 years ago

The State part threads two pieces of information:

Why the State then? Because we have the worker function, which implements the recursion-and-stop-when-needed steps. Right now the call structure is worker -> symEvalOneStep -> return to worker. So if we somehow can remove that "going back", we should be able to make everything parallel.

serras commented 2 years ago

I've been talking with @lucaspena about how to change the weighted list into a Tree.

serras commented 2 years ago

In fact, I think that we can more or less easily use the following monad:

data Tree lang a = Leaf a | Node (Maybe (TermMeta lang SymVar)) [Tree lang a]

which keeps the branching and at each point records "the term at this point." At the very list it has the usual Functor, Applicative and Alternative instances. And during symEvalDestructor and the evaluation of built-ins we could use the Node to record whatever we are doing there.

@lucaspena will you give it a go? Otherwise I can try tomorrow!

serras commented 2 years ago

Current progress: