blog: add jit-compiler for real

aya/blog/jit-compile.aya.md

@@ -48,12 +48,13 @@ inductive TermV2 : Type
 | lam (body : ClosureV2)
 | app (fun : TermV2) (arg : TermV2)
 
-def subst (t : ClosureV2) (s : TermV2) : TermV2 => {??}
+def substV2 (t : ClosureV2) (s : TermV2) : TermV2 => {??}
 ```
 
 We can view HOAS as essentially a different implementation of closures,
 which instead of traversing and replacing `TermV2::bound`{} with a term,
-it constructs terms directly by using a function in the meta-level language:
+it constructs terms directly by using a function in the meta-level language
+(the definition below is accepted because Aya doesn't yet have a positivity checker):
 
 ```aya
 inductive ClosureV3 : Type
@@ -70,17 +71,95 @@ so it must be a lot faster. In reality, this is true, but only if these meta-lev
 time of the interpreter -- an assumption that is usually false. In practice, we parse the AST from a string,
 resolve the names in it, desugar it, and then type check it before producing a term that can be interpreted.
 This means we do not know the body of the closure at the compile time. Also, the terms during type checking are _mutable_:
-we have _local type inference_ (also known as _solving metavariables_), which involves in creating unknown terms
-and replace them with known terms later. This means we also need to _traverse_ the terms, which is unrealistic to HOAS.
+
+1.  We have _local type inference_ (also known as _solving metavariables_), which involves in creating unknown terms
+   and replace them with known terms later. This means we also need to _traverse_ and _mutate_ the terms, which is unrealistic for HOAS.
+2. We suppor type checking _recursive_ functions. When checking the body of a recursive function, the recursive calls cannot be unfolded
+   because the body is not yet constructed, and before termination check we cannot really know if unfolding such definitions is a good idea.
+   But once the type checking finishes, these self-references will become unfoldable. So, at least something needs to be modified -- either
+   the terms or the evaluation context.
 
 To solve this problem, Aya  introduces a _hybrid_ approach.
 
-## Hybrid mode
+## Combining HOAS and Locally Nameless
+
+We introduce the closure to allow _two_ representations of closures:
+one for HOAS, and one for any first-order syntax such as locally nameless.
+Then, we define substitution on both variants.
+
+```aya
+inductive ClosureV4 : Type
+| mkJit (body : TermV4 -> TermV4)
+| mkLn (body : TermV4)
+
+// The locally-nameless substitution,
+// replacing the outermost bound variable in `t` with `s`.
+def substV4 (t : TermV4) (s : TermV4) : TermV4 => {??}
 
+def applyV4 (t : ClosureV4) (s : TermV4) : TermV4
+| mkJit body => body s
+| mkLn body => substV4 body s
+```
 
+During type checking, we use the locally nameless representation, so we have the freedom to mutate them,
+and after finish type checking a cluster of definitions, we generate the code for the HOAS function bodies,
+and then we dynamically compile these functions and replace the closures with the compiled functions.
 
+This process is very similar to JIT-compilation in the usual sense, but slightly different:
+since the terms are used for type checking, we have to preserve all the typing information at runtime,
+and the JIT-compiled code should deal with open terms. These can be handled well using HOAS.
+The dynamic compilation is based on the class loading mechanism of the JVM,
+therefore we refer to this process as _JJH_ (JVM JIT HOAS). All of the three components are essential to the approach!
 
+To support locally nameless we have to also include `TermV4::bound`{}:
 
+```aya
+inductive TermV4 : Type
+| bound (deBruijnIndex : Nat)
+| free (name : UID)
+| lam (body : ClosureV4)
+| app (fun : TermV4) (arg : TermV4)
+```
 
+In fact we can extend it with more constructors with closures, and it is very clear how the binders work just by looking at
+the term structure:
 
+```aya
+| pi (domain : TermV4) (codomain : ClosureV4)
+```
 
+We will never forget to substitute the codomain of a pi type because otherwise there will be a type error in the meta-level language.
+
+## Related Work
+
+Coq has two tactics that seemingly do similar things: `vm_compute` and `native_compute`.
+The `vm_compute` tactic translates Coq terms to an abstract machine (not using HOAS),
+evaluate it and _read-back_ the result to Coq terms (also not in HOAS),
+while `native_compute` produces machine code and do something similar, but using HOAS in the generated code.
+For the purpose of conversion checking, it is enough to just compare the results of
+the abstract machine, and reading back the result is not necessary.
+
+The native code generation is known to be faster than the VM-based approaches,
+as described in the paper _Full Reduction at Full Throttle_,
+and the prior work on `vm_compute` is described in _A Compiled Implementation of Strong Reduction_.
+
+Aya reuses JVM, a highly optimized VM with two JIT compilers that produce machine code,
+and has HOAS built-in to the core language, so there is not need of reading back -- the result of compilation is in our core
+language rather than a separately defined language. This also makes it less error-prone because a bug in the compiled code is
+a bug in the core language, which is well-understood and well-tested.
+But then the correctness (mainly type safety) of the core language relies on the correctness of the JJH compiler,
+which we do not intend to formally verify, but we believe (with reasonable confidence due to the amount of testing) that it is correct.
+
+Speaking of VM-based evaluation, Lean4 also has an evaluator based on a VM for interpreting code,
+and Agda also seems to have an abstract machine for reducing code.
+These two evaluators, together with `vm_compute`, are based on a VM written by the proof assistant developers,
+which may not be the most efficient VM, and apparently these VMs do not have a second JIT compiler that produces machine code.
+
+JJH relies on the fact that the type checker is written in a VM-based language, but we can do the same thing in a native language
+by using the JIT compilation feature of LLVM or GCC.
+In the first _Workshop on Implementations of Type Systems_ (WITS), I had the privilege to listen to an exciting talk on an
+ongoing work on Lean4 that JIT-compiles tactics to native code. They will have a similar advantage to JJH, but it only works on
+tactics rather than the whole language.
+
+When I was at the workshop, I was very jealous of the Lean team to have the manpower and resource to do such a thing,
+but now I am satisfied ♪(≧∀≦)ゞ.

src/.vitepress/config.mts

@@ -43,6 +43,7 @@ export default defineConfig({
         text: 'Blog',
         items: [
           // { text: 'Nameless classes', link: '/blog/nameless-classes' },
+          { text: 'JVM JIT HOAS compiler', link: '/blog/jit-compile' },
           { text: 'TT in TT using QIIT', link: '/blog/tt-in-tt-qiit' },
           { text: 'Extended Pruning', link: '/blog/extended-pruning' },
           { text: 'Farewell, Univalence', link: '/blog/bye-hott' },