From 9b873e1b645decd1c944229c41f2979f01e5d438 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 4 Dec 2024 16:08:58 -0500 Subject: [PATCH] blog: jit-compile --- aya/blog/jit-compile.aya.md | 86 ++++++++++++++++++++++++++++++++ aya/guide/prover-tutorial.aya.md | 8 +-- scripts/build-aya.js | 10 ++-- src/.gitignore | 1 + src/blog/bye-hott.md | 4 +- 5 files changed, 102 insertions(+), 7 deletions(-) create mode 100644 aya/blog/jit-compile.aya.md diff --git a/aya/blog/jit-compile.aya.md b/aya/blog/jit-compile.aya.md new file mode 100644 index 0000000..51bcd61 --- /dev/null +++ b/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 + + + + + + + + diff --git a/aya/guide/prover-tutorial.aya.md b/aya/guide/prover-tutorial.aya.md index fa8ea81..2acf03a 100644 --- a/aya/guide/prover-tutorial.aya.md +++ b/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. diff --git a/scripts/build-aya.js b/scripts/build-aya.js index 2abb4e9..6198dac 100644 --- a/scripts/build-aya.js +++ b/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 = ""; diff --git a/src/.gitignore b/src/.gitignore index 99129a5..c9f52d2 100644 --- a/src/.gitignore +++ b/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 diff --git a/src/blog/bye-hott.md b/src/blog/bye-hott.md index e53d7fd..4728a3b 100644 --- a/src/blog/bye-hott.md +++ b/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.