1d24907f84
examples/sort.ail.json: insertion sort over IntList. Defines `insert :: Int -> IntList -> IntList` and `sort :: IntList -> IntList` recursively, plus print_list using Iter 10's seq. Sorts an 11-element input and prints `1 1 2 3 3 4 5 5 5 6 9` one-per-line. Validates that the language handles deeper ADT recursion + branching (if + <=) + ctor construction + IO sequencing without surprises. Wrote, typechecked, ran first try. The Iter 11 plan called for polymorphism, but on reflection the right move was one more validation cycle before disturbing the pipeline. Polymorphism is now queued explicitly as Iter 12 (12a typechecker substitution, 12b codegen monomorphisation, 12c docs + generic example). Tests: 52 green (was 51). New e2e `insertion_sort_orders_list`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
293 lines
12 KiB
Markdown
293 lines
12 KiB
Markdown
# AILang — design decisions
|
|
|
|
This document records the core decisions for AILang. It is my contract with
|
|
myself across future iterations. Prefer cuts over growth.
|
|
|
|
## Goal
|
|
|
|
AILang is a programming language for LLM authors. It compiles to LLVM IR.
|
|
Performance: native, no GC for the MVP.
|
|
|
|
Optimised for:
|
|
|
|
- **Machine readability** over human ergonomics. The source is structured.
|
|
- **Local reasoning.** Every definition carries its full type and effects.
|
|
- **Provability.** Pure core language, explicit effects, optional refinements.
|
|
- **Robustness against hallucinations.** Symbols are hashable; tools can verify
|
|
existence without spending context window.
|
|
|
|
## Project ecosystem
|
|
|
|
AILang is not just a language but an ecosystem. The language on its own is
|
|
only valuable when its surroundings make it usable, checkable, and
|
|
extensible for its target user (LLM authors). The repo therefore contains
|
|
several equally important components — none of them optional, all of them
|
|
evolving in lockstep with the language:
|
|
|
|
- **Language core** (`crates/ailang-core`, `crates/ailang-check`,
|
|
`crates/ailang-codegen`): AST, type system, codegen.
|
|
- **CLI** (`crates/ail`): toolchain for tooling consumers — `manifest`,
|
|
`describe`, `deps`, `check`, `build`, etc., preferably with `--json` for
|
|
machine consumption.
|
|
- **Examples** (`examples/`): canonical `.ail.json` programs. They are
|
|
specification anchors, not demos — the E2E suite hangs off them.
|
|
- **Agents** (`agents/`): specialised sub-prompts (implementer,
|
|
architect, tester, debugger) that form the project's own LLM tooling.
|
|
They are a versioned part of the repo. See `agents/README.md`.
|
|
- **Docs** (`docs/`): DESIGN.md (what and why), JOURNAL.md (history).
|
|
- **Tests**: unit tests per crate plus E2E in `crates/ail/tests/e2e.rs`. Every
|
|
new compiler path needs a test, otherwise the feature does not count as done.
|
|
|
|
When the language grows, these components grow with it. New tools that
|
|
strengthen the LLM tooling (e.g. `ail diff`, IR snapshot diffs, new agents)
|
|
explicitly belong in the ecosystem inventory of this section and are added
|
|
here as soon as they are established.
|
|
|
|
## Project language: English
|
|
|
|
All in-tree content is written in English: source code (identifiers,
|
|
comments, string literals, CLI help), design documents, the journal, agent
|
|
prompts, READMEs, commit messages, examples, and `CLAUDE.md`. The live
|
|
conversation between user and me stays German for ergonomic reasons;
|
|
everything that lands in git is English. This keeps diffs and tooling output
|
|
uniform and matches the audience for AILang (LLM authors), for whom English
|
|
is the default.
|
|
|
|
## Decision 1: source = data, not text
|
|
|
|
A module is a JSON object with a fixed schema. There is no parser for
|
|
free-form text. Typos in identifiers turn into hash-lookup errors that the
|
|
compiler proposes a fix for directly.
|
|
|
|
A textual form exists (`.ail`, S-expression-like), but only as a
|
|
bidirectional projection of the JSON form. It is intended for human reviews
|
|
and diffs.
|
|
|
|
**Canonical format:** `.ail.json` with deterministic key order.
|
|
|
|
## Decision 2: content-addressed definitions
|
|
|
|
Every top-level definition has a `hash` value (BLAKE3 over canonical JSON
|
|
without the `hash` field itself). References between definitions go primarily
|
|
by name — names are for readability. The hash is the canonical identity.
|
|
|
|
Advantages:
|
|
|
|
- Refactoring by adding new defs, not by in-place change. Old versions stay
|
|
callable until manually removed.
|
|
- Caching of typecheck results and codegen per hash.
|
|
- Diffs show exactly which def has changed.
|
|
|
|
## Decision 3: pure core language + algebraic effects
|
|
|
|
The default is total, pure functions. Effects are declared as a set in the
|
|
function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic
|
|
(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
|
|
loops) are wired up.
|
|
|
|
This is the most important LLM property: when I read a function, I can trust
|
|
its signature without reading the body.
|
|
|
|
## Decision 4: Hindley-Milner + optional refinements
|
|
|
|
MVP: HM with let-polymorphism. All types are inferable, but at the top level
|
|
they must always be explicitly annotated (for local reasoning).
|
|
|
|
Later: refinement annotations that escalate to SMT. `(i: Int | i >= 0)`. They
|
|
are reserved in the AST from the start, but in the MVP they are simply passed
|
|
through as opaque strings.
|
|
|
|
## Decision 5: emit LLVM IR as text
|
|
|
|
Instead of `inkwell` or `llvm-sys`: AILang produces `.ll` files as strings
|
|
and hands them to `clang` for linking.
|
|
|
|
Rationale:
|
|
|
|
- The LLVM IR text syntax is largely stable across versions.
|
|
- No build dependency on a specific libllvm version.
|
|
- Generated code is trivially inspectable, which makes debugging much easier.
|
|
- An LLM can read the generated IR directly, which is harder with opaque
|
|
library calls.
|
|
|
|
Trade-off: no inline optimisations through the LLVM API. We rely on
|
|
`clang -O2` as the standard pipeline.
|
|
|
|
## Mangling scheme (Iter 5c)
|
|
|
|
All AILang functions are mangled to `@ail_<module>_<def>` — even in the
|
|
single-module case. Constants likewise (`@ail_<module>_<const>`). Global
|
|
string literals carry a short hint for readability:
|
|
`@.str_<module>_<hint>_<idx>` (e.g. `@.str_sum_fmt_int_0`). The entry point
|
|
is a `define i32 @main()` trampoline (C / LLVM ABI) that calls
|
|
`@ail_<entry-module>_main()`. `source_filename` exists exactly once per
|
|
workspace and carries the entry-module name (`<entry-module>.ail`).
|
|
|
|
## Convention: qualified cross-module references (Iter 5b)
|
|
|
|
Cross-module calls use **no** new AST node. Instead, a `Term::Var { name }`
|
|
with exactly one dot in the name is a qualified reference: `<prefix>.<def>`.
|
|
|
|
- `<prefix>` is an import alias (`import { module: "X", as: "<prefix>" }`)
|
|
or, when imported without an alias, the module name itself.
|
|
- `<def>` is the name of a top-level definition in the target module.
|
|
- Def names MUST NOT contain a dot — the typechecker reports
|
|
`invalid-def-name` with `ctx: { "reason": "contains-dot" }`.
|
|
- The workspace loader (Iter 5a) finds all reachable modules; the
|
|
typechecker (Iter 5b, `check_workspace`) resolves dotted names through the
|
|
import map. Diagnostic codes: `unknown-module` (prefix not imported),
|
|
`unknown-import` (module found, def not).
|
|
|
|
Hash stability: no new AST node, no renamed fields — all previous module
|
|
hashes stay bit-identical.
|
|
|
|
## Data model (MVP)
|
|
|
|
### Module
|
|
|
|
```jsonc
|
|
{
|
|
"schema": "ailang/v0",
|
|
"name": "<id>",
|
|
"imports": [{ "module": "<id>", "as": "<id>" }],
|
|
"defs": [Def...]
|
|
}
|
|
```
|
|
|
|
### Def
|
|
|
|
`kind ∈ { "fn", "type", "effect", "const" }`. In the MVP only `fn` and `const`.
|
|
|
|
```jsonc
|
|
{
|
|
"kind": "fn",
|
|
"name": "<id>",
|
|
"type": Type,
|
|
"params": ["<id>"...],
|
|
"body": Term,
|
|
"doc": "<optional string>"
|
|
}
|
|
```
|
|
|
|
### Term (expression)
|
|
|
|
```jsonc
|
|
{ "t": "lit", "lit": { "kind": "int" | "bool" | "unit", "value": ... } }
|
|
{ "t": "var", "name": "<id>" }
|
|
{ "t": "app", "fn": Term, "args": [Term...] }
|
|
{ "t": "let", "name": "<id>", "value": Term, "body": Term }
|
|
{ "t": "if", "cond": Term, "then": Term, "else": Term }
|
|
{ "t": "do", "op": "<eff>/<op>", "args": [Term...] }
|
|
{ "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }
|
|
{ "t": "match", "scrutinee": Term, "arms": [Arm...] }
|
|
{ "t": "lam",
|
|
"params": ["<id>"...],
|
|
"paramTypes": [Type...],
|
|
"retType": Type,
|
|
"effects": ["<id>"...],
|
|
"body": Term }
|
|
{ "t": "seq", "lhs": Term, "rhs": Term }
|
|
```
|
|
|
|
In the MVP, `do` is only a direct call to a built-in effect op (no handler).
|
|
A `lam` term constructs an anonymous function value; free variables of
|
|
its body are captured from the enclosing scope (see Iter 8 closure
|
|
conversion in JOURNAL). A `seq` term evaluates `lhs` for its effects
|
|
(its result must be Unit) and yields `rhs`'s value — equivalent to
|
|
`let _ = lhs in rhs`.
|
|
|
|
### Type
|
|
|
|
```jsonc
|
|
{ "k": "con", "name": "Int" }
|
|
{ "k": "con", "name": "Bool" }
|
|
{ "k": "con", "name": "Unit" }
|
|
{ "k": "fn", "params": [Type...], "ret": Type, "effects": ["IO"...] }
|
|
{ "k": "var", "name": "a" }
|
|
{ "k": "forall", "vars": ["a"...], "body": Type }
|
|
```
|
|
|
|
## Pipeline
|
|
|
|
```
|
|
.ail.json ─┐
|
|
├─ load + validate schema
|
|
├─ resolve names + assign hashes
|
|
├─ typecheck (HM, effect rows)
|
|
├─ lower to MIR (SSA-like, named SSA values)
|
|
├─ emit LLVM IR (.ll)
|
|
└─ clang -O2 *.ll -o binary
|
|
```
|
|
|
|
## 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
|
|
ail render <module> — JSON → pretty-print
|
|
ail parse <module.ail> — pretty-print → JSON (for bootstrapping)
|
|
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/`.
|
|
|
|
## What is not (yet) supported
|
|
|
|
Snapshot of the boundary at the end of Iter 8. Items move out of this list
|
|
as iterations land; the JOURNAL records the exact iteration.
|
|
|
|
- No effect handlers — only the built-in IO and Diverge ops.
|
|
- No refinements / SMT escalation.
|
|
- No polymorphism in inference. `Type::Forall` is parseable but the
|
|
typechecker rejects polymorphic uses inside a body (`PolymorphicNot
|
|
Supported`). Generic functions must be monomorphised by the author
|
|
via separate top-level defs.
|
|
- No cross-module ADTs. ADTs are local to a module; ctor names must be
|
|
unique within their module but may collide across modules.
|
|
- No visibility rules in imports. Every top-level def of an imported module
|
|
is reachable; there is no `pub` / `priv`.
|
|
- No GC. ADT boxes, lambda envs, and closure pairs all leak. Acceptable
|
|
for current example programs; required before any longer-running
|
|
program.
|
|
|
|
What **is** supported (and used as the smoke test for the pipeline):
|
|
|
|
- Int, Bool, Unit, **Str** as primitive types.
|
|
- `if`, `let`, function calls, recursion.
|
|
- Effects on function signatures, with `do op(args)` for direct effect
|
|
ops (`io/print_int`, `io/print_bool`, `io/print_str`).
|
|
- **ADTs + flat pattern matching** (Iter 3). Sub-patterns of a Ctor
|
|
pattern are restricted to `Var` / `Wild`.
|
|
- **Imports + qualified cross-module references** via dotted names
|
|
(Iter 5).
|
|
- **First-class function references** (Iter 7). A top-level fn name (or
|
|
qualified `prefix.def`) used as a `Term::Var` is a fn-value.
|
|
- **Anonymous lambdas with capture** (Iter 8). `Term::Lam` constructs a
|
|
closure that captures any free variables of its body from the
|
|
enclosing scope. All fn-values share a single ABI: a `ptr` to a
|
|
closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto-
|
|
generated adapter and a static closure pair (env = null) so they
|
|
remain passable as values without heap overhead.
|
|
|
|
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).
|