spec: kernel-extension-mechanics — three-iter prep milestone
docs/specs/2026-05-28-kernel-extension-mechanics.md: per-milestone implementation container for the four language-level mechanisms described in design/models/kernel-extensions.md. Three iterations, each independently shippable: - prep.1 — Type-scoped namespacing. Resolver change so `<TypeName>.<member>` resolves to the type's home module. Migrates ~14 std-library example fixtures from `std_X.Y`-style cross-module references to type-scoped form. Hash pins refreshed in lockstep (ailang-core + ailang-surface — full blast-radius walk, per the hash-pin-audit lesson from schema-camelcase-fix). - prep.2 — Term::New. New AST variant and Form-A keyword `(new T args...)`, calls the `new` def in T's home module. Uses prep.1's resolution. - prep.3 — Kernel-tier modules + `param-in`. Schema flag `Module.kernel` + TypeDef `param-in` field. Workspace-load generalises the existing hardcoded prelude auto-injection (loader.rs:98-108 + workspace.rs:308-311, 467, 2655) into a flag-driven mechanism; prelude itself gains `kernel: true` as a code-path migration (consumer-observable behaviour unchanged — prelude_free_fns.rs regression test stays green). A new minimal ailang-kernel-stub crate ratifies the mechanism without domain content. Five new diagnostics across the three iters: TypeScopedMemberNotFound, TypeScopedReceiverNotAType, NewTypeNotConstructible, NewArgKindMismatch, ParamNotInRestrictedSet. BareCrossModuleTypeRef and BadCrossModuleTypeRef diagnostics repositioned (still "type name not resolvable" but with revised remediation pointers). Each iter's spec section carries explicit `## Canonical form decision`, `## Blast radius`, and `## Integration with existing mechanisms` subsections — the migration-policy discipline made visible per spec section. Grounding-check (two dispatches): first BLOCK on prelude auto-injection mis-framing (claimed it was a new mechanism; in fact prelude is hardcoded-auto-injected today), corrected inline; second PASS after the revised two-tier-architecture framing also landed. All load-bearing assumptions ratified by named tests in the working tree. Out of scope, named explicitly: the raw-buf milestone (#7), the series milestone (#8), record-element SoA support, LSP/MCP integration for `ail describe`, higher-kinded `param-in`, and primitive-instance intercept migration (deferred to #7 when there is a real second consumer for the registry). Refs Gitea milestone #6.
This commit is contained in:
@@ -0,0 +1,713 @@
|
||||
# Kernel extension mechanics — Design Spec
|
||||
|
||||
**Date:** 2026-05-28
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
**Reference:** `design/models/kernel-extensions.md` for the
|
||||
architectural whitepaper. This spec covers the *first* of three
|
||||
milestones implementing the kernel-extensions design: the
|
||||
language-level mechanisms (this milestone), the `raw-buf` base
|
||||
extension (Rust intercepts emitting LLVM IR — the only tier that
|
||||
needs implementation outside AILang itself), and the `series`
|
||||
library extension (pure AILang code wrapping RawBuf). The two
|
||||
follow-up milestones will be brainstormed after this one closes.
|
||||
|
||||
## Goal
|
||||
|
||||
Ship the four language-level mechanisms that the kernel-extensions
|
||||
design requires, with zero domain-specific code (no Series, no
|
||||
Matrix, nothing per-extension). After this milestone, the language
|
||||
supports:
|
||||
|
||||
1. Type-scoped namespacing — `<TypeName>.<member>` resolves to the
|
||||
member's def in the type's home module.
|
||||
2. The `new` term construct — `(new T arg1 arg2 ...)` calls the
|
||||
`new` def in T's home module.
|
||||
3. Kernel-tier modules — `Module.kernel: bool` flag with
|
||||
auto-import of all top-level defs and types.
|
||||
4. `param-in` — closed-set type-parameter restriction on TypeDefs.
|
||||
|
||||
The milestone closes when all four mechanisms are on main, their
|
||||
diagnostics are formulated and tested, the schema-drift pin
|
||||
ratifies the new tags, and a stub kernel-tier module exists
|
||||
purely as a test fixture to exercise the mechanism end-to-end
|
||||
(no domain operations, just a marker type with a `new`).
|
||||
|
||||
## Architecture
|
||||
|
||||
The four mechanisms live in different layers:
|
||||
|
||||
- **Schema layer** (`ailang-core`): `Module.kernel`, `TypeDef.param-in`,
|
||||
`Term::New`. Three additive fields/variants, each `skip_serializing_if`
|
||||
so existing fixtures hash-stable.
|
||||
- **Surface layer** (`ailang-surface`): new keyword `new`,
|
||||
new module header attribute `(kernel)`. Print symmetry preserved.
|
||||
- **Resolver / Checker layer** (`ailang-check`): type-scoped member
|
||||
resolution, `param-in` enforcement, `Term::New` arg-kind checking.
|
||||
- **Workspace-load layer** (`ailang-core::workspace`): kernel-tier
|
||||
auto-import.
|
||||
|
||||
Codegen layer is *not* touched in this milestone. `Term::New` with
|
||||
a kernel-tier consumer would need codegen support, but we ship the
|
||||
mechanisms first and exercise them with non-codegen tests
|
||||
(`ail check` clean is the bar). Codegen integration for kernel
|
||||
extensions happens in the Series milestone, where the first real
|
||||
intercept-registry use case forces the codegen-side mechanism.
|
||||
|
||||
A stub kernel module (`crates/ailang-kernel-stub/`) ships as part
|
||||
of this milestone purely to ratify the mechanism. It contains:
|
||||
|
||||
- One TypeDef with `param-in` set to a small allowed set.
|
||||
- One `new` def with a deliberately constrained signature.
|
||||
- The `kernel: true` flag.
|
||||
|
||||
The stub never reaches codegen — `ail check` is the verification
|
||||
endpoint. When the Series milestone follows, the stub may be
|
||||
retired or repositioned as a regression fixture.
|
||||
|
||||
## Concrete code shapes
|
||||
|
||||
### Iteration prep.1 — Type-scoped namespacing
|
||||
|
||||
**Worked author example (this is what the LLM writes after prep.1
|
||||
lands):**
|
||||
|
||||
```
|
||||
(module consumer
|
||||
(import std_maybe)
|
||||
|
||||
(fn classify
|
||||
(type (fn-type
|
||||
(params (con Int))
|
||||
(ret (con Maybe (con Int)))))
|
||||
(params x)
|
||||
(body
|
||||
(if (app eq x 0)
|
||||
(term-ctor Maybe Nothing)
|
||||
(term-ctor Maybe Just x))))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(app print (app Maybe.from_maybe 99 (app classify 7))))))
|
||||
```
|
||||
|
||||
Key shifts from today's surface:
|
||||
|
||||
- `(con Maybe (con Int))` — bare type, no `std_maybe.` prefix in
|
||||
the type position. (Today this is `(con std_maybe.Maybe (con Int))`.)
|
||||
- `(app Maybe.from_maybe 99 ...)` — type-scoped op access. (Today:
|
||||
`(app std_maybe.from_maybe 99 ...)`.)
|
||||
- `(term-ctor Maybe Just x)` — bare type name in `term-ctor`. (Today:
|
||||
`(term-ctor std_maybe.Maybe Just x)`.)
|
||||
- The `(import std_maybe)` declaration stays — it brings the
|
||||
`Maybe` type into the consumer's type namespace. (Future
|
||||
alternative `(import Maybe from std_maybe)` is out of scope.)
|
||||
|
||||
**Implementation shape (before → after).**
|
||||
|
||||
`ailang-check`'s resolver: today, when seeing `Term::Var { name: "std_maybe.from_maybe" }`,
|
||||
it splits at `.`, looks up `std_maybe` as a module, finds
|
||||
`from_maybe` in that module's defs. After: the same call site
|
||||
with `Term::Var { name: "Maybe.from_maybe" }` first tries to
|
||||
resolve `Maybe` as a type (look up TypeDef in the workspace),
|
||||
then if a TypeDef is found, locates the home module, then looks
|
||||
up `from_maybe` in the home module's defs. If the receiver is
|
||||
neither a module nor a type, emit `TypeScopedReceiverNotAType`.
|
||||
If the receiver is a known type but the member is not in its
|
||||
home module, emit `TypeScopedMemberNotFound`.
|
||||
|
||||
The module-as-receiver path remains supported for free-standing
|
||||
defs (not associated with a single type) but is no longer the
|
||||
canonical form for type-associated operations.
|
||||
|
||||
**Type-position resolution.** `Type::Con { name: "Maybe", args }`
|
||||
in a signature: today the workspace-load rejects bare cross-module
|
||||
type refs via `BareCrossModuleTypeRef`. After prep.1, the resolver
|
||||
first checks whether `Maybe` is in scope (imported by name); if
|
||||
yes, it resolves to the imported type. The `BareCrossModuleTypeRef`
|
||||
diagnostic narrows to: "type name not in scope (no matching import,
|
||||
no kernel-tier provider)". Kernel-tier types are in scope without
|
||||
imports (prep.3).
|
||||
|
||||
**Canonical form decision.** Type-scoped form is canonical for
|
||||
type-associated operations. Module-scoped form is retired for
|
||||
this use case; it remains valid only for module-free defs (defs
|
||||
that do not take a specific type as receiver) and as a workspace
|
||||
collision disambiguator (no current collisions exist).
|
||||
|
||||
**Blast radius.** Per `grep -rE 'std_(maybe|pair|list|either)\.' examples/ crates/`:
|
||||
|
||||
- **`.ail` example fixtures** (~14 files): `ct_2_bare_cross_module.ail`,
|
||||
`ct_3b_bad_qualified_known_module.ail`, `nested_pat.ail`,
|
||||
`std_either.ail`, `std_either_demo.ail`, `std_either_list.ail`,
|
||||
`std_either_list_demo.ail`, `std_list.ail`, `std_list_demo.ail`,
|
||||
`std_list_more_demo.ail`, `std_list_stress.ail`, `std_maybe.ail`,
|
||||
`std_maybe_demo.ail`, `std_pair.ail`, `std_pair_demo.ail`.
|
||||
Each rewritten from `std_X.Y` to `Y` (type-scoped) where Y is
|
||||
type-associated. The defining modules (`std_maybe.ail` etc.)
|
||||
may keep their internal references unchanged (intra-module refs
|
||||
are bare today already).
|
||||
- **Corresponding `.ail.json` fixtures** for round-trip and hash-pin tests.
|
||||
- **Hash-pin files** (2): `crates/ailang-core/tests/hash_pin.rs` and
|
||||
`crates/ailang-surface/tests/prelude_module_hash_pin.rs`. Both
|
||||
refreshed with new hashes. Each refresh carries an Honesty-Rule
|
||||
provenance comment quoting the prep.1 commit and naming the
|
||||
surface change.
|
||||
- **Source-side reference** in `crates/ailang-{check,codegen,surface}/src/`
|
||||
and `crates/ail/tests/e2e.rs` (~7 files): inspect during recon
|
||||
whether they hardcode `std_maybe`/`std_pair`-style identifiers
|
||||
in diagnostic strings or test fixtures. Diagnostic strings
|
||||
update to new vocabulary; test fixtures update to type-scoped.
|
||||
Production type-resolution logic is the new code.
|
||||
- **Drift test** `crates/ailang-core/tests/design_schema_drift.rs`
|
||||
gains a new pin that exercises the type-scoped resolution end-
|
||||
to-end at the schema level.
|
||||
|
||||
The 14 `.ail` examples are rewritten atomically with the resolver
|
||||
change in a single iteration commit. Walking *every* test crate
|
||||
for hash-pin sites is mandatory (per the
|
||||
`hash-pin blast-radius audit` lesson from `schema-camelcase-fix`).
|
||||
|
||||
**Integration with existing mechanisms.**
|
||||
|
||||
- `BareCrossModuleTypeRef` / `BadCrossModuleTypeRef` diagnostics
|
||||
are repurposed: they fire when a type name is not in scope by
|
||||
any path (import, kernel-tier, type-scoped). The class of
|
||||
errors they detect narrows, the underlying user-facing message
|
||||
becomes more helpful (it can suggest the import or the
|
||||
type-scoped form).
|
||||
- Module-scoped access remains the path for free-standing fns
|
||||
(e.g. a hypothetical `std_math.factorial` that doesn't have a
|
||||
receiver type). No retirement of the module-scope mechanism
|
||||
itself.
|
||||
- Class method dispatch (see [method-dispatch](../../design/contracts/method-dispatch.md))
|
||||
is orthogonal. `(app show x)` continues to type-dispatch via the
|
||||
Show instance; this is not type-scoped namespacing.
|
||||
- `term-ctor` and `pat-ctor` continue to use bare ctor names
|
||||
inside the scrutinee — `(term-ctor Maybe Just x)` works
|
||||
because `Maybe` is now in scope via type-scoped resolution.
|
||||
|
||||
### Iteration prep.2 — `new` term construct
|
||||
|
||||
**Worked author example (after prep.2; uses a non-kernel test
|
||||
type to exercise the construct):**
|
||||
|
||||
```
|
||||
(module new_demo
|
||||
(data Counter
|
||||
(ctor MkCounter (con Int)))
|
||||
|
||||
(fn new
|
||||
(doc "Build a Counter initialised to the given value.")
|
||||
(type (fn-type (params (con Int)) (ret (con Counter))))
|
||||
(params n)
|
||||
(body (term-ctor Counter MkCounter n)))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(let c (new Counter 42)
|
||||
(match c
|
||||
(case (pat-ctor MkCounter x) (app print x)))))))
|
||||
```
|
||||
|
||||
The `(new Counter 42)` desugars to: look up `Counter`'s home
|
||||
module (this very module), find the `new` def, call it with `42`.
|
||||
|
||||
For a future kernel-tier consumer with a `new` taking a Type arg:
|
||||
|
||||
```
|
||||
; (Future Series, exercised in milestone 2.)
|
||||
(let s (new Series (con Float) 3)
|
||||
...)
|
||||
```
|
||||
|
||||
Here the first arg `(con Float)` is parsed as a Type (per the
|
||||
`NewArg::Type` discriminator), the second `3` as a Term.
|
||||
|
||||
**Implementation shape.**
|
||||
|
||||
New AST variant in `ailang-core/src/ast.rs`:
|
||||
|
||||
```rust
|
||||
pub enum Term {
|
||||
// ...
|
||||
New {
|
||||
type_name: TypeName,
|
||||
args: Vec<NewArg>,
|
||||
},
|
||||
}
|
||||
|
||||
pub enum NewArg {
|
||||
Type(Type),
|
||||
Value(Term),
|
||||
}
|
||||
```
|
||||
|
||||
Serialised JSON:
|
||||
|
||||
```jsonc
|
||||
{ "t": "new",
|
||||
"type": "Series",
|
||||
"args": [
|
||||
{ "kind": "type", "value": { ... type expr ... } },
|
||||
{ "kind": "value", "value": { ... term expr ... } }
|
||||
]
|
||||
}
|
||||
```
|
||||
|
||||
`type_name` carries no module qualifier — it is resolved via
|
||||
type-scoped lookup at check time (depends on prep.1).
|
||||
|
||||
**Form-A surface.** Lex/Parse adds `new` as a keyword. Production:
|
||||
|
||||
```
|
||||
⟨new⟩ ::= '(' 'new' ⟨TypeName⟩ ⟨NewArg⟩+ ')'
|
||||
⟨NewArg⟩ ::= ⟨Type⟩ ; matches if token sequence parses as a Type production
|
||||
| ⟨Term⟩ ; otherwise
|
||||
```
|
||||
|
||||
The disambiguation between Type and Term args is by syntactic
|
||||
form: a Type starts with `(con …)`, `(fn-type …)`, `(borrow …)`,
|
||||
`(own …)`, etc. — the existing Type-production keywords. A Term
|
||||
in arg position is anything else.
|
||||
|
||||
**Checker.** When elaborating `Term::New { type_name, args }`:
|
||||
|
||||
1. Look up `type_name` via type-scoped resolution → home module.
|
||||
2. Find `new` def in that home module. If missing, emit
|
||||
`NewTypeNotConstructible`.
|
||||
3. Check arg count against `new`'s signature.
|
||||
4. For each arg position: the signature's param kind (Type or
|
||||
Value) must match the `NewArg` kind. Mismatch emits
|
||||
`NewArgKindMismatch`.
|
||||
5. If `new`'s signature includes a `forall` over a type variable
|
||||
instantiated by a Type-positional arg, bind that variable to
|
||||
the supplied type. Apply `param-in` restriction (prep.3) if
|
||||
declared.
|
||||
|
||||
**Canonical form decision.** `new` is the canonical construction
|
||||
form when construction is *functional* (calls a function). It
|
||||
does not replace `term-ctor`, which remains canonical for
|
||||
named-data-ctor construction in ADTs.
|
||||
|
||||
**Blast radius.** Small. No existing fixture uses a `new` keyword
|
||||
or pattern, since the keyword does not exist today. The schema
|
||||
additions are new variants and new JSON tags; existing fixtures
|
||||
emit unchanged bytes (no `t: "new"` appears anywhere today).
|
||||
A new in-source test in `ailang-check/src/lib.rs`'s
|
||||
`#[cfg(test)]` module exercises the resolution path on the
|
||||
`new_demo` example fixture above.
|
||||
|
||||
**Integration with existing mechanisms.**
|
||||
|
||||
- `term-ctor` continues to construct ADT values via named data
|
||||
ctors. The two constructs answer different design needs (see
|
||||
whitepaper).
|
||||
- The `new` keyword does not collide with any existing identifier
|
||||
(no def named `new` exists in current workspace per `grep`).
|
||||
If a user-defined module ever wanted to call something `new`,
|
||||
that name is now reserved as a Form-A keyword — they have to
|
||||
pick a different name. Pre-production stage, no breakage risk.
|
||||
- Type-scoped resolution (prep.1) is the dependency: `Term::New`
|
||||
uses it to find the home module of `type_name`.
|
||||
|
||||
### Iteration prep.3 — Kernel-tier modules + `param-in`
|
||||
|
||||
This iteration ships two coupled mechanisms in one atomic step,
|
||||
because the `param-in` restriction is the first checker behavior
|
||||
that depends on the workspace knowing about kernel-tier modules
|
||||
(the stub kernel module is the test fixture for both).
|
||||
|
||||
**Worked author example — kernel-tier stub module (this is the
|
||||
test fixture, not user-facing code):**
|
||||
|
||||
```
|
||||
; crates/ailang-kernel-stub/module.ail.json (or programmatic form)
|
||||
; The stub module exists only to exercise the mechanism — both
|
||||
; `kernel: true` auto-import and `param-in` enforcement.
|
||||
(module kernel_stub (kernel)
|
||||
|
||||
(type StubT (vars a)
|
||||
(param-in (a Int Float))
|
||||
(ctors (Stub a)))
|
||||
|
||||
(fn new
|
||||
(doc "Construct StubT<Int> — exercises Term::New end-to-end.")
|
||||
(type (fn-type (params (con Int)) (ret (con StubT (con Int)))))
|
||||
(params x)
|
||||
(body (term-ctor StubT Stub x))))
|
||||
```
|
||||
|
||||
**Worked consumer (no `(import kernel_stub)` needed — kernel-tier):**
|
||||
|
||||
```
|
||||
(module stub_consumer
|
||||
; No import line. kernel_stub is auto-imported.
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(let s (new StubT 42)
|
||||
(match s
|
||||
(case (pat-ctor Stub x) (app print x)))))))
|
||||
```
|
||||
|
||||
The `(new StubT 42)` form names the unapplied type constructor
|
||||
`StubT`; the resolver looks up `StubT`'s home module (`kernel_stub`),
|
||||
finds `new` there, types the call against `new`'s signature
|
||||
`(Int) -> StubT Int`. The result type `StubT Int` triggers a
|
||||
`param-in` check on the type-arg `Int` — `Int ∈ {Int, Float}` so
|
||||
it passes. A pattern match on `(pat-ctor Stub x)` extracts and
|
||||
prints the wrapped Int.
|
||||
|
||||
**Worked rejection — `param-in` violation:**
|
||||
|
||||
```
|
||||
(fn bad
|
||||
(type (fn-type
|
||||
(params (con StubT (con Str))) ; Str not in {Int, Float}
|
||||
(ret (con Unit))))
|
||||
(params s)
|
||||
(body unit))
|
||||
; expected: ParamNotInRestrictedSet on `(con StubT (con Str))`
|
||||
```
|
||||
|
||||
**Implementation shape.**
|
||||
|
||||
Schema additions in `ailang-core/src/ast.rs`:
|
||||
|
||||
```rust
|
||||
pub struct Module {
|
||||
// ...
|
||||
#[serde(default, skip_serializing_if = "is_false")]
|
||||
pub kernel: bool,
|
||||
}
|
||||
|
||||
pub struct TypeDef {
|
||||
// ...
|
||||
#[serde(default, skip_serializing_if = "BTreeMap::is_empty",
|
||||
rename = "param-in")]
|
||||
pub param_in: BTreeMap<String, BTreeSet<TypeName>>,
|
||||
}
|
||||
```
|
||||
|
||||
Both `skip_serializing_if` so existing TypeDefs and Modules hash-
|
||||
identical.
|
||||
|
||||
**Form-A surface.** Module header gains `(kernel)` attribute:
|
||||
|
||||
```
|
||||
(module foo (kernel) ...)
|
||||
```
|
||||
|
||||
TypeDef body gains optional `(param-in (var type1 type2 ...))` block:
|
||||
|
||||
```
|
||||
(type T (vars a)
|
||||
(param-in (a Int Float))
|
||||
(ctors))
|
||||
```
|
||||
|
||||
**Workspace-load.** Today, the loader hardcodes a single auto-
|
||||
injected module: `crates/ailang-surface/src/loader.rs:98-108`
|
||||
unconditionally calls `parse_prelude()` and threads the literal
|
||||
`&["prelude"]` slice into `ailang_core::workspace::build_workspace`
|
||||
as the implicit-imports list. The reservation of `prelude` as
|
||||
an auto-injected name is documented at `workspace.rs:308-311`,
|
||||
and the build contract at `workspace.rs:467`. This is the
|
||||
mechanism that makes the prelude's 12 free fns (`ne`, `lt`,
|
||||
`le`, `gt`, `ge`, `print`, `float_eq`...`float_ge`) callable bare
|
||||
in every consumer module today (ratified by
|
||||
`crates/ail/tests/prelude_free_fns.rs`).
|
||||
|
||||
prep.3 *generalises* this single-name auto-injection into a
|
||||
flag-driven multi-module mechanism. After prep.3:
|
||||
|
||||
- `workspace::build_workspace`'s implicit-imports parameter is
|
||||
derived from "all modules in the workspace with `kernel: true`",
|
||||
not from a hardcoded literal.
|
||||
- `loader.rs`'s `parse_prelude()` injection remains (prelude is a
|
||||
built-in module — it has no on-disk manifest in user
|
||||
workspaces and must be injected from the compiler's own
|
||||
resources), but the *naming* of `prelude` as the implicit
|
||||
import is no longer hardcoded; it follows from prelude's
|
||||
`kernel: true` flag.
|
||||
- Other kernel-tier modules (e.g. the stub crate, future Series
|
||||
crate) are loaded through the normal workspace discovery and
|
||||
picked up by the same `kernel: true` filter.
|
||||
|
||||
The name-resolution precedence rule (explicit imports beat
|
||||
auto-import) is the existing behaviour, retained.
|
||||
|
||||
**Checker.** When resolving `Type::Con { name, args }`:
|
||||
|
||||
1. After standard TypeDef lookup, fetch `param_in` from the
|
||||
TypeDef.
|
||||
2. For each entry `(var, allowed_set)`:
|
||||
- Locate the positional `args[i]` corresponding to `var` (by
|
||||
name lookup in TypeDef's `vars`).
|
||||
- Walk `args[i]` to its outermost type-name (peel through
|
||||
mode wrappers).
|
||||
- If not a primitive type name in `allowed_set`, emit
|
||||
`ParamNotInRestrictedSet { type_name, var, found, allowed }`.
|
||||
|
||||
The check is *generic*: nothing in the checker mentions Series
|
||||
or any specific extension type. The restriction is data-driven
|
||||
from the TypeDef.
|
||||
|
||||
**Canonical form decision.** `param-in` is the canonical form for
|
||||
closed-set type-parameter restrictions. Marker classes (a class
|
||||
with no methods, used solely for type-tagging) are not
|
||||
introduced as a parallel mechanism.
|
||||
|
||||
**Blast radius.**
|
||||
|
||||
- The `prelude` module gains `kernel: true`. **This is a code-
|
||||
path migration, not a behaviour change.** Prelude has 12 free
|
||||
fns today (`examples/prelude.ail:85-148`: `ne`, `lt`, `le`,
|
||||
`gt`, `ge`, `print`, `float_eq`, `float_ne`, `float_lt`,
|
||||
`float_le`, `float_gt`, `float_ge`) plus its three classes.
|
||||
All 12 free fns are already callable bare in consumer modules
|
||||
via the hardcoded auto-injection at `loader.rs:98-108`. After
|
||||
prep.3, the same 12 fns remain callable bare — but the
|
||||
reachability path is the generic `kernel: true` filter, not
|
||||
the hardcoded `&["prelude"]` literal. Consumer-observable
|
||||
behaviour: identical. Code-path: rewritten. The hash-pin
|
||||
refresh in `crates/ailang-surface/tests/prelude_module_hash_pin.rs`
|
||||
is required because the canonical-JSON of the prelude module
|
||||
now contains `"kernel": true`, which changes the module hash;
|
||||
the test file gets the new hash plus an Honesty-Rule
|
||||
provenance comment quoting prep.3.
|
||||
- `crates/ailang-surface/src/loader.rs` and
|
||||
`crates/ailang-core/src/workspace.rs` lose the hardcoded
|
||||
prelude-specific paths; they gain the flag-driven equivalent.
|
||||
Detailed sites: `loader.rs:98-108`, `workspace.rs:308-311,
|
||||
467, 2655`. The `WorkspaceLoadError::ReservedModuleName`
|
||||
diagnostic (currently fires when a user workspace contains a
|
||||
module named `prelude`) is repositioned: any module named the
|
||||
same as an auto-injected built-in kernel module is reserved,
|
||||
not specifically `prelude`. For this milestone the list is
|
||||
still just `prelude` + the new stub.
|
||||
- The new `crates/ailang-kernel-stub/` crate is created with
|
||||
its `module.ail.json` and the build wiring to feed it into
|
||||
the workspace load.
|
||||
- The schema-drift pin in `crates/ailang-core/tests/design_schema_drift.rs`
|
||||
gains entries for `kernel`, `param-in`, and a basic stub
|
||||
module round-trip.
|
||||
- `crates/ail/tests/prelude_free_fns.rs` continues to pass
|
||||
unchanged — that is the explicit regression-protection that
|
||||
the prelude code-path migration is behaviour-equivalent.
|
||||
- Workspace-load tests under `crates/ailang-core/tests/` gain
|
||||
a new fixture exercising auto-import of the stub kernel
|
||||
module from a consumer with no `(import ...)` declaration.
|
||||
|
||||
**Integration with existing mechanisms.**
|
||||
|
||||
- The prelude module's role in the workspace loader is unified
|
||||
with the kernel-tier mechanism. The hardcoded prelude-name
|
||||
paths today exist concretely at `loader.rs:98-108` (the
|
||||
`parse_prelude()` injection + `&["prelude"]` literal) and
|
||||
`workspace.rs:308-311, 467, 2655` (reservation + contract
|
||||
docs). They are migrated to read `module.kernel` from each
|
||||
loaded module's schema and build the implicit-imports list
|
||||
from the resulting set. Single named mechanism for
|
||||
"module is auto-imported"; no module name is hardcoded as
|
||||
special.
|
||||
- Class constraints (existing) and `param-in` (new) coexist —
|
||||
see the whitepaper's "marker class" discussion.
|
||||
- `Term::New` (prep.2) uses `param-in` via the standard checker
|
||||
path — when `new`'s return type is `T<a>` with `a` restricted,
|
||||
the type-arg supplied at the new-site is validated.
|
||||
- The existing primitive-instance codegen intercept
|
||||
(`try_emit_primitive_instance_body` in `ailang-codegen`) is
|
||||
*not* touched in this milestone. Its migration to a plugin
|
||||
registry happens in the Series milestone, where there is a
|
||||
real second consumer for the registry. Single-consumer
|
||||
registries are premature mechanism.
|
||||
|
||||
## Components
|
||||
|
||||
| Component | Crate | What changes |
|
||||
|-----------|-------|-------------|
|
||||
| AST schema | `ailang-core` | `Module.kernel`, `TypeDef.param-in`, `Term::New`, `NewArg` |
|
||||
| Form-A surface | `ailang-surface` | `new` keyword, `(kernel)` module attr, `(param-in ...)` typedef attr |
|
||||
| Workspace-load | `ailang-core::workspace` | Kernel-tier auto-import scope |
|
||||
| Resolver | `ailang-check` | Type-scoped member resolution, `Term::New` arg-kind check, `param-in` enforcement |
|
||||
| Drift pin | `ailang-core/tests/design_schema_drift.rs` | New schema tags ratified |
|
||||
| Hash pins | `ailang-core/tests/hash_pin.rs`, `ailang-surface/tests/prelude_module_hash_pin.rs` | Refreshed for the rewrites |
|
||||
| Std fixture migration | `examples/*.ail` (~14 files) | `std_X.Y` → type-scoped form |
|
||||
| Stub kernel crate | `crates/ailang-kernel-stub/` | New, minimal — exercises the mechanism |
|
||||
|
||||
## Data flow
|
||||
|
||||
A `.ail` consumer module that uses a kernel-tier type:
|
||||
|
||||
1. **Workspace load.** Each module's manifest is read. Kernel-tier
|
||||
modules are collected; their type names and def names enter
|
||||
the auto-import scope.
|
||||
2. **Parse.** The consumer's `(con Series ...)` (or `(con StubT ...)`
|
||||
in this milestone's stub) parses to `Type::Con { name: "Series" }`.
|
||||
`(new Series ...)` parses to `Term::New { type_name: "Series", args: [...] }`.
|
||||
`(app Series.at s i)` parses to `Term::App { callee: Term::Var { name: "Series.at" }, args }`.
|
||||
3. **Resolve.** Type-scoped resolver looks up `Series` in the
|
||||
workspace TypeDef registry (auto-imported via kernel-tier).
|
||||
`Series.at` resolves to the `at` def in Series's home module
|
||||
(the stub or, in milestone 2, the Series crate).
|
||||
4. **Type-check.** `param-in` enforcement runs on `Type::Con {
|
||||
name: "Series", args }` — element type must be in the allowed
|
||||
set. `Term::New` arg-kind check runs on the args. Standard
|
||||
type-check otherwise.
|
||||
5. **Done at `ail check`.** Codegen is out of scope this milestone.
|
||||
|
||||
## Error handling
|
||||
|
||||
New diagnostics introduced this milestone (all in `ailang-check`):
|
||||
|
||||
| Diagnostic | Trigger | Iteration |
|
||||
|------------|---------|-----------|
|
||||
| `TypeScopedMemberNotFound` | `T.x` where T is a type but `x` not in T's home module | prep.1 |
|
||||
| `TypeScopedReceiverNotAType` | `X.y` where X is neither a known type nor a known module | prep.1 |
|
||||
| `NewTypeNotConstructible` | `(new T args)` where T has no `new` def in its home module | prep.2 |
|
||||
| `NewArgKindMismatch` | `(new T args)` where an arg is Type-positional where Value expected (or vice versa) | prep.2 |
|
||||
| `ParamNotInRestrictedSet` | `Type::Con { name, args }` where `args[i]` violates the TypeDef's `param-in` for the corresponding var | prep.3 |
|
||||
|
||||
`BareCrossModuleTypeRef` and `BadCrossModuleTypeRef` (pre-existing)
|
||||
are repurposed in prep.1: they now fire when a type name resolves
|
||||
through neither type-scoped lookup, nor an explicit import, nor a
|
||||
kernel-tier auto-import. The semantic class of error remains "type
|
||||
name not resolvable", but the suggested fix in the message
|
||||
changes.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
**Layer 1 — Schema drift** (`crates/ailang-core/tests/design_schema_drift.rs`):
|
||||
- `module_kernel_flag_round_trips` — pins `Module.kernel = true`
|
||||
serialises and deserialises with bit-identical bytes; `kernel:
|
||||
false` is omitted from output.
|
||||
- `typedef_param_in_round_trips` — pins `TypeDef.param_in` map
|
||||
serialises with the `param-in` key (kebab); empty map omitted.
|
||||
- `term_new_round_trips` — pins `Term::New { type_name, args }`
|
||||
serialises with `t: "new"`, each arg with `kind: "type"|"value"`.
|
||||
|
||||
**Layer 2 — Round-trip surface** (`crates/ailang-surface/tests/round_trip.rs`):
|
||||
- Fixture for `(kernel)` in module header.
|
||||
- Fixture for `(new T ...)` with mixed-kind args.
|
||||
- Fixture for `(param-in (var t1 t2))` in TypeDef.
|
||||
- All fixtures round-trip Form-A → JSON → Form-A bit-identical.
|
||||
|
||||
**Layer 3 — Checker** (`crates/ailang-check/src/*.rs` in-source tests):
|
||||
- `type_scoped_member_resolves` — `Maybe.from_maybe` resolves to
|
||||
`std_maybe.from_maybe`'s def.
|
||||
- `type_scoped_member_not_found` — `Maybe.bogus` emits diagnostic.
|
||||
- `type_scoped_receiver_not_a_type` — `NotAType.x` emits diagnostic.
|
||||
- `new_resolves_via_type_scope` — `(new Counter 42)` finds local
|
||||
`new` def.
|
||||
- `new_type_not_constructible` — `(new IntList ...)` (no `new` def
|
||||
in IntList's home module) emits diagnostic.
|
||||
- `new_arg_kind_mismatch_value_where_type` — `(new Series 3 (con Float))`
|
||||
emits diagnostic.
|
||||
- `param_in_accepts_allowed_type` — `(con StubT (con Int))`
|
||||
type-checks.
|
||||
- `param_in_rejects_disallowed_type` — `(con StubT (con Str))`
|
||||
emits `ParamNotInRestrictedSet`.
|
||||
|
||||
**Layer 4 — Workspace load** (`crates/ailang-core/tests/workspace_kernel.rs`,
|
||||
new):
|
||||
- Kernel-tier module's types are visible to a consumer without
|
||||
any `(import ...)` declaration.
|
||||
- Two kernel-tier modules with non-colliding names co-load.
|
||||
- Explicit import overrides auto-import (precedence test).
|
||||
|
||||
**Layer 5 — End-to-end via `ail check`** (`crates/ail/tests/e2e.rs`):
|
||||
- The stub kernel module + a stub consumer checks clean.
|
||||
- The `param-in` violation example produces the expected
|
||||
diagnostic.
|
||||
|
||||
**Layer 6 — Migrated std-library examples**:
|
||||
- All migrated `.ail` examples (std_maybe_demo, std_list_demo,
|
||||
etc.) check clean. Their `.ail.json` round-trip pins refreshed.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
Milestone closes when:
|
||||
|
||||
1. All four mechanisms (type-scoped namespacing, `Term::New`,
|
||||
kernel-tier modules + auto-import, `param-in`) are implemented
|
||||
and merged to main.
|
||||
2. All five new diagnostics fire on their RED fixtures and do
|
||||
not fire on green code.
|
||||
3. The schema-drift pin ratifies `kernel`, `param-in`, `new`,
|
||||
`NewArg` JSON tags.
|
||||
4. The round-trip test exercises all new surface forms.
|
||||
5. The stub kernel crate's module checks clean and is auto-
|
||||
imported by a consumer module with no explicit import.
|
||||
6. All 14-ish migrated `.ail` examples in `examples/` check
|
||||
clean and round-trip to byte-identical Form-A.
|
||||
7. Hash pins refreshed in both `crates/ailang-core/tests/hash_pin.rs`
|
||||
and `crates/ailang-surface/tests/prelude_module_hash_pin.rs`,
|
||||
each with an Honesty-Rule provenance comment.
|
||||
8. The whitepaper `design/models/kernel-extensions.md` is
|
||||
updated: sections describing prep.1, prep.2, prep.3 transition
|
||||
from forward-looking ("will resolve…") to present-state
|
||||
("resolves…") where appropriate; STATUS header updated to
|
||||
"Mechanisms milestone closed YYYY-MM-DD; Series milestone
|
||||
pending."
|
||||
9. The `design/INDEX.md` ledger entry's "design accepted
|
||||
2026-05-28; impl in progress" annotation is updated to reflect
|
||||
the milestone close.
|
||||
10. `bench/check.py` clean — no performance regression on the
|
||||
existing benches (this milestone touches resolver / parser /
|
||||
schema, not codegen or runtime; regression is unexpected
|
||||
but bench is part of the close-out per audit discipline).
|
||||
|
||||
## Out of scope (explicit)
|
||||
|
||||
- The `RawBuf` base extension — kernel-tier module with Rust
|
||||
codegen intercepts emitting LLVM IR for `new`/`get`/`set`/`size`,
|
||||
element-type restriction via `param-in`. Future Gitea milestone
|
||||
`raw-buf`.
|
||||
- The `Series` library extension — kernel-tier `.ail` module
|
||||
defining the Series ADT and its operations (push/at/len/
|
||||
total_count) in AILang itself, on top of RawBuf. Future Gitea
|
||||
milestone `series`.
|
||||
- Migration of `try_emit_primitive_instance_body` into a plugin
|
||||
intercept registry. Happens in the `raw-buf` milestone when
|
||||
the first base-extension consumer exists.
|
||||
- LSP / MCP integration for `ail describe Series`. Out of scope
|
||||
for all three milestones; future axis.
|
||||
- Higher-kinded `param-in` (the restriction is currently
|
||||
flat — type variable to set of named types; future variants
|
||||
might restrict to "any type satisfying some structural
|
||||
predicate", but that is not specified here).
|
||||
- Type-scoped access on user types ≠ home-module defs (e.g.
|
||||
cross-module-extension methods). Out of scope; the mechanism
|
||||
is strictly "type T's home module's defs are accessible as
|
||||
T.x".
|
||||
- An auto-import precedence override syntax (the explicit-import
|
||||
wins behaviour is implementation; no new author syntax is added
|
||||
for it).
|
||||
- Record-element support in RawBuf (the struct-of-arrays layout
|
||||
for `Series Record`). The architecture accommodates it (see
|
||||
whitepaper § "Forward axis: SoA for records") but it is a
|
||||
later RawBuf-internal change that does not touch Series's
|
||||
AILang code; out of scope for the three named milestones.
|
||||
|
||||
## Iteration scope
|
||||
|
||||
The plan that follows this spec carves the work into three
|
||||
iterations:
|
||||
|
||||
- **prep.1** — Type-scoped namespacing. Resolver change + 14
|
||||
example rewrites + 2 hash-pin refreshes.
|
||||
- **prep.2** — `Term::New`. AST + surface + checker arg-kind
|
||||
enforcement.
|
||||
- **prep.3** — Kernel-tier modules + `param-in`. Schema +
|
||||
workspace-load + checker enforcement + stub crate.
|
||||
|
||||
Each iteration is independently shippable; main is green at every
|
||||
iteration boundary.
|
||||
Reference in New Issue
Block a user