Brummel
e3ecf4f0cd
Replaces the earlier "RC + inference, no annotations" position with a two-layer architecture: inference (intra-fn) + mandatory LLM-author mode annotations on fn signatures (inter-fn). Adds structured rationale for rejecting region inference (regions assume stack-shaped lifetimes; real programs need non-stack-shaped lifetimes for caches / memo tables) and linear types as primary mechanism. Schema additions enumerated for the 18-series: Type::Borrow / Type::Own (Iter 18a) Term::Clone (Iter 18c) Term::ReuseAs (Iter 18d) TypeDef.drop_iterative (Iter 18e) Migration plan extended from 18a-d (4 iters) to 18a-f (6 iters). JOURNAL records the regions excursion, the scope-shape reduction, and the LLM-author lever as the structural advantage Decision 10 cashes in on.
1341 lines
60 KiB
Markdown
1341 lines
60 KiB
Markdown
# AILang — design decisions
|
||
|
||
This document records the core decisions for AILang. It is my contract with
|
||
myself across future iterations. Prefer cuts over growth.
|
||
|
||
## Goal
|
||
|
||
AILang is a programming language for LLM authors. It compiles to LLVM IR.
|
||
Performance: native, no GC for the MVP.
|
||
|
||
Optimised for:
|
||
|
||
- **Machine readability** over human ergonomics. The source is structured.
|
||
- **Local reasoning.** Every definition carries its full type and effects.
|
||
- **Provability.** Pure core language, explicit effects, optional refinements.
|
||
- **Robustness against hallucinations.** Symbols are hashable; tools can verify
|
||
existence without spending context window.
|
||
|
||
## Project ecosystem
|
||
|
||
AILang is not just a language but an ecosystem. The language on its own is
|
||
only valuable when its surroundings make it usable, checkable, and
|
||
extensible for its target user (LLM authors). The repo therefore contains
|
||
several equally important components — none of them optional, all of them
|
||
evolving in lockstep with the language:
|
||
|
||
- **Language core** (`crates/ailang-core`, `crates/ailang-check`,
|
||
`crates/ailang-codegen`): AST, type system, codegen.
|
||
- **CLI** (`crates/ail`): toolchain for tooling consumers — `manifest`,
|
||
`describe`, `deps`, `check`, `build`, etc., preferably with `--json` for
|
||
machine consumption.
|
||
- **Examples** (`examples/`): canonical `.ail.json` programs. They are
|
||
specification anchors, not demos — the E2E suite hangs off them.
|
||
- **Agents** (`agents/`): specialised sub-prompts (implementer,
|
||
architect, tester, debugger) that form the project's own LLM tooling.
|
||
They are a versioned part of the repo. See `agents/README.md`.
|
||
- **Docs** (`docs/`): DESIGN.md (what and why), JOURNAL.md (history).
|
||
- **Tests**: unit tests per crate plus E2E in `crates/ail/tests/e2e.rs`. Every
|
||
new compiler path needs a test, otherwise the feature does not count as done.
|
||
|
||
When the language grows, these components grow with it. New tools that
|
||
strengthen the LLM tooling (e.g. `ail diff`, IR snapshot diffs, new agents)
|
||
explicitly belong in the ecosystem inventory of this section and are added
|
||
here as soon as they are established.
|
||
|
||
## Project language: English
|
||
|
||
All in-tree content is written in English: source code (identifiers,
|
||
comments, string literals, CLI help), design documents, the journal, agent
|
||
prompts, READMEs, commit messages, examples, and `CLAUDE.md`. The live
|
||
conversation between user and me stays German for ergonomic reasons;
|
||
everything that lands in git is English. This keeps diffs and tooling output
|
||
uniform and matches the audience for AILang (LLM authors), for whom English
|
||
is the default.
|
||
|
||
## Decision 1: source = data, not text
|
||
|
||
A module is a JSON object with a fixed schema. There is no parser for
|
||
free-form text. Typos in identifiers turn into hash-lookup errors that the
|
||
compiler proposes a fix for directly.
|
||
|
||
A textual form exists (`.ail`, S-expression-like), but only as a
|
||
bidirectional projection of the JSON form. It is intended for human reviews
|
||
and diffs.
|
||
|
||
**Canonical format:** `.ail.json` with deterministic key order.
|
||
|
||
## Decision 2: content-addressed definitions
|
||
|
||
Every top-level definition has a `hash` value (BLAKE3 over canonical JSON
|
||
without the `hash` field itself). References between definitions go primarily
|
||
by name — names are for readability. The hash is the canonical identity.
|
||
|
||
Advantages:
|
||
|
||
- Refactoring by adding new defs, not by in-place change. Old versions stay
|
||
callable until manually removed.
|
||
- Caching of typecheck results and codegen per hash.
|
||
- Diffs show exactly which def has changed.
|
||
|
||
## Decision 3: pure core language + algebraic effects
|
||
|
||
The default is total, pure functions. Effects are declared as a set in the
|
||
function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic
|
||
(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
|
||
loops) are wired up.
|
||
|
||
This is the most important LLM property: when I read a function, I can trust
|
||
its signature without reading the body.
|
||
|
||
## Decision 4: Hindley-Milner + optional refinements
|
||
|
||
MVP: HM with let-polymorphism. All types are inferable, but at the top level
|
||
they must always be explicitly annotated (for local reasoning).
|
||
|
||
Later: refinement annotations that escalate to SMT. `(i: Int | i >= 0)`. They
|
||
are reserved in the AST from the start, but in the MVP they are simply passed
|
||
through as opaque strings.
|
||
|
||
## Decision 5: emit LLVM IR as text
|
||
|
||
Instead of `inkwell` or `llvm-sys`: AILang produces `.ll` files as strings
|
||
and hands them to `clang` for linking.
|
||
|
||
Rationale:
|
||
|
||
- The LLVM IR text syntax is largely stable across versions.
|
||
- No build dependency on a specific libllvm version.
|
||
- Generated code is trivially inspectable, which makes debugging much easier.
|
||
- An LLM can read the generated IR directly, which is harder with opaque
|
||
library calls.
|
||
|
||
Trade-off: no inline optimisations through the LLVM API. We rely on
|
||
`clang -O2` as the standard pipeline.
|
||
|
||
## Decision 6: authoring surface (Iter 14b)
|
||
|
||
**Status: shipped.** Form (A) was chosen in Iter 14b and implemented as
|
||
the `ailang-surface` crate (parser + printer) in Iter 14c. Form-A is
|
||
gated against drift by `ailang-surface/tests/round_trip.rs`, which
|
||
parses every `.ailx` fixture, prints it back, re-parses, and demands
|
||
canonical-byte equality. In Iter 15e, `ail render` and both branches
|
||
of `ail describe` were rewired to use `ailang_surface::print`, making
|
||
form (A) the **sole** text projection of a module — the legacy
|
||
non-round-tripping pretty-printer code in `pretty.rs` was deleted in
|
||
the same iter, leaving only diagnostic helpers (`type_to_string`,
|
||
`pattern_to_string`, `manifest`) public. The rest of this section
|
||
records the *why* of Decision 6 for the audit trail; the constraints
|
||
listed below describe the surface as shipped.
|
||
|
||
### Why this is opening up
|
||
|
||
Iters 1 through 14a authored everything as raw `*.ail.json`. That worked
|
||
for 17 fixture files (each ≤ 60 LOC of JSON) but does not scale. Two
|
||
breaking signals:
|
||
|
||
1. The token-economy cost of the JSON-AST is massive: a single integer
|
||
literal `1` is encoded as `{"t":"lit","lit":{"kind":"int","value":1}}`
|
||
— ~38 tokens of structural overhead per bit of semantics. For a stdlib
|
||
in the 200–500 def range this displaces real attention budget.
|
||
2. JSON-AST authoring exposes a class of errors (wrong field names,
|
||
silently-accepted extra fields under `#[serde(default)]`,
|
||
inconsistent ctor casing) that surface only at load time. The
|
||
schema is correct-by-construction in storage but **error-prone in
|
||
authoring**.
|
||
|
||
Decision 1 anticipated this: it says a textual form exists "as a
|
||
bidirectional projection of the JSON form." The pretty-printer already
|
||
emits S-expression-style text (see `crates/ailang-core/src/pretty.rs`).
|
||
What is missing is the inverse direction — text → AST. Decision 6
|
||
adds that inverse as **one** authoring projection alongside the
|
||
existing pretty-printer; the JSON-AST remains the source of truth.
|
||
|
||
### Architectural pin: data structure is the source of truth
|
||
|
||
The textual surface is **not** a replacement for the JSON-AST. It is
|
||
one projection among potentially many. Concretely:
|
||
|
||
- The JSON-AST keeps its role as the canonical, hashable, content-
|
||
addressed representation of a module. All hashing, content-
|
||
addressing, cross-module references, and typecheck/codegen input
|
||
flow through the JSON-AST. **No new hashable form is introduced.**
|
||
- The textual surface (form A, this Decision) is the **AI authoring
|
||
projection**: optimised for me producing programs token-efficiently
|
||
and for foreign LLMs producing programs from a spec. It is not
|
||
optimised for human authors and does not need to be human-pleasant.
|
||
- Future projections are explicitly anticipated: a visual / graphical
|
||
front-end is a plausible second projection for human review and
|
||
inspection (display being the one case where non-AI eyes matter).
|
||
The architecture leaves room: any producer of well-formed
|
||
`ailang-core::ast::Module` values is a valid front-end.
|
||
- **No human is expected to author AILang seriously.** Authoring is
|
||
AI work. Display and verification, by contrast, are concerns where
|
||
human-facing alternatives may be useful — and which can therefore
|
||
layer their own projections on top of the same AST without
|
||
touching the surface or the core.
|
||
|
||
In code terms: `ailang-core` owns the AST. `ailang-surface` (new in
|
||
Iter 14c) is one producer/consumer pair: text-form-A → AST → text-
|
||
form-A. A hypothetical `ailang-visual` would be a different producer
|
||
of the same AST. `ailang-check` and `ailang-codegen` consume only
|
||
the AST and remain projection-agnostic.
|
||
|
||
### Constraints (hard, in priority order)
|
||
|
||
1. **Formalizable for a foreign LLM.** The grammar must fit in an
|
||
EBNF/PEG spec of ≤ 30 productions. A model that has never seen
|
||
AILang must be able to read the spec and produce conforming source
|
||
zero-shot. Rules out: precedence between binary operators,
|
||
semantic indentation, maximal-munch lexing, context-sensitive
|
||
reductions.
|
||
2. **AST-isomorphic.** Every surface form maps to exactly one AST
|
||
shape. Round-trip surface → AST → canonical JSON → AST → surface
|
||
is the identity (modulo formatting). Hashes computed via the
|
||
round-tripped JSON must equal hashes of the same module written
|
||
directly in JSON.
|
||
3. **No external symbols.** ASCII only. No Greek (`∀`), no arrows
|
||
(`→`), no subscripts. Reasoning: I substitute mojibake for
|
||
non-ASCII characters under context pressure; foreign LLMs vary
|
||
in how they tokenize Unicode.
|
||
4. **No precedence.** Either everything is parenthesized, or there
|
||
are no infix operators. Prefer the latter — `add(x, 1)` over
|
||
`x + 1`. Removes a fail mode for both me and foreign LLMs.
|
||
5. **No semantic indentation.** Block structure expressed by paired
|
||
delimiters or terminator tokens. Indentation is informational
|
||
only; the parser ignores it.
|
||
6. **One construct per token-list.** Every AST node corresponds to
|
||
exactly one parenthesized form (or atom). No "sometimes you can
|
||
omit the parens" rules.
|
||
7. **AST surface stays frozen.** The surface adapts to the AST, not
|
||
the other way around. We do not change the JSON schema or
|
||
invalidate hashes to make the surface prettier.
|
||
|
||
### Candidate notations (same `map` encoded in each)
|
||
|
||
The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`:
|
||
|
||
```
|
||
data List a where Nil | Cons a (List a)
|
||
fn map : forall a b. ((a) -> b, List a) -> List b
|
||
= \f xs. match xs of Nil -> Nil
|
||
| Cons h t -> Cons(f(h), map(f, t))
|
||
```
|
||
|
||
#### (A) S-expression with fully-tagged AST nodes
|
||
|
||
```
|
||
(module list_map_poly
|
||
|
||
(data List (vars a)
|
||
(ctor Nil)
|
||
(ctor Cons a (con List a)))
|
||
|
||
(fn inc
|
||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||
(params x)
|
||
(body (app + x 1)))
|
||
|
||
(fn map
|
||
(type
|
||
(forall (vars a b)
|
||
(fn-type
|
||
(params (fn-type (params a) (ret b)) (con List a))
|
||
(ret (con List b)))))
|
||
(params f xs)
|
||
(body
|
||
(match xs
|
||
(case (pat-ctor Nil) (term-ctor List Nil))
|
||
(case (pat-ctor Cons h t)
|
||
(term-ctor List Cons
|
||
(app f h)
|
||
(app map f t)))))))
|
||
```
|
||
|
||
Grammar core (3-rule lexical layer + ~25 named-form productions):
|
||
```
|
||
sexpr ::= atom | "(" sexpr* ")"
|
||
atom ::= integer | string | ident
|
||
ident ::= any maximal non-whitespace, non-paren run that is not
|
||
a recognised integer or string literal.
|
||
```
|
||
|
||
The lexer recognises one delimiter (`(` / `)`) and whitespace.
|
||
Every other maximal token is classified post-hoc:
|
||
- All-digit run with optional leading `-` → integer atom.
|
||
- `"`-delimited run → string atom.
|
||
- Otherwise → ident.
|
||
|
||
Consequence: operators like `+`, `==`, `<=`, `**`, qualified
|
||
names like `io/print_int`, and cross-module references like
|
||
`std_list.map` are all single ident tokens with no special lex
|
||
rule. The only reserved tokens are `(`, `)`, and whitespace.
|
||
Bool literals (`true`, `false`) and unit (`(lit-unit)`) are
|
||
disambiguated by parser context, not by lex.
|
||
|
||
Every AST node form has a unique head keyword (`module`, `data`,
|
||
`fn`, `forall`, `fn-type`, `con`, `var`, `app`, `lam`, `match`,
|
||
`case`, `pat-ctor`, `term-ctor`, `do`, `seq`, ...). A bare atom in
|
||
a positional slot (e.g. inside `(con List a)` second position) is
|
||
a name reference whose **sort** is determined by the parent slot:
|
||
|
||
- inside `(con NAME args...)` second-and-later positions → type
|
||
expression. Bare atom there ⇒ `Type::Var { name }`.
|
||
- inside `(app HEAD args...)` first position ⇒ `Term::Var`.
|
||
- inside `(pat-ctor CTOR fields...)` field positions ⇒
|
||
`Pattern::Var`.
|
||
- inside `(case PAT BODY)` second position ⇒ term.
|
||
|
||
There is **no lexical case rule**. To construct a value with a
|
||
ctor, write `(term-ctor TypeName CtorName args...)`. To match
|
||
against one, write `(pat-ctor CtorName fields...)`. Capitalised
|
||
identifiers carry no special meaning to the parser. This rules
|
||
out a class of silent errors ("I forgot to capitalise `Cons` and
|
||
it parsed as a function call").
|
||
|
||
**Pros:** smallest formal grammar of any candidate (the lexical
|
||
core is 3 rules; the named-form productions are uniform — every
|
||
node a tagged list). Foreign-LLM bar lowest. Round-trip with the
|
||
existing pretty-printer is a refactor of `pretty.rs` to emit this
|
||
tagged form, plus a new parser.
|
||
|
||
**Cons:** paren density is high. `(forall (vars a b) (fn-type
|
||
...))` has more visual nesting than the current pretty-printer's
|
||
`forall a. (...) -> ...`. Verbosity is ~2× JSON for the same node
|
||
when measured in characters, but ~8× shorter in lines (the
|
||
existing JSON `box.ail.json` of 160 lines becomes ~20 lines in
|
||
this form).
|
||
|
||
#### (B) Indented record-style with explicit terminators
|
||
|
||
```
|
||
module std_list
|
||
|
||
data List(a):
|
||
Nil
|
||
Cons(a, List(a))
|
||
end
|
||
|
||
fn map:
|
||
type: forall a b. fn(fn(a) -> b, List(a)) -> List(b)
|
||
params: f, xs
|
||
body:
|
||
match xs:
|
||
Nil => Nil
|
||
Cons(h, t) => Cons(f(h), map(f, t))
|
||
end
|
||
end
|
||
```
|
||
|
||
Grammar core (~20–30 productions): module-level (def/data/end), type
|
||
sub-grammar (forall, fn, con, var), term sub-grammar (lam, match,
|
||
ctor, app, lit, var, seq), pattern sub-grammar.
|
||
|
||
**Pros:** higher information density per line, closer to mainstream
|
||
ML/Haskell shape. **Cons:** four sub-grammars instead of one.
|
||
`forall a b. fn(...)` keeps a pseudo-precedence (`->` binds tighter
|
||
than the outer `fn(...)` wrapper). Foreign-LLM bar higher.
|
||
|
||
#### (C) Pretty-printer-as-source
|
||
|
||
Use exactly the format `pretty::module` already emits, plus a parser
|
||
that accepts it. The existing pretty-printer's quirks (`::` for
|
||
type-of, `[params]` for fn-params, `<a>` for type-args, `forall a. ...`,
|
||
`!IO`, `()` ambiguous between unit-arg-list and empty-form) become
|
||
the spec.
|
||
|
||
**Pros:** zero churn — the existing pretty-printer is already the
|
||
spec; only the inverse is missing. Round-trip is the identity by
|
||
construction. **Cons:** the existing format mixes four mini-dialects
|
||
(s-expr at term level, ML-shape at type level, square brackets for
|
||
params, `<>` for type args). Formalising it crisply is harder than
|
||
designing a uniform form from scratch.
|
||
|
||
### First choice and rollback plan
|
||
|
||
**Try (A) first.** Reasoning: constraint 1 (formalizable) outweighs
|
||
constraint readability. (A) has a 3-rule core grammar with one
|
||
lexical disambiguation rule. (B) doubles the rule count and
|
||
re-introduces a soft form of precedence (`->` inside `forall`).
|
||
(C) is tempting because it is zero-design but the resulting spec is
|
||
visibly heterogeneous, which is exactly what constraint 1 was meant
|
||
to rule out.
|
||
|
||
If implementing (A) reveals that paren density actively hurts my
|
||
authoring (measurable: I make more wrong-paren errors than the
|
||
JSON-AST shape produced before), roll back and try (C). (B) stays
|
||
on the shelf for a future iter only if both fail.
|
||
|
||
### Implementation outline (Iter 14c onwards, not done in 14b)
|
||
|
||
- `crates/ailang-surface` — new crate. **Strictly additive.** PEG
|
||
parser produces existing `ailang-core::ast` types. No new AST
|
||
nodes, no schema changes, no new hashable form. Pretty-printer
|
||
for form (A) lives here too (the round-trip is the contract).
|
||
- `ailang-check`, `ailang-codegen` are **not modified**. They
|
||
continue to consume `ailang-core::ast::Module` values regardless
|
||
of which projection produced them.
|
||
- Round-trip test: for every `examples/*.ail.json`, parse the
|
||
corresponding hand-written `*.ailx`, canonicalise, and assert
|
||
hash-equivalence to the original. Hash equivalence is the truth
|
||
check; the surface ships only if every fixture round-trips
|
||
identically.
|
||
- CLI: `ail parse <file.ailx> -o <file.ail.json>`. Symmetric to
|
||
existing `ail render`. **`.ail.json` remains a first-class input**
|
||
to every existing subcommand; the parser is a producer, not a
|
||
gatekeeper.
|
||
- Iter 14d: stdlib (`std_list`, `std_maybe`, ...) authored in
|
||
form (A) from day one **because that is the AI authoring
|
||
projection**, not because JSON authoring is forbidden. The
|
||
resulting `.ail.json` is what tests and downstream tools see.
|
||
|
||
### What this Decision deliberately does not do
|
||
|
||
- It does not promote form (A) to the source of truth. Form (A) is
|
||
one projection; the JSON-AST stays canonical.
|
||
- It does not foreclose visual or graphical front-ends. The crate
|
||
layout (`core` owns AST; `surface`/`visual`/... are siblings)
|
||
reserves that lane.
|
||
- It does not remove `.ail.json` as input. Every existing
|
||
CLI subcommand (`check`, `render`, `describe`, `emit-ir`,
|
||
`build`, `run`, `manifest`, `deps`, `diff`, `workspace`,
|
||
`builtins`) keeps its current `.ail.json` interface.
|
||
|
||
### Form refinements during Iter 14c implementation
|
||
|
||
Two productions in the original 14b sketch had to be widened
|
||
during implementation to round-trip the existing AST faithfully.
|
||
Captured here for the spec record:
|
||
|
||
1. **`lam-term` carries types and effects.** The AST's `Term::Lam`
|
||
stores parallel `params`, `param_tys`, `ret_ty`, and `effects`
|
||
fields. The 14b sketch had only names. The implemented form is
|
||
|
||
```
|
||
lam-term ::= "(" "lam" "(" "params" typed-param* ")"
|
||
"(" "ret" type ")"
|
||
effects-clause? body-attr ")"
|
||
typed-param ::= "(" "typed" ident type ")"
|
||
```
|
||
|
||
This keeps the no-precedence / one-construct-per-token-list
|
||
invariants and adds no new lexical rules.
|
||
|
||
2. **`import-clause` admits an optional alias.** The AST's
|
||
`Import.alias` is `Option<String>`; the original sketch only
|
||
supported the `None` case. The implemented form is
|
||
|
||
```
|
||
import-clause ::= "(" "import" ident ("as" ident)? ")"
|
||
```
|
||
|
||
`as` is a bare ident token in this position; no special lexical
|
||
rule is needed.
|
||
|
||
Neither change extends the grammar's rule budget meaningfully:
|
||
the 30-production ceiling of constraint 1 is intact (the parser
|
||
implements ~28 named productions). All 17 `examples/*.ail.json`
|
||
fixtures round-trip identically through `print → parse → canonical
|
||
JSON`; the three hand-written `.ailx` exhibits parse to canonical
|
||
JSON identical to their corresponding `.ail.json` files.
|
||
|
||
3. **Tail-call surface (Iter 14e).** Decision 8 ships two new
|
||
productions, both positional analogues of their non-tail
|
||
counterparts. Their result terms set `Term::App.tail = true` /
|
||
`Term::Do.tail = true`; the typechecker's `verify_tail_positions`
|
||
pass enforces that the marker is only used in tail position.
|
||
|
||
```
|
||
tail-app-term ::= "(" "tail-app" term term+ ")"
|
||
tail-do-term ::= "(" "tail-do" ident term* ")"
|
||
```
|
||
|
||
Production count after Iter 14e: ~30, still inside the 30-rule
|
||
constraint-1 budget. No new lexical rule (`tail-app` / `tail-do`
|
||
are bare ident tokens; no special casing).
|
||
|
||
## Decision 7: redundancy removal — `Term::If` is not a primitive
|
||
|
||
**Status: REVERTED in Iter 14g.** This decision was made on shaky grounds —
|
||
applying CLAUDE.md's "no redundancies" rule to a case that turned out to
|
||
be primitive control flow, not redundancy. The post-removal match-on-Bool
|
||
form (3× the tokens, asymmetric `pat-wild` for the false case) was
|
||
worse for token economy and worse for the natural shape of the language.
|
||
`Term::If` is restored. The text below is preserved for the audit trail.
|
||
|
||
`Term::If { cond, then, else_ }` is semantically a subset of
|
||
`Term::Match` on `Bool`. Per CLAUDE.md the language must contain no
|
||
redundancies; two AST nodes for the same operation produces an
|
||
authoring decision with no semantic content and an extra codegen
|
||
path. Iter 14d removes `Term::If`. Migration shape on the JSON side:
|
||
|
||
{"t":"if","cond":C,"then":A,"else":B}
|
||
→
|
||
{"t":"match","scrutinee":C,
|
||
"arms":[
|
||
{"pat":{"p":"lit","lit":{"kind":"bool","value":true}},"body":A},
|
||
{"pat":{"p":"wild"},"body":B}]}
|
||
|
||
The wildcard arm satisfies the typechecker's
|
||
`primitive-needs-wildcard` rule. A future iter may upgrade the
|
||
exhaustiveness check to recognise the `true`+`false` arm pair as
|
||
covering Bool without a wildcard; until then, wildcard is the
|
||
canonical migration target.
|
||
|
||
No schema version bump (no third-party consumes `ailang/v0`).
|
||
Hash invalidation for the three migrated fixtures (`sum`, `sort`,
|
||
`max3`) is intentional; the new hashes become the new identity.
|
||
|
||
## Decision 8: explicit, verified tail calls
|
||
|
||
For an LLM author, recursion is the natural iteration form
|
||
(`\n. if n == 0 then () else loop(n-1)` is what I reach for, not
|
||
a `for`-loop). Without a tail-call guarantee, every recursive
|
||
program has a silent stack-depth ceiling that no compile-time
|
||
diagnostic warns about. That is exactly the class of correctness
|
||
hazard the language exists to eliminate.
|
||
|
||
Solution: explicit, verified tail calls.
|
||
|
||
- **AST.** `Term::App { fn, args, tail: bool }` and
|
||
`Term::Do { op, args, tail: bool }` gain a `tail` flag,
|
||
serde-defaulting to `false` so existing fixtures load with
|
||
`tail: false` and their hashes stay bit-identical.
|
||
- **Typecheck.** A new pass `verify_tail_positions(fn_body)`
|
||
runs after the main type-check. It walks the body with an
|
||
`is_tail_context: bool` threaded down. The flag is `true` at
|
||
the start, `true` for the body of every `Term::Match` arm,
|
||
`true` for the right operand of `Term::Seq`, `true` for the
|
||
body of `Term::Let`, `true` for the body of `Term::Lam` (each
|
||
Lam opens its own tail scope). The flag is `false` for: args
|
||
of any `App`/`Do`/`Ctor`, scrutinee of `Match`, left of
|
||
`Seq`, condition of `Let`-bound expression. When the walker
|
||
visits an `App { tail: true }` or `Do { tail: true }`, the
|
||
flag must be `true` at that visit; otherwise emit diagnostic
|
||
`tail-call-not-in-tail-position`.
|
||
- **Codegen.** Emit `musttail call` (LLVM IR) for marked calls
|
||
instead of plain `call`. LLVM rejects at IR-verification
|
||
time if the call cannot physically be a tail call (calling
|
||
convention mismatch, signature divergence, etc.). The reject
|
||
surfaces as a hard build error, not a silent runtime
|
||
surprise.
|
||
- **Form (A).** Two new keywords: `tail-app`, `tail-do`.
|
||
Productions are positional analogues of `app`/`do` with
|
||
`tail: true` set on the resulting term. EBNF gains 2 lines;
|
||
total production count goes from ~28 to ~30, still inside
|
||
the constraint-1 budget.
|
||
|
||
**What this does NOT promise.** Per the 14d tail-call survey,
|
||
many existing recursive calls are *not* in tail position
|
||
because they are arguments to constructor calls (e.g.
|
||
`Cons (f h) (map f t)`). 14e adds annotation + verification;
|
||
it does **not** add a CPS transform or accumulator-form
|
||
rewrite. Programs whose recursion is constructor-blocked
|
||
will continue to be stack-bounded by recursion depth. The
|
||
canonical authoring pattern in such cases is to write the
|
||
accumulator-form variant (`map_acc`, `fold_left`, etc.)
|
||
explicitly. The stdlib (15a onward) ships both forms where
|
||
relevant.
|
||
|
||
The 14d migration of existing fixtures will be partial: only
|
||
`print_list`-style terminal recursions get marked. The
|
||
constructor-blocked recursions in `map`, `sort`, `insert`
|
||
remain unmarked — they cannot benefit from `musttail`
|
||
without a source-level rewrite.
|
||
|
||
## Decision 9: transitional allocator — Boehm conservative GC
|
||
|
||
**Status: superseded by Decision 10 (RC + Uniqueness, 2026-05-08).**
|
||
This section documents the active runtime as of Iter 17a / the
|
||
GC bench, but it is no longer the canonical memory model. Boehm
|
||
remains linked behind `--alloc=gc` (the current default) until
|
||
the RC pipeline (Iters 18a–18d) is validated and the default
|
||
flips. The `--alloc=bump` mode introduced for the bench is a
|
||
measurement tool, not a production target.
|
||
|
||
Through Iter 14e, every ADT box, lambda env, and closure pair was
|
||
allocated with bare `malloc` and never freed. That worked for the
|
||
17 test fixtures (all small, all short-lived) but is incompatible
|
||
with any real workload — a stdlib `fold` over a million-element
|
||
list would leak a million boxes. The "Goal" section's "no GC for
|
||
the MVP" framing predates the parameterised-ADT pipeline (Iter 13)
|
||
and the explicit-recursion expectation (Iter 14e); both make a
|
||
collector necessary.
|
||
|
||
**Choice: Boehm-Demers-Weiser conservative GC.** The simplest
|
||
working option:
|
||
|
||
- Replace `malloc(...)` with `GC_malloc(...)` in every IR site
|
||
(currently `lower_ctor`'s ADT box, `lower_lambda`'s env block
|
||
and closure pair).
|
||
- Replace the IR-level `declare ptr @malloc(i64)` with
|
||
`declare ptr @GC_malloc(i64)`.
|
||
- Add `-lgc` to the `clang` link command (in
|
||
`crates/ail/src/main.rs`'s `Build` / `Run` paths).
|
||
- No language-level change. No AST change. No schema change.
|
||
|
||
Rationale:
|
||
|
||
- **Mature.** Boehm has been the default conservative GC for
|
||
decades. Linux distros ship it as `libgc` / `libgc-dev` /
|
||
`gc` (Arch).
|
||
- **No language work.** Conservative scan of the C stack handles
|
||
AILang's stack frames without LLVM stack-map infrastructure
|
||
(which is its own multi-iter design).
|
||
- **Single-iter integration.** Lift-and-shift of the four
|
||
allocation sites; all existing tests must still pass with
|
||
identical output.
|
||
|
||
Trade-offs accepted:
|
||
|
||
- **Conservative over-retention.** A user-supplied `Int` field
|
||
whose value happens to coincide with a heap address will pin
|
||
that allocation. In practice, vanishingly rare for typical
|
||
values; survivable.
|
||
- **Pause time non-deterministic.** Boehm uses stop-the-world
|
||
mark-sweep. For LLM-author-written stdlib code at MVP scale,
|
||
pause times are not the bottleneck.
|
||
- **Build-time dependency.** `libgc` must be installed on the
|
||
build host. Users without it get a link-time error from
|
||
clang, not a silent failure.
|
||
|
||
A future iter may layer a per-fn-arena optimisation on top: when
|
||
a fn's return type contains no boxed ADT, ADT boxes allocated
|
||
inside that fn cannot escape, so an arena freed at fn return is
|
||
sound by construction (per the 14e GC notes). That requires
|
||
escape analysis, the corresponding AST/IR plumbing, and is its
|
||
own design pass. Boehm-everything is the floor; arena is an
|
||
optimisation above it.
|
||
|
||
### Per-fn arena via stack `alloca` (Iter 17a)
|
||
|
||
Iter 17a layers exactly that optimisation, in its simplest form.
|
||
`ailang-codegen` runs an escape-analysis pre-pass over every fn
|
||
body (and every lifted lambda thunk body); allocations the pass
|
||
proves do not outlive the fn frame are lowered to LLVM `alloca`
|
||
instead of `@GC_malloc`. Allocations that may escape continue to
|
||
use `@GC_malloc`. The Boehm collector is still linked and
|
||
unchanged; this is purely an optimisation above the floor.
|
||
|
||
**Allocation mechanism: LLVM `alloca`** (not a heap arena). Stack
|
||
allocation matches the "freed at fn return" lifetime exactly,
|
||
needs no malloc/free pair, and integrates with LLVM's existing
|
||
optimiser (mem2reg / SROA may further promote the alloca'd box
|
||
to registers if the box is small and its uses are simple). No
|
||
new runtime is introduced; no language-level change; no AST or
|
||
schema change.
|
||
|
||
**Escape rule (conservative).** A `Term::Ctor` or `Term::Lam`
|
||
allocation is non-escaping iff (1) it is the value of a
|
||
`Term::Let { name = X, value = ALLOC, body = B }`, and (2) the
|
||
body `B` does not let any value derived from `X` flow past the
|
||
fn frame. "Derived from" follows two propagation rules:
|
||
- A `Term::Match` whose scrutinee is a `Var` referring to a
|
||
tainted name propagates taint to every pattern-bound name in
|
||
every arm. (Pattern bindings hold field projections of the
|
||
scrutinee, which live inside the same allocation.)
|
||
- A `Term::Let { name = Y, value = Var(t), ... }` where `t` is
|
||
tainted makes `Y` tainted in the let's body.
|
||
|
||
A tainted name "escapes" if it appears in any of: the tail
|
||
position of `B`, the arg list of any `Term::App` / `Term::Do`,
|
||
the field list of a `Term::Ctor`, or the free-var capture set of
|
||
a `Term::Lam`. The closure-pair-callee position of `Term::App`
|
||
where the callee is a bare `Var` to the tainted name is NOT an
|
||
escape (calling locally is fine).
|
||
|
||
**What this is not.** Not a region-inference system. Not
|
||
flow-sensitive within an arm. Not field-sensitive (pattern
|
||
bindings are tainted wholesale). Precision can be improved later;
|
||
correctness is the priority for this iter. A pessimistic answer
|
||
(claiming an allocation escapes when it does not) only loses
|
||
optimisation, never correctness.
|
||
|
||
**Codegen integration.** Three sites in
|
||
`ailang-codegen/src/lib.rs`:
|
||
- `lower_ctor` — ADT box.
|
||
- `lower_lambda` env block (when there are captures).
|
||
- `lower_lambda` closure pair (always 16 bytes).
|
||
|
||
Each site queries the per-fn `non_escape: BTreeSet<usize>` (raw
|
||
pointer addresses of `Term::Ctor` / `Term::Lam` AST nodes flagged
|
||
as non-escaping). On a hit the emitter writes
|
||
`alloca i8, i64 <size>, align 8`; on a miss it writes
|
||
`call ptr @GC_malloc(i64 <size>)`. The rest of the lowering (tag
|
||
store, field stores, closure-pair packing) is identical.
|
||
|
||
The closure-pair and its env share an escape verdict — they have
|
||
parallel lifetimes. If the closure pair is non-escaping, the env
|
||
is too.
|
||
|
||
## Decision 10: memory model — RC + Uniqueness with LLM-author annotations
|
||
|
||
**Committed 2026-05-08, after the GC bench (`bench/run.sh`) showed
|
||
Boehm contributing ~60% of runtime on allocation-heavy workloads
|
||
that hold the heap fully live. Sharpened later the same day: the
|
||
mainstream "RC + inference" position was extended with mandatory
|
||
LLM-author mode annotations (`borrow` / `own`), explicit `clone`,
|
||
first-class `reuse-as`, and `drop-iterative` data attrs.**
|
||
|
||
The cost of GC is structurally in the allocate path — Boehm's
|
||
`GC_malloc` is ~2.8× slower than a bump pointer, and the bench
|
||
workloads exercised allocate cost without collection cost.
|
||
Tracing GC's irreducible variability cannot be tuned away; RC's
|
||
costs are bounded and analysable per program point. A corpus
|
||
committed to one memory model is expensive to switch — pre-
|
||
stdlib is the cheapest moment to commit.
|
||
|
||
**Choice.** AILang's canonical memory model is reference counting
|
||
with static uniqueness inference **and explicit LLM-author
|
||
annotations on fn signatures**, in the lineage of Lean 4 / Roc /
|
||
Koka. Boehm becomes a transitional allocator (Decision 9) and is
|
||
retired when the RC pipeline matches the bump-allocator floor
|
||
within an acceptable margin (target 1.3× on `bench/run.sh`).
|
||
|
||
The architecture has two layers:
|
||
|
||
1. **Inference.** A post-typecheck pass produces a per-node
|
||
uniqueness side table. Codegen uses it to elide inc/dec
|
||
wherever provably redundant.
|
||
2. **LLM-author annotations.** Fn signatures carry mandatory
|
||
`(borrow T)` / `(own T)` mode markers. Authors mark
|
||
sharing-vs-consumption explicitly. The compiler verifies
|
||
rather than guesses.
|
||
|
||
The combination plays to what LLMs are good at (writing slightly
|
||
more annotation per definition) and avoids what compilers are
|
||
bad at (proving sharing absent in the face of recursion +
|
||
closures + match).
|
||
|
||
### Why not other memory models
|
||
|
||
**Tracing GC.** Open-ended. Boehm's bench number (~60% allocate-
|
||
path overhead) is structural; tuning Boehm cannot move that
|
||
needle. A precise tracing GC would need read/write barriers,
|
||
root maps, generational machinery — months of work, with
|
||
irreducible pause-time variability at the end. The user's
|
||
framing was decisive: "Am GC kannst du ewig rumschrauben (und
|
||
bekommst trotzdem auch in 100 Jahren keine berechnbare
|
||
Performance)."
|
||
|
||
**Region inference (Tofte/Talpin / MLton-style).** Considered
|
||
seriously; rejected. Regions tie lifetimes to dynamic scope —
|
||
every value lives in some region, regions stack on entry/exit,
|
||
deallocation is bulk-by-region. The reduction: a region is an
|
||
explicit allocator with sugar plus a static check that nothing
|
||
escapes its lifetime. The deeper problem: regions assume
|
||
**stack-shaped lifetimes**. Real programs have non-stack-shaped
|
||
lifetimes — caches, memo tables, registries, lookup structures
|
||
whose lifetimes are not nested. Regions would either force these
|
||
into a `letregion` at the top of `main` (everyone's allocator
|
||
becomes the root region — useless), or require a region per
|
||
cache variant (combinatorial). RC has no lifetime-shape
|
||
assumption; it works for any DAG.
|
||
|
||
**Linear / ownership types as primary mechanism (Rust-style).**
|
||
Considered as a general-purpose alternative; rejected as primary.
|
||
Rust's borrow-checker is a great mechanism but requires the
|
||
author to thread lifetimes through every signature and accept
|
||
that some programs cannot be expressed without `unsafe`. For an
|
||
LLM-targeted language with recursion + closures everywhere, that
|
||
cost is too high — most of the source surface would be lifetime
|
||
annotations rather than logic. AILang uses a *subset* of these
|
||
ideas (mode annotations, linear consumption discipline)
|
||
selectively, layered on top of RC, where the annotations buy
|
||
concrete optimisations and never have to thread lifetimes
|
||
through callees.
|
||
|
||
### The LLM-aware sharpening
|
||
|
||
A mainstream RC implementation (think Lean 4 in default mode)
|
||
infers everything from naked AST plus a few optional hints. The
|
||
inference is conservative; whatever it can't prove unique becomes
|
||
shared and pays runtime inc/dec. AILang exploits its target
|
||
audience to push that conservative ceiling higher.
|
||
|
||
Five mechanisms.
|
||
|
||
**(1) Mandatory `(borrow T)` / `(own T)` on fn signatures.**
|
||
|
||
```
|
||
(fn list_length
|
||
(type (fn-type (params (borrow (List Int))) (ret (con Int))))
|
||
...)
|
||
|
||
(fn sum_list_consume
|
||
(type (fn-type (params (own (List Int))) (ret (con Int))))
|
||
...)
|
||
```
|
||
|
||
`(borrow T)` declares the parameter is read-only and lives at
|
||
most until the call returns; the caller still owns it; the
|
||
callee performs no inc/dec on it. `(own T)` declares ownership
|
||
transfer; the callee consumes the value and is responsible for
|
||
its end-of-life. The declaration is structural (visible in JSON)
|
||
and binding (the typechecker rejects bodies that contradict it).
|
||
|
||
For a Lean 4 / Roc author this is all *optional* and inferred
|
||
when omitted. AILang makes it mandatory because the LLM author
|
||
can carry the cognitive cost trivially, and the compiler gains a
|
||
precise contract at every call site instead of a probabilistic
|
||
guess.
|
||
|
||
**(2) Linear-by-default consumption with explicit `(clone X)`.**
|
||
|
||
In bodies, every binder is consumed by exactly one `own`-mode
|
||
use. If the LLM writes:
|
||
|
||
```
|
||
(let p (expensive_fn x)
|
||
(let r1 (consume_a p) ; consume_a takes (own); consumes p
|
||
(let r2 (consume_b p) ; ERROR: p already consumed
|
||
...)))
|
||
```
|
||
|
||
the compiler emits a structured non-linear-use diagnostic with
|
||
concrete `suggested_rewrites`:
|
||
|
||
- "make consume_a borrow": refactor consume_a's signature, no
|
||
body change at the call site;
|
||
- "explicit clone": insert `(clone p)` at the first use;
|
||
- "fuse traversal": replace the two separate calls with a fused fn.
|
||
|
||
The LLM picks one. There is no implicit clone — sharing always
|
||
costs visible source.
|
||
|
||
**(3) Reuse hints as first-class.**
|
||
|
||
```
|
||
(fn map_inc
|
||
(type (fn-type (params (own (List Int))) (ret (own (List Int)))))
|
||
(params xs)
|
||
(body
|
||
(match xs
|
||
(case Nil Nil)
|
||
(case (Cons h t)
|
||
(reuse-as xs (term-ctor List Cons (app + h 1) (app map_inc t)))))))
|
||
```
|
||
|
||
`(reuse-as SRC NEW-CTOR)` asks the codegen to allocate `NEW-CTOR`
|
||
in `SRC`'s memory slot. Compiler verifies: `SRC` is owned, this
|
||
is its last use, sizes match. On a hit: no malloc, no free — the
|
||
box is overwritten in place. On a miss: structured diagnostic
|
||
explains which precondition failed; the LLM either adjusts the
|
||
surrounding code or removes the hint.
|
||
|
||
This matches Lean 4 / Roc reuse analysis but lifts it from
|
||
"compiler-inferred when possible" to "author-asserted, compiler-
|
||
verified". The LLM applies it everywhere it expects to fire and
|
||
lets the compiler bounce the request when it can't.
|
||
|
||
**(4) `(drop-iterative)` annotation on data declarations.**
|
||
|
||
```
|
||
(data Tree (vars a)
|
||
(ctor Leaf)
|
||
(ctor Node a (Tree a) (Tree a))
|
||
(drop-iterative))
|
||
```
|
||
|
||
When the refcount of a `Tree` value reaches zero, the synthesised
|
||
dec-on-zero traversal is iterative (worklist + heap-allocated
|
||
stack) instead of recursive. Avoids stack overflow on deep
|
||
structures. The LLM adds the annotation where appropriate; the
|
||
compiler refuses to emit recursive dec-cascade on annotated types.
|
||
|
||
**(5) Structured compiler diagnostics with `suggested_rewrites`.**
|
||
|
||
Every RC-mode error (use-after-consume, mode-mismatch,
|
||
reuse-as-fail, drop-cascade-too-deep) emits a JSON object
|
||
containing the failure kind, the source span, and a list of
|
||
concrete rewrite suggestions in form-A AILang. The LLM consumes
|
||
these without prose-parsing. This is the missing half of the
|
||
LLM-as-author story: the language spec defines not only what
|
||
compiles, but what the compiler tells the author when it doesn't.
|
||
|
||
### Language-design constraints (binding)
|
||
|
||
The four constraints below are necessary preconditions for RC to
|
||
be sound and complete *without* a cycle-collector backstop. They
|
||
are not new — AILang already satisfies all four — but Decision 10
|
||
makes them load-bearing rather than incidental:
|
||
|
||
1. **Strict evaluation.** Every `Term::App` argument is fully
|
||
evaluated before the call. No laziness, no thunks. (Already
|
||
true.)
|
||
2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
|
||
`EXPR` in a scope where `x` is *not* bound. Recursion is
|
||
exclusively via `Term::LetRec` (which binds a fn, not a value)
|
||
and module-level fn defs. (Already true.)
|
||
3. **No shared mutable refs.** Values are immutable once
|
||
constructed. There is no `ref`, `IORef`, `Mutex`, or any
|
||
primitive that allows a value to be mutated from a position
|
||
outside its allocation. (Already true.)
|
||
4. **ADTs are acyclic by construction.** Strict evaluation +
|
||
no-recursive-value-bindings + no-shared-mutable-refs together
|
||
guarantee that any value graph reachable from a binding is a
|
||
DAG. The reference graph has no cycles. (Follows from 1–3.)
|
||
|
||
A future iter that proposes any of laziness, recursive value
|
||
bindings, shared mutable state, or any feature that creates
|
||
cycles must either prove the cycle is collectible by an
|
||
extension (e.g. linear ownership) or be rejected at design time.
|
||
|
||
### Schema additions
|
||
|
||
**Iter 18a — mode wrappers on `Type`.**
|
||
|
||
```
|
||
Type::Borrow(Box<Type>) ; `(borrow T)` in form-A
|
||
Type::Own(Box<Type>) ; `(own T)` in form-A
|
||
```
|
||
|
||
Both are transparent for unification (they erase to their inner
|
||
`Type` for HM purposes) but carry binding mode metadata for the
|
||
RC pipeline. Skipped during JSON serialisation when absent so
|
||
canonical hashes of every pre-18a fixture stay bit-identical.
|
||
The legacy `(con T)` form is treated as `(own T)` semantically
|
||
throughout the 18-series; a later iter (deferred) makes the
|
||
explicit annotation mandatory and rejects bare `(con T)` for
|
||
boxed parameter types.
|
||
|
||
**Iter 18c/18d — new `Term` variants.**
|
||
|
||
```
|
||
Term::Clone { value: Box<Term> } ; `(clone X)` — explicit RC inc
|
||
Term::ReuseAs { source: Box<Term>, body: Box<Term> } ; `(reuse-as SRC NEW-CTOR)`
|
||
```
|
||
|
||
**Iter 18e — `TypeDef` attribute.**
|
||
|
||
```
|
||
TypeDef.drop_iterative: bool ; `(drop-iterative)`
|
||
```
|
||
|
||
All four are skipped during serialisation when absent / false /
|
||
None so canonical-JSON hashes of every fixture remain stable
|
||
until the fixture intentionally adopts the feature.
|
||
|
||
### Inference algorithm (Iter 18c)
|
||
|
||
Post-typecheck, post-`lift_letrecs`, pre-codegen pass over the
|
||
elaborated module. For each `Term` node that produces or binds a
|
||
boxed value, the pass computes a uniqueness flag:
|
||
|
||
- **Unique:** at this program point, the reference is the only
|
||
outstanding reference to its referent.
|
||
- **Shared:** there may be multiple outstanding references.
|
||
|
||
A reference is *unique* if every path from its allocation to the
|
||
current program point passes through exactly one binding. The
|
||
inference is a forward dataflow over the AST. The annotations
|
||
from 18a (`borrow` / `own`) provide the inter-fn contract; the
|
||
inference fills in intra-fn detail. (Implementer-level detail in
|
||
the Iter 18c brief.)
|
||
|
||
### Codegen contract (Iter 18b, 18c)
|
||
|
||
Memory layout (Iter 18b):
|
||
|
||
- Every heap allocation has an 8-byte refcount header, followed
|
||
by the payload. `ailang_rc_alloc(size)` returns a pointer to
|
||
the *payload*; the header is at `ptr - 8`.
|
||
- `ailang_rc_inc(ptr)`: load `ptr - 8`, +1, store. Non-atomic
|
||
(single-threaded).
|
||
- `ailang_rc_dec(ptr)`: load, -1, store; if zero, recurse-dec
|
||
child references and `free(ptr - 8)`. For `(drop-iterative)`
|
||
types, the recursion is replaced by a worklist loop (Iter 18e).
|
||
|
||
Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under
|
||
`--memory=rc` calls `ailang_rc_alloc(SIZE)`. Iter 18b stops there
|
||
— inc/dec instrumentation is added in Iter 18c, once the
|
||
inference is wired up. Until then, `--memory=rc` deliberately
|
||
leaks like the pre-Boehm era; this is purely about plumbing.
|
||
|
||
### Migration plan
|
||
|
||
1. **Iter 18a:** `(borrow T)` / `(own T)` annotations as a
|
||
language feature. Schema, parser, JSON, typechecker. No
|
||
codegen change. `(con T)` ≡ `(own T)`. Existing fixtures
|
||
unchanged.
|
||
2. **Iter 18b:** RC runtime. `runtime/rc.c` with header layout +
|
||
alloc/inc/dec. Codegen `--memory=rc` routes allocation through
|
||
`rc_alloc`; **no inc/dec yet**. `--memory=gc` remains default.
|
||
3. **Iter 18c:** uniqueness inference + codegen inc/dec
|
||
instrumentation. Combines 18a's annotations with intra-fn
|
||
dataflow. Linear-by-default enforcement turns on. `(clone X)`
|
||
in the `Term` schema.
|
||
4. **Iter 18d:** reuse hints + reuse analysis. `(reuse-as ...)`
|
||
form. Codegen rewrites dec+malloc into in-place overwrite when
|
||
the precondition holds.
|
||
5. **Iter 18e:** `(drop-iterative)` data attr. Worklist-based
|
||
free for annotated types.
|
||
6. **Iter 18f:** RC validation bench. If RC within 1.3× of bump
|
||
on `bench/run.sh`, retire Boehm: flip default to RC, drop
|
||
`-lgc`, mark Decision 9 historical.
|
||
|
||
### Adjacent extensions for mutability (out of Decision 10's scope)
|
||
|
||
If future workloads need mutable arrays, hash tables, or other
|
||
inherently mutable primitives, the answer is **not** a tracing GC
|
||
backstop. The answer is a separate ownership/linear extension
|
||
that gates mutability behind static single-owner discipline. RC
|
||
+ uniqueness is the universal floor; ownership extends it for
|
||
specific high-performance primitives without rebreaking the
|
||
acyclicity invariant. Concrete design deferred until the need
|
||
materialises with a real workload.
|
||
|
||
### What this Decision deliberately does not do
|
||
|
||
- **Does not infer everything.** An earlier draft of this
|
||
Decision said "uniqueness is fully inferred" — that was the
|
||
mainstream RC position. The 2026-05-08 follow-up discussion
|
||
replaced it: AILang demands annotations *because* the LLM
|
||
author can produce them effortlessly. The compiler does
|
||
inference *plus* verification of contracts.
|
||
- **Does not require existing fixtures to migrate immediately.**
|
||
Iter 18a treats `(con T)` as `(own T)`. Existing JSON hashes
|
||
stay bit-identical until the fixture is intentionally updated.
|
||
- **Does not commit to atomic refcounts.** AILang is currently
|
||
single-threaded. If/when concurrency arrives, atomic-vs-non-
|
||
atomic will be a separate decision per allocation kind.
|
||
- **Does not introduce regions.** Regions were considered and
|
||
rejected; see "Why not other memory models" above.
|
||
|
||
## Mangling scheme (Iter 5c)
|
||
|
||
All AILang functions are mangled to `@ail_<module>_<def>` — even in the
|
||
single-module case. Constants likewise (`@ail_<module>_<const>`). Global
|
||
string literals carry a short hint for readability:
|
||
`@.str_<module>_<hint>_<idx>` (e.g. `@.str_sum_fmt_int_0`). The entry point
|
||
is a `define i32 @main()` trampoline (C / LLVM ABI) that calls
|
||
`@ail_<entry-module>_main()`. `source_filename` exists exactly once per
|
||
workspace and carries the entry-module name (`<entry-module>.ail`).
|
||
|
||
## Convention: qualified cross-module references (Iter 5b)
|
||
|
||
Cross-module calls use **no** new AST node. Instead, a `Term::Var { name }`
|
||
with exactly one dot in the name is a qualified reference: `<prefix>.<def>`.
|
||
|
||
- `<prefix>` is an import alias (`import { module: "X", as: "<prefix>" }`)
|
||
or, when imported without an alias, the module name itself.
|
||
- `<def>` is the name of a top-level definition in the target module.
|
||
- Def names MUST NOT contain a dot — the typechecker reports
|
||
`invalid-def-name` with `ctx: { "reason": "contains-dot" }`.
|
||
- The workspace loader (Iter 5a) finds all reachable modules; the
|
||
typechecker (Iter 5b, `check_workspace`) resolves dotted names through the
|
||
import map. Diagnostic codes: `unknown-module` (prefix not imported),
|
||
`unknown-import` (module found, def not).
|
||
|
||
Hash stability: no new AST node, no renamed fields — all previous module
|
||
hashes stay bit-identical.
|
||
|
||
## Data model (MVP)
|
||
|
||
### Module
|
||
|
||
```jsonc
|
||
{
|
||
"schema": "ailang/v0",
|
||
"name": "<id>",
|
||
"imports": [{ "module": "<id>", "as": "<id>" }],
|
||
"defs": [Def...]
|
||
}
|
||
```
|
||
|
||
### Def
|
||
|
||
`kind ∈ { "fn", "type", "effect", "const" }`. In the MVP only `fn` and `const`.
|
||
|
||
```jsonc
|
||
{
|
||
"kind": "fn",
|
||
"name": "<id>",
|
||
"type": Type,
|
||
"params": ["<id>"...],
|
||
"body": Term,
|
||
"doc": "<optional string>"
|
||
}
|
||
```
|
||
|
||
### Term (expression)
|
||
|
||
```jsonc
|
||
{ "t": "lit", "lit": { "kind": "int" | "bool" | "unit", "value": ... } }
|
||
{ "t": "var", "name": "<id>" }
|
||
{ "t": "app", "fn": Term, "args": [Term...] }
|
||
{ "t": "let", "name": "<id>", "value": Term, "body": Term }
|
||
{ "t": "if", "cond": Term, "then": Term, "else": Term }
|
||
{ "t": "do", "op": "<eff>/<op>", "args": [Term...] }
|
||
{ "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }
|
||
{ "t": "match", "scrutinee": Term, "arms": [Arm...] }
|
||
{ "t": "lam",
|
||
"params": ["<id>"...],
|
||
"paramTypes": [Type...],
|
||
"retType": Type,
|
||
"effects": ["<id>"...],
|
||
"body": Term }
|
||
{ "t": "seq", "lhs": Term, "rhs": Term }
|
||
```
|
||
|
||
In the MVP, `do` is only a direct call to a built-in effect op (no handler).
|
||
A `lam` term constructs an anonymous function value; free variables of
|
||
its body are captured from the enclosing scope (see Iter 8 closure
|
||
conversion in JOURNAL). A `seq` term evaluates `lhs` for its effects
|
||
(its result must be Unit) and yields `rhs`'s value — equivalent to
|
||
`let _ = lhs in rhs`.
|
||
|
||
### Type
|
||
|
||
```jsonc
|
||
{ "k": "con", "name": "Int" }
|
||
{ "k": "con", "name": "Bool" }
|
||
{ "k": "con", "name": "Unit" }
|
||
{ "k": "fn", "params": [Type...], "ret": Type, "effects": ["IO"...] }
|
||
{ "k": "var", "name": "a" }
|
||
{ "k": "forall", "vars": ["a"...], "body": Type }
|
||
```
|
||
|
||
## Pipeline
|
||
|
||
```
|
||
.ail.json ─┐
|
||
├─ load + validate schema
|
||
├─ resolve names + assign hashes
|
||
├─ desugar (AST → AST, Iter 16a)
|
||
├─ typecheck (HM, effect rows)
|
||
├─ lift_letrecs (post-typecheck AST → AST, Iter 16b.3)
|
||
├─ lower to MIR (SSA-like, named SSA values)
|
||
├─ emit LLVM IR (.ll)
|
||
└─ clang -O2 *.ll -o binary (links libgc for @GC_malloc)
|
||
```
|
||
|
||
The **desugar** pass (`ailang-core::desugar::desugar_module`) runs
|
||
before typecheck and codegen in every entry point of `ailang-check`
|
||
and `ailang-codegen`. It is a pure AST → AST rewriter — currently
|
||
only flattens nested constructor patterns (16a), but is the chosen
|
||
home for any future surface-smoothing rewrites that should not bloat
|
||
the core AST or the backends. **Critical invariant:** `CheckedModule.symbols`
|
||
in the `check` entry point continues to hash from the *original*
|
||
on-disk module, not the desugared one, so `ail diff` and `ail manifest`
|
||
report identities that match the canonical JSON the user is editing.
|
||
|
||
The **lift_letrecs** pass (`ailang-check::lift_letrecs`, Iter 16b.3)
|
||
runs **after** typecheck and **before** codegen, but only on the
|
||
`build` / `run` paths — the `check` subcommand stops at typecheck
|
||
and never sees a lifted module. It eliminates every `Term::LetRec`
|
||
that the desugar pass left in place (the case where at least one
|
||
capture is `Term::Let`-bound, so its type is only knowable after
|
||
inference). The output is a module with synthetic `<hint>$lr_N`
|
||
top-level fns appended, ready for codegen. Synthetic FnDefs added
|
||
by this pass do **not** appear in `CheckedModule.symbols` — same
|
||
invariant as the 16b.2 lifts in desugar.
|
||
|
||
## CLI
|
||
|
||
```
|
||
ail check <module.ail.json> — loads, validates, typechecks
|
||
ail manifest <module.ail.json> — table: name :: type !effects [hash]
|
||
ail describe <module> <name> — detail of a definition (form-A body)
|
||
ail render <module.ail.json> — JSON-AST → form-A text (exact inverse of `parse`)
|
||
ail parse <module.ailx> — form-A text → canonical JSON-AST
|
||
ail deps <module.ail.json> — list cross-module references
|
||
ail diff <a.ail.json> <b.ail.json> — content-addressed def-level diff
|
||
ail workspace <entry.ail.json> — list all modules transitively reachable from entry
|
||
(`--json` for machine output;
|
||
`manifest --workspace` and `diff --workspace`
|
||
extend single-module subcommands to workspaces)
|
||
ail builtins — list built-in fns and effect ops
|
||
ail emit-ir <module> — writes .ll
|
||
ail build <module> — full pipeline → binary
|
||
ail run <module> — build + execute (tempdir), passthrough exit code
|
||
```
|
||
|
||
## Verification and correctness (across cycles)
|
||
|
||
1. **Snapshot tests** for the pretty-printer and IR emit. The diff makes
|
||
regressions visible immediately.
|
||
2. **Property tests** for the JSON ↔ pretty-print roundtrip.
|
||
3. **End-to-end tests** for `examples/` with expected program output.
|
||
4. **Hash stability**: a test ensures the same def always produces the same
|
||
hash.
|
||
5. **CI pin** of the outputs in `tests/expected/`.
|
||
6. **Rustdoc cleanliness**: `cargo doc --no-deps` runs warning-free.
|
||
Maintained by the `ailang-docwriter` agent (Iter 13d onward); fixing a
|
||
rustdoc warning is part of the iter that introduced it, not a follow-up.
|
||
|
||
## What is not (yet) supported
|
||
|
||
Snapshot of the boundary as of Iter 16a. Items move out of this list
|
||
as iterations land; the JOURNAL records the exact iteration. Recently
|
||
**lifted** gates that used to live here: cross-module ADTs (lifted in
|
||
Iter 14h via qualified `module.Type` / `module.Ctor` references in
|
||
both `(con ...)` and `(term-ctor ...)` / `(pat-ctor ...)` positions);
|
||
GC for ADT boxes, lambda envs, and closure pairs (Boehm conservative
|
||
collector wired up in Iter 14f, see Decision 9); nested constructor
|
||
sub-patterns inside `match` (lifted in Iter 16a via the desugar pass);
|
||
literal sub-patterns inside a Ctor pattern (lifted in Iter 16c — the
|
||
desugar pass rewrites every `Pattern::Lit` to a `Term::If` on `==`,
|
||
both at the top level of an arm and inside a Ctor sub-pattern);
|
||
`==` extended from Int-only to a polymorphic
|
||
`forall a. (a, a) -> Bool` over `Int`/`Bool`/`Str`/`Unit` (lifted
|
||
in Iter 16e — codegen monomorphises and dispatches on the
|
||
resolved arg type; ADT/Fn arg types are rejected at codegen).
|
||
|
||
- No effect handlers — only the built-in IO and Diverge ops.
|
||
- No refinements / SMT escalation.
|
||
- 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 local recursive `let`. `let f = ... in ...` only sees `f`'s
|
||
binding inside the body, not inside its own RHS — recursion needs
|
||
a top-level def.
|
||
- No visibility rules in imports. Every top-level def of an imported module
|
||
is reachable; there is no `pub` / `priv`.
|
||
|
||
What **is** supported (and used as the smoke test for the pipeline):
|
||
|
||
- Int, Bool, Unit, **Str** as primitive types.
|
||
- `if`, `let`, function calls, recursion.
|
||
- Effects on function signatures, with `do op(args)` for direct effect
|
||
ops (`io/print_int`, `io/print_bool`, `io/print_str`).
|
||
- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`, `%`) of
|
||
type `(Int, Int) -> Int`; ordering operators and `!=` (`!=`,
|
||
`<`, `<=`, `>`, `>=`) of type `(Int, Int) -> Bool`; logical
|
||
`not : (Bool) -> Bool`; the IO effect ops listed above;
|
||
**`==` : forall a. (a, a) -> Bool** (Iter 16e); and
|
||
**`__unreachable__ : forall a. a`** (Iter 16d).
|
||
- **`==` is polymorphic** (Iter 16e). The typechecker accepts
|
||
`==` at any type whose two sides agree (the rigid `a` of the
|
||
`Forall` is unified by HM at the use site). Codegen
|
||
monomorphises and dispatches on the resolved AIL arg type:
|
||
`Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
|
||
`Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
|
||
(`@strcmp` is declared in the LLVM IR header alongside
|
||
`@printf` / `@GC_malloc`); `Unit` → constant `i1 true`
|
||
(Unit has a single inhabitant; both sides are still
|
||
evaluated for any side effects). ADT and `Fn` arg types are
|
||
rejected at codegen with a `CodegenError::Internal`
|
||
mentioning `==` and the offending type — neither has a
|
||
canonical structural-equality scheme yet, and the language
|
||
deliberately does not silently elide the check. The other
|
||
comparison ops stay Int-only; their codegen path emits
|
||
`icmp s{lt,le,gt,ge,ne}` over `i64`.
|
||
- **`__unreachable__`** is a polymorphic bottom value: a use of
|
||
`__unreachable__` typechecks against any expected type at
|
||
the use site and codegens to the LLVM `unreachable`
|
||
instruction (UB if ever executed). It is the chain
|
||
machinery's deepest fall-through for matches that the
|
||
typechecker proved exhaustive, and it is available to user
|
||
code as an explicit panic primitive
|
||
(`(if cond __unreachable__ ...)` for assertions or
|
||
impossible branches). Reference site is
|
||
`Term::Var { name = "__unreachable__" }` / form-A bare
|
||
`__unreachable__`.
|
||
- **ADTs + pattern matching** (Iter 3, extended in Iter 16a/16c).
|
||
Sub-patterns of a Ctor pattern may be `Var`, `Wild`, another `Ctor`
|
||
(Iter 16a), or a literal (Iter 16c). The desugar pass flattens
|
||
nested Ctor patterns into a chain of let + match and rewrites every
|
||
`Pattern::Lit` (top-level or sub-) to a `Term::If` on `==` before
|
||
typecheck/codegen — see `ailang-core::desugar` and Pipeline above.
|
||
- Literal patterns at top level and inside Ctor sub-patterns (Iter 16c,
|
||
via desugar). `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
|
||
parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`,
|
||
so any literal kind whose `==` is supported is authorable. After
|
||
Iter 16e (`==` polymorphic over `Int`/`Bool`/`Str`/`Unit`), that
|
||
covers every lit kind the AST ships — including `(pat-lit "hi")`
|
||
over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`.
|
||
- **Imports + qualified cross-module references** via dotted names
|
||
(Iter 5). Extends to **types and constructors** (Iter 14h): a foreign
|
||
module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as
|
||
`(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)`
|
||
inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`)
|
||
exercise this end-to-end.
|
||
- **AI-authoring text surface, form (A)** (Decision 6 / Iter 14b–14c,
|
||
exclusive in 15e). The `ailang-surface` crate parses `.ailx` form-A
|
||
text into a canonical `ailang-core::ast::Module` and prints any module
|
||
back as form-A text. `ail render` and `ail describe` use it as the
|
||
sole text projection; `ail parse` is the inverse direction. Round-trip
|
||
identity (text → AST → JSON → AST → text) is gated by
|
||
`ailang-surface/tests/round_trip.rs` over every shipped fixture.
|
||
- **Memory management via Boehm conservative GC** (Decision 9 / Iter 14f),
|
||
with **per-fn arena via stack `alloca` for non-escaping allocations**
|
||
layered on top (Iter 17a). Every ADT box, lambda env, and closure
|
||
pair allocates either via `@GC_malloc` (escaping; Boehm-managed) or
|
||
via LLVM `alloca` (non-escaping; freed at fn return). The decision
|
||
is made by an escape-analysis pre-pass over the fn body — see
|
||
Decision 9's "Per-fn arena via stack `alloca`" subsection.
|
||
Boehm-only soak tests are unchanged: `examples/gc_stress.ail.json`
|
||
and `examples/std_list_stress.ail.json` still allocate via
|
||
`@GC_malloc` because their boxes flow into other fns and escape.
|
||
The per-fn-arena path is exercised end-to-end by
|
||
`examples/escape_local_demo.ail.json` (Iter 17a fixture).
|
||
- **First-class function references** (Iter 7). A top-level fn name (or
|
||
qualified `prefix.def`) used as a `Term::Var` is a fn-value.
|
||
- **Anonymous lambdas with capture** (Iter 8). `Term::Lam` constructs a
|
||
closure that captures any free variables of its body from the
|
||
enclosing scope. All fn-values share a single ABI: a `ptr` to a
|
||
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_<m>_<def>__<descriptor>` (e.g. `id__I` for `id` at
|
||
`Int`, `apply__I_I` for `apply` at `(Int, Int)`).
|
||
- **Parameterised ADTs** (Iter 13). `TypeDef.vars: Vec<String>`
|
||
declares type parameters; `Type::Con.args: Vec<Type>` carries the
|
||
type arguments at use sites. Both fields default to empty and are
|
||
skipped during serialization, so canonical-JSON hashes of every
|
||
pre-13a definition stay bit-identical (regression test in
|
||
`crates/ailang-core/src/hash.rs`). Ctor and match codegen stay
|
||
inline at every use site — there is no specialised ADT symbol —
|
||
but LLVM field types are derived per use site by substituting
|
||
through `cdef.ail_fields`. The substitution is read off the call's
|
||
arg types (ctor) or the scrutinee's `Type::Con.args` (match). An
|
||
unresolved `Type::Var` reaching `llvm_type` is a hard error
|
||
rather than a silent fallback to `ptr`.
|
||
|
||
Pipeline regression smoke tests:
|
||
|
||
- `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
|
||
- `examples/list.ail.json` → prints 42 (ADTs + match).
|
||
- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
|
||
- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).
|
||
- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive
|
||
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)`).
|
||
- `examples/box.ail.json` → prints 42 (parameterised ADT round-
|
||
trip: `MkBox(42)` constructed, then projected by a polymorphic
|
||
`unbox : forall a. (Box<a>) -> a` and printed).
|
||
- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
|
||
over `Maybe<Int>`: `or_else(Some(7), 99)` then
|
||
`or_else(None, 99)`).
|
||
- `examples/std_list_demo.ail.json` (Iter 15a/15b) → exercises
|
||
`std_list`'s combinators (length, sum, reverse, take/drop-style
|
||
uses) end-to-end against `std_list`'s `List<a>`.
|
||
- `examples/std_maybe_demo.ail.json` (Iter 15c) → exercises `std_maybe`
|
||
combinators over `Maybe<Int>`, including `from_maybe` and `map`.
|
||
- `examples/std_either_demo.ail.json` (Iter 15d) → first program with
|
||
three distinct type variables in a single fn (the `either`
|
||
eliminator), monomorphised six different ways in the IR.
|
||
- `examples/std_pair_demo.ail.json` (Iter 15f) → drives every
|
||
`std_pair` combinator (fst, snd, swap, map_first, map_second);
|
||
expected output 7, 9, 9, 7, 8, 18.
|
||
- `examples/nested_pat.ail.json` (Iter 16a) → first program to use a
|
||
nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass
|
||
flattens it into a chain that the existing flat-match codegen
|
||
consumes. Prints 30 for a 3-element input list.
|