diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 58ab4f3..08efd76 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -244,15 +244,25 @@ ail run — build + execute (tempdir), passthrough exit ## What is not (yet) supported -Snapshot of the boundary at the end of Iter 8. Items move out of this list +Snapshot of the boundary at the end of Iter 12. Items move out of this list as iterations land; the JOURNAL records the exact iteration. - No effect handlers — only the built-in IO and Diverge ops. - No refinements / SMT escalation. -- No polymorphism in inference. `Type::Forall` is parseable but the - typechecker rejects polymorphic uses inside a body (`PolymorphicNot - Supported`). Generic functions must be monomorphised by the author - via separate top-level defs. +- No parameterised ADTs. `List a` / `Maybe a` aren't expressible — + ADTs are concrete (`IntList`, `Maybe_Int`, ...). Polymorphism over + primitives and fn-typed values works, but a generic `map :: forall + a b. ((a) -> b, List a) -> List b` is blocked on this. Queued + next. +- No HM inference inside bodies. Top-level def types are explicit; + polymorphism is opt-in via `Type::Forall { vars, body }`. Inside + a body, lambdas check monomorphically against their declared type. +- Polymorphic fns must be **directly called** at the use site. + Passing a polymorphic fn as a value (`let f = id in f(42)`) is + not yet supported — it would need one closure-pair global per + instantiation, deferred. +- No higher-rank polymorphism. Passing a polymorphic fn to another + polymorphic fn (`apply(id, 42)`) is not supported. - No cross-module ADTs. ADTs are local to a module; ctor names must be unique within their module but may collide across modules. - No visibility rules in imports. Every top-level def of an imported module @@ -279,6 +289,12 @@ What **is** supported (and used as the smoke test for the pipeline): closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto- generated adapter and a static closure pair (env = null) so they remain passable as values without heap overhead. +- **Polymorphism via `Type::Forall`** at top-level def types (Iter 12). + Use sites instantiate fresh metavars; unification pins them against + the concrete types of the call args. Codegen monomorphises on + demand: each unique instantiation emits a specialised LLVM fn + mangled `@ail____` (e.g. `id__I` for `id` at + `Int`, `apply__I_I` for `apply` at `(Int, Int)`). Pipeline regression smoke tests: @@ -290,3 +306,7 @@ Pipeline regression smoke tests: HOF + IO; the dogfood smoke test). - `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5] one-per-line (insertion sort over an 11-element list). +- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic + identity at `Int` and `Bool`; two specialised fns emitted). +- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply` + with a fn-typed parameter; `apply(succ, 41)`). diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 57c1f03..feace86 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -892,3 +892,135 @@ actually needs generic data — is HM inference + let-generalisation types in fn signatures. 12c. Docs + a polymorphic `id` test + a generic `map :: (a -> b) -> List a -> List b` rewrite of `list_map.ail.json`. + +## 2026-05-07 — Iter 12a/b done: polymorphism reaches the binary + +Skipped 12c's "polymorphic map" — without parameterised ADTs (which +the MVP doesn't have), the rewrite would still be over a concrete +`IntList`, defeating the purpose. So 12c becomes lighter: docs + +two new examples (`poly_id`, `poly_apply`) that prove polymorphism +end-to-end on primitive types and on fn-typed parameters. The big +test is whether *I* would use the language now for a poly-flavoured +program; the answer below. + +**12a — typechecker:** + +`Type::Forall { vars, body }` is now legal at top-level fn types. +Implementation is the textbook ML rule: peel the Forall when +checking the body (rigid vars go into `Env.rigid_vars` so +`check_type_well_formed` accepts them), instantiate fresh metavars +at every var-resolution site, unify on every formerly-`expect_eq` +edge. + +The metavar encoding sidesteps an AST schema change: a metavar is +just `Type::Var { name: "$m" }`. The `$` prefix can't collide +with source identifiers, the JSON layout doesn't shift, and module +hashes stay bit-identical (verified: `sum.ail.json` keeps +`db33f57cb329935e` / `d9a916a0ed10a3d3`). I considered adding a +new `Type::Meta` variant under `#[serde(skip)]` but that would +have pulled hashing concerns into serde; the naming convention +keeps the AST untouched. + +`Subst` is a flat `BTreeMap`; `unify` is the standard +occurs-check version with effects compared as a set. Constants +still reject Forall outright; ADT fields still reject vars. No +let-generalisation: lambdas inside fn bodies are checked +monomorphically against their declared types — keeps the +implementation small and matches DESIGN.md's "top-level types +must always be explicitly annotated". + +**12b — codegen:** + +Direct calls to a polymorphic def get monomorphised on demand. +Each unique (def, instantiation) pair emits a specialised LLVM fn +with mangling `@ail____`. Descriptor scheme: +`Int → I`, `Bool → B`, `Unit → U`, `Str → S`, ADT `Foo → FFoo`, +`Fn(a)→b → Fn___r_`. So `id(42)` and `id(true)` produce +`@ail_poly_id_id__I` and `@ail_poly_id_id__B` side by side. + +Pass 1 of `lower_workspace` now splits fn-typed defs into mono +(`module_user_fns`, LLVM-typed FnSig as before) and poly +(`module_polymorphic_fns`, full FnDef). A unified +`module_def_ail_types` carries AILang types for both, used by +the codegen-side type tracker. + +The hard part was getting AILang types at call sites. The +typechecker has them but doesn't hand its annotations down (no +TIR yet). I considered three paths: + 1. Typechecker sidetable keyed by AST node ids — would need + to assign ids deterministically, brittle. + 2. Uniform representation (everything passes as ptr/i64) — + contradicts CLAUDE.md's "performance is extremely important". + 3. Codegen replays the type derivation locally. +Picked (3). The trade-off is duplication (`synth_arg_type` +mirrors what the typechecker already did), but it's contained +to a small recursive walk and uses the same `locals`/`extras` +shadowing pattern. Worth it for the MVP — once a TIR stage +materialises (it's still on the debt list), the duplication +collapses into a single pass. + +`locals` grew from 3-tuple to 4-tuple `(name, ssa, llvm_type, +ail_type)`. Six push sites updated mechanically. Lambda capture +metadata grew the same way. `CtorRef` got `ail_fields` so match +arm bindings inherit the AILang type. + +The drain phase iterates until `mono_queue` is empty — +specialised bodies can themselves invoke polymorphic defs and +queue further entries. `apply_subst_to_term` substitutes rigid +vars in `Term::Lam` annotations (the only Term arm carrying +types). + +**Architecture self-check:** + +- *Would I use this language now?* For monomorphic programs: + yes (already established). For polymorphism over primitives + and fn-typed parameters: yes — `id` and `apply` write out the + way the textbook says they should, with no language-level + bookkeeping leaking into the source. The `poly_apply` example + was particularly revealing: the closure-pair ABI (Iter 8a) + composes cleanly with monomorphisation. Specialised body of + `apply__I_I` keeps `f` as a fn-typed local; the existing + indirect-call path already handles the lower from there. +- *Did I think of everything?* No, two known gaps: + 1. **Polymorphic fn passed as a value** (`let f = id in f(42)`) + fails in codegen — `resolve_top_level_fn` looks in + `module_user_fns` only. Adding this means emitting one + closure-pair global per instantiation, possibly via the + same drain pass. Defer. + 2. **Higher-rank polymorphism** (`apply(id, 42)`) trips + `unify_for_subst` which doesn't handle Forall on the param + side. Real higher-rank polymorphism is a substantial step + and not on the near horizon — deferred to a later iter. +- *Visualisation:* `ail manifest poly_id.ail.json` now shows + `forall a. (a) -> a` correctly. The pretty-printer carried + `Type::Forall` rendering since Iter 1; nothing to do. +- *KISS:* +1 typechecker file edit (~430 LOC inserted, mostly + Subst+unify+four tests), +1 codegen extension (~600 LOC + inserted, mostly the drain path + helpers + locals widening). + Two new examples, two new e2e tests. Could be smaller if I + bit the bullet on TIR; not yet worth the upfront cost. + +**Tests:** 58/58 (was 56/56). Added 4 typechecker unit tests in +12a, 2 e2e tests in 12b. Hash invariant holds. + +**Plan iteration 13 (queued, not started):** + +The natural next step depends on what I want to use the language +for. Two candidates, in order of expected payoff: + +13a. **Parameterised ADTs** — `List a`, `Maybe a`, etc. Without + these, polymorphism is half-useful: a generic `map` still + can't transform an `IntList` into a `BoolList`. ADT defs + would gain a `vars: Vec` field; ctor field types + could mention them; codegen monomorphises ADT instances + just like fns. This is the bigger expressivity unlock. +13b. **GC or arena** — every ADT box, lambda env, and closure + pair currently leaks. For sort over an 11-element list, + fine. For anything longer-running, required. The current + lifetime model is "leak"; the right MVP is probably + bumpalloc per top-level fn invocation. Could be done + before parameterised ADTs but doesn't unlock new examples. + +Leaning 13a — it's the more interesting architectural step and +makes the "polymorphic map" rewrite from the original 12c plan +finally meaningful.