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

[VictorCMiraldo]

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

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]

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]

Another piece of information to use: #110 (comment)

[serras]

The State part threads two pieces of information:

• the current known facts,
• the statistics about found constructors, and so on.
  Those two things always "grow", and in a sense it's like a tree.

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]

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

[serras]

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]

Current progress:

• @0xd34df00d turned the two layers of ReaderT into a single on (Replace two nested ReaderTs with one in SymEval #116)
• @serras has introduced a new TreeT monad (Introduce our own TreeT monad #115)