From ade18764fe56933bcde37a90d05765df0db68863 Mon Sep 17 00:00:00 2001 From: LukasK Date: Fri, 17 Jul 2026 11:24:19 +0000 Subject: [PATCH 1/4] ai: rewrite 2ltt skill against original papers and reference implementation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reviewed all sources from CREDITS.md (Kovács ICFP'22/'24 LaTeX sources, the staged demo Haskell code, KACC) and fixed the discrepancies: - Remove fabricated guardStage: the reference demo repairs stage mismatches via coercive subtyping (adjustStage/coe), it does not stage-check lookups - Untangle conversion checking from staging strictness: full object beta/eta is the 2022 design, no-beta/eta is the CFTT 2024 design; both documented as an explicit up-front decision - Add missing content: 2022 object-language variations (monomorphization, Rep indexing), subtyping rules, cofibrancy, intensional-analysis options, CFTT computation products, join points + SOP, generativity axiom, KACC kind grammar with mono-rep/mono-conv restrictions - Complete the demo notes: meta machinery, smart constructors, quote insertion, coe, zonk, README design notes - Deduplicate: one topic per file with cross-references; fold the redundant slides notes into the 2022 file; keep the skill generic (no project refs) Co-Authored-By: Claude Fable 5 --- .opencode/skills/2ltt/CREDITS.md | 32 +- .opencode/skills/2ltt/SKILL.md | 90 +-- .opencode/skills/2ltt/demo-implementation.md | 472 ++++++---------- ...wnen-2020-kinds-are-calling-conventions.md | 212 ++++--- .opencode/skills/2ltt/implementation-guide.md | 529 ++++++------------ .../skills/2ltt/kovacs-2022-icfp22-slides.md | 143 ----- .../kovacs-2022-staged-compilation-2ltt.md | 354 +++++++----- .../2ltt/kovacs-2024-closure-free-2ltt.md | 372 +++++++----- 8 files changed, 982 insertions(+), 1222 deletions(-) delete mode 100644 .opencode/skills/2ltt/kovacs-2022-icfp22-slides.md diff --git a/.opencode/skills/2ltt/CREDITS.md b/.opencode/skills/2ltt/CREDITS.md index e0e062ef..941a6a3a 100644 --- a/.opencode/skills/2ltt/CREDITS.md +++ b/.opencode/skills/2ltt/CREDITS.md @@ -1,6 +1,6 @@ # Credits / sources -This skill is derived from (and intended to be read alongside) the following papers. +This skill is derived from (and intended to be read alongside) the following sources. ## Primary sources @@ -8,28 +8,42 @@ This skill is derived from (and intended to be read alongside) the following pap *Staged Compilation with Two-Level Type Theory.* Proc. ACM Program. Lang. 6, ICFP, Article 110 (August 2022), 30 pages. DOI: 10.1145/3547641 - Source PDF (original URL): https://andraskovacs.github.io/pdfs/2ltt.pdf + PDF: https://andraskovacs.github.io/pdfs/2ltt.pdf + (LaTeX source: `icfp22paper/` in the repository below.) 2. András Kovács. *Closure-Free Functional Programming in a Two-Level Type Theory.* Proc. ACM Program. Lang. 8, ICFP, Article 259 (August 2024), 34 pages. DOI: 10.1145/3674648 - Source PDF (original URL): https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf + PDF: https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf + (LaTeX source and Agda/Haskell supplements: `icfp24paper/` in the repository below.) 3. Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. *Kinds Are Calling Conventions.* Proc. ACM Program. Lang. 4, ICFP, Article 104 (August 2020), 51 pages. DOI: 10.1145/3408986 - Source PDF (original URL): https://pauldownen.com/publications/kacc.pdf + PDF: https://pauldownen.com/publications/kacc.pdf 4. András Kovács. *ICFP 2022 presentation slides: Staged Compilation with Two-Level Type Theory.* Presented 12 September 2022, ICFP Ljubljana. - Source PDF (original URL): https://github.com/AndrasKovacs/staged/blob/main/icfp22prez/ICFP-Kov%C3%A1cs-StagedCompilationwithTwoLevelTypeTheory.pdf + (Content folded into `kovacs-2022-staged-compilation-2ltt.md`; no separate notes file.) -## Reference implementation +## Reference implementations -5. András Kovács. - *staged* demo implementation. - GitHub repository: https://github.com/AndrasKovacs/staged +5. András Kovács. *staged* — demo implementation, paper sources, Agda embeddings. + https://github.com/AndrasKovacs/staged + (The `demo/` directory and its `README.md` are the basis of `demo-implementation.md`.) + +6. András Kovács. *elaboration-zoo* — minimal NbE / bidirectional elaboration + references (see branch `01-eval-closures-debruijn` and later branches for + metavariables and implicits). + https://github.com/AndrasKovacs/elaboration-zoo + +## Background + +7. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler. + *Two-Level Type Theory and Applications.* (origin of 2LTT; homotopy-type-theory + motivation, cofibrancy) + https://arxiv.org/abs/1705.03307 diff --git a/.opencode/skills/2ltt/SKILL.md b/.opencode/skills/2ltt/SKILL.md index 76340a63..cafcbf51 100644 --- a/.opencode/skills/2ltt/SKILL.md +++ b/.opencode/skills/2ltt/SKILL.md @@ -1,59 +1,69 @@ --- name: 2ltt -description: Implement (or typecheck + unstage) a practical two-level type theory (2LTT) / staged dependent type system, including a closure-free object language variant and optional representation/calling-convention indexing. +description: Implement (or typecheck + stage) a practical two-level type theory (2LTT) / staged dependent type system, including a closure-free object language variant and optional representation/calling-convention indexing. compatibility: opencode --- ## What I do -I'm a project-local reference for implementing a **two-level type theory (2LTT)**: a dependently typed meta-language with a staged object-language, connected via **lift/quote/splice**. +I'm a reference for implementing a **two-level type theory (2LTT)**: a dependently typed +meta-language over a staged object-language, connected via **lift/quote/splice** +(`⇑A` / `⟨t⟩` / `∼t`). I cover syntax, typing, definitional-equality design, elaboration, +and the staging algorithm that runs metaprograms to produce splice-free object code. -I focus on implementation details: syntax, typing, definitional equality choices, and an *unstaging* (staging) algorithm that runs metaprograms to produce splice-free object code. +## Files (each owns its topic; minimal overlap) -## Files to read (in order) +1. **`implementation-guide.md`** — start here. Pipeline architecture, the up-front + design decisions (object-equality strength, stage repair vs. reject), NbE core, + elaboration guardrails, staging-pass essentials, pitfalls checklist, glossary. -1. **`implementation-guide.md`** - - Practical "how to build it" plan: core judgments, AST design, typechecker structure, definitional equality strategy, and an executable unstager. - - Includes pseudocode and implementation checklists. +2. **`demo-implementation.md`** — code-level walkthrough of the reference Haskell + implementation (https://github.com/AndrasKovacs/staged): core syntax, conversion + evaluator with stuck splices, two-domain staging evaluator, coercive-subtyping + elaboration, unification extensions, what to copy vs. reconsider. -2. **`demo-implementation.md`** - - Code snippets from the reference Haskell implementation at https://github.com/AndrasKovacs/staged - - Syntax, semantic values, meta evaluation, and staging algorithm. - - Useful for seeing how the theory maps to actual code. +3. **`kovacs-2022-staged-compilation-2ltt.md`** — the core theory (*Staged Compilation + with Two-Level Type Theory*): rules, programming patterns, binding-time improvement + and inference, staging-by-evaluation with soundness/stability/strictness, + object-language variations (monomorphization, representation polymorphism), + intensional-analysis options. Also covers the ICFP'22 slides' examples. -3. **`kovacs-2022-staged-compilation-2ltt.md`** - - Rewrites the main content of *Staged Compilation with Two-Level Type Theory* (Kovács 2022): - universes-by-stage, lift/quote/splice rules, and *staging-by-evaluation* (presheaf-model-inspired) as an algorithmic blueprint. +4. **`kovacs-2024-closure-free-2ltt.md`** — the CFTT deltas (*Closure-Free Functional + Programming in a 2LTT*): first-order object language with `ValTy`/`CompTy`, weak + object equality, `Gen`/let-insertion, `Improve` monad library, join points + SOP, + stream fusion, generativity axiom. -4. **`kovacs-2024-closure-free-2ltt.md`** - - Rewrites the main content of *Closure-Free Functional Programming in a Two-Level Type Theory* (Kovács 2024): - a closure-free object language split into **value types vs computation types**, call-saturation idea, let-insertion via a codegen monad, and the "no intensional code analysis" / generativity theme. - -5. **`downen-2020-kinds-are-calling-conventions.md`** - - Rewrites the parts of *Kinds Are Calling Conventions* (Downen et al. 2020) that are useful when you want the staged object language to control **representation**, **arity**, and **evaluation order** via kind/index information. - - Treat this as an optional extension for "layout control" / low-level compilation friendliness. - -6. **`kovacs-2022-icfp22-slides.md`** - - Deduplicated implementation notes extracted from the ICFP’22 presentation slides (rules, examples: Vec3, and the inference/isomorphism trick for reducing quote/splice annotations). +5. **`downen-2020-kinds-are-calling-conventions.md`** — optional layout/arity control: + `TYPE ρ ν` kinds, levity, `mono-rep`/`mono-conv` restrictions, closure boxing, + lowering to machine language; how it composes with a 2LTT. ## When to use me -Use me when you are: -- implementing a 2LTT core calculus (or a prototype) with **compile-time evaluation** and **typed splicing**; -- designing an object language meant to compile efficiently (optionally closure-free); -- adding representation/calling-convention indices to types/kinds for lower-level codegen. +- implementing or debugging a 2LTT core calculus with compile-time evaluation and + typed splicing; +- designing an object language meant to compile predictably (optionally closure-free); +- adding representation/calling-convention indices for low-level codegen; +- reasoning about staging correctness (soundness/stability/strictness) or about what + metaprograms can and cannot observe. ## Guardrails (important) -- Prefer an object-level definitional equality that is **simple and syntax-directed** (often: *no* β/η for object lambdas), so typechecking and unstaging stay predictable. -- Unstaging should be an evaluation procedure: **run meta**, construct **object AST**, eliminate splices. -- Avoid "intensional analysis of object code" (pattern matching on AST) if you want the semantic/parametricity properties these papers rely on. - -## Elaboration guardrails - -These invariants prevent whole classes of bugs; see `implementation-guide.md §13` for detail. - -- **`infer` returns `(Term, VTy)`** — always return the elaborated term *and* its type. Never recover types after the fact by pattern-matching on the elaborated term (`typeOf`-style helpers are a red flag). -- **`checkU` / `check_universe`** — when a term must be a type, check it against the appropriate universe directly (`check t (VU s)`). Don't infer and then ad-hoc test whether the returned type is a universe. -- **Stuck splices are a neutral** — `Value` needs a `Splice(v)` neutral alongside `Rigid`. Without it, `eval(Quote(Splice(v)))` silently drops the splice. Cancellation rules: `eval(Quote(Splice(v))) = v` and `eval(Splice(Quote(v))) = v`. -- **Stage-check variables** — record each binding's stage in the context; check it against the current elaboration stage on lookup (`guardStage` in the reference). Otherwise meta variables leak into object code and produce confusing type errors instead of clear stage errors. +- **Conversion vs. staging are different evaluators.** Staging never β-reduces object + code (strictness). Whether *conversion checking* computes object redexes depends on + the chosen object theory: full-MLTT object level (2022) — yes; CFTT-style first-order + object level — no β/η/let-unfolding at all. Pick one coherently + (`implementation-guide.md` §2.1). +- **`infer` returns `(Term, VTy, Stage)`** — never reconstruct types (or stages) from + elaborated terms afterwards. +- **`checkU`** — when a term must be a type, check it against `U s` directly; don't + infer-and-test. +- **Stuck splices need a representation** in the semantic domain (spine entry or + neutral), with cancellation in both directions: `∼⟨t⟩ = t` and `⟨∼n⟩ = n`. Otherwise + splices are silently dropped or crash on neutrals. +- **Track a stage for every binding**; on mismatch either *repair* via coercive + subtyping (`A ≤ ⇑A`, `⇑A ≤ A` — what the reference implementation does) or *reject* + with a clear stage error — but decide explicitly. Keep `let` stages explicit; avoid + stage metavariables. +- **Keep object code opaque** (build/compose/insert only — no pattern-matching on code) + unless you deliberately adopt a weakening-only or closed-modality setup; opacity is + what makes the standard semantics and the generativity axiom work. diff --git a/.opencode/skills/2ltt/demo-implementation.md b/.opencode/skills/2ltt/demo-implementation.md index 98cd411a..fe9a600d 100644 --- a/.opencode/skills/2ltt/demo-implementation.md +++ b/.opencode/skills/2ltt/demo-implementation.md @@ -1,345 +1,229 @@ -# Demo implementation (Kovács staged) +# Reference implementation (Kovács `staged` demo) -This file contains code snippets from the reference implementation at: -https://github.com/AndrasKovacs/staged/tree/main/demo +Code-level reference for https://github.com/AndrasKovacs/staged/tree/main/demo — the +prototype accompanying the 2022 paper (theory: `kovacs-2022-staged-compilation-2ltt.md`). +Features: two stages, dependent functions, type-in-type (no sigma; data is +lambda-encoded), `Nat` at both stages, Agda-style implicits with higher-order +unification, and strong inference for staging operations. -## 1. Core types (Common.hs) +Pipeline: parse → elaborate (bidirectional, NbE, metavariables) → zonk → stage. -```hs -data Stage = S0 | S1 -- S0 = object (runtime), S1 = meta (compile-time) +## 1. Core syntax (Syntax.hs) -newtype Ix = Ix {unIx :: Int} -- De Bruijn index -newtype Lvl = Lvl {unLvl :: Int} -- De Bruijn level -newtype MetaVar = MetaVar {unMetaVar :: Int} +```hs +data Tm + = Var Ix + | Lam Name Icit Tm Tm Verbosity -- λ (domain annotation, body) + | App Tm Tm Icit Verbosity + | Pi Name Icit Ty Ty + | Let Stage Name Ty Tm Tm Verbosity -- let with EXPLICIT stage (S0 | S1) + | U Stage -- U0 / U1 + | Lift Ty -- ⇑A + | Quote Tm -- ⟨t⟩ (surface syntax: ) + | Splice Tm -- ∼t (surface syntax: [t]) + | Nat Stage | Zero Stage | Suc Stage | NatElim Stage + -- metavariable machinery (elaboration only; gone after zonking): + | Meta MetaVar + | InsertedMeta MetaVar Pruning -- fresh meta applied to the bound-var mask + | AppPruning Tm Pruning + | Wk Tm -- explicit weakening, used by subtyping coercions ``` -## 2. Syntax (Syntax.hs) +`Verbosity` (`V0`/`V1`) marks elaboration-inserted material for printing. Smart +constructors cancel quote/splice **already at elaboration time**: ```hs -data Tm - = Var Ix - | Lam Name Icit Tm Tm Verbosity -- lambda - | App Tm Tm Icit Verbosity -- application - | Pi Name Icit Ty Ty -- dependent function - | Let Stage Name Ty Tm Tm Verbosity -- let (with stage) - - | U Stage -- universes - | Quote Tm -- ⟨t⟩ - | Splice Tm -- [t] (splice) - | Lift Ty -- ⇑A - - | Nat Stage -- natural numbers - | Zero Stage - | Suc Stage - | NatElim Stage -- dependent elimination - deriving Show +tQuote (Splice t) = t ; tQuote t = Quote t +tSplice (Quote t) = t ; tSplice t = Splice t ``` -Key differences from paper notation: -- Paper uses `~t` for splice, demo uses `[t]` -- `Let` is annotated with a `Stage` (S0 or S1) +## 2. Values for conversion checking (Value.hs, Evaluation.hs) -## 3. Semantic values for meta evaluation (Value.hs) +One shared semantic domain for elaboration-time evaluation (used by unification and +conversion). De Bruijn **indices** in terms, **levels** in values; closures are Haskell +functions `Val -> Val`. ```hs -data Spine - = SId - | SApp Spine Val Icit Verbosity - | SSplice Spine - | SNatElim Stage Val Val Val Spine +data Spine = SId | SApp Spine ~Val Icit Verbosity + | SSplice Spine -- stuck splice, as a spine entry + | SNatElim Stage Val Val Val Spine data Val - = VFlex MetaVar Spine -- unsolved meta variable - | VRigid Lvl Spine -- variable - | VLam Name Icit VTy (Val -> Val) Verbosity - | VPi Name Icit VTy (Val -> Val) - | VU Stage - | VLift Val -- lifted value - | VQuote Val -- quoted object term - | VNat Stage - | VZero Stage - | VSuc Stage Val + = VFlex MetaVar Spine -- stuck on an unsolved meta + | VRigid Lvl Spine -- stuck on a variable + | VLam Name Icit ~VTy (Val -> Val) Verbosity + | VPi Name Icit ~VTy (Val -> Val) + | VU Stage | VLift Val | VQuote Val + | VNat Stage | VZero Stage | VSuc Stage Val ``` -The `Spine` tracks pending applications and special operations during evaluation. - -## 4. Meta evaluator (Evaluation.hs) +Key evaluation cases — quote/splice cancellation on both canonical values and neutrals: ```hs -vApp :: Val -> Val -> Icit -> Verbosity -> Val -vApp t ~u i o = case t of - VLam _ _ _ t o -> t u - VFlex m sp -> VFlex m (SApp sp u i o) - VRigid x sp -> VRigid x (SApp sp u i o) - _ -> impossible - -vQuote :: Val -> Val -vQuote = \case - VFlex m (SSplice sp) -> VFlex m sp -- quote/splice cancel - VRigid x (SSplice sp) -> VRigid x sp - t -> VQuote t - -vSplice :: Val -> Val -vSplice = \case - VQuote t -> t -- splice of quote - VFlex m sp -> VFlex m (SSplice sp) - VRigid x sp -> VRigid x (SSplice sp) - _ -> impossible - -eval :: Env -> Tm -> Val -eval env = \case - Var x -> vVar env x - App t u i vr -> vApp (eval env t) (eval env u) i vr - Lam x i a t vr -> VLam x i (eval env a) (evalBind env t) vr - Pi x i a b -> VPi x i (eval env a) (evalBind env b) - Let _ _ _ t u _ -> eval (env :> eval env t) u - U s -> VU s - Quote t -> vQuote (eval env t) - Splice t -> vSplice (eval env t) - Lift t -> VLift (eval env t) - -- ... nat eliminator handling +vSplice (VQuote t) = t -- ∼⟨t⟩ = t +vSplice (VFlex m sp) = VFlex m (SSplice sp) -- stuck: push splice onto spine +vSplice (VRigid x sp) = VRigid x (SSplice sp) +vSplice _ = impossible -- (well-typed input) + +vQuote (VFlex m (SSplice sp)) = VFlex m sp -- ⟨∼n⟩ = n on neutrals +vQuote (VRigid x (SSplice sp)) = VRigid x sp +vQuote t = VQuote t -- canonical ``` -Quotation (value back to syntax): -```hs -quote :: Lvl -> Val -> Tm -quote l t = case force t of - VFlex m sp -> quoteSp l (Meta m) sp - VRigid x sp -> quoteSp l (Var (lvl2Ix l x)) sp - VLam x i a t o -> Lam x i (quote l a) (quote (l + 1) (t (VVar l))) o - VPi x i a b -> Pi x i (quote l a) (quote (l + 1) (b (VVar l))) - VU s -> U s - VLift t -> Lift (quote l t) - VQuote t -> Quote (quote l t) - VNat s -> Nat s - -- ... -``` +Takeaways for any NbE 2LTT checker: +- A stuck splice must be *representable* (here: `SSplice` spine entry on `VRigid`/`VFlex`). + Without it, splices on neutrals have nowhere to go. +- Both cancellation directions are needed; the `⟨∼n⟩` direction fires when quoting a + neutral whose spine ends in a splice. +- **This evaluator computes all redexes, object-level included** (the demo's object + theory has full β) — conversion checking is stage-agnostic here. Contrast staging (§3) + and the CFTT weak-equality alternative. + +`quote :: Lvl -> Val -> Tm` reads values back (standard NbE); `nf = quote ∘ eval`. +`force` unfolds solved metas at the head. `zonk` inlines all solved metas into a term +without evaluating anything else — run before staging. -## 5. Staging / Unstaging (Staging.hs) +## 3. Staging (Staging.hs) -The staging module separates meta and object evaluation: +Separate pass over zonked core syntax, with **two value domains and two evaluators** — +meta values never appear in output, object values are the output: ```hs -data Env = Nil | Def0 Env Val0 | Def1 Env Val1 +data Env = Nil | Def0 Env Val0 | Def1 Env Val1 -- one mixed-stage environment -data Val1 -- meta (compile-time) values +data Val1 -- meta values: computed with, then discarded = VLam1 (Val1 -> Val1) - | VQuote Val0 - | VSomeU1 -- meta types ignored during staging - | VZero1 - | VSuc1 Val1 + | VQuote Val0 -- ⟨t⟩ evaluates its body with eval0 + | VSomeU1 -- ALL meta-level types erase to this dummy + | VZero1 | VSuc1 Val1 -data Val0 -- object (runtime) values - = VVar0 Lvl +data Val0 -- object values: mirror the object syntax + = VVar0 Lvl -- levels ⇒ no weakening/shifting ever | VApp0 Val0 Val0 Icit Verbosity - | VPi0 Name Icit Val0 (Val0 -> Val0) - | VLam0 Name Icit Val0 (Val0 -> Val0) Verbosity + | VLam0 Name Icit Val0 (Val0 -> Val0) Verbosity -- closure per binder + | VPi0 Name Icit Val0 (Val0 -> Val0) | VLet0 Name Val0 Val0 (Val0 -> Val0) Verbosity - | VU0 - | VNat0 - | VZero0 - | VSuc0 - | VNatElim0 + | VU0 | VNat0 | VZero0 | VSuc0 | VNatElim0 ``` -Meta evaluation (only runs at compile time): ```hs -eval1 :: Env -> Tm -> Val1 -eval1 env = \case - Var x -> vVar1 env x - Lam x i a t o -> VLam1 (eval1Bind env t) - App t u i o -> vApp1 (eval1 env t) (eval1 env u) - Quote t -> VQuote (eval0 env t) -- quote object to meta - -- ... - Splice{} -> impossible -- splices only in object context - Lift{} -> VSomeU1 -``` +eval1 env (Lam _ _ _ t _) = VLam1 (eval1Bind env t) -- β computed via vApp1 +eval1 env (Quote t) = VQuote (eval0 env t) -- switch to object evaluation +eval1 env (U{}|Pi{}|Lift{}|Nat{}) = VSomeU1 -- types erased +eval1 env (Splice{}) = impossible -- splice never in meta position -Object evaluation (staging output): -```hs -eval0 :: Env -> Tm -> Val0 -eval0 env = \case - Var x -> vVar0 env x - Lam x i a t o -> VLam0 x i (eval0 env a) (eval0Bind env t) o - App t u i o -> VApp0 (eval0 env t) (eval0 env u) i o - Splice t -> vSplice (eval1 env t) -- splice evaluates meta, embeds object - -- ... - Quote{} -> impossible -- quotes only in meta context -``` +eval0 env (Lam x i a t o) = VLam0 x i (eval0 env a) (eval0Bind env t) o -- NO β +eval0 env (App t u i o) = VApp0 (eval0 env t) (eval0 env u) i o -- structural +eval0 env (Splice t) = vSplice (eval1 env t) -- run metaprogram, embed result + where vSplice (VQuote v) = v ; vSplice _ = impossible +eval0 env (Quote{}) = impossible -Unstaging entry point: -```hs stage :: Tm -> Tm -stage t = quote0 0 $ eval0 Nil t -``` - -The key staging invariant: `stage` takes a mixed-stage term and produces a splice-free object term. - -## 6. Typechecking / Elaboration (Elaboration.hs) - -The demo uses bidirectional typechecking with separate checking and inference modes. - -### Implicit argument insertion: - -```hs -insert' :: Cxt -> IO (Tm, VTy, Stage) -> IO (Tm, VTy, Stage) -insert' cxt act = go =<< act where - go (!t, !va, !st) = case force va of - VPi x Impl a b -> do - m <- freshMeta cxt a st - let mv = eval (env cxt) m - go (App t m Impl V1, b $ mv, st) - va -> pure (t, va, st) +stage t = quote0 0 (eval0 Nil t) -- mixed-stage closed term → splice-free object term ``` -### Subtyping / stage coercion: +Notes: +- `eval0` is "evaluation" only in the sense of resolving variables/splices — it copies + object structure verbatim (strictness: no object β). It implements delayed renamings + via closures + levels. +- Both evaluators error on `Meta`/`InsertedMeta`: **unsolved metas are a staging-time + error** (with a hint to inspect `elab-verbose`). +- Variables in `Env` are stage-tagged (`Def0`/`Def1`); lookup projects the right domain. -```hs -adjustStage :: Cxt -> Tm -> VTy -> Stage -> Stage -> IO (Tm, VTy) -adjustStage cxt t a s s' = case compare s s' of - EQ -> pure (t, a) - LT -> pure (tQuote t, VLift a) - GT -> case force a of - VLift a -> pure (tSplice t, a) - a -> do - m <- freshMeta cxt (VU S0) S0 - unifyCatch cxt a (VLift m) - pure (tSplice t, m) -``` +## 4. Elaboration (Elaboration.hs, Cxt.hs) -### Checking (mode where expected type is known): +Bidirectional: `check :: Cxt -> P.Tm -> VTy -> Stage -> IO Tm` and +`infer :: Cxt -> P.Tm -> IO (Tm, VTy, Stage)` — **infer returns the type *and* the +stage**. `inferS` is infer with an expected stage, reconciled via `adjustStage`. -```hs -check :: Cxt -> P.Tm -> VTy -> Stage -> IO Tm -check cxt t a st = case (t, force a) of - - (P.Lam x a i t, VPi x' i' a' b) | either (\x -> x == x' && i' == Impl) (==i') i -> do - (a, va) <- case a of - Just a -> do - a <- checkU cxt a st - let va = eval (env cxt) a - unifyCatch cxt va a' - pure (a, va) - Nothing -> pure (quote (lvl cxt) a', a') - Lam x i' a <$!> check (bind cxt x va st) t (b $ VVar (lvl cxt)) st - - (P.Quote t, VLift a) -> - tQuote <$!> check cxt t a S0 - - (P.Let st' x a t u, a') | st == st' -> do - (!a, !va, !t, !vt, !verbosity) <- case a of - Nothing -> do - (t, a) <- inferS cxt t st - pure (quote (lvl cxt) a, a, t, eval (env cxt) t, V1) - Just a -> do - a <- checkU cxt a st - let ~va = eval (env cxt) a - t <- check cxt t va st - pure (a, va, t, eval (env cxt) t, V0) - u <- check (define cxt x t vt a va st) u a' st - pure (Let st' x a t u verbosity) - - (P.Hole, a) -> - freshMeta cxt a st -``` +### 4.1 Context (Cxt.hs) +`Cxt = { env :: [Val], lvl, path :: Path, pruning, srcNames :: Map Name (Lvl, VTy, Stage), pos }`. +Every binding records its **stage** in `srcNames`; `Path` is a context zipper used to +build closed Pi types for fresh metas cheaply. `bind` (bound var), `newBinder` +(elaboration-inserted, invisible to source), `define` (let). -### Inference (mode where type is synthesized): +### 4.2 Stage handling: repair, not reject +There is **no stage check at variable lookup** — `infer (Var x)` just returns the stored +stage. Mismatches between inferred and expected stage/type are *repaired* by coercive +subtyping (rules `A ≤ ⇑A`, `⇑A ≤ A`, `U0 ≤ U1`; theory in +`kovacs-2022-staged-compilation-2ltt.md` §3.3): ```hs -infer :: Cxt -> P.Tm -> IO (Tm, VTy, Stage) -infer cxt = \case - P.Var x -> case M.lookup x (srcNames cxt) of - Just (x', a, st) -> pure (Var (lvl2Ix (lvl cxt) x'), a, st) - Nothing -> throwIO $ Error cxt $ NameNotInScope x - - P.App t u i -> do - (i, t, tty, st) <- case i of - Left name -> do - (!t, !tty, !ts) <- insertUntilName cxt name $ infer cxt t - pure (Impl, t, tty, ts) - Right Impl -> do - (!t, !tty, !ts) <- infer cxt t - pure (Impl, t, tty, ts) - Right Expl -> do - (!t, !tty, !ts) <- insert' cxt $ infer cxt t - pure (Expl, t, tty, ts) - - (!t, !a, !b) <- case force tty of - VPi x i' a b -> do - unless (i == i') $ throwIO $ Error cxt $ IcitMismatch i i' - pure (t, a, b) - tty -> do - a <- freshMeta cxt (VU st) st - b <- freshMeta (bind cxt "x" a st) (VU st) st - t <- coe cxt t tty st (VPi "x" i a b) st - pure (t, a, b) - - u <- check cxt u a st - pure (App t u i V0, b $ eval (env cxt) u, st) - - P.Quote t -> do - (!t, !a) <- inferS cxt t S0 - pure (tQuote t, VLift a, S1) - - P.Splice t -> do - (!t, !a) <- inferS cxt t S1 - (!t, !a) <- adjustStage cxt t a S1 S0 - pure (t, a, S0) +adjustStage cxt t a s s' -- move (t : a : U s) to stage s' + | s == s' = (t, a) + | s < s' = (tQuote t, VLift a) -- 0→1: quote + | s > s' = case force a of -- 1→0: splice + VLift a -> (tSplice t, a) + a -> do m <- freshMeta (VU S0) S0 -- a must be ⇑?m + unifyCatch cxt a (VLift m) + (tSplice t, m) + +coe cxt t a s a' s' -- full coercion (t : a : U s) to (a' : U s') + -- Pi vs Pi: contravariant/covariant, η-expanding with Wk for the shifted body; + -- tracks "trivial coercion" (Nothing) to avoid inserting useless η-expansions + -- (VU S0, VU S1) -> Lift t -- U0 ≤ U1 witnessed by Lift + -- (VLift a, VLift a') -> unify a a' + -- (VLift a, a') -> coe (tSplice t) ... -- unwrap and retry + -- (a, VLift a') -> tQuote <$> coe t ... + -- otherwise -> adjustStage then unify ``` -## 7. Unification (Unification.hs) - -Higher-order unification with pruning for implicit arguments. - -### Meta variable solving: - -```hs -solve :: Lvl -> MetaVar -> Spine -> Val -> IO () -solve l m topSp topRhs = do - (!sp, !outer) <- pure $! splitSpine topSp - (!m, !sp) <- expandVFlex m sp - psub <- invert l sp - if isSId outer then do - solveWithPSub m psub topRhs - else case force topRhs of - VRigid x rhsSp -> do - let go SId sp' = solveWithPSub m psub (VRigid x sp') - go (SApp sp u _ _) (SApp sp' u' _ _) = go sp sp' >> unify l u u' - go (SSplice sp) (SSplice sp') = go sp sp' - go (SNatElim _ p s z sp) (SNatElim _ p' s' z' sp') = unify l p p' >> unify l s s' >> unify l z z' >> go sp sp' - go _ _ = throwIO UnifyError - go outer rhsSp - _ -> throwIO UnifyError -``` +`Wk` (explicit weakening) exists solely so `coe` can reuse `t` under the binders it +introduces. Stage errors thus surface as *unification* failures, not as a dedicated +"wrong stage" error. (A simpler checker without subtyping can instead make stage +mismatch a hard error at lookup — a valid design choice, but not what this demo does.) -### Main unify function: +### 4.3 Notable check/infer cases ```hs -unify :: Lvl -> Val -> Val -> IO () -unify l t u = case (force t, force u) of - (VU s , VU s' ) | s == s' -> pure () - (VPi x i a b , VPi x' i' a' b') | i == i' -> unify l a a' >> unify (l + 1) (b $ VVar l) (b' $ VVar l) - (VLift t , VLift t' ) -> unify l t t' - (VQuote t , VQuote t' ) -> unify l t t' - (VRigid x sp , VRigid x' sp' ) | x == x' -> unifySp l sp sp' - (VFlex m sp , VFlex m' sp' ) | m == m' -> intersect l m sp sp' - | True -> flexFlex l m sp m' sp' - (VFlex m sp , t' ) -> solve l m sp t' - (t , VFlex m' sp' ) -> solve l m' sp' t - _ -> throwIO UnifyError +checkU cxt t s = check cxt t (VU s) s -- "this must be a type at stage s" + +check (P.Quote t) (VLift a) = tQuote <$> check t a S0 +check t (VLift a) = tQuote <$> check t a S0 + -- quote INSERTION: checking any non-quote against ⇑A recurses at stage 0. + -- Loses no solutions: every value of ⇑A is ⟨t⟩ up to defeq. Major inference win. + +check (P.Let st' x a t u) a' | st == st' -- let stage must match the + -- current stage; body elaborated in `define`d context + +infer (P.Quote t) = do (t, a) <- inferS t S0; pure (tQuote t, VLift a, S1) +infer (P.Splice t) = do (t, a) <- inferS t S1 + (t, a) <- adjustStage t a S1 S0 -- forces a ≅ ⇑?m + pure (t, a, S0) +infer (P.App t u i) -- implicit insertion (insert'/insertUntilName), then: + -- if head type isn't Pi, coerce it to a fresh Pi (coe) — subsumes stage repair ``` -Key features: -- **Partial substitution**: Used for inverting spines during meta solving -- **Pruning**: Removes arguments from meta solutions to handle nonlinearity -- **Eta-expansion**: Expands splices in spines to enable solving -- **Occurs check**: Prevents infinite types - -## 8. Key design notes - -- **Two separate value types**: `Val1` for meta-level computation, `Val0` for object-level code. They never mix. -- **Quote/Splice as primitives**: Quote converts object → meta (as value), splice runs meta and embeds object. -- **Stage-annotated let**: `Let S0` for object lets, `Let S1` for meta lets. -- **No object beta reduction during staging**: object lambdas are opaque; only meta computation runs. -- **Bidirectional elaboration**: separate checking and inference passes. -- **Implicit inference**: uses Agda-style implicit arguments with higher-order unification. +Fallback cases of `check` infer + `coe`. Implicit-argument insertion (`insert`, +`insert'`, `insertUntilName`) is standard elaboration-zoo style. + +### 4.4 Design notes (from the demo README) +- **Stages must be unambiguous in source**: no stage metavariables/stage unification. + Explicit stages on every `let` turn out to make the rest of inference highly effective; + stage metavariables were tried in earlier prototypes and dropped as useless complexity. +- **Contextual metavariables** abstract over mixed-stage scopes — formally *outside* + 2LTT (no 2LTT type former crosses stages). Fine in practice; after zonking, pure 2LTT + syntax remains. A fresh meta's type is a closed iterated Pi over its scope (`closeTy`). +- Coercion avoidance: `coe` returns `Nothing` for trivial coercions so e.g. + `(Nat0 → Nat0) ≤ (Nat0 → Nat0)` doesn't η-expand. + +## 5. Unification (Unification.hs) + +Pattern unification with pruning, à la elaboration-zoo, extended for staging: +- spine inversion treats **quote/splice like a unary record's constructor/projection** + (analogous to Σ projections), so metas can be solved under splices; +- meta η-expansion to eliminate splices from spines; +- intersection/pruning for nonlinear spines; occurs check; no postponed constraints; +- `unify` has `VLift/VLift` and `VQuote/VQuote` congruence cases; `solve` splits the + spine at outer non-invertible entries (e.g. `SSplice`) and η-expands as needed. + +## 6. What to copy vs. reconsider + +Copy: smart constructors; stage-tagged bindings + `infer` returning stage; quote +insertion in `check`; stuck-splice spines; zonk-before-stage; unsolved-meta staging +error; two-domain staging with levels + closures; meta-type erasure in staging. + +Reconsider per design: the coercive-subtyping repair (powerful but complex — a hard +stage error is the simple alternative); full object β in conversion (fits the 2022-style +object theory; a CFTT-style object language wants weak object equality instead — see +`kovacs-2024-closure-free-2ltt.md` §2.4); type-in-type (demo-only shortcut). diff --git a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md index 464436a9..8486aace 100644 --- a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md +++ b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md @@ -1,87 +1,125 @@ -# Downen/Ariola/Peyton Jones/Eisenberg 2020 — *Kinds Are Calling Conventions* (substantive rewrite, implementation-focused) - -This note extracts and rewrites the parts most relevant to implementing a staged language where types carry low-level compilation information. - -## 1. Motivation: polymorphism vs efficient code - -Polymorphism is great for source languages, but compilers need concrete calling conventions and concrete representations to generate efficient code. - -This work proposes an intermediate language (IL) where you can still write polymorphic programs, but the type/kind system tracks: -- runtime representation of values (boxed pointer vs unboxed int, etc.) -- arity / calling convention information for functions -- evaluation order / strictness (e.g. call-by-name vs call-by-value variants) - -Key slogan: -- store calling-convention info in **kinds** (or kind-like indices), not as ad-hoc compiler metadata. - -## 2. "Boxing/unboxing is explicit" as an optimizer-enabling design - -A recurring pattern in the IL: -- There is a primitive/unboxed representation (fast, low-level) -- There is a boxed/wrapped representation (uniform, convenient) -- There are explicit constructors/destructors to move between them - -Examples discussed include: -- closure wrappers for arity/evaluation control (`Clos`/`App`) -- boxed vs unboxed integers (`I#` and case on `I#`) - -Implementation takeaway for a staged system: -- if metaprograms can choose representations, you want those choices reflected explicitly in the object language output so downstream optimization is simpler and more reliable. - -## 3. Indexing types by representation and convention (core technique) - -A simplified view of the IL's approach: - -### 3.1 Representation indices -Introduce a kind/index `Rep` describing runtime storage (pointer, int register, etc.). - -Then define a family `TYPE : Rep -> *` (or "types classified by representation"). -So a type is not just `Int`, but `Int : TYPE IntR` (illustrative). - -### 3.2 Conventions / levity / evaluation order indices -In addition to representation, the paper supports indices that describe: -- evaluation strategy of arguments/results -- function arity / calling protocol -- (and related "levity polymorphism" concerns) - -The point is to precisely control what can be polymorphic: -- some functions can be representation-polymorphic -- but some combinations are rejected because codegen would not know how to pass arguments - -The paper gives examples where a seemingly innocent "polymorphic application helper" must be rejected unless it restricts representations to pointer-like ones, because otherwise the call sequence is not statically determined. - -## 4. Type system structure (what to reuse) - -The IL has typing rules that: -- prevent "unknown representation" values from being used in ways that require a concrete calling convention -- ensure you only call primitive ops with the right number/kind of arguments -- ensure closure wrappers are used where needed to preserve language-level semantics (e.g. call-by-value polymorphic lambdas must remain values after erasure) - -Implementation takeaway for 2LTT/CFTT: -- if you want *layout control* as a staged feature, adopt the same discipline: - make representation/convention indices part of object typing, so unstaging outputs code that is already "codegen-determined". - -## 5. How this complements 2LTT - -2LTT gives you: -- a meta language where you can compute programs/types - -KACC gives you: -- a way to make the object language's types rich enough to express low-level calling/representation choices safely - -Combined design sketch: -- Meta level computes object types that include representation indices. -- Unstaging produces an IL-like object program whose typing guarantees calling convention correctness. - -This is especially relevant if you want to reproduce "memory layout control" / "monomorphization-by-staging" style applications mentioned in the staging literature. - -## 6. Practical "minimum viable" adaptation - -If the full IL is too large, start with: -- `Rep = Ptr | I64 | F64 | ...` -- `Ty rep` object types, so every object term is typed with a rep -- restrict polymorphism so that: - - fully representation-polymorphic functions can only do things that are representation-agnostic - - calling a function at a rep-polymorphic type is restricted unless you wrap it into a uniform calling convention (closure) that erases the rep differences - -This gives you a stepping stone toward the richer kind discipline described in the paper. +# Downen/Ariola/Peyton Jones/Eisenberg 2020 — *Kinds Are Calling Conventions* (implementation-oriented rewrite) + +An intermediate language (**IL**) where the *kind* of a type carries everything codegen +needs: representation, evaluation strategy, and function arity. Polymorphic code compiles +to a single block of machine code (type erasure, no monomorphization), with kind-level +side conditions ruling out exactly the uncompilable cases. + +## 1. The three axes + +- **Representation** — how a value is stored (heap pointer, machine int, …). Determines + registers/moves. +- **Levity** — `L` (lifted: may be a thunk, evaluated lazily) vs `U` (unlifted: always a + value, evaluated eagerly). Lets one IL serve both eager and lazy source languages. +- **Arity** — how many arguments (and of what representations) a primitive function + needs before it does work; determines the call sequence. + +Arity is *intensional* — types like `Int → Int → Int` don't determine it (`λx λy. e` has +arity 2; `λx. let z = expensive x in λy. e` has arity 1). The IL exists to *memorialize* +the result of an arity analysis, not to perform it. + +## 2. Kind grammar + +``` +κ ::= TYPE ρ ν -- every type former yields TYPE ρ ν +ρ ::= r | PtrR | IntR | ... -- representation (r: rep variable) +γ ::= g | L | U -- levity (g: levity variable) +ν ::= n | Eval γ | Call[α] -- convention (n: convention variable) +α ::= ρ, α | ε | arity(ν) -- arity: list of argument reps +``` + +A type's convention is *either* `Eval γ` (data: levity) *or* `Call[α]` (primitive +function: arity) — functions are **called, not evaluated**, so they have no levity. +Examples: + +``` +Int# : TYPE IntR (Eval U) IntL : TYPE PtrR (Eval L) +Int# ⤳ Int# ⤳ Int# : TYPE PtrR Call[IntR, IntR] +``` + +Haskell's default kind `★` = `TYPE PtrR (Eval L)`; an eager language's default is +`TYPE PtrR (Eval U)`. Function-type formation *concatenates* arities: if +`τ₁ : TYPE ρ₁ ν₁` and `τ₂ : TYPE ρ' Call[ρ₂,…,ρₘ]` then +`τ₁ ⤳ τ₂ : TYPE PtrR Call[ρ₁,ρ₂,…,ρₘ]` (if `τ₂` is `Eval γ`, arity is just `[ρ₁]`); +`arity(ν)` may be stuck on a convention variable. `∀` is kind-transparent (erased at +runtime) but its variable must not escape into the kind. + +## 3. Explicit boxing, in two parallel instances + +The same box/unbox pattern applies to representations and to arities; making both +explicit in IL is what lets the optimizer remove redundant round-trips: + +| primitive (fast) | boxed (uniform) | box | unbox | +|---|---|---|---| +| `Int#` (machine int) | `Int γ` (heap) | `I# e` | `case e of I# x → …` | +| `τ ⤳ σ` (arity-n code) | `γ{τ ⤳ σ}` (closure) | `Clos e` | `App e` | + +`Clos`/`App` convert between statically-called primitive functions and first-class +closures with a uniform (arity-1-ish) calling convention. Wherever a function must be +stored, passed at unknown convention, or kept as a value after erasure (e.g. CBV source +lambdas), it gets `Clos`-boxed. + +## 4. Polymorphism restrictions: `mono-rep` / `mono-conv` + +Instead of forbidding quantification over unboxed/function kinds (GHC's old "draconian" +rule — too restrictive, and broken by kind polymorphism), IL allows *all* quantification +and puts **side conditions on the term rules**: + +``` +Fun-I: λx:τ. e requires τ mono-rep +Fun-E: e e' requires τ mono-rep and τ mono-conv (τ = argument type) +Clo-I: Clos e requires the function's arity to be statically known +``` + +`mono-rep`/`mono-conv` = the representation/convention contains no variables. Rationale: +compiling an *application* requires knowing how the argument is stored (rep) and when to +evaluate it / what code shape to build for it (conv). A variant rule (`Fun-A-E`) relaxes +`mono-conv` when the argument is syntactically an answer (value) — lazy vs eager is then +indistinguishable. These conditions are validated by the lowering translation (§6): they +are exactly what the compilation scheme needs, no more. + +What *can* be polymorphic — perhaps surprisingly much: +- `error : ∀ (r : Rep) (a : TYPE r ν). String → a` — never returns, so the result rep + is irrelevant; one code block serves all instantiations. +- Return types may be rep/levity-polymorphic thanks to tail calls (the callee returns to + the caller's caller): `revapp : ∀ n r g (t₁ : TYPE PtrR n) (t₂ : TYPE r (Eval g)). t₁ ⤳ (t₁ ⤳ t₂) ⤳ t₂` + — `t₁` may be convention-polymorphic (only moved, never called/evaluated) but must be + pointer-represented; `t₂` fully rep/levity-polymorphic but *not* conv-polymorphic + (the λ-bound `f` gets called, so its arity must be known). +- `twice f x = f (f x)` must fix `Eval L` *or* `Eval U` for the intermediate result — + polymorphism boundaries are exactly where a strategy decision is forced. +- Data types may be levity/convention-polymorphic: + `data List (g : Lev) (n : Conv) (t : TYPE PtrR n)`; a fully strict function like `sum` + is levity-polymorphic in everything, while `map` must pick the result spine's levity + (it changes evaluation order — same IL definition, different machine code). + +## 5. Equational theory: substitutability by type, not syntax + +β for primitive functions fires only on **substitutable** arguments `S`, defined by +*kind*: all answers are substitutable; any expression of `Eval L` type is substitutable +(CBN-style); `Eval U` arguments must be reduced to answers first (CBV-style). This +integrates multiple evaluation orders in one calculus. Primitive function types enjoy +**unrestricted η** (in both directions) — precisely because functions cannot be observed, +only called. (Same property Kovács cites for CFTT's object language.) + +## 6. Lowering to machine language (ML) + +IL compiles (kind-directed, type-erasing) to **ML**: uncurried, fully η-expanded +functions, fully saturated calls, types = representations only. E.g. arity-3 `g` becomes +`λ(x:PtrR, y:PtrR, z:IntR). …` and every call site passes all three at once. The paper +also gives CBN and CBV System F translations *into* IL (CBN: everything `★ = TYPE PtrR +(Eval L)`; CBV: functions must be `Clos`-boxed to stay values), with correctness theorems +end-to-end. §7 adds optional *dynamic* arity dispatch on closures (runtime arity check to +use the best available calling convention). + +## 7. Use with a 2LTT + +KACC is orthogonal kit for the *object language*: index object types by +rep/levity/arity so unstaging emits codegen-determined code. In a 2LTT the meta level +replaces IL's quantifiers: rep/levity/arity polymorphism becomes meta-level abstraction +that staging eliminates, so the `mono-*` side conditions reappear as "these indices must +be canonical by staging time" (cf. the memory-representation-polymorphism variation in +`kovacs-2022-staged-compilation-2ltt.md` §5.2, and the CFTT ≈ simply-typed-IL-fragment +remark in `kovacs-2024-closure-free-2ltt.md` §7). A minimal adaptation: `Rep` as a meta +type, object types indexed by `Rep`, and — if functions are first-class — a `Clos`-style +boxing former to recover uniform representation where needed. diff --git a/.opencode/skills/2ltt/implementation-guide.md b/.opencode/skills/2ltt/implementation-guide.md index 1761e81e..c5e71cef 100644 --- a/.opencode/skills/2ltt/implementation-guide.md +++ b/.opencode/skills/2ltt/implementation-guide.md @@ -1,392 +1,189 @@ -# Practical implementation guide for 2LTT / CFTT-style systems +# Practical implementation guide for 2LTT-based staged compilers -This file is the "do this in code" companion to the three paper rewrites in this skill. +The "do this in code" companion to the paper notes in this skill. Theory lives in the +paper files; this file covers architecture, design decisions, and pitfalls. Notation: +`⇑A` lift, `⟨t⟩` quote, `∼t` splice, `U0`/`U1` object/meta universes. -## 0. Terminology (consistent with the papers) +## 1. Pipeline shape -- **Meta level** (compile time, stage 1): runs during unstaging. -- **Object level** (run time, stage 0): the output program after unstaging. - -Core bridge primitives: - -- `⇑A` (lift): a meta type meaning "code that will produce an object term of type `A`". -- `⟨t⟩` (quote): make code from an object term. -- `∼u` (splice): run meta code `u : ⇑A` and insert resulting object term into object term. - -A crucial design choice: -- Meta level has "real computation" (β-reduction, recursion, induction, etc.). -- Object level is often treated as *code* during meta computation; definitional equality may be intentionally weak. - ---- - -## 1. Minimal core syntax & judgments (implementation-oriented) - -A practical way to structure the implementation is a *two-sorted* AST with a shared front-end. - -### 1.1 Contexts - -Keep two contexts (or a single context with a stage tag): -- `Δ` = meta context (compile-time variables) -- `Γ` = object context (runtime variables) - -You will frequently need mixed judgments, e.g. meta terms that mention object variables *only through* quoted object syntax. - -### 1.2 Object language (stage 0) AST (example) - -You can start with a typed or untyped object AST. Typed helps invariants; untyped is simpler. - -Example (untyped-ish, but with constructors you'll need): -- Variables / de Bruijn indices -- Let -- Lambdas + application (if your object language is higher-order) -- Data constructors + case -- (Optional) letrec for recursive functions - -```hs -data ObjTm - = OVar Ix - | OLam Name ObjTy ObjTm - | OApp ObjTm ObjTm - | OLet Name ObjTy ObjTm ObjTm - | OCon ConName [ObjTm] - | OCase ObjTm [(Pat, ObjTm)] - | OLetRec [(Name, ObjTy, ObjTm)] ObjTm ``` - -### 1.3 Meta language (stage 1) AST (example) - -Meta level is a dependently typed λ-calculus (whatever subset you implement). - -Add explicit constructors for: -- Lifted types: `Lift ObjTy` -- Quotation of object terms: `Quote ObjTm` -- Splice into object terms: represented **in the object AST** as `OSplice MetaTm` - (or in a combined AST before you split). - -A simple combined representation during elaboration: -```hs -data Tm - = Var Ix - | Lam Name Ty Tm - | App Tm Tm - | Pi Name Ty Ty - | -- ... - | Lift Ty0 -- ⇑A - | Quote Tm0 -- ⟨t⟩ - | Splice Tm1 -- ∼u (only valid when typechecking an object term) +parse → elaborate (bidirectional, NbE conversion, metavariables) → zonk → stage → backend ``` -Then, after typechecking/elaboration, you can separate into `MetaTm` vs `ObjTmWithSplice` vs `ObjTm`. - ---- - -## 2. Typing rules you actually need (core) - -### 2.1 Stage separation invariants -Enforce: -- Ordinary type formers (Π/Σ/Id/inductives) do not mix stages "accidentally". -- Functions do not cross stages as ordinary terms. -- Interaction happens only via `⇑`, `⟨⟩`, `∼`. - -### 2.2 Lift/Quote/Splice (schematic rules) - -Let object types be `A : U0` (or `A : Ty`), meta types be `MetaTy` (or `U1`). - -- Lift formation: - - If `A` is an object type, then `⇑A` is a meta type. - -- Quote introduction: - - If `t` is an object term of type `A`, then `⟨t⟩` is a meta term of type `⇑A`. - -- Splice elimination: - - If `u` is a meta term of type `⇑A`, then `∼u` is an object term of type `A`. - -- Definitional equalities (treat as computation rules): - - `∼⟨t⟩ ≡ t` - - `⟨∼u⟩ ≡ u` - -In code, you'll likely implement these as *normalization* / *evaluation* rules in the meta evaluator and/or in conversion checking. - ---- - -## 3. Definitional equality strategy (practical + matches the papers) +Two distinct evaluation mechanisms, easy to conflate: -You need two conversion relations in practice: +1. **Conversion-checking evaluation** (inside elaboration): decides definitional + equality of types/terms. Operates on one mixed semantic domain. Whether it computes + *object*-level redexes is a design decision (§2.1). +2. **Staging** (after elaboration): runs all metaprograms, eliminates every + quote/splice, outputs pure object syntax. Never β-reduces object code + (*strictness*), regardless of what conversion does. -### 3.1 Meta definitional equality (strong) -Meta definitional equality should compute: -- β for meta lambdas -- unfolding of meta let / (maybe) meta recursors -- computation for meta inductives / eliminators +Both are NbE-style: eval into a semantic domain with De Bruijn levels + closures, read +back into syntax with indices. See `demo-implementation.md` for the reference shapes +(§2 conversion evaluator, §3 two-domain staging evaluator). -This is how unstaging "runs". +## 2. Design decisions to make up front -### 3.2 Object definitional equality (weak) -To avoid needing an evaluator for the object language at compile time, you can intentionally set: +### 2.1 Object language strength ⇒ object definitional equality +Two coherent points in the space — pick one deliberately: -- **No β/η for object lambdas** -- No let-unfolding at the object level -- Possibly only α-equivalence / structural congruence +- **2022-style**: object level is a full dependent type theory with β/η. Conversion + checking must then compute object redexes too (the demo evaluator is stage-agnostic). + Needed if object types depend on object terms. +- **CFTT-style** (2024): object level is simply-typed/first-order with general + recursion; **no β, no η, no let-unfolding** for object code — conversion compares + object terms essentially syntactically. Rationale: code size/efficiency aren't stable + under βη; general recursion has no decidable equality anyway. Object types are + meta-level data (`Ty : MetaTy`) and never depend on object terms. -This is explicitly used in the 2024 closure-free paper to keep things simple when typechecking object code embedded in a dependent meta system. +Mixing them accidentally (e.g. weak equality but object-term-dependent types) breaks +things: dependent typing needs substitution and conversion at the object level. ---- +### 2.2 Stage bookkeeping: repair vs. reject +Record the stage of **every binding** in the elaboration context, and have `infer` +return `(Term, VTy, Stage)`. On a stage mismatch there are two designs: -## 4. Unstaging algorithm (the deliverable) +- **Repair (reference demo)**: coercive subtyping `A ≤ ⇑A` (insert quote), `⇑A ≤ A` + (insert splice), optionally `U0 ≤ U1` (insert `Lift`), with contravariant/covariant + function rule. Powerful inference (quotes/splices mostly disappear from surface + syntax); costs a coercion pass, explicit weakening in the core, coercion-avoidance + logic. See `demo-implementation.md` §4.2–4.3. +- **Reject**: hard "stage mismatch" error at the point of use. Much simpler; forces + explicit staging operators in the surface language. Fine as a first iteration — + the type structure is identical, only elaboration ergonomics differ. -### 4.1 What unstaging does -Input: a well-typed "mixed-stage" program. -Output: a splice-free object program + splice-free object types. +Either way: **explicit stages on `let`-definitions** (no stage metavariables). The +reference implementation found this single annotation makes the rest of stage inference +effective and stage unification unnecessary. -### 4.2 Staging-by-evaluation (engineering form) +### 2.3 Optional extensions (see the respective files) +- Closure-free discipline `ValTy`/`CompTy`, computation products, call saturation — + `kovacs-2024-closure-free-2ltt.md` §2. +- Representation/arity/levity indexing of object types — + `downen-2020-kinds-are-calling-conventions.md`; meta-level `Rep` indexing — + `kovacs-2022-staged-compilation-2ltt.md` §5.2. +- Intensional analysis (needs a non-standard setup) — + `kovacs-2022-staged-compilation-2ltt.md` §6. -Implement a function (names vary): -- `unstageObj : MetaEnv -> ObjEnv -> ObjTmWithSplice -> ObjTm` -- `evalMeta : MetaEnv -> ObjEnv -> MetaTm -> MetaVal` +## 3. NbE core (checker) -Key case: splicing inside object terms: -1. Evaluate the meta term `u : ⇑A` to a meta value that *represents code*. -2. Extract the produced object AST. -3. Recurse to ensure the result contains no splices. +Terms use **De Bruijn indices** (0 = nearest binder); semantic values use **levels** +(0 = outermost), so weakening of values is free and staging/splicing needs no shifting. -Pseudocode: -```hs -unstageObj envM envO (OSplice u) = - case evalMeta envM envO u of - VCode a obj -> unstageObj envM envO obj - _ -> error "impossible: splice must evaluate to code" - -unstageObj envM envO (OLet x ty rhs body) = - OLet x (unstageTy envM envO ty) - (unstageObj envM envO rhs) - (unstageObj envM (envO.ext x) body) - --- other constructors: recurse structurally ``` - -### 4.3 Representing code at the meta level -The easiest representation for values of type `⇑A` is literally: -```hs -data MetaVal - = ... - | VCode ObjTy ObjTmWithSplice -- (optionally also carry A) +lvl_to_ix(depth, lvl) = depth - lvl - 1 (and symmetrically ix→lvl) ``` -Then evaluation of `⟨t⟩` returns `VCode _ t`. - ---- - -## 5. Let-insertion / sharing (needed for good codegen) - -Naively, `down (up x)`-style conversions duplicate splices and can duplicate runtime work. - -Solution pattern: a meta-level code-generation monad (CFTT uses `Gen`) that: -- introduces object-level `let` bindings to ensure sharing -- structures codegen in CPS so you can "emit lets" in order - -You can implement a minimal writer-like CPS monad: -```hs -newtype Gen a = Gen { runGenK :: (a -> VCode) -> VCode } - -gen :: VCode -> Gen VCode -- bind code to an object-level let, then pass variable code onward -runGen :: Gen VCode -> VCode -``` - -The key contract: `gen` makes sure the produced object code is a variable reference, so reusing it is cheap. - ---- - -## 6. Closure-free object language (optional but central to Kovács 2024) - -If you want a guarantee of "no dynamic closures", design the object language so that: -- **values** (data) cannot contain functions -- **computations** (functions) cannot be stored/passed around - -Mechanically: split object types into: -- `ValTy` — types whose inhabitants are runtime values that can be stored -- `CompTy` — computations (not storable), e.g. functions, call-by-name-ish - -Then enforce that constructor fields are in `ValTy`, and that function types live in `CompTy`. - -This still permits lambdas under `case`/`let` syntactically, but compilation can use **call-saturation** / hoisting so calls are always saturated and closures are not needed. - ---- - -## 7. Representation/calling convention indexing (optional; from KACC) - -If you want "layout control" / "arity/eval-order control": -- add a kind/index level describing runtime representation and calling convention -- have object types carry these indices so codegen is type-directed - -A minimal adaptation: -- `Rep` kind: pointer, int, float, unboxed tuple, etc. -- `Conv` kind: calling convention (arity, evaluation strategy) -- `TYPE rep conv` kind (or `Ty rep conv`) for object types whose runtime calling convention is known - -Meta code can compute these indices and select specialized representations, and unstaging produces an IL-like typed program. - ---- - -## 8. Implementation Architecture: NbE + Staging - -Modern practical implementations use **Normalization by Evaluation (NbE)** for type checking and evaluation for staging. - -### Type Checker NbE (Kovács 2022 §3–4, elaboration-zoo 01-eval-closures-debruijn) -The type checker maintains a **semantic domain** separate from syntax: - -```haskell --- Haskell pseudocode (elaboration-zoo style) -data Value - = VRigid Lvl Spine -- stuck on a local variable - | VLam Name (Val -> Val) -- closure as a function - | VPi Name (Val -> Val) VTy -- dependent Pi with closure - | VLit Int - | VGlobal Name - | VLift Val - | VQuote Val - --- Evaluation: interpret terms in an environment -eval :: Env Val -> Term -> Val -eval env (Var ix) = env !! (env.len - 1 - ix) -- index to stack -eval env (Lam x t) = VLam x (\v -> eval (v:env) t) -eval env (Pi x a b) = VPi x (\v -> eval (v:env) b) (eval env a) -eval env (App f args) = vApp (eval env f) (map (eval env) args) - --- Quotation: convert value back to term (for errors, output) -quote :: Lvl -> Val -> Term -quote lvl (VRigid x sp) = quoteSp lvl (Var (lvl2Ix lvl x)) sp -quote lvl (VLam x t) = Lam x (quote (lvl+1) (t (VRigid lvl))) -quote lvl (VPi x a b) = Pi x (quote lvl a) (quote (lvl+1) (b (VRigid lvl))) -``` - -**Key design choices:** -- Terms use **De Bruijn indices** (count from nearest binder). -- Values use **De Bruijn levels** (count from outermost binder). -- Closures are functions `Val -> Val` in the metalanguage (or `Closure { env, body }` in Rust). -- No syntactic substitution — substitution is modeled via environment extension. - -**Why this works:** -- Indices are pure syntax — portable, no external state. -- Levels are the natural output of evaluation — fresh variables are just the current depth. -- Closures capture the evaluation environment, eliminating variable-capture bugs. - ---- - -## 9. De Bruijn Representation and Shifting - -### Indices vs Levels - -Terms use **De Bruijn indices** (0 = nearest binder): - -``` -\x . \y . x --> Lam("x", Lam("y", Var(Ix(1)))) - The reference to x is 1 step from the nearest binder (y). -``` - -Evaluation uses **De Bruijn levels** (0 = outermost): - -``` -context: [x : u64, y : u64, z : u64] at depth 3 -x is at level 0, y at level 1, z at level 2. -Fresh var is at level 3. - -When quoting Rigid(1), convert to Var(Ix(3 - 1 - 1)) = Var(Ix(1)). -``` - -Conversions: ```rust -ix_to_lvl(depth: Lvl, ix: Ix) -> Lvl = Lvl(depth.0 - ix.0 - 1) -lvl_to_ix(depth: Lvl, lvl: Lvl) -> Ix = Ix(depth.0 - lvl.0 - 1) -``` - ---- - -## 10. Reference Implementations - -- **elaboration-zoo** (Kovács, 2020): https://github.com/AndrasKovacs/elaboration-zoo - - Branch `01-eval-closures-debruijn` is the canonical reference for NbE + De Bruijn. - - Haskell source is clean and readable; comments explain each step. - - Shows the minimal NbE setup needed for dependent type checking. - -- **2LTT skill / Splic** (this project): - - `compiler/src/core/value.rs`: Core NbE data structures and functions. - - `compiler/src/core/mod.rs`: De Bruijn index/level types and conversions. - - `docs/bs/nbe_and_debruijn.md`: Detailed walkthrough of the architecture and index shifting. - -- **Kovács papers**: - - *Staged Compilation with Two-Level Type Theory* (ICFP 2022): Foundational theory and properties. - - *Closure-Free Functional Programming in a Two-Level Type Theory* (ICFP 2024): Object-level closure optimization. - ---- - -## 11. Bidirectional Elaboration Patterns (anti-drift guardrails) - -The type-checker is a **bidirectional elaborator**: `infer` synthesises a type, `check` verifies one. Getting these right avoids a class of ad-hoc workarounds. - -### 11.1 `infer` must return its type - -```haskell -infer :: Ctx -> Stage -> Tm -> (CoreTm, VTy) -``` - -Returning the type directly means callers never need to reconstruct the type from the elaborated term. A helper like `typeOf` that pattern-matches the core term to recover a type is a signal that `infer` is not returning enough information. - -### 11.2 `checkU` / `check_universe` - -Instead of: -```haskell -(t, ty) <- infer ctx s e -unless (isUniverseType ty) $ fail "expected a type" -``` - -Use: -```haskell -t <- checkU ctx s e -- checkU cxt t s = check cxt t (VU s) s -``` - -This directly encodes the kinding rule and avoids fragile `isUniverseType` predicates. See the reference implementation (`Elaboration.hs: checkU`). - -### 11.3 Stuck splices are a neutral form - -`Value` needs a `Splice` neutral alongside `Rigid` (stuck variable): - -``` -eval(Quote(Splice(v))) = v -- cancel -eval(Splice(Quote(v))) = v -- cancel -eval(Splice(v)) = Splice(v) -- stuck: v is not a Quote -eval(Quote(v)) = Quote(v) -- stuck: v is not a Splice -``` - -Without the `Splice` neutral, `eval(Splice(v))` has nowhere to go and either panics or silently drops the splice, breaking quote/splice cancellation in the NbE type-checker. - -### 11.4 Stage-check variables at lookup - -The context should record the stage of each binding and verify it matches the current elaboration stage when a variable is looked up: - -```haskell -infer cxt (Var x) = do - let (x', a, s) = lookupVar cxt x - when (stage cxt /= s) $ fail "stage mismatch for variable" - pure (Var x', a) -``` - -Without this, a meta-phase variable referenced in an object context produces a confusing type error instead of a clear stage error. The reference calls this `guardStage` (`Cxt.hs`). - ---- - -## 12. Glossary +// shape, not literal code +enum Value { + Rigid(Lvl, Spine), // stuck on a variable + Flex(MetaVar, Spine), // stuck on an unsolved meta (if you have metas) + Lam(Name, Closure), + Pi(Name, VTy, Closure), + U(Stage), Lift(VTy), Quote(Value), + ... +} +``` + +- Closures: `{ env, body }` (or a host-language function). Substitution is *never* + performed on syntax; going under a binder extends the environment with a fresh + `Rigid(depth)`. +- Spines record stuck eliminations. **A stuck splice is a spine entry** (or a dedicated + neutral): `splice(Rigid x sp) = Rigid x (sp . Splice)`. Cancellation both ways: + `∼⟨t⟩ = t` in `vSplice`, and `⟨n·∼⟩ = n` when quoting a neutral ending in a splice. + Without a stuck-splice representation, `eval` on a splice of a variable has nowhere + to go and either panics or drops the splice. +- Read-back (`quote : Lvl → Value → Term`, a.k.a. "quotation" in NbE jargon — distinct + from the staging operation ⟨⟩!) applies closures to fresh rigids at the current depth. + +## 4. Elaboration guardrails + +These invariants prevent whole classes of bugs: + +- **`infer` returns `(Term, VTy)`** (plus stage). Never recover a type after the fact by + pattern-matching elaborated terms — a `typeOf`-style helper is a red flag that + `infer` returns too little. +- **`checkU`**: when a term must be a type, check against the universe directly — + `checkU cxt t s = check cxt t (VU s) s`. Don't infer-then-test with an + `isUniverseType` predicate. +- **Quote insertion in `check`**: when checking any non-quote term against `⇑A`, check + the term against `A` at stage 0 and wrap with quote. Sound because every value of + `⇑A` is `⟨t⟩` up to definitional equality; big ergonomics win. +- **Smart constructors** `tQuote`/`tSplice` that cancel `Quote(Splice t)`/`Splice(Quote t)` + syntactically, so elaboration output stays small and staging sees fewer no-ops. +- If using metavariables: **zonk before staging**; staging must treat a remaining + unsolved meta as a hard error with a good message. + +## 5. Staging pass essentials + +(Reference shape: `demo-implementation.md` §3.) + +- Separate pass over elaborated (zonked) syntax; do not reuse the conversion evaluator. +- **Two value domains**: meta values (functions-as-closures, inductive values, quoted + object values) and object values (mirror of object syntax with levels + closures). + One environment with stage-tagged entries. +- `eval_meta` β-reduces and runs eliminators; **erases all meta-level types to a dummy** + (they cannot appear in output). `eval_obj` is structural — it only resolves variables + and splices; `Splice t → eval_meta t` must yield a quoted object value, anything else + is a compiler bug (`unreachable!`, not a user error). +- Output invariant: read-back of the object value contains no quote, splice, lift, or + meta-level residue. Worth asserting in tests. +- Correctness properties worth testing: *stability* (staging splice-free input is + identity) and *strictness* (object redexes in the input survive verbatim). + +## 6. Code generation quality + +Meta-level use of object code duplicates it (using `x : ⇑A` twice pastes the expression +twice). The toolkit — `Gen` monad (CPS let-insertion, polymorphic answer type), +`gen`/`genRec`, case-splitting via `Split`, join points via `MonadJoin` + SOP — is +library-level metaprogramming, specified in `kovacs-2024-closure-free-2ltt.md` §3–4. +A staged compiler doesn't need built-in support, but its object language must offer +`let`/`letrec` insertable at arbitrary positions for these libraries to be writable. +Deduplication/caching of generated code across splice sites is an open engineering +problem (flagged in both papers). + +## 7. Pitfalls checklist + +- Dropped stuck splices (missing neutral case) — silent wrong output. (§3) +- Object β performed during staging — violates strictness, destroys inlining control. +- Conversion checker computing object redexes in a CFTT-style design (or failing to in + a 2022-style design). (§2.1) +- Quote/splice cancellation implemented in only one direction. +- Meta code leaking into staging output because meta types weren't erased or a meta + binding was staged as object. +- Recovering types from elaborated terms instead of returning them from `infer`. (§4) +- Index/level mix-ups when splicing object values into deeper contexts — use levels in + all semantic domains; convert only at read-back. +- Treating internal invariant violations after type checking as recoverable errors — + they are bugs; fail loudly. + +## 8. Reference implementations + +- **elaboration-zoo** (Kovács): https://github.com/AndrasKovacs/elaboration-zoo — + branch `01-eval-closures-debruijn` is the minimal NbE + De Bruijn reference; + later branches add metas/implicits. +- **staged demo** (Kovács): https://github.com/AndrasKovacs/staged/tree/main/demo — + full 2LTT elaborator + stager; excerpted in `demo-implementation.md`. The repo also + contains the LaTeX sources of both Kovács papers and an Agda embedding of CFTT + (`icfp24paper/supplement`). + +## 9. Glossary | Term | Definition | |------|-----------| -| **NbE** | Normalization by Evaluation. Interpreter-based type checking that maintains semantic values and quotes back to syntax. | -| **Closure** | `{ env: &[Value], body: &Term }`. Captured environment + unevaluated body for lazy evaluation. | -| **Neutral / Rigid** | A value that cannot be reduced further (e.g., stuck on a free variable). | -| **Canonical** | A value in "normal form" (fully evaluated). | -| **De Bruijn index** | Variable reference counting from the nearest binder (0 = innermost). | -| **De Bruijn level** | Variable position counting from the outermost binder (0 = root). | -| **Quote** | Convert a value back to term syntax. | -| **Free variable** | A variable not bound by any enclosing lambda/pi in the term. | -| **Shift** | Adjust De Bruijn indices when moving code to a different binding depth. | -| **Splice** | `$(e)`. Run meta code and insert the result into an object context. | -| **Quote** | `#(e)`. Embed an object term as meta code (lift to `[[T]]`). | -| **Lift** | `[[T]]`. Meta type of object code producing type `T`. | +| **Stage** | 0 = object/runtime, 1 = meta/compile-time. Some implementations say "phase". | +| **Lift `⇑A`** | Meta type of metaprograms producing object code of type `A`. | +| **Quote `⟨t⟩`** | Staging intro: object term `t : A` as meta value of `⇑A`. | +| **Splice `∼t`** | Staging elim: run `t : ⇑A` during staging, insert resulting object term. | +| **Staging / unstaging** | Running all metaprograms; output is splice-free object code. Same operation, two names (2022 / 2024 papers). | +| **Soundness / stability / strictness** | Staging output ≈ input up to conversion / staging is identity on object code / staging preserves object term formers exactly. | +| **NbE** | Normalization by evaluation: eval syntax → semantic values, read back to syntax. | +| **Read-back ("quotation" in NbE jargon)** | `Lvl → Value → Term`. Not the staging quote. | +| **Neutral** | Value stuck on a variable/meta, carrying a spine of pending eliminations. | +| **Closure** | Captured environment + unevaluated body; applied by environment extension. | +| **De Bruijn index / level** | Count from nearest binder (syntax) / from outermost (values). | +| **Zonk** | Inline solved metavariables into a term. | +| **Binding-time improvement** | Rewriting toward meta-level structure (e.g. `⇑(A→B)` → `⇑A→⇑B`) so more computes at staging time. | +| **Generativity** | Metaprograms can't inspect object terms; internalizable as an axiom (CFTT). | diff --git a/.opencode/skills/2ltt/kovacs-2022-icfp22-slides.md b/.opencode/skills/2ltt/kovacs-2022-icfp22-slides.md deleted file mode 100644 index 6e0f5137..00000000 --- a/.opencode/skills/2ltt/kovacs-2022-icfp22-slides.md +++ /dev/null @@ -1,143 +0,0 @@ -# Kovács (ICFP 2022 slides) — selected implementation notes (rules + Vec + inlining + inference) - -This document includes **only** the implementation-relevant material from the following slides: -- Rules of 2LTT -- map with inlining -- Inference for staging operations -- Staging types (Vec / Tuple3) -- map for Vec - -It’s intended as a compact companion to the fuller ICFP’22 paper notes in this skill. - ---- - -## 1) Rules of 2LTT (core calculus you must implement) - -1. **Two universes** `U0`, `U1`, closed under arbitrary type formers. - - `U0` is the universe of runtime (object-level) types. - - `U1` is the universe of compile-time (meta-level) types. - -2. **Stage separation:** all type/term formers and eliminators stay within the same universe. - -3. **Lifting:** for `A : U0`, we have `⇑A : U1`. - -4. **Quoting:** for `A : U0` and `t : A`, we have ` : ⇑A`. - -5. **Splicing:** for `t : ⇑A`, we have `∼t : A`. - -6. **Computation laws:** - - `<∼t> ≡ t` - - `∼ ≡ t` - -**Operational staging principle:** staging runs all metaprograms in splices and inserts their result in the code output. - ---- - -## 2) Example: `map` with inlining (staged higher-order programming) - -### Input -```text -inlMap : - {A B : ⇑U0} → - (⇑∼A → ⇑∼B) → - ⇑(List0 ∼A) → ⇑(List0 ∼B) - -inlMap = - λ f as. - ) bs) nil0 ∼as> - -f : List0 Nat0 → List0 Nat0 -f = λ xs. ∼(inlMap (λ n. <∼n + 2>) ) -``` - -### Output (after staging) -```text -f : List0 Nat0 → List0 Nat0 -f = λ xs. foldr0 (λ a bs. cons0 (a + 2) bs) nil0 xs -``` - -**Implementation check:** this exercises that you can (1) pass a meta-level function producing code, and (2) eliminate all splices by evaluating meta code, yielding pure object code. - ---- - -## 3) Inference for staging operations (reduce annotation burden) - -### 3.1 Definitional isomorphisms (negative types) -Lifting preserves negative types up to definitional isomorphism: - -```text -⇑ ⊤0 ≃ ⊤1 -⇑ ((a : A) → B a) ≃ ((a : ⇑A) → ⇑(B ∼a)) -⇑ ((a : A) × B a) ≃ ((a : ⇑A) × ⇑(B ∼a)) -``` - -### 3.2 Elaboration strategy suggested by the slides -Use: -- **bidirectional elaboration**, and -- **coercive subtyping along these isomorphisms** - -to infer most quotes/splices automatically. - -The slide’s “post-inference” presentation: - -```text -inlMap : {A B : ⇑U0} → (⇑A → ⇑B) → ⇑(List0 A) → ⇑(List0 B) -inlMap = λ f. foldr0 (λ a bs. cons0 (f a) bs) nil0 - -f : List0 Nat0 → List0 Nat0 -f = inlMap (λ n. n + 2) -``` - -**Implementation note:** a practical approach is: -- keep a core language with explicit `< >` / `∼`, -- elaborate from a surface language where many are implicit, -- insert coercions (or treat these isos as definitional equalities in conversion). - ---- - -## 4) Staging types: `Vec` computed at compile time, spliced into `U0` - -### Input -```text -Vec : Nat1 → ⇑U0 → ⇑U0 -Vec zero1 A = <⊤0> -Vec (suc1 n) A = <∼A × ∼(Vec n A)> - -Tuple3 : U0 → U0 -Tuple3 A = ∼(Vec 3 ) -``` - -### Output (after staging) -```text -Tuple3 : U0 → U0 -Tuple3 A = A × (A × (A × ⊤0)) -``` - -**Implementation check:** staging must normalize meta computation that produces *object types* (i.e. produce a splice-free `U0` type). - ---- - -## 5) `map` for staged `Vec` (dependent-ish staging across `Nat1`) - -### Input -```text -map : {A B : ⇑U0} → (n : Nat1) → (⇑∼A → ⇑∼B) - → ⇑(Vec n A) → ⇑(Vec n B) - -map zero1 f as = -map (suc1 n) f as = <(∼(f ), ∼(map n f ))> - -f : ∼(Vec 2 ) → ∼(Vec 2 ) -f xs = ∼(map 2 (λ x. <∼x + 2>) ) -``` - -### Output (after staging) -```text -f : Nat0 × (Nat0 × ⊤0) → Nat0 × (Nat0 × ⊤0) -f xs = (fst0 xs + 2, (fst0 (snd0 xs) + 2, tt0)) -``` - -**Implementation check:** this confirms that: -- meta recursion over `Nat1` expands the `Vec` shape, -- object projections (`fst0`, `snd0`) appear in the final object code, -- splices are fully eliminated. diff --git a/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md b/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md index 94f097bc..32f75824 100644 --- a/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md +++ b/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md @@ -1,129 +1,225 @@ -# Kovács 2022 — *Staged Compilation with Two-Level Type Theory* (substantive rewrite) - -This note rewrites the main implementation-relevant ideas. - -## 1. Core 2LTT idea for staging - -Two-level type theory provides: -- an **object theory** (runtime language) and -- a **meta theory** (compile-time language) - -with a disciplined interface that ensures meta computation can be fully executed away, producing a splice-free object program. - -### 1.1 Universes by stage -A common presentation is two universes: -- `U0` — object (runtime) types -- `U1` — meta (compile-time) types - -There can also be size levels, but staging is orthogonal to sizing. - -### 1.2 Stage-local type formers -Type formers typically exist separately at each stage. A guiding restriction: - -> introduction/elimination forms for a stage stay in that stage - -Examples: -- if `Nat0 : U0`, then recursion/induction on `Nat0` only produces terms in stage 0 -- meta recursion/induction produces meta terms - -This forces computation to be explicit and avoids "accidental" compile-time execution of runtime computation. - ---- - -## 2. The three primitives: lift/quote/splice - -The bridge between stages is not by ordinary functions, but by dedicated constructs: - -### 2.1 Lift (type former) -For `A : U0`, there is a meta type: -- `⇑A : U1` - -Interpretation: `⇑A` is "meta programs that produce object terms of type `A`". - -### 2.2 Quote (term former) -For `t : A` where `A : U0`: -- `⟨t⟩ : ⇑A` - -Quote is the trivial code producer: it returns `t` as code. - -### 2.3 Splice (term former) -For `u : ⇑A`: -- `∼u : A` - -Splice runs `u` during unstaging and inserts its produced object term into the surrounding object term. - -### 2.4 Computation rules -Quote and splice cancel definitionally: -- `∼⟨t⟩` computes to `t` -- `⟨∼u⟩` computes to `u` - -A practical compiler will implement these via evaluation/normalization of meta terms and/or definitional equality. - ---- - -## 3. What "staging"/"unstaging" computes - -Given a closed mixed-stage object term `t : A` at stage 0, unstaging: -- executes all meta computations inside splices -- replaces each splice by the computed object term -- produces a splice-free object term and type - -A key point: this applies to **types too** (unrestricted staging for types), so meta code can compute object types. - ---- - -## 4. Inlining control, partial evaluation, and why duplication happens - -Because lifted code `⇑A` is a meta value, using it multiple times duplicates code. - -This is useful for inlining, but can also duplicate runtime computations. - -A typical pitfall (also emphasized later in the 2024 paper): -- converting between `⇑(A×B)` and `⇑A×⇑B` can duplicate uses of the underlying code unless you insert a let. - -### 4.1 Let-insertion as an engineering requirement -A standard technique is to define meta-level combinators that generate object `let` bindings so the produced object code shares results. - -The paper discusses ad-hoc let insertion and notes that more systematic let insertion can be built meta-theoretically (e.g. with continuation-based codegen). - ---- - -## 5. Staging-by-evaluation (algorithmic blueprint) - -The paper presents an algorithmic view: -- staging is "like normalization-by-evaluation" -- instead of reducing syntax directly, you interpret terms in a semantic domain where staging happens "by running the interpreter" - -### 5.1 Soundness / stability / strictness (properties) -The paper identifies three desirable properties of a staging algorithm: - -- **Soundness**: embedding the staged output recovers the original (up to conversion) -- **Stability**: staging an already object-level term is the identity (up to conversion) -- **Strictness**: staging preserves constructors strictly (not merely propositionally) - -In implementation terms: -- you want `unstage(embed(obj)) == obj` -- and `embed(unstage(mixed))` converts back to `mixed` - -### 5.2 Why the presheaf perspective matters (implementation takeaway) -To unstage open terms that depend on object variables, the semantic domain must support: -- object-variable dependency -- substitution/weakening stability ("naturality") - -Implementation translation: -- treat object vars as neutrals -- meta evaluation may produce code that mentions those neutrals -- unstaging should commute with object substitution - ---- - -## 6. Limits: intensional code analysis clashes with stability - -The paper explains that if the meta language can *inspect* object code (e.g. decide definitional equality of two quoted boolean expressions), that generally breaks the substitution stability/naturality constraints that make the standard semantics work cleanly. - -Implementation takeaway: -- if you want the clean semantic story and robust unstaging, keep object code opaque: - only build it (quote), compose it (meta functions), and run it (splice), - but do not pattern match on its structure in the meta language. - -(If you *do* want inspection, you'll need a different setup and should expect trade-offs.) \ No newline at end of file +# Kovács 2022 — *Staged Compilation with Two-Level Type Theory* (implementation-oriented rewrite) + +Faithful summary of the implementation-relevant content, checked against the paper's +LaTeX source. Section references are to the paper. + +## 1. The system (§2) + +### 1.1 Universes +Universes `U_{i,j}` with stage `i ∈ {0,1}` and size `j ∈ ℕ`: +- `U0` — object-level (runtime) types. Every closed `A : U0` stages to a type of the + object language. +- `U1` — meta-level (compile-time) types. Guaranteed to be computed away by staging. + +Sizing (`j`) is orthogonal to staging. The surface syntax uses Russell-style universes; +the formal core uses **Coquand-style universes** (`U`, `El`, `Code` with `El ∘ Code = id`), +which elaboration inserts. There is no cumulativity; `NatElim` may eliminate from level `j` +into any level `k`. + +### 1.2 Stage separation +Both universes may be closed under arbitrary type formers (Π, Σ, Id, inductives), but +**every type former, constructor and eliminator stays within one stage**: +- function domain and codomain are at the same stage; +- recursion/induction on `Nat0` can only target types in `U0`, meta recursion targets `U1`. + +The two stages need not have the *same* type formers — see §5 below (variations). + +### 1.3 The staging operations +None of these are expressible as functions (functions can't cross stages): +- **Lifting**: `A : U0` gives `⇑A : U1` — the type of metaprograms computing runtime + expressions of type `A`. +- **Quoting**: `t : A : U0` gives `⟨t⟩ : ⇑A` — the metaprogram immediately returning `t`. +- **Splicing**: `t : ⇑A` gives `∼t : A` — during staging, the metaprogram runs and its + result is inserted into the output. Splice binds tighter than application: `∼f x ≡ (∼f) x`. +- **Definitional inverses**: `∼⟨t⟩ = t` and `⟨∼t⟩ = t`. Formally, quote is an *invertible + natural transformation* `Tm0 Γ A → Tm1 Γ (⇑A)`. + +Note the stage index convention: `0` is runtime because a multi-level generalization would +lift `U_i` to `U_{i+1}` with a bottom-most object theory. + +### 1.4 Contrast with MetaML / typed Template Haskell +Those systems have `Code A` where `A` and `Code A` live in the same universe of types, so +binder stages need extra scope-based disambiguation (e.g. TH top-level binders act as runtime +or static depending on quoting context). In 2LTT the stage of everything is enforced *purely +by typing* — no syntactic or scope-based restrictions. 2LTT is also the first system with +unrestricted staging *for types* (types computed by metaprograms), enabled by meta-level +dependent types + large elimination. + +## 2. Programming patterns (§2.2–2.3) + +- `id1 : (A : U1) → A → A` computes at compile time; applied to runtime data via + `∼(id1 (⇑Bool0) ⟨true0⟩)`. +- `id⇑ : (A : ⇑U0) → ⇑∼A → ⇑∼A` — quantify over `⇑U0` (code of runtime types) when the + type must be used at the object level, e.g. as a parameter of `List0 : U0 → U0`. + There is no generic map from `U1` to `U0`, so `⇑U0`-quantification is the way to + abstract over runtime types in meta code. +- Inlined map: + `map : (A B : ⇑U0) → (⇑∼A → ⇑∼B) → ⇑(List0 ∼A) → ⇑(List0 ∼B)` + implemented with `foldr0` under a quote; the meta function argument is inlined at + each use site during staging. +- Compile-time recursion: `exp : Nat1 → ⇑Nat0 → ⇑Nat0` via `iter1`; + `∼(exp 3 ⟨n⟩)` stages to `n *0 n *0 n *0 1`. +- **Staging types**: `Vec : Nat1 → ⇑U0 → ⇑U0` by meta-iteration produces nested pairs; + `∼(Vec 3 ⟨Nat0⟩)` stages to `Nat0 × (Nat0 × (Nat0 × ⊤0))`. `map` over such vectors uses + induction on `Nat1` and stages to fully unrolled projections. +- **Let-insertion** (ad hoc): bind a runtime expression with an object-level `let` and pass + code of the *variable* into the metaprogram, so only the variable is duplicated. +- **Partially static data / partial evaluators**: a well-typed interpreter for an embedded + language becomes a partial evaluator; e.g. `EvalTy : Ty → ⇑U0`, + `EvalCon : Con → U1` (a *static* list storing *runtime* expressions), + `EvalTm : Tm Γ A → EvalCon Γ → ⇑∼(EvalTy A)`; environment lookups are fully + eliminated in the output. + +## 3. Lifting properties, binding-time improvement, inference (§2.3) + +### 3.1 Preservation of negative type formers +`⇑` has no computation rules but preserves negative type formers up to **definitional +isomorphism**: + +``` +⇑((x : A) → B x) ≃ ((x : ⇑A) → ⇑(B ∼x)) pres→ f := λ x. ⟨∼f ∼x⟩ ; pres→⁻¹ f := ⟨λ x. ∼(f ⟨x⟩)⟩ +⇑((x : A) × B x) ≃ ((x : ⇑A) × ⇑(B ∼x)) +⇑⊤0 ≃ ⊤1 +``` + +Rewriting left-to-right is **binding-time improvement**: the improved form supports more +compile-time computation (meta λ instead of runtime λ). Going right-to-left introduces a +runtime binder — occasionally desirable to limit code size (like let-insertion). +The unimproved `id⇑ : (A : ⇑U0) → ⇑(∼A → ∼A)` stages to a useless β-redex +`(λ x. x) true0` — improved forms are the sensible default. + +### 3.2 Positive types: serialization, cofibrancy, "the trick" +Inductive types are only preserved in one direction: `Bool1 → ⇑Bool0` exists +("serialization"); the other direction admits only constant functions (no elimination for +`⇑A` — code cannot be inspected). There is *no* map `(Nat1 → Nat1) → ⇑(Nat0 → Nat0)`. +But if `A : U1` is **finite** and `B` serializable, `A → B` is serializable (it's a finite +product) — `A` is called *cofibrant* in 2LTT jargon. This is the 2LTT form of the partial +evaluation "trick" (η-expanding functions out of finite sums). Fusion (foldr/build via +Böhm–Berarducci encoding, stream fusion via colists) is binding-time improvement for +general inductive types. + +### 3.3 Inferring quotes and splices +Extract a **coercive subtyping** system used during bidirectional elaboration: +- `A ≤ ⇑A` (insert quote) and `⇑A ≤ A` (insert splice); +- contravariant–covariant rule for functions, covariant for Σ; +- optionally `U0 ≤ U1`, witnessed by `Lift` itself (a *type* coercion). + +When comparing inferred vs. expected type, insert coercions. With this plus Agda-style +implicits + pattern unification, `map` can be written with no quotes/splices at all. +Where the elaborator must choose between improved/unimproved types, default to +**improved**, with explicit lifting to opt out. (See `demo-implementation.md` for the +actual algorithm, including coercion avoidance.) + +## 4. Staging: definition, algorithm, correctness (§3–5) + +### 4.1 What staging is (Def. 3.1) +Staging maps 2LTT types/terms *in purely object-level contexts* to object-theory +types/terms: + +``` +Stage : Ty0,j ⌜Γ⌝ → TyO,j Γ Stage : Tm0,j ⌜Γ⌝ A → TmO,j Γ (Stage A) +``` + +where `⌜–⌝` embeds object syntax into 2LTT. Properties: +- **Soundness**: `⌜Stage A⌝ = A` (up to conversion) — staging output is convertible to input. +- **Stability**: `Stage ⌜A⌝ = A` — staging is identity on splice-free terms. +- **Strictness**: the extracted algorithm preserves all type/term formers *strictly* — + staging performs **no object-level β-reduction**. (Full normalization of 2LTT would be a + sound+stable staging algorithm, but useless: no inlining control.) + +Soundness + stability = embedding is a bijection up to conversion = **strong +conservativity** of 2LTT over the object theory. + +Important distinction: strictness constrains the *staging output*, not definitional +equality. In this paper's 2LTT the object theory is full MLTT (Π with β/η, NatElim +β-rules), so *conversion checking during elaboration* does compute object-level redexes. +(Making object conversion weak is a separate design choice — see CFTT 2024.) + +### 4.2 Staging-by-evaluation +Staging = evaluation of 2LTT syntax in the **presheaf model over the object theory's +syntactic category** (analogous to NbE). Intuition: +- Presheaves are "sets varying over object contexts"; the interpreter's semantic values may + embed object-level types/terms that depend on their context. +- Meta-level types get standard semantic interpretations (`Nat1` ↦ ℕ, `Σ1` ↦ pairs, + functions ↦ Kripke-style functions abstracting over context extensions). +- Object-level `Ty0`/`Tm0` are interpreted by *syntactic* object types/terms: + `|A| : env → TyO Δ`, `|t| : (γ : env) → TmO Δ (|A| γ)`. +- `⇑A` is interpreted as `TmO[A]` — so quote and splice are **identity functions in the + model**. Their cost is zero; all real work is meta-level computation. +- Open staging: interpret a purely-object context `Γ` by the **generic environment** + `Γᴾ` = the list of `Γ`'s variables (≅ identity substitution). Stability falls out of this. + +Everything in the model must be **stable under object substitution** (natural). This is the +core trade-off: metaprograms cannot observe things not preserved by substitution (e.g. +scope sizes, structure of code) — in exchange, implementations never need to track +object contexts/substitutions explicitly. + +### 4.3 Extracted algorithm & optimizations (§3.4) +The naively extracted algorithm weakens semantic environments when going under object +binders (`γ[p]`) — potentially deep traversals. Standard fixes, used in the demo: +- **De Bruijn levels in the semantic domain** (weakening becomes free); indices in syntax. +- Closures in object-level binders; drop explicit substitutions from the core syntax. +- Untyped, tagged representation of semantic values (separate constructors for functions, + literals, quoted expressions). +- Meta evaluation is closed (no free meta variables at staging time) and syntax-directed. + **Meta-level types are erased during staging** (evaluated to a dummy value): they never + appear in the output. Object-level types are staged for real, since they do appear in + the output. +- **Caching/deduplication** of generated code (e.g. reusing specializations of `map` at the + same arguments) is future work in the paper — a production system needs it. + +### 4.4 Soundness proof shape (§5, skimmable) +Proof-relevant logical relation between the evaluation morphism and a *restriction* +morphism (2LTT syntax restricted to object contexts), defined internally to the presheaf +category. Only relevant if you want to port the correctness argument. + +## 5. Variations of the object language (§2.5) — directly relevant to low-level targets + +Restricting the object language makes it easier to compile; the meta level compensates. + +### 5.1 Monomorphization +Object language is **simply typed** (every runtime type statically known — easy layout +and codegen): +- a judgment `A type0` for well-formed runtime types (closed under simple type formers); +- a meta-level type `Ty0 : U1` *replacing* `⇑U0`; +- for each `A type0`, `⇑A : Ty0`; quoting sends types `A type0` to `⟨A⟩ : Ty0` and terms + `t : A` to `⟨t⟩ : ⇑A`. + +2LTT still supports arbitrary higher-rank polymorphism over `Ty0` at compile time, e.g. +`((A : Ty0) → ⇑∼A → ⇑∼A) → ⇑Bool0` — it just must be staged away. The user-facing +restriction: **polymorphic functions cannot be stored inside runtime data**. + +### 5.2 Memory-representation polymorphism +Refinement: internalize representations as a meta type and index runtime types by them: +- `Rep : U1` with e.g. `Ref : Rep`, `Prod : Rep → Rep → Rep`, primitive machine reps; +- `U_{0,j} : Rep → U_{0,j+1} r` — runtime universes indexed by representation; +- unboxed Σ: for `A : U0 r`, `B : A → U0 r'`, `(x : A) × B x : U0 (Prod r r')` — + type dependency without representation dependency. + +`Rep` is meta-level, so it cannot be abstracted over at runtime; staging computes all +`Rep` indices to canonical representations. This reconciles dependent types with memory +layout control. (Compare *Kinds Are Calling Conventions* for a much richer treatment of +the same axis — see `downen-2020-kinds-are-calling-conventions.md`.) + +## 6. Intensional analysis (§6) + +Analyzing the structure of `⇑A` values clashes with the standard semantics: +- Purely-object contexts are **representable** presheaves, so by the Yoneda lemma a + meta-level function out of `⇑Bool0` has at most as many behaviors as `Bool` has + elements — `decEq : (x y : ⇑Bool0) → (x =1 y) +1 (x ≠1 y)` cannot actually decide + definitional equality. More directly: definitional *inequality* is not stable under + substitution (unequal variables can be mapped to equal terms). + +Two workable alternative setups, with trade-offs: +1. **Stability under weakenings only**: take only weakenings as base-category morphisms. + Many analyses (including `decEq`, term strengthening/let-floating) are weakening-stable. + Cost: without substitution in the object theory you cannot specify dependent or + polymorphic object types (no dependent elimination / instantiation). Works fine for the + monomorphization setup of §5.1. +2. **Closed modality**: a modality for *closed* object terms; closed terms are unaffected + by substitution, so they can be analyzed (and safely `run`, MetaOCaml-style). C-like + function pointers are a natural use case (closed after staging). + +Default guidance stands: keep object code opaque — build (quote), compose (meta +functions), insert (splice) — unless you deliberately adopt one of the above setups. +The 2024 paper turns this opacity into a *feature* (generativity axiom). diff --git a/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md b/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md index 1654612f..2d26c07c 100644 --- a/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md +++ b/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md @@ -1,154 +1,218 @@ -# Kovács 2024 — *Closure-Free Functional Programming in a Two-Level Type Theory* (substantive rewrite) - -This note rewrites the implementation-relevant parts of the 2024 system ("CFTT" in the paper). - -## 1. Goal: staged compilation that eliminates abstraction overhead - -The paper's theme: -- instead of relying on heavy optimizer passes, use staged metaprogramming to *compute away* abstraction layers (e.g. monads/transformers, stream fusion machinery), -- while producing object code that is well-typed and (in the presented object language) does not require dynamic closures. - ---- - -## 2. Meta language vs object language - -### 2.1 MetaTy (compile time) -MetaTy is a dependent type theory with: -- dependent functions, Σ-types -- indexed inductive types - -This is where you implement libraries (monads, codegen, fusion) so they execute during unstaging. - -### 2.2 Ty (object types) as a meta-level entity -The object type universe `Ty` lives as a meta type (`Ty : MetaTy`), i.e. object types are "data" at compile time but remain opaque in ways that preserve staged semantics. - ---- - -## 3. Splitting object types: ValTy vs CompTy (closure-free core) - -The object universe is split into sub-universes: - -### 3.1 ValTy (value types) -- used for runtime-storable values -- supports algebraic data types (parameters may be general, but constructor fields are restricted to ValTy) -- `ValTy ⊆ Ty` - -### 3.2 CompTy (computation types) -- used for computations that must not be stored as values -- contains (at least) function types, with restrictions that support closure-free execution -- `CompTy ⊆ Ty` - -### 3.3 The key restriction that buys "no dynamic closures" -Functions (computations) cannot be: -- stored in data constructors -- passed as ordinary value arguments -- returned as values that escape scope - -The runtime semantics can treat computations as call-by-name-ish in a controlled way, because they cannot be duplicated arbitrarily as first-class values. - -Implementation note: -- the paper allows fairly liberal syntax (e.g. lambdas under case/let), but relies on a compilation step (call saturation / restructuring) to ensure calls become saturated in a way that avoids closures. - ---- - -## 4. Object-level definitional equality is intentionally minimal - -To keep typechecking and unstaging simple when object programs are embedded in a dependent meta system, object definitional equality is set up without: -- β/η rules for object functions -- let unfolding - -Implementation takeaway: -- treat object terms as *code*, not as something you compute during typechecking. - ---- - -## 5. Lift/quote/splice in CFTT - -The bridge primitives are the same as in 2LTT: - -- `⇑A : MetaTy` for `A : Ty` -- `⟨t⟩ : ⇑A` for `t : A` -- `∼u : A` for `u : ⇑A` - -This yields *unstaging*: evaluate meta-level computation in splices and produce object code. - ---- - -## 6. Binding-time improvements ("up/down") as library patterns - -A recurring technique is to convert between: -- `⇑(A → B)` and `⇑A → ⇑B` -- and similarly for products, etc. - -These conversions enable more compile-time computation by moving structure to the meta level. - -Example pattern (functions): -- `up : ⇑(A → B) → ⇑A → ⇑B` -- `down : (⇑A → ⇑B) → ⇑(A → B)` - -Engineering warning: -- these conversions can duplicate uses of code, so without care they can duplicate runtime computations. -- thus, you need let insertion / sharing (next section). - ---- - -## 7. Let-insertion via a code generation monad (Gen) - -To avoid duplication, the paper introduces a meta-level codegen facility (`Gen`) that generates object `let`/`letrec`. - -Key operations (paraphrased into implementable intent): - -- `gen : ⇑A -> Gen (⇑A)` - - run the code `a`, bind it to an object-level `let x := ...`, and return code for `x` - -- `genRec : (⇑A -> ⇑A) -> Gen (⇑A)` for computation types - - generate object-level `letrec x := ...` for recursive computations - -Running `Gen` yields code containing a sequence of lets with sharing. - -Implementation note: -- a CPS representation of `Gen` is typical: - it makes it easy to "emit lets" before continuing. - ---- - -## 8. Monads & monad transformers: "Improve" class - -The paper's library strategy: -- keep "real monads" at the meta level (so binds compute at unstaging time) -- convert object structures into meta monads and back when needed - -This is packaged as a typeclass-like interface (conceptually): - -- `up : ⇑(F A) -> M (⇑A)` -- `down : M (⇑A) -> ⇑(F A)` - -where: -- `F : ValTy -> Ty` is an object-level effect encoding -- `M : MetaTy -> MetaTy` is a meta-level monad (or monad transformer stack) -- using `up/down`, the meta-level monadic structure disappears during unstaging, leaving efficient object code - -The paper works through examples like MaybeT/StateT/ReaderT in this style. - ---- - -## 9. "No intensional analysis" + generativity (and why it matters) - -A notable theme: -- the system benefits from the inability to inspect quoted object terms structurally. -- this "opacity" gives a parametricity-like payoff and supports an axiom ("generativity") that is validated in the staged semantics model used. - -Implementation takeaway: -- if you implement `⇑A` as an opaque code type with only quote/splice/combinators, you naturally enforce the "no inspection" discipline. -- if you embed into a system like Template Haskell where you can inspect ASTs, the generativity principle fails; the paper discusses workarounds involving runtime-checked coercions that disappear if users respect the discipline. - ---- - -## 10. Engineering summary: what to copy into your compiler/prototype - -Minimum to reproduce the paper's practical benefits: -1. Two-stage calculus with `⇑/⟨⟩/∼` -2. Strong meta evaluation; weak object definitional equality -3. Let-insertion API (`Gen`) for sharing -4. Optional: closure-free object typing discipline (`ValTy`/`CompTy`) -5. Library patterns for binding-time improvements (`up/down`) and effect abstraction elimination +# Kovács 2024 — *Closure-Free Functional Programming in a Two-Level Type Theory* (implementation-oriented rewrite) + +Checked against the paper's LaTeX source. The system is called **CFTT** ("closure-free +type theory"). This file only covers what CFTT *adds or changes* relative to the 2022 +2LTT — for the shared core (lift/quote/splice rules, staging-by-evaluation, +soundness/stability/strictness, binding-time improvement, inference) see +`kovacs-2022-staged-compilation-2ltt.md`. + +Terminology: this paper says **unstaging** for what the 2022 paper calls "staging" +(running metaprograms in splices to extract object code). Same thing. + +## 1. What changes vs. 2022 + +| | 2022 2LTT | 2024 CFTT | +|---|---|---| +| Object language | full dependent MLTT | **simply-typed, first-order**, general recursion, finitary ADTs | +| Object definitional equality | full β/η | **none** (no β, no η, no let-unfolding) | +| Object universe | `U0`, a stage-0 universe | `Ty : MetaTy` — object types are meta-level *data*, split into `ValTy`/`CompTy` | +| Meta language | MLTT | MLTT + indexed inductive families (via W-types) + identity type | +| Closures at runtime | possible | **guaranteed absent** | + +Goal: shift work from general-purpose optimizers to metaprograms; get *guarantees* that +abstraction (monads, transformers, fusion) is eliminated at staging time. + +## 2. The object language + +### 2.1 ValTy / CompTy +`Ty : MetaTy`, with two sub-universes (formally Tarski-style with explicit inclusions +`V : ValTy → Ty`, `C : CompTy → Ty`; surface syntax uses implicit coercion): + +- **`ValTy`** — value types: runtime-storable, call-by-value. Supports parameterized ADTs; + parameters may have arbitrary types but **all constructor fields must be in `ValTy`**. +- **`CompTy`** — computation types: call-by-name, *not* storable. Contains: + - functions `_→_ : ValTy → Ty → CompTy` — domain must be a value type, codomain + arbitrary (so `Bool → Bool → Bool` is fine, `(Bool → Bool) → Bool` is ill-formed); + - **finite products of computations**: `() : CompTy`, `(_,_) : CompTy → CompTy → CompTy` + with pairing/projections. These exist to express **mutually recursive** function + blocks: a `letrec` at type `(A → B, A → B)` compiles to a pair of mutual functions. + +Since object types are meta-level terms, **object types never depend on object terms** +(no runtime type dependency) — a key invariant used by generativity (§6). + +### 2.2 Binders and recursion +- `let x : A := t; u` — non-recursive, any type, allows shadowing. Object-level + definitions use `:=`, meta-level use `=` (stages of definitions are always explicit). +- `letrec x : A := t; u` — **computations only** (only functions/computation products can + be recursive). General recursion, no termination checking. +- λ-abstractions are allowed under `case` branches and `let` bodies (liberal syntax chosen + deliberately: unrestricted `let`-insertion into any position is what makes + metaprogramming convenient). + +### 2.3 Why no closures are needed +Computations cannot be stored in constructors, passed as (value) arguments, or escape +their scope. With call-by-name semantics for computations, every program can be +transformed so that **every call is saturated** (`f t1 … tn` where `f`'s definition +immediately λ-binds `n` args) — e.g. `case b of True → λx.x+10; False → λx.x*10` +transforms to `λb x. case b of …`. Local functions then compile to lambda-lifted +top-level functions or join points. The call-saturation translation is formalized (per +step) in the paper's Agda supplement; CBN for computations causes no significant work +duplication *because* computations can't be duplicated as first-class values. + +Contrast CBPV: similar value/computation split, but CBPV only binds value variables +(functions must be thunked into values to be let-bound) — unusable here. Contrast +defunctionalization: that makes closures *transparent* (constructor + dispatch) but does +not remove dynamic control flow; unstaging instead runs higher-order metaprograms that +never put functions in the output. + +### 2.4 Object definitional equality: none +No β, no η, no let-unfolding for object programs, because: +- code size/efficiency are the point of staging, and they are **not stable under + βη-conversion or let-unfolding**; +- with general recursion there is no decidable, sensible program equivalence anyway. + +Typechecking compares object code essentially syntactically (this is the "weak object +equality" option; the 2022-style full-MLTT object theory is the other end of the +spectrum). Consequence: `up`/`down` (below) cannot be proven inverse internally — that's +expected and fine. + +## 3. The code generation monad `Gen` + +Binding-time improvement `up : ⇑(A,B) → (⇑A, ⇑B)` duplicates its argument — code +duplication and repeated runtime work. Let-insertion is impossible in a plain meta +function (can't introduce object binders from `MetaTy`). Fix: CPS code generators +(Bondorf-style), packaged as a monad: + +``` +newtype Gen (A : MetaTy) = Gen { unGen : {R : Ty} → (A → ⇑R) → ⇑R } + +return a = Gen λk. k a +ga >>= f = Gen λk. unGen ga (λa. unGen (f a) k) + +runGen : Gen (⇑A) → ⇑A runGen ma = unGen ma id + +gen : {A : Ty} → ⇑A → Gen (⇑A) -- let-insertion +gen a = Gen λk. ⟨let x : A := ∼a; ∼(k ⟨x⟩)⟩ + +genRec : {A : CompTy} → (⇑A → ⇑A) → Gen (⇑A) -- letrec-insertion +genRec f = Gen λk. ⟨letrec x : A := ∼(f ⟨x⟩); ∼(k ⟨x⟩)⟩ +``` + +The **answer type `R` is polymorphic** (a deliberate improvement over prior art with a +fixed answer-type parameter): generators need not anticipate the output type. +`gen` returns code that is a *variable*, so reuse is free. Don't write everything in +`Gen` reflexively — implicit emission makes generated-code size harder to reason about +(analogy: `IO` in Haskell). + +## 4. The monad-transformer library pattern + +Strategy: keep *real* monads at the meta level (their binds compute at unstaging time); +convert to/from object-level effect encodings only at runtime boundaries. + +``` +class Monad M => MonadGen M where liftGen : Gen A → M A + -- gen/genRec generalize to any MonadGen + +class MonadGen M => Improve (F : ValTy → Ty) (M : MetaTy → MetaTy) where + up : {A : ValTy} → ⇑(F A) → M (⇑A) -- object action → meta action + down : {A : ValTy} → M (⇑A) → ⇑(F A) -- meta action → object code +``` + +- Base case: `Improve Identity Gen`. +- Compositional: `Improve F M => Improve (MaybeT F) (MaybeTₘ M)`, similarly + `StateT S` (with `S : ValTy`, improved as `StateTₘ (⇑S) M`) and `ReaderT`. + Meta side reuses standard `mtl` definitions unchanged. `ContT` is the one transformer + that cannot be improved (needs real closures). +- Object-level recursive calls inside monadic code: just wrap in `up ⟨f ∼x⟩`. +- `modify`/`put`/`local` naively substitute *expressions* for the state (inline-style, + duplicating work); define strict variants that `gen`-bind first, e.g. + `put' s = do {s ← gen s; put s; return ⟨()⟩}`. + +### 4.1 Case splitting on object values ("the trick", monadic form) +Cannot eliminate `⇑A` into `MetaTy` directly; instead *generate* an object `case` whose +branches continue code generation: + +``` +data SplitList A = Nil' | Cons' (⇑A) (⇑(List A)) +split : ⇑(List A) → Gen (SplitList A) +split as = Gen λk. ⟨case ∼as of Nil → ∼(k Nil'); Cons a as → ∼(k (Cons' ⟨a⟩ ⟨as⟩))⟩ +``` + +Generalized as a class `Split (A : ValTy) { SplitTo : MetaTy; split : ⇑A → Gen SplitTo }`. +A native implementation would elaborate `case` on object values in do-notation to `split`. + +### 4.2 Join points (`MonadJoin`) — avoiding exponential code size +Monadic bind after a `split` continues generation *in each branch*: sequential Boolean +cases ⇒ exponential blowup. Naive fix (`gen` the branchy action via `down`/`up`) forces +runtime constructors + re-matching. Better: **join points** — let-bind one continuation +per constructor of the result, fusing away the constructors: + +- `USOP = List (List ValTy)` — a Tarski universe of **sums of products** of value types, + with decoding `El_SOP : USOP → MetaTy`; closed under value types, finite sums, finite + products (products taken at the *meta* level, so they keep β/η — this is why SOP, not + plain finite sums). +- `class IsSOP (A : MetaTy) { Rep : USOP; rep : A ≃ El_SOP Rep }` (isomorphism with + proofs). Conjectured to coincide with the *cofibrant* types of 2LTT. +- `Fun_SOP : USOP → Ty → CompTy` tabulates `El_SOP A → ⇑R` as a computation product of + first-order functions; `tabulate`/`index` convert back and forth; `letrec` over it + yields mutually recursive functions. +- `class Monad M => MonadJoin M { join : IsSOP A => M A → M A }`; the `Gen` instance + tabulates the continuation, `gen`-binds every join point, then dispatches. Transformer + instances just delegate (StateT additionally needs `IsSOP S`). + +Rule of thumb: `join` every object-level case with ≥2 branches (dead join points are +trivial downstream cleanup); skip it when a branch short-circuits at the meta level +(e.g. `fail` in `MaybeT`). + +## 5. Pull-stream fusion (dependent types earning their keep) + +``` +data Step S A = Stop | Skip S | Yield A S +data Pull A where + Pull : (S : MetaTy) → IsSOP S ⇒ Gen S → (S → Gen (Step S A)) → Pull A +``` + +Machine states are meta-level SOP data; `foldr` tabulates the transition function into a +`letrec`-bound computation product of **mutually recursive** functions (one per state +shape), and e.g. `foldl` derived from `foldr` produces tail-recursive accumulator code +with no closures. Combinators (`zip`-style applicative, `<>`, `filter`, `take`…) are the +standard Coutts-style definitions plus `Gen`/`IsSOP` noise. + +`concatMap : IsSOP A ⇒ (A → Pull B) → Pull A → Pull B` needs the inner machine state +`Σ A (projS ∘ f)` to be SOP — i.e. **`USOP` closed under Σ** — which needs generativity: + +## 6. Generativity: exploiting the *absence* of intensional analysis + +**Axiom.** For `f : El_P A → USOP` (domain: finite products of object terms; codomain: a +"constant" metatype) and any `x y`, `f x = f y` — such functions are constant. Justified +in the presheaf model by Yoneda: products of object terms form a representable presheaf, +`USOP` a constant one, so natural transformations between them are constant. It reflects +that metaprograms cannot inspect object *terms* (inspecting object *types* would be +consistent, though). + +Used to define `Σ_SOP`: instantiate the family at arbitrary inhabitants (products of +`letrec x := x` loops) — generativity says the choice doesn't matter — then concatenate +`A_i × B(inject_i loop)` per summand. With β/η for meta products, this gives +pairing/projections and the `IsSOP (Σ A B)` instance. + +**Soundness up to erasure**: axioms block computation, so unstaging first *erases all +identity proofs and transports* (a syntactic translation into CFTT + equality +reflection), then evaluates. Soundness of unstaging holds up to this erasure; strictness +is trivial (no object conversion rules); stability as in 2022. Implementation notes: the +Agda embedding uses `primTrustMe` to erase the axiom; in typed Template Haskell +generativity is *false* (quotes can be inspected), so runtime-checked coercions are used +which vanish if users respect the discipline. + +## 7. Practical notes + +- Quote/splice/`up`/`down` noise is expected to be almost fully inferable with + bidirectional elaboration + the subtyping of the 2022 demo, *given* explicit stages on + let-definitions. +- Closure-freedom costs surprisingly little; a real language would add an opt-in closure + type former (`CompTy → ValTy` boxing) and keep both, plus push streams (a proper + monad, bottom of transformer stacks) alongside pull streams (top of stacks). +- Downstream compiler still wants: dead code elimination, unused-arg removal, + de-duplication of generated code. +- The object language is close to a simply-typed fragment of the KACC intermediate + language (see `downen-2020-kinds-are-calling-conventions.md`): function types distinct + from closure types, universal η, explicit arity — KACC lacks only `letrec`. From cabd2a6aec4c5c20589c172814887bf417a4ae97 Mon Sep 17 00:00:00 2001 From: LukasK Date: Thu, 23 Jul 2026 14:21:53 +0000 Subject: [PATCH 2/4] ai: address 2ltt skill review (glossary, wording, cross-links) - Extract the glossary from implementation-guide.md into glossary.md and list it in SKILL.md for visibility (#3614753068). - Reword "memorialize" to "record" in the Downen notes (#3637774438). - Turn bare backtick .md cross-references into clickable markdown links across all skill files (#3638642647). Co-Authored-By: Claude Opus 4.8 --- .opencode/skills/2ltt/CREDITS.md | 4 +- .opencode/skills/2ltt/SKILL.md | 17 +++++---- .opencode/skills/2ltt/demo-implementation.md | 6 +-- ...wnen-2020-kinds-are-calling-conventions.md | 6 +-- .opencode/skills/2ltt/glossary.md | 21 +++++++++++ .opencode/skills/2ltt/implementation-guide.md | 37 +++++-------------- .../kovacs-2022-staged-compilation-2ltt.md | 4 +- .../2ltt/kovacs-2024-closure-free-2ltt.md | 4 +- 8 files changed, 52 insertions(+), 47 deletions(-) create mode 100644 .opencode/skills/2ltt/glossary.md diff --git a/.opencode/skills/2ltt/CREDITS.md b/.opencode/skills/2ltt/CREDITS.md index 941a6a3a..9783458e 100644 --- a/.opencode/skills/2ltt/CREDITS.md +++ b/.opencode/skills/2ltt/CREDITS.md @@ -28,13 +28,13 @@ This skill is derived from (and intended to be read alongside) the following sou *ICFP 2022 presentation slides: Staged Compilation with Two-Level Type Theory.* Presented 12 September 2022, ICFP Ljubljana. https://github.com/AndrasKovacs/staged/blob/main/icfp22prez/ICFP-Kov%C3%A1cs-StagedCompilationwithTwoLevelTypeTheory.pdf - (Content folded into `kovacs-2022-staged-compilation-2ltt.md`; no separate notes file.) + (Content folded into [`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md); no separate notes file.) ## Reference implementations 5. András Kovács. *staged* — demo implementation, paper sources, Agda embeddings. https://github.com/AndrasKovacs/staged - (The `demo/` directory and its `README.md` are the basis of `demo-implementation.md`.) + (The `demo/` directory and its `README.md` are the basis of [`demo-implementation.md`](demo-implementation.md).) 6. András Kovács. *elaboration-zoo* — minimal NbE / bidirectional elaboration references (see branch `01-eval-closures-debruijn` and later branches for diff --git a/.opencode/skills/2ltt/SKILL.md b/.opencode/skills/2ltt/SKILL.md index cafcbf51..e1d41771 100644 --- a/.opencode/skills/2ltt/SKILL.md +++ b/.opencode/skills/2ltt/SKILL.md @@ -13,30 +13,33 @@ and the staging algorithm that runs metaprograms to produce splice-free object c ## Files (each owns its topic; minimal overlap) -1. **`implementation-guide.md`** — start here. Pipeline architecture, the up-front +1. **[`implementation-guide.md`](implementation-guide.md)** — start here. Pipeline architecture, the up-front design decisions (object-equality strength, stage repair vs. reject), NbE core, - elaboration guardrails, staging-pass essentials, pitfalls checklist, glossary. + elaboration guardrails, staging-pass essentials, pitfalls checklist. -2. **`demo-implementation.md`** — code-level walkthrough of the reference Haskell +2. **[`demo-implementation.md`](demo-implementation.md)** — code-level walkthrough of the reference Haskell implementation (https://github.com/AndrasKovacs/staged): core syntax, conversion evaluator with stuck splices, two-domain staging evaluator, coercive-subtyping elaboration, unification extensions, what to copy vs. reconsider. -3. **`kovacs-2022-staged-compilation-2ltt.md`** — the core theory (*Staged Compilation +3. **[`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md)** — the core theory (*Staged Compilation with Two-Level Type Theory*): rules, programming patterns, binding-time improvement and inference, staging-by-evaluation with soundness/stability/strictness, object-language variations (monomorphization, representation polymorphism), intensional-analysis options. Also covers the ICFP'22 slides' examples. -4. **`kovacs-2024-closure-free-2ltt.md`** — the CFTT deltas (*Closure-Free Functional +4. **[`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md)** — the CFTT deltas (*Closure-Free Functional Programming in a 2LTT*): first-order object language with `ValTy`/`CompTy`, weak object equality, `Gen`/let-insertion, `Improve` monad library, join points + SOP, stream fusion, generativity axiom. -5. **`downen-2020-kinds-are-calling-conventions.md`** — optional layout/arity control: +5. **[`downen-2020-kinds-are-calling-conventions.md`](downen-2020-kinds-are-calling-conventions.md)** — optional layout/arity control: `TYPE ρ ν` kinds, levity, `mono-rep`/`mono-conv` restrictions, closure boxing, lowering to machine language; how it composes with a 2LTT. +6. **[`glossary.md`](glossary.md)** — shared terminology (stage, lift/quote/splice, + NbE, read-back, neutral, closure, zonk, binding-time improvement, generativity). + ## When to use me - implementing or debugging a 2LTT core calculus with compile-time evaluation and @@ -52,7 +55,7 @@ and the staging algorithm that runs metaprograms to produce splice-free object c code (strictness). Whether *conversion checking* computes object redexes depends on the chosen object theory: full-MLTT object level (2022) — yes; CFTT-style first-order object level — no β/η/let-unfolding at all. Pick one coherently - (`implementation-guide.md` §2.1). + ([`implementation-guide.md`](implementation-guide.md) §2.1). - **`infer` returns `(Term, VTy, Stage)`** — never reconstruct types (or stages) from elaborated terms afterwards. - **`checkU`** — when a term must be a type, check it against `U s` directly; don't diff --git a/.opencode/skills/2ltt/demo-implementation.md b/.opencode/skills/2ltt/demo-implementation.md index fe9a600d..7f866a49 100644 --- a/.opencode/skills/2ltt/demo-implementation.md +++ b/.opencode/skills/2ltt/demo-implementation.md @@ -1,7 +1,7 @@ # Reference implementation (Kovács `staged` demo) Code-level reference for https://github.com/AndrasKovacs/staged/tree/main/demo — the -prototype accompanying the 2022 paper (theory: `kovacs-2022-staged-compilation-2ltt.md`). +prototype accompanying the 2022 paper (theory: [`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md)). Features: two stages, dependent functions, type-in-type (no sigma; data is lambda-encoded), `Nat` at both stages, Agda-style implicits with higher-order unification, and strong inference for staging operations. @@ -146,7 +146,7 @@ build closed Pi types for fresh metas cheaply. `bind` (bound var), `newBinder` There is **no stage check at variable lookup** — `infer (Var x)` just returns the stored stage. Mismatches between inferred and expected stage/type are *repaired* by coercive subtyping (rules `A ≤ ⇑A`, `⇑A ≤ A`, `U0 ≤ U1`; theory in -`kovacs-2022-staged-compilation-2ltt.md` §3.3): +[`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md) §3.3): ```hs adjustStage cxt t a s s' -- move (t : a : U s) to stage s' @@ -226,4 +226,4 @@ error; two-domain staging with levels + closures; meta-type erasure in staging. Reconsider per design: the coercive-subtyping repair (powerful but complex — a hard stage error is the simple alternative); full object β in conversion (fits the 2022-style object theory; a CFTT-style object language wants weak object equality instead — see -`kovacs-2024-closure-free-2ltt.md` §2.4); type-in-type (demo-only shortcut). +[`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md) §2.4); type-in-type (demo-only shortcut). diff --git a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md index 8486aace..ee6ec911 100644 --- a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md +++ b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md @@ -15,7 +15,7 @@ side conditions ruling out exactly the uncompilable cases. needs before it does work; determines the call sequence. Arity is *intensional* — types like `Int → Int → Int` don't determine it (`λx λy. e` has -arity 2; `λx. let z = expensive x in λy. e` has arity 1). The IL exists to *memorialize* +arity 2; `λx. let z = expensive x in λy. e` has arity 1). The IL exists to *record* the result of an arity analysis, not to perform it. ## 2. Kind grammar @@ -119,7 +119,7 @@ rep/levity/arity so unstaging emits codegen-determined code. In a 2LTT the meta replaces IL's quantifiers: rep/levity/arity polymorphism becomes meta-level abstraction that staging eliminates, so the `mono-*` side conditions reappear as "these indices must be canonical by staging time" (cf. the memory-representation-polymorphism variation in -`kovacs-2022-staged-compilation-2ltt.md` §5.2, and the CFTT ≈ simply-typed-IL-fragment -remark in `kovacs-2024-closure-free-2ltt.md` §7). A minimal adaptation: `Rep` as a meta +[`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md) §5.2, and the CFTT ≈ simply-typed-IL-fragment +remark in [`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md) §7). A minimal adaptation: `Rep` as a meta type, object types indexed by `Rep`, and — if functions are first-class — a `Clos`-style boxing former to recover uniform representation where needed. diff --git a/.opencode/skills/2ltt/glossary.md b/.opencode/skills/2ltt/glossary.md new file mode 100644 index 00000000..ed47f763 --- /dev/null +++ b/.opencode/skills/2ltt/glossary.md @@ -0,0 +1,21 @@ +# Glossary + +Shared terminology for the 2LTT skill. Referenced from +[`implementation-guide.md`](implementation-guide.md) and the paper notes. + +| Term | Definition | +|------|-----------| +| **Stage** | 0 = object/runtime, 1 = meta/compile-time. Some implementations say "phase". | +| **Lift `⇑A`** | Meta type of metaprograms producing object code of type `A`. | +| **Quote `⟨t⟩`** | Staging intro: object term `t : A` as meta value of `⇑A`. | +| **Splice `∼t`** | Staging elim: run `t : ⇑A` during staging, insert resulting object term. | +| **Staging / unstaging** | Running all metaprograms; output is splice-free object code. Same operation, two names (2022 / 2024 papers). | +| **Soundness / stability / strictness** | Staging output ≈ input up to conversion / staging is identity on object code / staging preserves object term formers exactly. | +| **NbE** | Normalization by evaluation: eval syntax → semantic values, read back to syntax. | +| **Read-back ("quotation" in NbE jargon)** | `Lvl → Value → Term`. Not the staging quote. | +| **Neutral** | Value stuck on a variable/meta, carrying a spine of pending eliminations. | +| **Closure** | Captured environment + unevaluated body; applied by environment extension. | +| **De Bruijn index / level** | Count from nearest binder (syntax) / from outermost (values). | +| **Zonk** | Inline solved metavariables into a term. | +| **Binding-time improvement** | Rewriting toward meta-level structure (e.g. `⇑(A→B)` → `⇑A→⇑B`) so more computes at staging time. | +| **Generativity** | Metaprograms can't inspect object terms; internalizable as an axiom (CFTT). | diff --git a/.opencode/skills/2ltt/implementation-guide.md b/.opencode/skills/2ltt/implementation-guide.md index c5e71cef..9d7b041e 100644 --- a/.opencode/skills/2ltt/implementation-guide.md +++ b/.opencode/skills/2ltt/implementation-guide.md @@ -20,7 +20,7 @@ Two distinct evaluation mechanisms, easy to conflate: (*strictness*), regardless of what conversion does. Both are NbE-style: eval into a semantic domain with De Bruijn levels + closures, read -back into syntax with indices. See `demo-implementation.md` for the reference shapes +back into syntax with indices. See [`demo-implementation.md`](demo-implementation.md) for the reference shapes (§2 conversion evaluator, §3 two-domain staging evaluator). ## 2. Design decisions to make up front @@ -48,7 +48,7 @@ return `(Term, VTy, Stage)`. On a stage mismatch there are two designs: (insert splice), optionally `U0 ≤ U1` (insert `Lift`), with contravariant/covariant function rule. Powerful inference (quotes/splices mostly disappear from surface syntax); costs a coercion pass, explicit weakening in the core, coercion-avoidance - logic. See `demo-implementation.md` §4.2–4.3. + logic. See [`demo-implementation.md`](demo-implementation.md) §4.2–4.3. - **Reject**: hard "stage mismatch" error at the point of use. Much simpler; forces explicit staging operators in the surface language. Fine as a first iteration — the type structure is identical, only elaboration ergonomics differ. @@ -59,12 +59,12 @@ effective and stage unification unnecessary. ### 2.3 Optional extensions (see the respective files) - Closure-free discipline `ValTy`/`CompTy`, computation products, call saturation — - `kovacs-2024-closure-free-2ltt.md` §2. + [`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md) §2. - Representation/arity/levity indexing of object types — - `downen-2020-kinds-are-calling-conventions.md`; meta-level `Rep` indexing — - `kovacs-2022-staged-compilation-2ltt.md` §5.2. + [`downen-2020-kinds-are-calling-conventions.md`](downen-2020-kinds-are-calling-conventions.md); meta-level `Rep` indexing — + [`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md) §5.2. - Intensional analysis (needs a non-standard setup) — - `kovacs-2022-staged-compilation-2ltt.md` §6. + [`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md) §6. ## 3. NbE core (checker) @@ -118,7 +118,7 @@ These invariants prevent whole classes of bugs: ## 5. Staging pass essentials -(Reference shape: `demo-implementation.md` §3.) +(Reference shape: [`demo-implementation.md`](demo-implementation.md) §3.) - Separate pass over elaborated (zonked) syntax; do not reuse the conversion evaluator. - **Two value domains**: meta values (functions-as-closures, inductive values, quoted @@ -138,7 +138,7 @@ These invariants prevent whole classes of bugs: Meta-level use of object code duplicates it (using `x : ⇑A` twice pastes the expression twice). The toolkit — `Gen` monad (CPS let-insertion, polymorphic answer type), `gen`/`genRec`, case-splitting via `Split`, join points via `MonadJoin` + SOP — is -library-level metaprogramming, specified in `kovacs-2024-closure-free-2ltt.md` §3–4. +library-level metaprogramming, specified in [`kovacs-2024-closure-free-2ltt.md`](kovacs-2024-closure-free-2ltt.md) §3–4. A staged compiler doesn't need built-in support, but its object language must offer `let`/`letrec` insertable at arbitrary positions for these libraries to be writable. Deduplication/caching of generated code across splice sites is an open engineering @@ -165,25 +165,6 @@ problem (flagged in both papers). branch `01-eval-closures-debruijn` is the minimal NbE + De Bruijn reference; later branches add metas/implicits. - **staged demo** (Kovács): https://github.com/AndrasKovacs/staged/tree/main/demo — - full 2LTT elaborator + stager; excerpted in `demo-implementation.md`. The repo also + full 2LTT elaborator + stager; excerpted in [`demo-implementation.md`](demo-implementation.md). The repo also contains the LaTeX sources of both Kovács papers and an Agda embedding of CFTT (`icfp24paper/supplement`). - -## 9. Glossary - -| Term | Definition | -|------|-----------| -| **Stage** | 0 = object/runtime, 1 = meta/compile-time. Some implementations say "phase". | -| **Lift `⇑A`** | Meta type of metaprograms producing object code of type `A`. | -| **Quote `⟨t⟩`** | Staging intro: object term `t : A` as meta value of `⇑A`. | -| **Splice `∼t`** | Staging elim: run `t : ⇑A` during staging, insert resulting object term. | -| **Staging / unstaging** | Running all metaprograms; output is splice-free object code. Same operation, two names (2022 / 2024 papers). | -| **Soundness / stability / strictness** | Staging output ≈ input up to conversion / staging is identity on object code / staging preserves object term formers exactly. | -| **NbE** | Normalization by evaluation: eval syntax → semantic values, read back to syntax. | -| **Read-back ("quotation" in NbE jargon)** | `Lvl → Value → Term`. Not the staging quote. | -| **Neutral** | Value stuck on a variable/meta, carrying a spine of pending eliminations. | -| **Closure** | Captured environment + unevaluated body; applied by environment extension. | -| **De Bruijn index / level** | Count from nearest binder (syntax) / from outermost (values). | -| **Zonk** | Inline solved metavariables into a term. | -| **Binding-time improvement** | Rewriting toward meta-level structure (e.g. `⇑(A→B)` → `⇑A→⇑B`) so more computes at staging time. | -| **Generativity** | Metaprograms can't inspect object terms; internalizable as an axiom (CFTT). | diff --git a/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md b/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md index 32f75824..20ca2d81 100644 --- a/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md +++ b/.opencode/skills/2ltt/kovacs-2022-staged-compilation-2ltt.md @@ -107,7 +107,7 @@ Extract a **coercive subtyping** system used during bidirectional elaboration: When comparing inferred vs. expected type, insert coercions. With this plus Agda-style implicits + pattern unification, `map` can be written with no quotes/splices at all. Where the elaborator must choose between improved/unimproved types, default to -**improved**, with explicit lifting to opt out. (See `demo-implementation.md` for the +**improved**, with explicit lifting to opt out. (See [`demo-implementation.md`](demo-implementation.md) for the actual algorithm, including coercion avoidance.) ## 4. Staging: definition, algorithm, correctness (§3–5) @@ -199,7 +199,7 @@ Refinement: internalize representations as a meta type and index runtime types b `Rep` is meta-level, so it cannot be abstracted over at runtime; staging computes all `Rep` indices to canonical representations. This reconciles dependent types with memory layout control. (Compare *Kinds Are Calling Conventions* for a much richer treatment of -the same axis — see `downen-2020-kinds-are-calling-conventions.md`.) +the same axis — see [`downen-2020-kinds-are-calling-conventions.md`](downen-2020-kinds-are-calling-conventions.md).) ## 6. Intensional analysis (§6) diff --git a/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md b/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md index 2d26c07c..08406118 100644 --- a/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md +++ b/.opencode/skills/2ltt/kovacs-2024-closure-free-2ltt.md @@ -4,7 +4,7 @@ Checked against the paper's LaTeX source. The system is called **CFTT** ("closur type theory"). This file only covers what CFTT *adds or changes* relative to the 2022 2LTT — for the shared core (lift/quote/splice rules, staging-by-evaluation, soundness/stability/strictness, binding-time improvement, inference) see -`kovacs-2022-staged-compilation-2ltt.md`. +[`kovacs-2022-staged-compilation-2ltt.md`](kovacs-2022-staged-compilation-2ltt.md). Terminology: this paper says **unstaging** for what the 2022 paper calls "staging" (running metaprograms in splices to extract object code). Same thing. @@ -214,5 +214,5 @@ which vanish if users respect the discipline. - Downstream compiler still wants: dead code elimination, unused-arg removal, de-duplication of generated code. - The object language is close to a simply-typed fragment of the KACC intermediate - language (see `downen-2020-kinds-are-calling-conventions.md`): function types distinct + language (see [`downen-2020-kinds-are-calling-conventions.md`](downen-2020-kinds-are-calling-conventions.md)): function types distinct from closure types, universal η, explicit arity — KACC lacks only `letrec`. From e0388f979062b6cd930cfe054554d94d37bcd7bf Mon Sep 17 00:00:00 2001 From: LukasK Date: Thu, 23 Jul 2026 14:28:13 +0000 Subject: [PATCH 3/4] ai: clarify function-type kinds in Downen 2ltt notes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Explain, next to the arrow example, that the PtrR representation is that of the function value itself (a code pointer) and that the arity lists only the argument reps — the return type's representation deliberately never appears in the kind, which is what keeps return types rep/levity-polymorphic. (#3637766663) Co-Authored-By: Claude Opus 4.8 --- .../2ltt/downen-2020-kinds-are-calling-conventions.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md index ee6ec911..d7b367e8 100644 --- a/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md +++ b/.opencode/skills/2ltt/downen-2020-kinds-are-calling-conventions.md @@ -37,6 +37,13 @@ Int# : TYPE IntR (Eval U) IntL : TYPE PtrR (Eval L) Int# ⤳ Int# ⤳ Int# : TYPE PtrR Call[IntR, IntR] ``` +Reading the arrow kind: the representation `PtrR` is that of **the function value +itself** — a code/closure pointer — *not* of anything it takes or returns; the arity +`Call[IntR, IntR]` lists **only the argument** reps. The **return type's representation +never appears in the kind**: `Int# ⤳ Int#` and `Int# ⤳ Bool#` both have kind +`TYPE PtrR Call[IntR]`. That omission is deliberate — it is what lets return types stay +representation/levity-polymorphic (§4, tail-call return convention). + Haskell's default kind `★` = `TYPE PtrR (Eval L)`; an eager language's default is `TYPE PtrR (Eval U)`. Function-type formation *concatenates* arities: if `τ₁ : TYPE ρ₁ ν₁` and `τ₂ : TYPE ρ' Call[ρ₂,…,ρₘ]` then From a02eb1a10baee115f5f62d247da440715f106b38 Mon Sep 17 00:00:00 2001 From: LukasK Date: Thu, 23 Jul 2026 14:32:51 +0000 Subject: [PATCH 4/4] ai: present coe cases as prose bullets, not commented code The coe case summary was written as Haskell -- comments inside the same code block as the runnable adjustStage, making it read as disabled code. Lift it out into a bullet list so it is unambiguously a summary. (#3637848617) Co-Authored-By: Claude Opus 4.8 --- .opencode/skills/2ltt/demo-implementation.md | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/.opencode/skills/2ltt/demo-implementation.md b/.opencode/skills/2ltt/demo-implementation.md index 7f866a49..575160e6 100644 --- a/.opencode/skills/2ltt/demo-implementation.md +++ b/.opencode/skills/2ltt/demo-implementation.md @@ -157,17 +157,18 @@ adjustStage cxt t a s s' -- move (t : a : U s) to stage s' a -> do m <- freshMeta (VU S0) S0 -- a must be ⇑?m unifyCatch cxt a (VLift m) (tSplice t, m) - -coe cxt t a s a' s' -- full coercion (t : a : U s) to (a' : U s') - -- Pi vs Pi: contravariant/covariant, η-expanding with Wk for the shifted body; - -- tracks "trivial coercion" (Nothing) to avoid inserting useless η-expansions - -- (VU S0, VU S1) -> Lift t -- U0 ≤ U1 witnessed by Lift - -- (VLift a, VLift a') -> unify a a' - -- (VLift a, a') -> coe (tSplice t) ... -- unwrap and retry - -- (a, VLift a') -> tQuote <$> coe t ... - -- otherwise -> adjustStage then unify ``` +`coe cxt t a s a' s'` (full coercion of `t : a : U s` to `a' : U s'`) dispatches on +`(force a, force a')`: +- **Pi vs Pi** — contravariant/covariant, η-expanding with `Wk` for the shifted body; + tracks a "trivial coercion" (`Nothing`) to avoid inserting useless η-expansions. +- `(VU S0, VU S1)` → `Lift t` — `U0 ≤ U1`, witnessed by `Lift`. +- `(VLift a, VLift a')` → `unify a a'`. +- `(VLift a, a')` → `coe (tSplice t) …` — unwrap and retry. +- `(a, VLift a')` → `tQuote <$> coe t …`. +- otherwise → `adjustStage` then `unify`. + `Wk` (explicit weakening) exists solely so `coe` can reuse `t` under the binders it introduces. Stage errors thus surface as *unification* failures, not as a dedicated "wrong stage" error. (A simpler checker without subtyping can instead make stage