Our original pipeline was usable but carried the technical debt of Lean's complex type theory in its translations. There were a few problems:
"Lean deals with pattern matching and structural recursion is by converting it into a form using recursors. If it can't do that, it fails -- this is also a form of termination checking. The issue with this approach is that match expressions become very inefficient on some datatypes." -- Gabriel. See the explanation in much more detail in this thread.
Indeed, in practice this meant that transpiling a declaration like List.map generated some ~400 LOC. The benchmark iteration count for evaluating List.map on even small lists (size < 10) was upwards of 200k in lurkrs.
The transpiled code held all the raw expression artifacts that Lean generated. This included instances, proofs, and as noted before, auxiliary match statements.
In principle, all of these problems are problems Lean must deal with too. As a state of the art functional compiler, generated C++ code from compiling Lean is extremely fast, and Lean does this by lowering to much more efficient and compilation friendly internal representation. So, the idea is this: Let us fix all of the technical debt of Lean's type theory by using the tool built to do it: the Lean compiler itself. By bootstrapping the Lean compiler and building our pipeline on top of theirs, we could generate extremely efficient Lurk code.
The Lean compiler pipeline looks approximately like this: Lean.Expr -> LCNF -> LCNF.IR -> C/C++. In the first stage, we lower to an extended lambda calculus called "Lean Compiler Normal Form (LCNF)." The exact details of this datatype is not that important; it is based on this paper: Compiling Without Continuations. LCNF is quite similar to lurk and target agnostic. It is also the main optimization stage that deals with all of the problems we listed above. LCNF replaces match statements with case blocks, has compiler passes to remove instance wrappers, inline declarations, perform case-by-case conversions, and runs simp passes.
Thus, LCNF should be a great target to transpile from. This PR is a "proof of concept" test for this idea. So far, there have been a few changes:
The generated code is much more compact: List.map is now only 34 LOC, and runs within ~1k iterations of lurkrs for small lists (size < 10).
The transpiler pipeline is now disjoint from the compiler. Since we need to transpile code as code, we can forgo content addressing the transpiler phase.
Our original pipeline was usable but carried the technical debt of Lean's complex type theory in its translations. There were a few problems:
List.mapgenerated some ~400 LOC. The benchmark iteration count for evaluatingList.mapon even small lists (size < 10) was upwards of 200k inlurkrs.In principle, all of these problems are problems Lean must deal with too. As a state of the art functional compiler, generated C++ code from compiling Lean is extremely fast, and Lean does this by lowering to much more efficient and compilation friendly internal representation. So, the idea is this: Let us fix all of the technical debt of Lean's type theory by using the tool built to do it: the Lean compiler itself. By bootstrapping the Lean compiler and building our pipeline on top of theirs, we could generate extremely efficient Lurk code.
The Lean compiler pipeline looks approximately like this:
Lean.Expr -> LCNF -> LCNF.IR -> C/C++. In the first stage, we lower to an extended lambda calculus called "Lean Compiler Normal Form (LCNF)." The exact details of this datatype is not that important; it is based on this paper: Compiling Without Continuations.LCNFis quite similar tolurkand target agnostic. It is also the main optimization stage that deals with all of the problems we listed above.LCNFreplaces match statements withcaseblocks, has compiler passes to remove instance wrappers, inline declarations, perform case-by-case conversions, and runssimppasses.Thus,
LCNFshould be a great target to transpile from. This PR is a "proof of concept" test for this idea. So far, there have been a few changes:List.mapis now only 34 LOC, and runs within ~1k iterations oflurkrsfor small lists (size < 10).