61ed6d47c8
Anthropic now reserves /plan as a UI command, so the Skill tool refuses to dispatch it. Rename the project's plan skill to planner, update the symlink under .claude/skills/, and adjust references in CLAUDE.md, DESIGN.md, skills/README.md, and the cross-references between brainstorm / implement / audit / fieldtest / fieldtester. Plan files themselves (docs/plans/*.md) keep their name — only the skill ID changes.
2301 lines
103 KiB
Markdown
2301 lines
103 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.
|
||
- **Surface forms** (`crates/ailang-surface`, `crates/ailang-prose`):
|
||
the LLM-facing renderings of a module. `ailang-surface`
|
||
is the lossless Form-A printer/parser — the canonical authoring
|
||
surface fixed by Decision 6, with a round-trip property
|
||
`parse ∘ print = id` gating every release. `ailang-prose`
|
||
is the lossy Form-B projection — human-readable prose for review and
|
||
edit, with no parser; re-integration goes through the
|
||
LLM-mediator round-trip documented in `docs/PROSE_ROUNDTRIP.md`.
|
||
- **CLI** (`crates/ail`): toolchain for tooling consumers — `manifest`,
|
||
`describe`, `deps`, `check`, `build`, `parse`, `render`, `prose`,
|
||
`merge-prose`, 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.
|
||
- **Skills** (`skills/`): specialised disciplines
|
||
(`brainstorm`, `planner`, `implement`, `audit`, `debug`,
|
||
`fieldtest`) plus the agent rosters they dispatch
|
||
(`skills/<name>/agents/`). They form the project's own
|
||
development methodology and are versioned with the codebase.
|
||
See `skills/README.md`.
|
||
- **Docs** (`docs/`): `DESIGN.md` (canonical state),
|
||
`JOURNAL.md` (chronological decisions log),
|
||
`roadmap.md` (forward queue), `specs/` (per-milestone design
|
||
specs), `plans/` (per-iteration implementation plans).
|
||
- **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.
|
||
|
||
## Feature-acceptance criterion
|
||
|
||
A proposed feature ships only if both hold:
|
||
|
||
1. **An LLM author naturally produces code that uses it.** Without
|
||
prompting toward the feature, the LLM reaches for it as the clean
|
||
way to express the situation. If the feature is only used when
|
||
explicitly mentioned, it isn't earning its keep — the LLM is the
|
||
only author, and what the LLM doesn't reach for naturally is dead
|
||
surface area.
|
||
|
||
2. **The feature measurably improves correctness or removes
|
||
redundancy.** Either it eliminates a class of bugs structurally
|
||
(the schema forbids the wrong code), or it lets the LLM express the
|
||
same logic in fewer sites that have to stay consistent across
|
||
edits. Aesthetic appeal — "feels elegant", "is idiomatic" — does
|
||
not count.
|
||
|
||
This is the positive complement to the CLAUDE.md rule that
|
||
implementation effort is not a rationale: cost is not a reason *for* a
|
||
feature, and neither is human aesthetic preference. The only thing
|
||
that is, is LLM-author utility.
|
||
|
||
Two corollaries:
|
||
|
||
- **Human-attractive but LLM-neutral features are cut.** Point-free
|
||
style, operator overloading, implicit conversions, syntactic
|
||
shortcuts that hide structure. They reward human authors who enjoy
|
||
compression; they cost the LLM the explicit form it relies on to
|
||
keep RC, uniqueness, and effects locally legible.
|
||
|
||
- **Human-hostile but LLM-friendly features are kept.** JSON as
|
||
canonical authoring surface; mandatory mode annotations on every
|
||
fn parameter; mandatory top-level type signatures; explicit `clone`
|
||
for shared values. These cost a human author keystrokes; they let
|
||
the LLM reason locally without spending context window on
|
||
cross-references.
|
||
|
||
Empirically: if a feature is proposed and the LLM does not produce it
|
||
in unprompted code samples, the feature is proposed for the wrong
|
||
reason. The orchestrator's job is to notice that and cut.
|
||
|
||
## 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
|
||
|
||
Form (A) is implemented as
|
||
the `ailang-surface` crate (parser + printer). 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. `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 at
|
||
the same time, 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
|
||
|
||
Early development 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` 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
|
||
|
||
- `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.
|
||
- 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 implementation
|
||
|
||
Two productions in the original 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 original 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.** 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: ~30, still inside the 30-rule
|
||
constraint-1 budget. No new lexical rule (`tail-app` / `tail-do`
|
||
are bare ident tokens; no special casing).
|
||
|
||
### Form (B) — human prose projection
|
||
|
||
AILang ships a
|
||
second textual projection of the AST: `ailang-prose`, a one-way
|
||
projection from `Module → human-readable text`. It is **not** an
|
||
authoring surface; it is the "display" projection that Decision 6's
|
||
architectural pin (line 167–176) explicitly anticipated:
|
||
|
||
> *"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."*
|
||
|
||
Form (B) targets the specific failure mode where a human reviewer
|
||
needs to read an AILang module quickly. Form (A) was designed to
|
||
fit a 30-production EBNF spec and to be parsed zero-shot by foreign
|
||
LLMs; that prioritisation makes it dense and visually noisy for
|
||
human readers. Form (B) inverts the trade-offs:
|
||
|
||
- **Rust-flavoured surface.** Braces and `=>` for match arms,
|
||
Rust-aligned 4-level operator precedence, infix arithmetic
|
||
(`a + b`, not `+(a, b)`), unary `!` for `not`.
|
||
- **Lossy by design.** Projection elides machinery the LLM can
|
||
re-derive: `(con T)` wrappers (`(con Int)` → `Int`), the
|
||
`(fn-type (params ...) (ret ...))` wrap, `(term-ctor T C ...)`
|
||
collapses to `C(...)`, redundant parens. Only the AST machinery
|
||
whose information is recoverable from typecheck context.
|
||
- **Lossless on load-bearing detail.** Mode annotations
|
||
(`own T`, `borrow T`), effects (`with IO`), explicit `clone`,
|
||
`reuse-as`, doc strings, type annotations on signatures and
|
||
lambdas, the `tail` flag — all preserved verbatim.
|
||
|
||
Critically, **form (B) has no parser**. Form (A) is round-trippable
|
||
by construction (Decision 6 constraint 2); form (B) deliberately is
|
||
not. Re-integrating prose edits requires an external LLM mediator,
|
||
not a compiler pass — see `docs/PROSE_ROUNDTRIP.md` for the
|
||
six-step cycle and the prompt template `ail merge-prose` composes.
|
||
|
||
Form (B) does not weaken any Decision 6 invariant:
|
||
|
||
- The JSON-AST remains the only hashable artefact. Prose is not
|
||
hashed, not content-addressed, not load-bearing for any
|
||
cross-module reference.
|
||
- Form (A) remains the canonical authoring surface. Foreign LLMs
|
||
still author against form (A); humans review and edit through
|
||
form (B).
|
||
- The 30-production grammar of form (A) is unchanged.
|
||
- `ailang-check` and `ailang-codegen` remain projection-agnostic;
|
||
`ailang-prose` is a downstream consumer of `ailang-core::ast`,
|
||
parallel to `ailang-surface` but in the rendering direction only.
|
||
|
||
The CLI gains `ail prose <m.ail.json>` (the deterministic
|
||
projection) and `ail merge-prose <m.ail.json> <edited.prose.txt>`
|
||
(the mediator-prompt composer); both are listed in the CLI section
|
||
below.
|
||
|
||
**Form-A spec embedding.** An earlier `merge-prose`
|
||
prompt instructed the LLM to emit JSON-AST and offered a 12-line
|
||
schema-essentials reminder; that combination did not give a
|
||
foreign LLM enough to produce valid output. The current prompt revises this:
|
||
|
||
- The LLM emits **Form-A** (the canonical authoring surface), not
|
||
JSON. JSON-AST stays the only hashable artefact, but it is not
|
||
a writing surface. The user runs `ail parse foo.new.ailx`
|
||
before `ail check` to produce the canonical JSON.
|
||
- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted
|
||
Form-A specification — grammar, every term / pattern / type /
|
||
def keyword, schema invariants, pitfall catalogue, four
|
||
few-shot modules drawn from `examples/*.ailx`. It is exported
|
||
as `ailang_core::FORM_A_SPEC` and embedded verbatim in every
|
||
`merge-prose` prompt.
|
||
- `crates/ailang-core/tests/spec_drift.rs` walks every variant of
|
||
`Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive
|
||
`match` and asserts an anchor for each appears in the spec.
|
||
The exhaustive match is the load-bearing piece: adding a new
|
||
variant without updating the match fails compilation in this
|
||
test, before its assertions even run. Hand-written content,
|
||
mechanical drift detection.
|
||
|
||
The discussion of richer integration paths (LLM tool-use, MCP
|
||
server, LSP) was deferred — all three layer additively on the
|
||
static-prompt path ships, which remains the
|
||
lowest-common-denominator fallback that always works.
|
||
|
||
## 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 tail-call survey of existing fixtures,
|
||
many existing recursive calls are *not* in tail position
|
||
because they are arguments to constructor calls (e.g.
|
||
`Cons (f h) (map f t)`). The current pipeline 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 ships both forms where
|
||
relevant.
|
||
|
||
Migration of existing fixtures is 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: dual allocator — RC canonical, Boehm parity oracle
|
||
|
||
AILang ships two allocator backends with an asymmetric role:
|
||
|
||
- **RC is canonical.** `--alloc=rc` is the CLI default for
|
||
`ail build` and `ail run`. The runtime AILang's memory model
|
||
(RC + uniqueness inference) is designed for. New examples,
|
||
benches, and corpus tests run under RC unless they explicitly
|
||
pin GC.
|
||
- **Boehm stays as a parity oracle.** `--alloc=gc` remains
|
||
reachable. Its load-bearing job is differential diagnosis: when
|
||
RC produces a segfault, refcount underflow, or wrong stdout, the
|
||
GC build of the same module is the cheap "memory bug or logic
|
||
bug?" probe. The end-to-end suite includes per-example
|
||
parity tests that run both backends and assert byte-identical
|
||
stdout — those tests are what make the oracle real.
|
||
- **`--alloc=bump`** is unchanged: a leak-only bench instrument,
|
||
not a production target.
|
||
|
||
Full Boehm retirement (drop libgc, remove the gc backend) reopens
|
||
when the parity oracle stops paying its keep — concretely, when a
|
||
few iter families ship without the gc arm catching anything that
|
||
the rc arm did not already catch. Until then, the cost of
|
||
keeping libgc as a build dependency is accepted in exchange for
|
||
diagnostic leverage. Decision 10 (RC + uniqueness) holds as the
|
||
specification of the canonical runtime; the rest of this section
|
||
documents the Boehm half, retained as the oracle.
|
||
|
||
**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.
|
||
|
||
### Per-fn arena via stack `alloca`
|
||
|
||
This optimisation is layered on top of Boehm 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
|
||
|
||
**The GC bench (`bench/run.sh`) showed
|
||
Boehm contributing a substantial fraction of runtime on allocation-heavy workloads
|
||
that hold the heap fully live (bench notes in JOURNAL). The
|
||
mainstream "RC + inference" position is 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 structurally 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`).
|
||
|
||
**Workload scope of the 1.3× target.** The 1.3× target was
|
||
calibrated on the original `bench/run.sh` corpus: linear list
|
||
sum (`bench_list_sum`) and tree walk (`bench_tree_walk`) — uniform
|
||
single-allocation-per-step workloads where one inc/dec pair
|
||
amortises against one allocation. The corpus was later extended
|
||
with `bench_closure_chain` (closure-pair allocation: each step
|
||
allocates *two* heap objects, the closure cell and its captured
|
||
env struct) and `bench_hof_pipeline` (poly-ADT + indirect
|
||
dispatch). The closure-chain fixture measures wider than the 1.3×
|
||
linear/tree target: each step pays two allocs and two decs against
|
||
one bump-pointer bump, doubling the allocation tax on closure
|
||
construction (current ratio recorded in JOURNAL bench entries).
|
||
This is a representational cost of the closure-pair layout,
|
||
not a defect in the RC implementation; a future slab/pool
|
||
allocator for fixed-shape pair cells (Decision 9 retirement
|
||
follow-up) would compress this ratio without changing semantics.
|
||
|
||
The 1.3× retirement target therefore applies to the linear /
|
||
tree / poly-ADT subset of the corpus. Closure-heavy workloads are
|
||
tracked under a wider band (the closure-chain baseline records its rc/bump ratio as the `rc_over_bump` reference value with ±15% tolerance) and
|
||
are explicitly excluded from the Boehm-retirement gate until a
|
||
slab/pool answer ships. Decision-10's RC commitment is unchanged;
|
||
what is scoped is the *quantitative* retirement criterion, not
|
||
the choice of memory model.
|
||
|
||
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 overhead is structurally on the allocate path (JOURNAL bench notes); 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.)
|
||
|
||
Laziness, recursive value bindings, shared mutable state, or any
|
||
feature that creates cycles is rejected at design time unless the
|
||
proposal proves the cycle is collectible by an extension (e.g.
|
||
linear ownership).
|
||
|
||
### Schema additions
|
||
|
||
**Parameter modes on `Type::Fn`.**
|
||
|
||
The form-A surface for fn signatures gains mode wrappers:
|
||
|
||
```
|
||
(fn-type (params (borrow (List Int))) (ret (con Int)))
|
||
(fn-type (params (own (List Int))) (ret (own (List Int))))
|
||
```
|
||
|
||
Internally, this is *not* a new `Type` variant. Modes are
|
||
metadata on `Type::Fn` — `paramModes` and `retMode` fields run
|
||
parallel to `params` and `ret` (see §"Data model" for the JSON
|
||
schema). The substantive reasons for per-position metadata over a
|
||
`Type::Borrow` / `Type::Own` variant approach:
|
||
|
||
- **Semantic locality.** Modes are properties of fn-signature
|
||
parameter positions, not of types in general. `Int` does not
|
||
have a mode; a fn-parameter slot does. Embedding modes in
|
||
`Type` would let the schema express forms like
|
||
`(con List (borrow Int))` — syntactically possible, semantically
|
||
meaningless (you cannot separately own/borrow a list element
|
||
from the list it lives in). Decision 1 is "schema = data,
|
||
schema permits exactly what is meaningful"; per-position
|
||
metadata is the option that holds that line.
|
||
- **Compositional clarity.** A `Type` value's identity should
|
||
depend only on the type. Two functions with the same param /
|
||
ret types but different calling conventions share `Type::Fn.params`
|
||
and differ only in `param_modes`. That is the right factoring:
|
||
"what data does this carry" is one axis, "how is it transferred"
|
||
is another. Mixing them under a single hierarchy conflates the
|
||
two and makes both harder to reason about.
|
||
- **Future-proof against more position metadata.** If later iters
|
||
add other per-position properties (streaming receiver, captured-
|
||
by-closure, lifetime witness), they generalise as additional
|
||
metadata fields on `Type::Fn` — one consistent hierarchy. The
|
||
variant approach would force every new dimension into its own
|
||
`Type::*` variant (`Type::Streamed`, `Type::Captured`, ...) and
|
||
combinatorics blow up: `Type::Borrow(Type::Streamed(T))` versus
|
||
`Type::Streamed(Type::Borrow(T))` raise questions of canonical
|
||
ordering that don't exist when modes live in a flat metadata
|
||
vector.
|
||
|
||
`Implicit` is the legacy / back-compat state — semantically
|
||
equivalent to `Own` but printed bare (`(con T)`, no wrapper).
|
||
`Own` and `Borrow` are explicitly annotated.
|
||
|
||
JSON canonical hash for every existing fixture stays bit-
|
||
identical: `param_modes` is skipped when every entry is
|
||
`Implicit`, `ret_mode` is skipped when `Implicit`. Existing
|
||
modules emit the same bytes as before.
|
||
|
||
**Type::Con name scoping (canonical form, since ct.1).** Within a
|
||
`.ail.json`, a `Type::Con.name` is interpreted relative to the
|
||
file's top-level `"name"` field (the owning module). Bare names
|
||
(no `.`) refer to a TypeDef in the owning module's own `defs`.
|
||
Cross-module references MUST be qualified `<owning_module>.<TypeName>`
|
||
where `<owning_module>` is a known module in the workspace.
|
||
Primitives (`Int`, `Bool`, `Str`, `Unit`, `Float`) are bare and
|
||
have no module qualifier. Bare cross-module references are a
|
||
schema violation (`WorkspaceLoadError::BareCrossModuleTypeRef`);
|
||
qualified references whose owner is unknown are also a violation
|
||
(`WorkspaceLoadError::BadCrossModuleTypeRef`). The same rule
|
||
applies to `Term::Ctor.type_name`.
|
||
|
||
Class names (`ClassDef.name`, `InstanceDef.class`,
|
||
`SuperclassRef.class`, `Constraint.class`) are NOT module-scoped
|
||
under this rule; they remain workspace-flat with
|
||
`MethodNameCollision` enforced at load. Class-name scoping is a
|
||
future milestone with its own DESIGN amendment.
|
||
|
||
The legacy `(con T)` form is treated as `(own T)` semantically.
|
||
|
||
(An incidental observation, not a design reason: keeping `Type`
|
||
itself unchanged also avoids touching ~250 sites across the
|
||
typechecker / desugar / codegen that match on `Type` variants.
|
||
This is a tiebreaker, not a rationale — the substantive reasons
|
||
above are what justify the choice.)
|
||
|
||
**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)`
|
||
```
|
||
|
||
`Term::ReuseAs` is structured as a *wrapper* around a `body`
|
||
term rather than as a `reuse_from: Option<String>` modifier on
|
||
`Term::Ctor`. Two substantive reasons:
|
||
|
||
1. **Compositional flexibility.** Reuse-as is conceptually a
|
||
wrapper that says "this expression's allocation comes from
|
||
`<source>`'s slot". The wrapper form generalises naturally
|
||
if future iters introduce other allocating constructs
|
||
(record literals, opaque box wrappers, capability cells) —
|
||
they all become valid `body` positions. A modifier on
|
||
`Term::Ctor` would have to be replicated on every
|
||
constructible Term variant the language grows.
|
||
2. **Source-locality at the head.** `(reuse-as SRC NEW-CTOR)`
|
||
reads as a single sentence with the source-binder named at
|
||
the head. The modifier form would scatter the reuse intent
|
||
across a child position of the constructor's argument
|
||
syntax, separating the `source` from the rest of the
|
||
reuse-as semantics.
|
||
|
||
The trade-off this accepts: the schema permits `Term::ReuseAs
|
||
{ body }` where `body` is not an allocating form (e.g. a
|
||
literal, a var). Such terms are caught at typecheck via a
|
||
`reuse-as-non-allocating-body` diagnostic — structural rejection
|
||
in the typechecker, not the schema. The principle: prefer
|
||
composability over schema-level rejection where the typecheck
|
||
rule is unambiguous.
|
||
|
||
**`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.
|
||
|
||
**`FnDef.suppress`.** The `suppress` field on `FnDef` carries a
|
||
list of advisory-diagnostic suppress entries; each entry has a
|
||
`code` (the diagnostic being suppressed) and a `because` (a
|
||
mandatory non-empty reason). See §"Data model" for the canonical
|
||
schema.
|
||
|
||
Form-A surface: `(suppress (code "...") (because "..."))` clause
|
||
between fn name and `(type ...)`. Multiple clauses allowed; one
|
||
per entry. Form-B (prose) renders one
|
||
`// @suppress <code>: <because>` line per entry above the doc
|
||
string — lossless, contract metadata.
|
||
|
||
Skipped from serialisation when empty so existing fixtures keep
|
||
bit-identical canonical-JSON hashes (regression-pinned by
|
||
`iter19b_empty_suppress_preserves_pre_19b_hashes` and
|
||
`iter19b_schema_extension_preserves_pre_19b_hashes`).
|
||
The canonical-form tightening in ct.1 shifted the hashes of two
|
||
cross-module fixtures (`ordering_match.ail.json` and
|
||
`test_22b1_dup_a.ail.json`); all intra-module fixtures, including
|
||
the regression-pinned `sum.ail.json` and `list.ail.json`, remain
|
||
bit-identical. The new pins are
|
||
`ct4_migrated_fixtures_have_canonical_form_hashes` (locks the
|
||
post-migration hashes) and
|
||
`ct4_unmigrated_fixtures_remain_bit_identical` (re-asserts the
|
||
existing 13a/19b/22b.1 hashes still hold).
|
||
|
||
### Advisory diagnostics
|
||
|
||
The advisory-diagnostics arc introduces the language's first
|
||
**advisory** typechecker diagnostic and the suppression mechanism
|
||
that goes with it. Decision 10's mandatory-annotation rule is
|
||
unchanged: `param_modes` and `ret_mode` remain author-required;
|
||
the typechecker does not infer them. What's new is feedback when
|
||
an authored annotation is *stricter than necessary*.
|
||
|
||
**The lint: `over-strict-mode`.** Fires on a
|
||
fn-param `p` annotated `(own T)` when:
|
||
|
||
1. `p`'s `consume_count == 0` (uniqueness pass: the body
|
||
never consumes `p` as a whole).
|
||
2. For every match arm whose scrutinee is `p`, no
|
||
**heap-typed** pattern-binder has `consume_count > 0`.
|
||
|
||
The heap-type filter is load-bearing for soundness:
|
||
`match xs { Cons(h, t) => h }` records `consume_count(h) == 1`,
|
||
but `h: Int` is read by-value — no RC traffic, no heap data
|
||
moved out of `xs`'s allocation. Filtering primitive-typed
|
||
binders is what lets the lint correctly identify `head_or_zero`
|
||
as over-strict (could be `borrow`) while staying silent on
|
||
`sum_list` where `t: List` *is* moved out.
|
||
|
||
Severity: `Warning`. The first ever Warning-level diagnostic;
|
||
previously all diagnostics were `Error`. CLI exit semantics
|
||
adjusted: `ail check`, `ail build`, `ail emit-ir` exit 1 only on
|
||
at least one Error. Warnings print but do not abort.
|
||
|
||
**The suppression: `mode-strict-because`.** Authors
|
||
who want to keep an over-strict annotation deliberately (e.g.
|
||
RC codegen-test fixtures, fns reserved for planned in-place
|
||
mutation) attach a `Suppress` entry naming the diagnostic code
|
||
and a non-empty reason. The typechecker drops matching
|
||
diagnostics from the output. Empty `because` is a hard error
|
||
(`empty-suppress-reason`); wrong-code suppresses are silent
|
||
no-ops (open-set diagnostic registry — a suppress for a code
|
||
that doesn't fire today may exist defensively for a code that
|
||
might fire after a future edit).
|
||
|
||
### Why advisory + suppress instead of inference
|
||
|
||
Three reasons, all anchored in Decision 10's framing:
|
||
|
||
1. **Annotation states intent; inference picks
|
||
weakest-supporting.** These often coincide today but are
|
||
conceptually different. The annotation captures what the
|
||
author committed to (e.g. `(own T)` reserved for a planned
|
||
mutation that hasn't landed); inference would silently
|
||
relax it.
|
||
2. **Annotation is a drift-bremse.** Body change that flips
|
||
the inferred mode produces caller-side breakage at remote
|
||
sites. Annotation enforces the local-conflict-error pattern
|
||
instead.
|
||
3. **Forcing function for LLM authoring.** Without mandatory
|
||
annotation, the LLM never has to commit to ownership intent
|
||
before writing the body. The advisory lint plus suppress
|
||
lets us flag accidental over-strictness without weakening
|
||
the contract.
|
||
|
||
The suppress mechanism with mandatory-reason mirrors Rust's
|
||
`#[allow(...)]`-style escape hatch but sharpens it: the reason
|
||
is required (not optional), and it becomes part of the contract
|
||
the next reader sees. CLAUDE.md's "preserve correctness across
|
||
development cycles" is what this directly serves.
|
||
|
||
### Inference algorithm
|
||
|
||
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
|
||
(`borrow` / `own`) provide the inter-fn contract; the
|
||
inference fills in intra-fn detail.
|
||
|
||
### Codegen contract
|
||
|
||
Memory layout:
|
||
|
||
- 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 (via `drop-iterative`).
|
||
|
||
Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under
|
||
`--alloc=rc` calls `ailang_rc_alloc(SIZE)`. The initial RC plumbing
|
||
stops there — inc/dec instrumentation is added once the
|
||
inference is wired up. Until then, `--alloc=rc` deliberately
|
||
leaks like the pre-Boehm era; this is purely about plumbing.
|
||
|
||
### Mode metadata is load-bearing for codegen
|
||
|
||
`param_modes` and `ret_mode` on `Type::Fn` are not merely
|
||
typechecker metadata — codegen consults both to decide where to
|
||
emit drop calls. They were promoted from
|
||
"annotation that the typechecker enforces" to "annotation that
|
||
codegen reads to keep RC correct". Recorded here so the schema
|
||
metadata's role is explicit:
|
||
|
||
**`param_modes` — drop-emission gates.**
|
||
|
||
- **Iter B: Own-param dec at fn return.** When a fn body
|
||
fall-throughs to a `ret` (no tail-call), every parameter with
|
||
`param_modes[i] == Own` is dec'd before the `ret` iff its
|
||
uniqueness `consume_count == 0` and the ret value is not the
|
||
param itself. `Borrow` and `Implicit` parameters are skipped:
|
||
`Borrow` retains the caller's ownership by contract;
|
||
`Implicit` carries no static caller-handed-off-ownership
|
||
signal (it's the back-compat lane).
|
||
|
||
- **Iter A: arm-close pattern-binder dec.** When a match-arm's
|
||
body terminates without a tail-call, every ptr-typed
|
||
pattern-bound binder pushed by the arm is dec'd at arm close
|
||
iff its `consume_count == 0` and it is not the arm's tail
|
||
value, **gated on the scrutinee's static ownership**. If the
|
||
scrutinee is a fn-param, only `Own`-mode scrutinees enable
|
||
the dec — `Borrow` and `Implicit` scrutinees would let the
|
||
arm dec memory the caller still references.
|
||
|
||
- **Pre-tail-call shallow-dec.** When a match-arm's
|
||
body IS a tail call, both Iter A and Iter B are skipped (the
|
||
block is terminated). A separate seam in `lower_match` emits
|
||
a shallow `ailang_rc_dec` on the scrutinee outer cell BEFORE
|
||
the tail call, gated identically on the scrutinee mode plus
|
||
the requirement that every ptr-typed slot in the active
|
||
ctor's pattern is in `moved_slots[scrutinee]`.
|
||
|
||
**`ret_mode` — let-binder trackability.**
|
||
|
||
- **`Term::App` drop at let-scope close.** A
|
||
let-binder whose value is `Term::App { callee, .. }` is
|
||
trackable for scope-close drop iff the callee's
|
||
`ret_mode == Own`. The signal is the callee's static
|
||
contract that ownership of the freshly heap-allocated cell
|
||
flows to the caller. `Borrow`-returning calls remain
|
||
non-trackable (the callee retains ownership; the caller
|
||
holds a view, not an own ref). `Implicit`-returning calls
|
||
remain non-trackable (back-compat lane).
|
||
|
||
The drop fn's symbol resolution for an Own-returning App:
|
||
synthesise the call's return type, resolve `Type::Con { name }`
|
||
to `drop_<owner>_<T>` (with cross-module qualification through
|
||
the import map). Falls back to shallow `ailang_rc_dec` for
|
||
returns that are not `Type::Con` (e.g. unresolved type vars on
|
||
a polymorphic call's pre-monomorphisation site; the
|
||
monomorphised copies resolve to concrete drop fns).
|
||
|
||
**What this widening does NOT do.**
|
||
|
||
- Does not change the canonical hash. `param_modes` /
|
||
`ret_mode` were already hash-load-bearing when introduced;
|
||
subsequent work added codegen consumers, not new schema fields.
|
||
- Does not introduce a new `Type` variant. Mode metadata stays
|
||
flat on `Type::Fn` (see "Schema additions" above on why).
|
||
- Does not cover let-aliases of borrowed values. A let-binder
|
||
whose value is `Term::Var` referencing a `Borrow`-mode
|
||
param is not yet propagated through; the param-mode gates
|
||
treat such a binder as "owned" (its `current_param_modes`
|
||
lookup misses, default = owned). This is a known carve-out
|
||
shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass
|
||
through let-bindings that has not shipped yet.
|
||
|
||
### 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.
|
||
|
||
### 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. A 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.**
|
||
`(con T)` is treated 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.
|
||
|
||
## Decision 11: typeclasses — Haskell-lite, monomorphised, coherent
|
||
|
||
**The design pass for typeclasses. Codified after the Feature-acceptance
|
||
criterion (this document, above) was committed; the criterion is
|
||
the explicit basis for the choices below.**
|
||
|
||
AILang ships typeclasses to compress a real LLM-author redundancy:
|
||
without them, every comparable function must be written per-type
|
||
(`int_eq`, `string_eq`, `bool_eq`, `int_show`, `string_show`, …). With
|
||
typeclasses behind a monomorphising compiler, the LLM author writes
|
||
one signature with a class constraint and one method per concrete
|
||
type, and the compiler emits the same machine code as the per-type
|
||
version. No runtime cost, no dictionary passing, no vtables.
|
||
|
||
**Choice.** A deliberately narrow typeclass design — narrower than
|
||
Haskell, narrower than Rust traits — calibrated to what an LLM
|
||
author naturally produces. Five semantic axes are committed:
|
||
|
||
1. **Scope.** Multi-method, single-parameter, optional defaults,
|
||
single-superclass relation. No multi-param classes, no
|
||
functional dependencies, no associated types.
|
||
2. **Constraints in signatures.** Explicit and mandatory. A
|
||
function that calls a class method must declare the constraint
|
||
in its `forall` block. No constraint inference.
|
||
3. **Resolution.** Orphan-free coherence. An `instance C T` may be
|
||
declared only in the module of `C` or in the module of `T`.
|
||
Resolution is global type-directed against a workspace-built
|
||
registry; coherence makes the lookup unambiguous.
|
||
4. **Defaults.** Opt-in via an explicit `default` keyword in the
|
||
class body. Methods without `default` are abstract-required;
|
||
methods with `default` may be overridden or inherited per
|
||
instance.
|
||
5. **Class-parameter kind.** Concrete types only (kind `*`). No
|
||
higher-kinded class params; `Functor`/`Monad`-style abstractions
|
||
over type constructors are not expressible. The LLM-natural
|
||
pattern is `List.map` / `Tree.map` as separate functions per
|
||
type, which monomorphisation handles directly.
|
||
|
||
The five axes follow from the Feature-acceptance criterion: each
|
||
rejected mechanism (multi-param, higher-kinded, FunDeps, assoc
|
||
types) is one an LLM author does not unprompted produce.
|
||
|
||
### Form-A schema (the JSON authoring surface)
|
||
|
||
Three additive schema extensions; no existing module becomes invalid.
|
||
|
||
**`ClassDef`** — top-level definition kind, declares a class:
|
||
|
||
```
|
||
{ "kind": "class",
|
||
"name": "Show",
|
||
"param": "a",
|
||
"superclass": null,
|
||
"methods": [
|
||
{ "name": "show",
|
||
"type": { /* full FnSig over `a`, with mode annotations */ },
|
||
"default": null
|
||
}
|
||
]
|
||
}
|
||
```
|
||
|
||
`superclass` is either `null` or `{ "class": <name>, "type": "a" }`
|
||
where `"a"` MUST be the same identifier as the class's own `param`.
|
||
`default` is either `null` (method is abstract-required at instance
|
||
sites) or an AST body (method is optional with the body as fallback).
|
||
|
||
**`InstanceDef`** — top-level definition kind, declares an instance:
|
||
|
||
```
|
||
{ "kind": "instance",
|
||
"class": "Show",
|
||
"type": "Int",
|
||
"methods": [
|
||
{ "name": "show", "body": <AST> }
|
||
]
|
||
}
|
||
```
|
||
|
||
`type` is a concrete type expression, never the class param. `methods`
|
||
contains the bodies for every required method plus optional overrides
|
||
of default-bearing methods.
|
||
|
||
**`FnDef.type` extension** — the existing FnSig schema gains a
|
||
`constraints` sibling field next to `forall`:
|
||
|
||
```
|
||
"type": {
|
||
"forall": ["a"],
|
||
"constraints": [{ "class": "Show", "type": "a" }],
|
||
"type": ["Fn", [...], "String"]
|
||
}
|
||
```
|
||
|
||
When `forall` is empty, `constraints` is also empty (and may be
|
||
omitted for hash stability of older definitions). Each constraint's
|
||
`type` field MUST reference a type variable bound by the surrounding
|
||
`forall`.
|
||
|
||
**Method invocation sites do NOT get a new node.** A call to a class
|
||
method is a normal `Call` node; resolution against a class is the
|
||
typechecker's job, not the parser's. The LLM author writes `show x`
|
||
exactly as for any free function.
|
||
|
||
### Resolution and monomorphisation
|
||
|
||
**Constraint collection (per function body).** During typechecking
|
||
of a body, each method call generates a residual constraint of shape
|
||
`<Class> <Type>` where `<Type>` may still contain type variables.
|
||
After local typechecking, residual constraints are checked against
|
||
the function's declared constraints (modulo α-conversion and modulo
|
||
auto-expansion through superclasses; see below). Any residual not
|
||
covered by declared constraints fires `MissingConstraint`.
|
||
|
||
**Instance registry (workspace-global).** At workspace load (see
|
||
`crates/ailang-core/src/workspace.rs`), all `InstanceDef` nodes
|
||
across all reachable modules are collected into a registry keyed by
|
||
`(class-name, canonical-hash-of-instance-type)`. Registry build
|
||
performs three checks:
|
||
|
||
- **Coherence.** Each instance's module must be either the class's
|
||
defining module or the instance type's defining module. Otherwise
|
||
→ `OrphanInstance`.
|
||
- **Uniqueness.** No two entries share a key. Otherwise →
|
||
`DuplicateInstance`.
|
||
- **Method completeness.** Each instance specifies every required
|
||
(non-default) method of its class. Otherwise → `MissingMethod`.
|
||
|
||
Registry build is a one-time-per-build pass that fires before any
|
||
typechecking. Its errors are workspace-load errors, not per-call-site
|
||
errors.
|
||
|
||
**Resolution at call sites with concrete types.** When the typechecker
|
||
sees a method call where every type variable in the constraint is
|
||
substituted to a concrete type, it queries the registry. Hit →
|
||
resolved. Miss → `NoInstance`.
|
||
|
||
**Resolution at polymorphic call sites.** When type variables are
|
||
still free, the constraint propagates into the surrounding function's
|
||
constraint context — which the user MUST have declared explicitly
|
||
(per axis 2). No constraint is implicitly hoisted.
|
||
|
||
**Monomorphisation (post-typecheck, pre-codegen).** A pass between
|
||
typechecking and codegen replaces every resolved class-method call
|
||
with a call to a synthesised monomorphic `FnDef`. For each unique
|
||
`(method, concrete-type)` pair encountered, the pass:
|
||
|
||
1. Synthesises a top-level `FnDef` named deterministically from the
|
||
method name and the canonical hash of the instance type. Body is
|
||
the resolved instance method (or default body), with the class
|
||
parameter substituted to the concrete type.
|
||
2. Caches the synthesised def by `(method, type-hash)` so the same
|
||
pair is not emitted twice.
|
||
3. Rewrites the original `Call` to target the synthesised name.
|
||
|
||
After this pass, the IR contains no class machinery — only ordinary
|
||
monomorphic functions and direct calls. Codegen sees no difference
|
||
between a hand-written `show_int` and a synthesised `show__Int`.
|
||
|
||
**Why mono, not virtual dispatch.** Monomorphisation makes the call
|
||
target visible to the optimiser, unlocking inlining and downstream
|
||
loop transformations that virtual dispatch prevents in principle.
|
||
On a saturating branch predictor with a monomorphic indirect
|
||
target, the indirect call itself is comparable in cost to a
|
||
non-inlined direct call — the win is in what the optimiser can do
|
||
with the visible target, not in the call instruction. The
|
||
end-to-end gain shrinks toward zero on larger callee bodies and
|
||
cold call sites, but the architectural claim — "mono enables
|
||
optimisations vdisp forbids" — holds across the spectrum
|
||
(`bench/mono_dispatch.py` and the corresponding JOURNAL bench-notes
|
||
entry record the measured ratios).
|
||
|
||
The separator is `__` rather than `#` or `@` because `#` and `@`
|
||
are invalid in LLVM IR global identifiers (the IR verifier rejects
|
||
them inside `@ail_<module>_<def>` mangled names). `__` is legal in
|
||
both LLVM IR and the C ABI used by the runtime glue, and parses
|
||
unambiguously into `<method>__<type-surface-name>` because neither
|
||
component contains `__` by project convention.
|
||
|
||
**No runtime dispatch, no dictionary passing.** The monomorphisation
|
||
pass is the ONLY mechanism for class-method calls. A call that
|
||
cannot be monomorphised — for instance, because a constraint remains
|
||
unresolved at the entry point — is a static error, not a runtime one.
|
||
This is the LLVM-friendly form and is consistent with Decision 10's
|
||
performance commitment.
|
||
|
||
### Defaults and superclasses
|
||
|
||
**Defaults.** A `ClassDef.methods[i].default` is either `null` (the
|
||
method is required at instance level) or an AST body. When an
|
||
`InstanceDef` does not specify a method that has a default, the
|
||
typechecker uses the default body for that instance, with the class
|
||
param substituted to the instance type. Default bodies may call
|
||
other methods of the same class (the canonical example is
|
||
`default ne x y = not (eq x y)`); the called methods resolve at
|
||
monomorphisation time against the same instance.
|
||
|
||
**Superclasses.** A `ClassDef.superclass` of `{ "class": "Eq",
|
||
"type": "a" }` declares that any `instance C T` requires a
|
||
corresponding `instance Eq T` to exist. The check fires at
|
||
workspace-load time: for each `InstanceDef` whose class declares a
|
||
superclass, the registry is queried for the matching superclass
|
||
instance. Missing → `MissingSuperclassInstance`.
|
||
|
||
**Superclass auto-expansion in constraint contexts.** When a function
|
||
declares `Ord a` as a constraint, the typechecker treats the constraint
|
||
context as `{ Ord a, Eq a }` for the purposes of `MissingConstraint`
|
||
checking. This is the one deviation from "alles sichtbar": the
|
||
extension is anchored in the class's own `superclass` field, so the
|
||
relation is schema-visible at the class declaration even when the
|
||
constraint at the function site reads `Ord a` alone.
|
||
|
||
Superclass chains are linear (single-superclass relation per class)
|
||
and auto-expansion closes transitively across the chain.
|
||
|
||
**No `deriving`.** AILang does not auto-derive instances. `instance Eq
|
||
MyType` must be written by hand. Auto-derivation may land in a future
|
||
iteration if the Feature-acceptance criterion holds for it; that
|
||
discussion is out of scope here.
|
||
|
||
### Diagnostic categories
|
||
|
||
The typeclass layer introduces three families of diagnostics. Exact
|
||
wording is fixed; the categories and their triggers are:
|
||
|
||
**Workspace-load (registry-build) diagnostics:**
|
||
|
||
- `OrphanInstance` — instance is not in class's or type's module.
|
||
- `DuplicateInstance` — two instances match the same key.
|
||
- `MissingSuperclassInstance` — superclass instance absent.
|
||
- `MissingMethod` — instance omits a required method.
|
||
- `OverridingNonExistentMethod` — instance specifies a method not in
|
||
the class.
|
||
- `MethodNameCollision` — same method name across two in-scope
|
||
classes, or between a class method and a top-level function.
|
||
|
||
**Class-schema diagnostics** (validation of class declarations):
|
||
|
||
- `KindMismatch` — class param appears in applied position in any
|
||
method signature (e.g., `f a` where `f` is the class param).
|
||
- `InvalidSuperclassParam` — superclass `type` differs from the
|
||
class's own `param`.
|
||
- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a
|
||
type variable not bound by the surrounding `forall`.
|
||
|
||
**Typecheck diagnostics** (per function body):
|
||
|
||
- `MissingConstraint` — body's residual constraint is not covered
|
||
by declared (and superclass-expanded) constraints.
|
||
- `NoInstance` — fully concrete constraint has no registry entry.
|
||
|
||
There is no `AmbiguousInstance` diagnostic. Coherence (W2) makes
|
||
every `(class, type)` key globally unique; resolution is therefore
|
||
deterministic by construction.
|
||
|
||
### What the typeclass design explicitly does NOT support
|
||
|
||
Each of the following is rejected by either schema (parser cannot
|
||
express the construct) or by an enumerated diagnostic. The
|
||
combination of axis-1 (single-param, no FunDeps, no assoc) and
|
||
axis-5 (kind `*` only) covers the space.
|
||
|
||
- **Multi-parameter classes** (`class Foo a b where ...`). Schema
|
||
rejects: `ClassDef.param` is a string, not a list.
|
||
- **Higher-kinded class params** (`class Functor f`). Diagnostic
|
||
S1 (`KindMismatch`) at class declaration if any method applies
|
||
the param.
|
||
- **Higher-rank polymorphism** (`forall a. (forall b. b -> b) -> a`).
|
||
Already rejected at parse time per the typeclass-conversation
|
||
rationale recorded in JOURNAL; constraint-bearing
|
||
signatures inherit that prohibition.
|
||
- **Existential / dyn dispatch** (`exists a. Show a => a`,
|
||
heterogeneous lists like `[Show]`). Schema does not express
|
||
existentials. The LLM-natural alternative is sum types.
|
||
- **Associated types** (`class Container c where type Element c`).
|
||
Schema does not express type-level methods.
|
||
- **Functional dependencies** (`class Convert a b | a -> b`). Required
|
||
only for multi-param classes; entails by axis 1.
|
||
- **`deriving` / auto-derivation** (`data Foo = ... deriving (Eq)`).
|
||
Future iteration, gated separately on Feature-acceptance.
|
||
- **Numeric literal defaulting.** `1` does not auto-resolve to `Int`
|
||
under an ambiguous `Num a` constraint. Bare polymorphic literals
|
||
with multiple satisfying instances fire `NoInstance` with a hint
|
||
to annotate. The LLM-author writes `1 : Int` or `1 : Float`.
|
||
- **Orphan-with-warning mode.** Coherence is hard. `OrphanInstance`
|
||
is always an error, never a warning. The corollary `--allow-orphans`
|
||
flag is not provided.
|
||
|
||
### Prelude (built-in) classes
|
||
|
||
Milestone 22 ships **no built-in Prelude classes**. The original
|
||
An earlier draft committed to a fixed Prelude (Show / Eq / Ord on the
|
||
primitives), but the implementation work to wire `int_to_str` as a
|
||
heap-allocated-string runtime primitive proved substantively
|
||
separable from the typeclass machinery itself, and the LLM-utility
|
||
case for primitive `Show` is weak (LLM-natural form is `int_to_str
|
||
x`, not `show x` through a single-instance class). The user-class
|
||
end-to-end path is the milestone's typeclass acceptance gate
|
||
(the user-defined-class fixture: `class Foo a` + `data IntBox` +
|
||
`instance Foo IntBox`); see `docs/specs/2026-05-09-22-typeclasses.md`
|
||
"Amendments" for the substantive rationale.
|
||
|
||
Primitive output goes through `io/print_int` / `io/print_bool` /
|
||
`io/print_str` directly.
|
||
|
||
`==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators (unchanged
|
||
from the original draft). Class methods are accessed by name (`eq x y`,
|
||
`lt x y`, …), not via these operators. Routing operators through
|
||
classes is deliberately deferred — it would require migrating every
|
||
existing fixture and would re-baseline the bench corpus, which is a
|
||
new-baseline decision rather than an iter detail.
|
||
|
||
`Num` is NOT in milestone 22. Arithmetic operators (`+`, `-`, `*`,
|
||
`/`) stay primitive and per-type. Class-based numeric overloading
|
||
would invoke literal-defaulting which axis-7 already excluded.
|
||
|
||
### What this decision does NOT commit to
|
||
|
||
- **Operator routing.** `==`, `<`, etc. stay primitive in milestone
|
||
22. Class-routing operators is a future-iteration option, not a
|
||
Decision-11 commitment.
|
||
- **Form-B (prose) projection of class/instance.** The prose
|
||
renderer for the new schema nodes is one-way (no parser by
|
||
design) and was deferred from milestone 22 entirely; the
|
||
placeholder render in `crates/ailang-prose/src/lib.rs` is
|
||
informational only. A future iter ships the full prose
|
||
projection if/when prose-side authoring needs surface.
|
||
- **Specific monomorphised-symbol naming format.** Milestone 22
|
||
uses `<method>__<type-surface-name>` for primitive type targets
|
||
(e.g. `show__Int`) and `<method>__<8-hex-prefix>` for compound
|
||
types (where `<8-hex-prefix>` is the BLAKE3 hash of the canonical
|
||
type bytes). The `__` separator was chosen over `#` and `@` for
|
||
LLVM IR identifier legality.
|
||
- **Mode annotations on class methods.** Class method signatures
|
||
ARE full FnSigs and DO carry mode annotations per Decision 10;
|
||
the convention is `borrow` for read-only methods. User-defined
|
||
classes pick modes per method.
|
||
- **Number of Prelude classes.** Milestone 22 ships zero (no
|
||
Prelude). A future Prelude milestone gates class additions on
|
||
the Feature-acceptance criterion at the time of proposal.
|
||
|
||
## Mangling scheme
|
||
|
||
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
|
||
|
||
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 finds all reachable modules; the
|
||
typechecker (`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
|
||
|
||
The on-disk JSON-AST is what the toolchain hashes, typechecks, and
|
||
lowers. **This section is the canonical schema.** The Rust types in
|
||
`crates/ailang-core/src/ast.rs` are the in-memory projection of it;
|
||
when the two disagree, this section wins, and the drift test
|
||
`crates/ailang-core/tests/design_schema_drift.rs` fires. Every
|
||
additive field is declared with `skip_serializing_if` so pre-existing
|
||
fixtures keep bit-identical canonical-JSON hashes — that gating
|
||
contract is what makes growing the schema cheap.
|
||
|
||
### Module
|
||
|
||
```jsonc
|
||
{
|
||
"schema": "ailang/v0",
|
||
"name": "<id>",
|
||
"imports": [{ "module": "<id>", "as": "<id>" }],
|
||
"defs": [Def...]
|
||
}
|
||
```
|
||
|
||
### Def
|
||
|
||
`kind ∈ { "fn", "const", "type", "class", "instance" }`. All five
|
||
are real surface forms.
|
||
|
||
```jsonc
|
||
// fn (the unit that gets a content hash)
|
||
{ "kind": "fn",
|
||
"name": "<id>",
|
||
"type": Type, // typically Type::Fn, optionally wrapped in Forall
|
||
"params": ["<id>"...], // names bound in body, in type.params order
|
||
"body": Term,
|
||
"doc": "<optional string>",
|
||
"suppress": [Suppress...] // omitted when empty
|
||
}
|
||
|
||
// const (top-level value; codegen emits as a global; body must be pure)
|
||
{ "kind": "const",
|
||
"name": "<id>",
|
||
"type": Type,
|
||
"value": Term,
|
||
"doc": "<optional string>"
|
||
}
|
||
|
||
// type (algebraic data type; parameterised)
|
||
{ "kind": "type",
|
||
"name": "<id>",
|
||
"vars": ["<id>"...], // type parameters; omitted when empty (hash-stable when omitted)
|
||
"ctors": [
|
||
{ "name": "<id>", "fields": [Type...] } // nullary ctor: fields = []
|
||
...
|
||
],
|
||
"doc": "<optional string>",
|
||
"drop-iterative": true // opt-in; omitted when false (hash-stable when omitted)
|
||
}
|
||
|
||
// class (typeclass declaration; see Decision 11)
|
||
{ "kind": "class",
|
||
"name": "<id>", // class name (e.g. "Show")
|
||
"param": "<id>", // single class parameter, kind *
|
||
"superclass": null, // or { "class": "<id>", "type": "<param>" }
|
||
"methods": [
|
||
{ "name": "<id>",
|
||
"type": Type, // FnSig over the class param
|
||
"default": Term // optional fallback body; null = abstract-required
|
||
}
|
||
...
|
||
],
|
||
"doc": "<optional string>"
|
||
}
|
||
|
||
// instance (typeclass instance; see Decision 11)
|
||
{ "kind": "instance",
|
||
"class": "<id>", // class being instantiated
|
||
"type": Type, // concrete type expression (never the class param)
|
||
"methods": [
|
||
{ "name": "<id>", "body": Term }
|
||
...
|
||
],
|
||
"doc": "<optional string>"
|
||
}
|
||
```
|
||
|
||
**`Suppress`** (entry in `FnDef.suppress`):
|
||
|
||
```jsonc
|
||
{ "code": "<diagnostic-code>", // e.g. "over-strict-mode"
|
||
"because": "<author reason>" // must be non-empty;
|
||
// empty/whitespace fires `empty-suppress-reason` (Error)
|
||
}
|
||
```
|
||
|
||
### Term (expression)
|
||
|
||
```jsonc
|
||
{ "t": "lit", "lit": Literal }
|
||
{ "t": "var", "name": "<id>" }
|
||
|
||
// fn application; tail flag triggers musttail under codegen.
|
||
// `tail` is omitted when false (hash-stable when omitted).
|
||
{ "t": "app", "fn": Term, "args": [Term...], "tail": false }
|
||
|
||
{ "t": "let", "name": "<id>", "value": Term, "body": Term }
|
||
|
||
// Local recursive let. Always fn-shaped. The desugar pass
|
||
// lifts most `letrec` to a synthetic top-level fn; `lift_letrecs`
|
||
// finishes the job after typecheck for the residue that captures
|
||
// let-bound names. Post-codegen, no `letrec` survives.
|
||
{ "t": "letrec",
|
||
"name": "<id>", "type": Type, "params": ["<id>"...],
|
||
"body": Term, "in": Term }
|
||
|
||
{ "t": "if", "cond": Term, "then": Term, "else": Term }
|
||
|
||
// Effect-op invocation. `op` is "<eff>/<op>" (e.g. "io/print_int").
|
||
// `tail` triggers musttail (omitted when false).
|
||
{ "t": "do", "op": "<eff>/<op>", "args": [Term...], "tail": false }
|
||
|
||
// Ctor application; `args` omitted when empty.
|
||
{ "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }
|
||
|
||
{ "t": "match", "scrutinee": Term, "arms": [Arm...] }
|
||
|
||
// Anonymous fn value; free vars captured from enclosing scope.
|
||
{ "t": "lam",
|
||
"params": ["<id>"...],
|
||
"paramTypes": [Type...],
|
||
"retType": Type,
|
||
"effects": ["<id>"...],
|
||
"body": Term }
|
||
|
||
// Sequencing. Semantically `let _ = lhs in rhs`; lhs must be Unit.
|
||
{ "t": "seq", "lhs": Term, "rhs": Term }
|
||
|
||
// Explicit RC clone. Codegen lowers as
|
||
// `call void @ailang_rc_inc(ptr %v)` before returning %v under `--alloc=rc`.
|
||
{ "t": "clone", "value": Term }
|
||
|
||
// Explicit reuse-as hint. `body` must be allocating
|
||
// (typically `ctor` or `lam`); `source` must be a bare `var`. Codegen
|
||
// lowers as in-place rewrite under `--alloc=rc`.
|
||
{ "t": "reuse-as", "source": Term, "body": 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.
|
||
|
||
**`Literal`**:
|
||
|
||
```jsonc
|
||
{ "kind": "int", "value": <i64> }
|
||
{ "kind": "bool", "value": <bool> }
|
||
{ "kind": "str", "value": "<utf-8>" }
|
||
{ "kind": "unit" }
|
||
{ "kind": "float", "bits": "<16-lowercase-hex>" }
|
||
```
|
||
|
||
**`Pattern`** (the `pat` field of an `Arm`; discriminator `p`):
|
||
|
||
```jsonc
|
||
{ "p": "wild" } // _
|
||
{ "p": "var", "name": "<id>" } // x — binds the value
|
||
{ "p": "lit", "lit": Literal }
|
||
{ "p": "ctor", "ctor": "<id>", "fields": [Pattern...] } // fields omitted when empty
|
||
```
|
||
|
||
Patterns are linear: each pattern variable may appear at most once.
|
||
|
||
### Type
|
||
|
||
```jsonc
|
||
// Type-constructor application. `args` omitted when empty
|
||
// (hash-stable when omitted, for non-parameterised cases like Int, Bool, ...).
|
||
{ "k": "con", "name": "<id>", "args": [Type...] }
|
||
|
||
// Function type. Decision 10 added paramModes/retMode as
|
||
// metadata on Type::Fn — they are NOT separate Type variants, so every
|
||
// existing match-arm in the typechecker (unify, occurs, apply) keeps
|
||
// working. `paramModes` omitted when every entry is "implicit";
|
||
// `retMode` omitted when "implicit" (hash-stable when omitted).
|
||
{ "k": "fn",
|
||
"params": [Type...],
|
||
"paramModes": [ParamMode...],
|
||
"ret": Type,
|
||
"retMode": ParamMode,
|
||
"effects": ["<id>"...] }
|
||
|
||
{ "k": "var", "name": "<id>" }
|
||
|
||
// Top-level polymorphism only. `constraints` carries class
|
||
// constraints (Decision 11); omitted when empty (hash-stable when omitted).
|
||
{ "k": "forall",
|
||
"vars": ["<id>"...],
|
||
"constraints": [{ "class": "<id>", "type": "<id>" }, ...],
|
||
"body": Type }
|
||
```
|
||
|
||
**`ParamMode`** (Decision 10):
|
||
|
||
```
|
||
"implicit" — unannotated / back-compat. Treated as `own` by the typechecker.
|
||
"own" — (own T) — caller transfers ownership; callee consumes.
|
||
"borrow" — (borrow T) — caller retains ownership; callee may not consume.
|
||
```
|
||
|
||
`implicit ≡ own` semantically; the distinction exists so existing
|
||
unannotated fixtures continue to serialize without the mode wrapper and keep their
|
||
canonical-JSON hash.
|
||
|
||
## Pipeline
|
||
|
||
```
|
||
.ail.json ─┐
|
||
├─ load + validate schema
|
||
├─ resolve names + assign hashes
|
||
├─ desugar (AST → AST)
|
||
├─ typecheck (HM, effect rows; mode-strict per Decision 10)
|
||
├─ lift_letrecs (post-typecheck AST → AST)
|
||
├─ lower to MIR (SSA-like, named SSA values)
|
||
├─ emit LLVM IR (.ll)
|
||
└─ clang -O2 *.ll -o binary
|
||
--alloc=rc → emits inc/dec (@ailang_rc_inc / _dec; canonical, default)
|
||
--alloc=gc → links libgc (@GC_malloc; parity oracle)
|
||
```
|
||
|
||
Two allocator backends share the same MIR. `--alloc=rc` is the
|
||
canonical backend committed to in Decision 10 and the CLI default.
|
||
The typechecker enforces
|
||
`(own)` / `(borrow)` modes, codegen emits `ailang_rc_inc` / `_dec`
|
||
calls at the points dictated by linearity, and `Term::Clone` /
|
||
`Term::ReuseAs` materialise into actual rc-bumps and in-place
|
||
rewrites respectively. Boehm-on-`--alloc=gc` is on the path to
|
||
retirement; see `docs/roadmap.md` for the active queue.
|
||
|
||
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, 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`)
|
||
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 desugar-pass lifts.
|
||
|
||
## 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 prose <module.ail.json> — JSON-AST → form-B (lossy human prose, no parser)
|
||
ail merge-prose <m.ail.json> <m.prose.txt>
|
||
— compose the LLM-mediator prompt for the prose round-trip
|
||
(see docs/PROSE_ROUNDTRIP.md)
|
||
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.
|
||
Fixing a rustdoc warning is part of the iteration that
|
||
introduced it, not a follow-up.
|
||
|
||
## Float semantics
|
||
|
||
`Float` is IEEE-754 binary64 (LLVM `double`). One float type ships;
|
||
no `f32` variant. The runtime / codegen contract:
|
||
|
||
**Guaranteed:**
|
||
|
||
- Every individual builtin (`+`/`-`/`*`/`/`/`neg`/`<`/`==`/...) lowers
|
||
to a single LLVM IR instruction on the Float arm:
|
||
`fadd/fsub/fmul/fdiv double`, `fneg double`, `fcmp olt/ole/ogt/oge
|
||
double`, `fcmp oeq double`, `fcmp une double` (for `!=`). On a
|
||
fixed `(target triple, LLVM version)` pair, the bit pattern of
|
||
the result of any single op is reproducible.
|
||
- NaN and ±Inf propagate per IEEE 754 — no silent collapse to zero,
|
||
no trap. Arithmetic on a NaN operand produces NaN; division by
|
||
zero produces ±Inf; `0.0 / 0.0` produces NaN.
|
||
- `-0.0` and `+0.0` are distinct bit patterns at the canonical-JSON
|
||
hash level (`{"bits":"0000000000000000",...}` vs
|
||
`{"bits":"8000000000000000",...}` — distinct `def_hash`s) but
|
||
compare equal via `==` per IEEE (`fcmp oeq double` returns true
|
||
for `+0 == -0`). This asymmetry is the correct IEEE behaviour;
|
||
it does mean `def_hash`-equality is finer than `==`-equality on
|
||
Float.
|
||
- `==` returns `false` whenever either operand is NaN
|
||
(`fcmp oeq` is the ordered-equal predicate; ordered = both
|
||
operands non-NaN).
|
||
- `!=` returns `true` whenever either operand is NaN (`fcmp une`
|
||
is the unordered-or-not-equal predicate). This matches Rust
|
||
`f64::ne` and IEEE-`!=` exactly.
|
||
- `is_nan` (`fcmp uno double %x, %x`) returns `true` iff `x` is
|
||
NaN. Bit-pattern-based NaN detection without dependence on the
|
||
payload bits.
|
||
- `int_to_float` (`sitofp`) is exact for `|n| < 2^53`,
|
||
round-to-nearest-even otherwise.
|
||
- `float_to_int_truncate` (`@llvm.fptosi.sat.i64.f64`) is total:
|
||
NaN → 0, +Inf → i64::MAX, -Inf → i64::MIN, finite-out-of-range
|
||
saturates, finite-in-range truncates toward zero. Matches Rust
|
||
`as i64` semantics (since 1.45).
|
||
|
||
**Unspecified:**
|
||
|
||
- FMA contraction. LLVM may fold `fadd (fmul a b) c` into
|
||
`fma a b c`. Bit results may differ between an op-emitted-in-
|
||
isolation pattern and an op-folded-into-FMA pattern.
|
||
- Reassociation. The compiler may reorder a chain like
|
||
`(a + b) + c` into `a + (b + c)`, producing a bit-different
|
||
result on numerically sensitive inputs.
|
||
- Subnormal flushing modes. If the target enables FTZ (flush-to-
|
||
zero) or DAZ (denormals-are-zero), subnormal results round to
|
||
zero; AILang does not enable these flags but does not forbid the
|
||
target from doing so.
|
||
- The exact NaN bit pattern produced by an op. Any quiet NaN bit
|
||
pattern is conformant; `0.0 / 0.0` may produce
|
||
`0x7ff8000000000000` on one target and a different qNaN on
|
||
another.
|
||
- The textual rendering of NaN by `io/print_float`. The libc
|
||
`printf("%g", nan)` glue used by the runtime is permitted to
|
||
emit `nan` / `-nan` / `NaN` etc. depending on libc version and
|
||
the NaN's sign bit; AILang does not normalise this, since the
|
||
prose / surface-print paths render NaN as the explicit `"NaN"`
|
||
spelling and `io/print_float` is for human-readable output, not
|
||
round-trip.
|
||
|
||
These are the Rust / Swift / standard-LLVM defaults — not
|
||
research-grade reproducibility guarantees. The stronger guarantee
|
||
(e.g. Pythonic `float.fromhex`-level bit reproducibility across
|
||
ops) would require `-ffp-contract=off` plus per-op intrinsic
|
||
selection — out of scope for the milestone; revisit only if a real
|
||
use case appears.
|
||
|
||
**Form-A serialisation:** Float literals carry the IEEE-754
|
||
bit pattern as a 16-character lowercase hex string in the canonical
|
||
JSON: `{"kind":"float","bits":"<16-hex>"}`. Routing through the
|
||
JSON *string* path (not `serde_json::Number`) preserves bit
|
||
stability across `serde_json` versions and lets NaN / ±Inf
|
||
round-trip through Form-A — JSON numbers cannot represent them.
|
||
|
||
**Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard-
|
||
rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
|
||
semantics make Float patterns semantically dubious — NaN never
|
||
matches via IEEE-`==`, and bit-exact equality is rarely what an
|
||
LLM-author wants. Use ordering operators (`<`, `>`, ...) and
|
||
`is_nan` to discriminate Floats.
|
||
|
||
`float_to_str` (Float → Str) is **type-installed but codegen-
|
||
deferred** to a follow-up milestone: it requires runtime-allocated
|
||
`Str` (the current Str path uses only static `@.str_*` globals;
|
||
no malloc-backed dynamic-Str infrastructure). Calling it
|
||
typechecks but produces a structured `CodegenError::Internal`.
|
||
|
||
## What is not (yet) supported
|
||
|
||
Snapshot of the current boundary. Items move out of this list
|
||
as iterations land; the JOURNAL records when.
|
||
|
||
- 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 recursive `let` for non-fn values. Plain `let x = … in …` only
|
||
sees `x` inside the body, not inside its own RHS — recursive value
|
||
bindings would break Decision 10's acyclicity invariant. Recursive
|
||
*fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
|
||
... }`); the desugar pass lifts most occurrences to a synthetic
|
||
top-level fn, with `lift_letrecs` finishing the residue after
|
||
typecheck.
|
||
- 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**, **Float** 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
|
||
`forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
|
||
`%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
|
||
Float deferred); ordering operators and `!=` (`!=`, `<`, `<=`,
|
||
`>`, `>=`) of type `forall a. (a, a) -> Bool` (codegen-restricted
|
||
to `{Int, Float}`); polymorphic `neg : forall a. (a) -> a`
|
||
(codegen-restricted to `{Int, Float}`; Float arm uses LLVM
|
||
`fneg double` for correct `-0.0` handling); logical
|
||
`not : (Bool) -> Bool`; conversions
|
||
`int_to_float : (Int) -> Float`,
|
||
`float_to_int_truncate : (Float) -> Int` (saturating, NaN → 0),
|
||
`float_to_str : (Float) -> Str` (codegen lowering deferred —
|
||
symbol installed but errors at codegen pending runtime Str
|
||
allocation); inspection `is_nan : (Float) -> Bool` (LLVM
|
||
`fcmp uno`); Float bit-pattern constants `nan : Float`,
|
||
`inf : Float`, `neg_inf : Float` (resolved as bare values, lower
|
||
to direct hex-float `double` SSA constants at use site); the IO
|
||
effect ops (`io/print_int|bool|str|float`); **`==` : forall a.
|
||
(a, a) -> Bool**; and **`__unreachable__ : forall a. a`**.
|
||
- **`==` is polymorphic.** 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); `Float` → `fcmp oeq double`.
|
||
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. **`!=` for Float uses `fcmp UNE double` (NOT
|
||
`one`)** — `one` is "ordered and not equal" and would return
|
||
false for `nan != nan`, violating IEEE-`!=`.
|
||
- **`__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.** Sub-patterns of a Ctor pattern may be `Var`, `Wild`,
|
||
another `Ctor`, or a literal. 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 (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. With `==`
|
||
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.
|
||
Extends to **types and constructors**: 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). 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),
|
||
with **per-fn arena via stack `alloca` for non-escaping allocations**
|
||
layered on top. 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`.
|
||
- **First-class function references.** A top-level fn name (or
|
||
qualified `prefix.def`) used as a `Term::Var` is a fn-value.
|
||
- **Anonymous lambdas with capture.** `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.
|
||
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.** `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
|
||
existing 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` → 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` → exercises `std_maybe`
|
||
combinators over `Maybe<Int>`, including `from_maybe` and `map`.
|
||
- `examples/std_either_demo.ail.json` → 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` → 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` → 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.
|