feat: interpreter (faster evaluator-to-normal-form) #1187

brprice · 2023-11-29T15:34:53Z

The one feature of the old stepwise evaluator that we don't replicate is the ability not to evaluate under lambdas.
This may be annoying if this new interpreter is hooked up to a frontend, as then any evaluation of a recursive function will diverge, even if an evaluation of that same function applied to an argument may succeed. The possible mitigations for this include

only use this new interpreter for things of "base" type, i.e. things which have a type such that we expect them not to contain un-applied lambdas (note that if they contain holes, this expectation may be false, so a refinement would be "base type and not contain holes"). This is not quite "not an arrow/forall type", as we need to detect things like Maybe (Bool -> Char), or a return type of T where data T = C (Bool -> Char).
revisit this new interpreter to avoid the hard requirement that it evaluates under lambdas. This can be done by stepping outside of the AST domain and representing the interpretation of a lambda as a closure (a pair of the current environment and the body), and then applications will require the function-position to be a closure rather than a syntactic lambda. (This may also be useful if we want to make Expr spine-strict, since we need to step outside of the AST domain to keep laziness in that case anyway.)

When working on this PR, at one point we had an explicit
"fuel" counter so that the interpreter would not loop on a divergent term.
This has been replaced (and rebased) with an IO-based System.Timeout call,
but the old state is still in the history for https://github.com/hackworthltd/primer/tree/brprice/wip/interp.

The reason we changed track here is

We need to lazily produce the resultant AST, since the semantics of
Primer (the object language) are lazy
(in particular, code like head (letrec l = Cons True l in l) should
reduce to True (ignoring type annotations)
This means we can't use ExceptT (i.e. Either) to signal the
"recursion depth exceeded" error, since to pattern match on the (root
of the) AST of a recursive call would force the Either, and thus
divergent subterms would throw a Left, aborting the whole computation.
We can however throw an "imprecise exception" (e.g. Prelude's error,
or Control.Exceptions throw), from pure code. This is essentially
hiding an exception deep within a (recursively returned) AST, and will
not actually trigger unless it is forced.
However, to make this testable, we need to be able to catch the
"timeout" error in the testsuite, meaning we need to be able to run IO
actions in Hedgehog tests, and thus need to refactor our WT monad to
(optionally) include IO at the base.
Having done this, it is just as easy to not have the recursion-depth
check and use System.Timeout instead, which also works in IO,
and avoids some overhead due to not tracking the depth (and makes the
interpretation of recursive let bindings nicer.

Note that (c.f. comment in code) this new interpreter relies heavily on laziness and will break if Expr is made spine-strict.

brprice · 2023-11-30T15:16:53Z

@dhess: I'll leave some cleanup work for you to look at:

testsuite should be DRY'd between Interpreter and FullStep (currently I've copy-pasted the file and hacked the tests, removing some that are not super relevant).
enabling the last two tests about handleEvalFullRequest, as that requires essentially the same work as hooking up the interpreter to the OpenAPI.