Yeah, I think we'll eventually do the IR compilation in Lean 4 lazily to mostly avoid it in interactive use. The interpreter works on the IR as well, no more bytecode, so locality is at least as bad as for an AST interpreter. Probably worse. Native speedup is often >100x.
Conversation
So the eval command is AST interpreted, there's separate IR and core syntax, and you have to compile to the IR to use eval?
2
#eval interprets the lambda_RC IR from arxiv.org/abs/1908.05647 (any prior IR/Core could be problematic for guaranteeing destructive updates). The interpreter is designed for simplicity, not performance; the goal has always been to compile anything perf-sensitive to native code.
2
1
I'd however agree with András that NbE is easier than capture-avoiding substitution and about as easy as a normal CBV interpreter: essentially you just add the right traversal on the values produced by the interpreter, applying them to fresh variables :-)
1
1
Is it still easy if the host language is strict though? As András says in the readme, "at least some laziness is essential".
1
It requires mutation in a strict language, but if we have that, it's still easy.
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I thought at least that smalltt was implemented with the `Strict` language feature on, and the lazy stuff is opt-in with the tilde? Or are we talking about something different here?
1
GHC -XStrict is still lazy Haskell with more bangs; it doesn't add bangs to other modules, the stdlib, and it doesn't even add all possible bangs to the code being compiled (eg "Notice that we do not put bangs on nested patterns" from gitlab.haskell.org/ghc/ghc/-/wiki).
1
2
But maybe you know that and smalltt does even more? Dunno...
1
Ahh no that makes sense!