blog: jit-compile

aya/blog/jit-compile.aya.md

@@ -0,0 +1,86 @@
+# JJH (JVM JIT HOAS) compilation for Aya
+
+In this post I'd like to introduce the _JJH_ compilation architecture of the new Aya type checker,
+which is based on the JIT (Just-In-Time) compilation on the Java VM for closures implemented using HOAS (Higher-Order Abstract Syntax).
+I'll explain.
+
+```aya-hidden
+open inductive Nat | Zero | S Nat
+open inductive UID
+```
+
+## Pros and Cons of HOAS
+
+When implementing an interpreter, we have a meta-level language that we use to write the interpreter itself,
+and the object level language which we interpret. In case of higher-order languages,
+the object level language will have lambda expressions, and the representation of closures in the meta level language
+will be very important for the performance of the interpreter.
+To implement closures, we need to represent binders and variable references, and implement a substitution operation.
+
+[several ways]: https://jesper.sikanda.be/posts/1001-syntax-representations.html
+
+This is a relatively well-known and well-studied problem, and there are [several ways] (allow me to delegate the introduction
+of this subject to Jesper's blog) to implement it. In the context of Aya we are interested in the locally nameless (LN)
+representation and HOAS, and I'll assume brief familiarity with these concepts.
+
+Consider STLC, the syntax can be defined as the following type, assuming an appropriate type `UID`{}:
+
+```aya
+inductive TermV1 : Type
+| bound (deBruijnIndex : Nat)
+| free (name : UID)
+| lam (body : TermV1)
+| app (fun : TermV1) (arg : TermV1)
+```
+
+The important constructor to consider here is `TermV1::lam`{},
+whose body will allow the use of bound variables. If a term is completely outside of a `TermV1::lam`{},
+it will make no sense. The substitution operation is only performed on bodies of lambdas,
+by replacing a De Bruijn index with a term. It might make sense to use types to enforce that:
+
+```aya
+inductive ClosureV2 : Type
+| mkClosure (body : TermV2)
+
+inductive TermV2 : Type
+| bound (deBruijnIndex : Nat)
+| free (name : UID)
+| lam (body : ClosureV2)
+| app (fun : TermV2) (arg : TermV2)
+
+def subst (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:
+
+```aya
+inductive ClosureV3 : Type
+| mkClosure (body : TermV3 -> TermV3)
+
+inductive TermV3 : Type
+| free (name : UID)
+| lam (body : ClosureV3)
+| app (fun : TermV3) (arg : TermV3)
+```
+
+Intuitively, HOAS requires no term traversal to produce the result of substitution,
+so it must be a lot faster. In reality, this is true, but only if these meta-level functions are known at the compile
+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.
+
+To solve this problem, Aya  introduces a _hybrid_ approach.
+
+## Hybrid mode
+
+
+
+
+
+
+
+

aya/guide/prover-tutorial.aya.md

@@ -36,17 +36,19 @@ def id (x : Bool) => x
 def Goal => id = (fn x => not (not x))
 
 // {??} is the syntax for typed holes in Aya:
-// def question : Goal => {??}
+def question : Goal => {??}
 ```
 
-There is no way to prove it in Martin-Löf type theory or Calculus of Constructions.
+There is no way to prove it in Martin-Löf type theory or Calculus of Constructions,
+because by canonicity of these type theories, the normal form of `question`{} must be
+the constructor of its type, which is reflexivity, but the goal is not reflexive.
 However, you are very smart and realized you can instead show the following:
 
 ```aya
 def Goal' (x : Bool) => id x = not (not x)
 ```
 
-This is pretty much the same theorem!
+This is pretty much the same theorem, and can be proved by case analysis on `x`!
 
 Now, suppose we need to show a propositional equality between two records.
 This means we have to show they're memberwise equal.

scripts/build-aya.js

@@ -36,11 +36,15 @@ process.chdir("aya");
 // For each file, we call aya compiler
 walk(".", (file) => {
   console.log("Compiling: " + file);
-  child_process.execSync(ayaProg + " " + opts + " " + file,
-    (err) => {
+  try {
+    child_process.execSync(ayaProg + " " + opts + " " + file, (err) => {
       if (err) throw err;
     });
-});
+  } catch (err) {
+    // Aya returns 1 in case of holes, it is not necessarily an error.
+    // We need to manually look at compile errors, but it's quite easy.
+   }
+  });
 // Put preprocessed files to src/
 process.chdir("../build-aya");
 let gitignore = "";

src/.gitignore

@@ -1,4 +1,5 @@
 blog/extended-pruning.md
+blog/jit-compile.md
 blog/tt-in-tt-qiit.md
 guide/haskeller-tutorial.md
 guide/prover-tutorial.md

src/blog/bye-hott.md

@@ -13,7 +13,9 @@ true by definition.
 
 In case of cubical, this is automatic, due to how path types are defined.
 
-The reference for XTT can be found in the paper _A Cubical Language for Bishop Sets_ by
+[related papers]: /guide/readings
+
+The reference for XTT can be found (both linked in [related papers]) in the paper _A Cubical Language for Bishop Sets_ by
 Sterling, Angiuli, and Gratzer. This paper has a previous version which has a universe hierarchy,
 called _Cubical Syntax for Reflection-Free Extensional Equality_, by the same authors.