73fbb240be
The `series` library extension shipped (35a9bc6); model 0007's
Series section was an aspirational sketch with systematic defects
that no longer match the live tool. Bring it to present-state per
the honesty-rule:
- STATUS: the library-extension milestone now reads step-1 shipped
(primitive Series over {Int, Float}, Bool deferred), with SoA
step-2 (#62) still pending. INDEX.md row updated to match.
- The `series` code listing is replaced with the shipped source
(crates/ailang-kernel/src/series/source.ail, doc-strings elided),
cited as the source of truth. Every defect the sketch carried is
corrected in the shipped form it now shows: param-in (a Int Float)
not (... Bool); `(new RawBuf lookback)` with no type-arg; bare `a`
for the element type variable (not `(con a)`); forall-bound op
signatures; `lt` not `<`; and the at-index formula with the
correct sign on i — which already matched the section's own prose
(`head - 1 - i + 2*lookback`), so the sketch was internally
inconsistent and the prose was right.
- The SMA worked example uses `ge` (not the non-existent `>=`) and
emits each average followed by a newline, matching the committed
pin fixture so the doc and the test agree.
- The "four constructs not in today's AILang" framing is now
present-state: the mechanisms shipped via raw_buf, Series itself
via the step-1 library extension.
Both edited module blocks parse against the live tool.
refs #61
692 lines
29 KiB
Markdown
692 lines
29 KiB
Markdown
# Kernel extensions — plugin-style domain types whitepaper
|
|
|
|
**STATUS.** Mechanisms milestone closed 2026-05-28
|
|
(`kernel-extension-mechanics`; iterations prep.1, prep.2, prep.3
|
|
landed). The four language-level mechanisms — type-scoped
|
|
namespacing, `Term::New`, kernel-tier modules + auto-import, and
|
|
`param-in` — are shipped and ratified by the `raw_buf` base
|
|
extension (`crates/ailang-kernel/src/raw_buf/`). The base-extension
|
|
milestone (`raw-buf`) has shipped. The library-extension milestone
|
|
(`series`) has shipped its step-1 primitive Series over `{Int, Float}`
|
|
(`crates/ailang-kernel/src/series/`, the first pure-AILang library
|
|
extension; `param-in` defers `Bool`); step 2 — struct-of-arrays
|
|
record elements (#62) — is pending. This
|
|
whitepaper describes the design as a coherent whole; the
|
|
per-milestone specs in `docs/specs/` carry the implementation-
|
|
level detail. Sections describing the now-shipped mechanisms read
|
|
in present-state per the
|
|
[honesty-rule](../contracts/0007-honesty-rule.md); sections about
|
|
the still-pending milestones keep their forward-looking framing.
|
|
|
|
## The problem
|
|
|
|
AILang's core needs to stay small. Five primitive types (`Int`,
|
|
`Bool`, `Unit`, `Str`, `Float`), algebraic data types, typeclasses,
|
|
algebraic effects, RC + uniqueness — that is the language. New
|
|
primitive types are a tax: they inflate the schema, the checker,
|
|
the codegen, the documentation surface, and the LLM-author's
|
|
mental model of what the language is.
|
|
|
|
But: AILang authors will work in specific domains. Streaming
|
|
analytics wants a bounded ring buffer. Numerical work wants flat
|
|
arrays and matrices. Financial work wants fixed-precision decimals
|
|
and timestamps with arithmetic. None of these belong in
|
|
`ailang-core` — yet without them, the LLM author has to hand-roll
|
|
linked-list approximations that are algorithmically wrong (O(N²)
|
|
where O(N) is the natural complexity).
|
|
|
|
The resolution: **kernel extensions** — a plugin contract that
|
|
lets a domain-specific type live in its own crate, register with
|
|
the compiler at boot time, and present itself to user code as if
|
|
it were a built-in primitive. Core has no domain knowledge of any
|
|
specific extension; extensions have no core dependency beyond the
|
|
plugin contract.
|
|
|
|
The first consumer is `Series` — a bounded ring buffer for
|
|
streaming data. Future consumers are not specified here but the
|
|
shape is intentional: each new domain type is one new crate, zero
|
|
core changes.
|
|
|
|
## Worked example — `Series` for streaming analytics
|
|
|
|
What an LLM-author writes when given the task "compute simple
|
|
moving average over a stream of float values, window size 3":
|
|
|
|
```
|
|
(module sma_demo
|
|
|
|
(data FloatList
|
|
(ctor FNil)
|
|
(ctor FCons (con Float) (con FloatList)))
|
|
|
|
(fn sum_window_step
|
|
(type (fn-type
|
|
(params (borrow (con Series (con Float))) (own (con Int)) (own (con Int)) (own (con Float)))
|
|
(ret (own (con Float)))))
|
|
(params s n i acc)
|
|
(body
|
|
(if (app eq i n)
|
|
acc
|
|
(tail-app sum_window_step s n
|
|
(app + i 1)
|
|
(app + acc (app Series.at s i))))))
|
|
|
|
(fn emit_if_full
|
|
(type (fn-type
|
|
(params (borrow (con Series (con Float))) (own (con Int)))
|
|
(ret (own (con Unit))) (effects IO)))
|
|
(params s n)
|
|
(body
|
|
(if (app ge (app Series.total_count s) n)
|
|
(seq
|
|
(app print (app /
|
|
(app sum_window_step s n 0 0.0)
|
|
(app int_to_float n)))
|
|
(do io/print_str "\n"))
|
|
(do io/print_str ""))))
|
|
|
|
(fn run_stream
|
|
(type (fn-type
|
|
(params (own (con Series (con Float))) (own (con Int)) (own (con FloatList)))
|
|
(ret (own (con Unit))) (effects IO)))
|
|
(params s n input)
|
|
(body
|
|
(match input
|
|
(case (pat-ctor FNil) (do io/print_str ""))
|
|
(case (pat-ctor FCons v rest)
|
|
(let s_new (app Series.push s v)
|
|
(seq (app emit_if_full s_new n)
|
|
(tail-app run_stream s_new n rest)))))))
|
|
|
|
(fn main
|
|
(type (fn-type (params) (ret (own (con Unit))) (effects IO)))
|
|
(params)
|
|
(body
|
|
(let s (new Series (con Float) 3)
|
|
(app run_stream s 3
|
|
(term-ctor FloatList FCons 1.0
|
|
(term-ctor FloatList FCons 5.0
|
|
(term-ctor FloatList FCons 3.0
|
|
(term-ctor FloatList FCons 8.0
|
|
(term-ctor FloatList FCons 6.0
|
|
(term-ctor FloatList FCons 2.0
|
|
(term-ctor FloatList FNil))))))))))))
|
|
```
|
|
|
|
Four constructs in this program rest on the four mechanisms this
|
|
whitepaper defines — all now shipped (the mechanisms via the
|
|
`raw_buf` base extension, `Series` itself via the step-1 library
|
|
extension):
|
|
|
|
- `Series` appears in type position with no module qualifier
|
|
(`(con Series (con Float))`) — *kernel-tier modules*.
|
|
- `(new Series (con Float) 3)` constructs the series — *new term
|
|
construct*.
|
|
- `(app Series.at s i)`, `(app Series.total_count s)`,
|
|
`(app Series.push s v)` — *type-scoped namespacing*.
|
|
- The `(own (con Series ...))` mode on `run_stream` plus the linear
|
|
state-threading via `(let s_new ...)` is the *uniqueness mode*
|
|
discipline that already exists in AILang. Series carries no
|
|
separate algebraic effect; its mutation is mode-tracked, not
|
|
effect-tracked. Under uniqueness inference (Gitea #22), the
|
|
rebuild-on-push compiles to in-place mutation.
|
|
|
|
A fifth mechanism, `param-in`, is not visible at the call site but
|
|
enforces that `(con Series (con Str))` would be rejected.
|
|
|
|
## The four mechanisms
|
|
|
|
### 1. Type-scoped namespacing
|
|
|
|
**Form.** `<TypeName>.<member>` resolves to the `<member>`
|
|
definition in the home module of `<TypeName>`. The home module of
|
|
a type `T` is the module whose `defs` contains a `TypeDef` named
|
|
`T`.
|
|
|
|
**Canonical form.** Type-scoped access is the *canonical* form for
|
|
operations associated with a type. The pre-existing module-scoped
|
|
form (`<module>.<member>`) remains a valid surface only for
|
|
free-standing definitions not bound to a specific type receiver,
|
|
and as a collision disambiguator if two types in the workspace
|
|
ever shared a name (which is not the case today).
|
|
|
|
**Examples.**
|
|
|
|
```
|
|
(app Series.at s i) ; series_at via type-scope
|
|
(app Maybe.from_maybe 0 m) ; from_maybe via type-scope (was: std_maybe.from_maybe)
|
|
(con Series (con Float)) ; type itself accessible bare under kernel-tier
|
|
(con Maybe (con Int)) ; type itself, if Maybe is in scope via import
|
|
```
|
|
|
|
**Why this is LLM-natural.** When asked "what can I do with a
|
|
Series?", an LLM produces `Series.<x>` queries. When asked "what
|
|
can I do with a Maybe?", it produces `Maybe.<x>` queries. The
|
|
type, not the module, is the LLM's mental anchor. Module-scoped
|
|
access requires knowing where a function lives — extra cognitive
|
|
load with no expressive benefit.
|
|
|
|
**Schema impact.** Zero. The dotted form already parses today as
|
|
`Term::Var { name: "Maybe.from_maybe" }` (the `.` is a permitted
|
|
identifier character in the existing lexer). What changes is the
|
|
*resolver*: it tries the type-namespace branch first, falls back
|
|
to the module-namespace branch.
|
|
|
|
**Diagnostics.** `TypeScopedMemberNotFound` (the receiver is a
|
|
known type, but the member is not defined in its home module);
|
|
`TypeScopedReceiverNotAType` (the receiver name is neither a
|
|
module nor a type).
|
|
|
|
### 2. The `new` term construct
|
|
|
|
**Form.** `(new T arg1 arg2 ...)` where `T` is a `TypeName` and
|
|
`argN` is either a `Type` expression (e.g. `(con Float)`) or a
|
|
`Term` expression. The construct desugars to: look up `new` in the
|
|
home module of `T`, call it with the given args.
|
|
|
|
**AST.** New variant `Term::New { type_name: TypeName, args: Vec<NewArg> }`
|
|
where `NewArg = NewArg::Type(Type) | NewArg::Value(Term)`. Each arg
|
|
carries its kind in serialised JSON.
|
|
|
|
**Why complementary to `term-ctor`, not replacing it.** `term-ctor`
|
|
constructs an ADT value via a *named data constructor* (a tag in
|
|
the TypeDef's `ctors` list). `new` calls a *function* in the
|
|
type's home module. They serve different purposes:
|
|
|
|
- `(term-ctor IntList ICons 5 INil)` builds an `IntList` from its
|
|
`ICons` ctor. This is structural — the AST node carries the
|
|
ctor name and field args directly.
|
|
- `(new Series (con Float) 3)` calls `Series.new : (Type, Int) -> Series a`.
|
|
This is functional — there is no `Series` data ctor; the
|
|
type is opaque and construction is a defined operation.
|
|
|
|
A type can have both: an ADT could expose `term-ctor` for direct
|
|
ctor access plus a `new` def for builder-style construction. The
|
|
two paths are not in tension; they answer different design needs.
|
|
|
|
**Diagnostics.** `NewTypeNotConstructible` (no `new` def in the
|
|
type's home module); `NewArgKindMismatch` (a Type arg where the
|
|
signature expects a Value, or vice versa).
|
|
|
|
### 3. Kernel-tier modules with auto-import
|
|
|
|
**Form.** A new boolean field `kernel` on `Module` (omitted when
|
|
false, so existing modules hash-stable). When `kernel: true`:
|
|
|
|
- The module's top-level defs are accessible bare in every other
|
|
module of the workspace, with no `(import ...)` declaration
|
|
required.
|
|
- The module's types are accessible bare in type position.
|
|
|
|
**Why.** The architectural property the user wants is: the domain
|
|
type lives outside core, but at the call site it feels like a
|
|
primitive. Bare `Series` in `(con Series (con Float))` without
|
|
seeing `(import series)` somewhere is the ergonomic property.
|
|
|
|
**Single mechanism.** Auto-injection is a single load-time hop,
|
|
generalised from a hardcoded single-name path (prelude only,
|
|
pre-prep.3) to a flag-driven multi-module mechanism (since
|
|
prep.3 of `kernel-extension-mechanics`). The loader at
|
|
`crates/ailang-surface/src/loader.rs::load_workspace` injects
|
|
`parse_prelude()` and `parse_raw_buf()` programmatically,
|
|
then derives the implicit-imports list from
|
|
`modules.values().filter(|m| m.kernel)`. Every module in the
|
|
workspace's modules map that carries `kernel: true` enters the
|
|
auto-import set; consumers see those modules' top-level types
|
|
bare without an `(import …)` declaration.
|
|
|
|
Prelude carries `kernel: true` in `examples/prelude.ail`. Its 12
|
|
free fns (see `examples/prelude.ail:85-148`) remain callable bare
|
|
in every consumer module — ratified by
|
|
`crates/ail/tests/prelude_free_fns.rs` across the code-path
|
|
migration. The `raw_buf` base-extension kernel module
|
|
(`crates/ailang-kernel/src/raw_buf/`) and any future kernel-tier
|
|
consumers (Series, Matrix) auto-import through the same filter.
|
|
|
|
Class-method dispatch (a separate mechanism — see
|
|
[method dispatch](../contracts/0016-method-dispatch.md)) is
|
|
orthogonal: the dispatch is about how method calls are
|
|
resolved; the auto-import is about which names are in scope.
|
|
|
|
### 4. `param-in` — closed-set type parameter restriction
|
|
|
|
**Form.** Optional field on `TypeDef`: `param-in: Map<VarName, Set<TypeName>>`.
|
|
Skipped when absent. Each entry constrains a type variable to a
|
|
fixed set of named types.
|
|
|
|
**Example.**
|
|
|
|
```jsonc
|
|
// TypeDef Series
|
|
{ "kind": "type",
|
|
"name": "Series",
|
|
"vars": ["a"],
|
|
"ctors": [],
|
|
"param-in": { "a": ["Int", "Float", "Bool"] }
|
|
}
|
|
```
|
|
|
|
When the checker sees `Type::Con { name: "Series", args: [Type::Con { name: "Str", ... }] }`,
|
|
it looks up `Series`'s `param-in`, finds that `a` must be in
|
|
`{Int, Float, Bool}`, and rejects `Str`.
|
|
|
|
**Why not a marker class.** `class Primitive a` with three
|
|
instances (Int, Float, Bool) and no methods would express the
|
|
same restriction via existing typeclass machinery. Reason it is
|
|
not chosen: class constraints model *behaviour* (a type satisfies
|
|
some interface). `param-in` models *structural identity* (the
|
|
type's storage layout). Series's element-type restriction is
|
|
structural — the C-runtime ring buffer has a `data[]` whose layout
|
|
depends on whether the element is 8 bytes (Int/Float) or 1 byte
|
|
(Bool). A marker class would model this as "Int is a Primitive"
|
|
which is true but indirect. `param-in` says directly: "Series's
|
|
element variable must be one of these three named types". The
|
|
typecheck site is a set-membership lookup, not a class-instance
|
|
discharge.
|
|
|
|
**Diagnostic.** `ParamNotInRestrictedSet` names the offending
|
|
type and the allowed set.
|
|
|
|
## Two-tier extension architecture
|
|
|
|
Kernel extensions split into two tiers, distinguished by what
|
|
they need to provide:
|
|
|
|
### Base extensions
|
|
|
|
Provide primitives that are *not expressible in AILang itself* —
|
|
typically because they require mutable indexed storage,
|
|
hardware/OS interaction, or library-wrapping that has no AILang
|
|
surface. A base extension ships:
|
|
|
|
1. **A kernel-tier module manifest** with the TypeDef
|
|
(and `param-in` if applicable) plus the operation signatures.
|
|
2. **Codegen intercepts** — Rust code registered with the
|
|
compiler that, at each call site of an operation, emits the
|
|
appropriate LLVM IR text (using existing runtime symbols like
|
|
`@ailang_rc_alloc` for allocation). This follows the
|
|
`try_emit_primitive_instance_body` precedent: Rust returns IR
|
|
text, no separate C glue.
|
|
3. **Optional C runtime support** in `runtime/<extension>.c` —
|
|
only when the operations *truly cannot be expressed as IR
|
|
over existing runtime primitives* (e.g. wrapping PCRE2 for a
|
|
future Regex extension). For the foreseeable base extensions
|
|
(RawBuf, Matrix), no C is needed.
|
|
|
|
The first base extension is `RawBuf T` — a mutable, indexed,
|
|
bounded-size flat buffer of primitive elements. Element type is
|
|
restricted to `{Int, Float, Bool}` via `param-in` for the MVP.
|
|
|
|
### Library extensions
|
|
|
|
Provide domain-specific types that *are* expressible in AILang
|
|
once a base extension has been added. A library extension ships:
|
|
|
|
1. **A kernel-tier `.ail` module** (or `.ail.json`) — plain
|
|
AILang code, no Rust intercepts, no C. The module declares an
|
|
ADT and a set of fns; the fns call into a base extension's
|
|
API.
|
|
2. **Nothing else.** No codegen intercepts (regular AILang
|
|
codegen handles it), no C runtime (regular AILang RC handles
|
|
it), no compiler-side plug-ins.
|
|
|
|
The first library extension is `Series T` — a bounded ring
|
|
buffer with financial-style indexing. Implemented as an ADT
|
|
wrapping a `RawBuf T` plus four bookkeeping `Int` fields
|
|
(lookback, head, count, total). All operations are AILang fns.
|
|
|
|
### Why split
|
|
|
|
- **AILang-in-AILang where possible.** Domain types are written
|
|
in the language they are for. A LLM author who needs to
|
|
understand Series's eviction logic reads `series.ail`, not a
|
|
Rust intercept registry. The implementation language matches
|
|
the authoring language.
|
|
- **Composability.** Multiple library extensions can share one
|
|
base extension. Series, Matrix, Hashmap, and future Vector all
|
|
build on RawBuf. Each is a few hundred lines of AILang, not a
|
|
new Rust intercept.
|
|
- **Cost localisation.** The Rust-intercept layer is small and
|
|
centralised at the base. Domain growth (more library
|
|
extensions) does not enlarge the Rust footprint.
|
|
- **Forward axis: SoA for records.** When the day comes that
|
|
Series should hold records (e.g. `{price: Float, volume: Int}`),
|
|
the change is internal to RawBuf — its intercept dispatches on
|
|
whether the element type is primitive (flat buffer) or record
|
|
(struct-of-arrays). Series's AILang code does not change.
|
|
|
|
## The plugin contract (consolidated)
|
|
|
|
Base extension:
|
|
- Kernel-tier module manifest.
|
|
- Rust codegen intercepts emitting LLVM IR for each operation.
|
|
- Optional C runtime — only when LLVM IR over existing runtime
|
|
symbols cannot express the operation.
|
|
|
|
Library extension:
|
|
- Kernel-tier `.ail` module.
|
|
- Depends on one or more base extensions for its primitives.
|
|
|
|
Both register with the compiler via the kernel-tier
|
|
auto-injection mechanism described above. Core has no
|
|
per-extension code. The four mechanisms (type-scoped
|
|
namespacing, `new`, kernel-tier modules, `param-in`) are all
|
|
general — the same checker logic handles RawBuf, Series, and
|
|
any future extension.
|
|
|
|
The migration of existing hardcoded primitive-instance
|
|
intercepts (`try_emit_primitive_instance_body`) into the plugin
|
|
registry is triggered by the first real base extension shipping
|
|
(RawBuf). One registry mechanism for all intercepts, replacing
|
|
the current single-case hardcoded list.
|
|
|
|
CLI / discovery (`ail describe <T>`) consults the workspace
|
|
TypeDef registry and surfaces the `kernel: true` flag on the
|
|
home module — uniform for base and library extensions; the user
|
|
does not need to know which tier hosts the type.
|
|
|
|
## Series as the first library consumer (built on RawBuf)
|
|
|
|
### RawBuf — the base extension underneath
|
|
|
|
`RawBuf a` is a mutable, indexed, fixed-size buffer. Element
|
|
type `a` restricted to `{Int, Float, Bool}` for the MVP via
|
|
`param-in`. API:
|
|
|
|
- `(new RawBuf (con T) (size: Int)) : own (RawBuf T)` — allocates
|
|
an uninitialised buffer.
|
|
- `RawBuf.get : forall a. (borrow (RawBuf a), Int) -> a` —
|
|
indexed read. UB if `index >= RawBuf.size(b)`; caller checks
|
|
bounds.
|
|
- `RawBuf.set : forall a. (own (RawBuf a), Int, a) -> own (RawBuf a)` —
|
|
indexed write. Linear signature: caller hands over the buffer,
|
|
callee returns it after mutation. Under uniqueness inference,
|
|
the codegen rewrites this into in-place mutation; under
|
|
shared ownership it falls back to a full buffer copy
|
|
(Issue #22 territory).
|
|
- `RawBuf.size : forall a. (borrow (RawBuf a)) -> Int`.
|
|
|
|
Mutation discipline: ownership-mode-tracked, not effect-tracked.
|
|
The own/borrow signatures *are* the mutation contract. No
|
|
`RawBuf` effect is declared. This is consistent with AILang's
|
|
existing memory-model — RC + uniqueness as the canonical
|
|
mutation story.
|
|
|
|
The `own → own` signature of `RawBuf.set` is a *threading
|
|
discipline* enforced by the uniqueness/linearity check where that
|
|
check is active, not a runtime guard. The mode annotations drive
|
|
the borrow/consume analysis and the in-place-vs-copy codegen
|
|
decision. Where the linearity check runs — a fn whose parameters
|
|
all carry explicit `own`/`borrow` modes — a second consume of the
|
|
same owned binder *is* rejected at check time (`use-after-consume`):
|
|
a helper `(fn f (params (own (RawBuf Int))) …)` that hands its
|
|
buffer to two consuming calls is caught. The check has an
|
|
activation gate, though: it does not run on a fn with no parameters
|
|
(a paramless top-level `main`) or one with implicit-mode parameters.
|
|
A double-consume written directly in such an unchecked context —
|
|
`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))` inside a
|
|
paramless `main` — is not caught, and the two bindings alias one
|
|
slab (the second mutation is visible through the first). `RawBuf`'s
|
|
in-place `own → own` surface is the first place this alias produces
|
|
a *mutated-in-place* surprise rather than a benign re-read. Single-
|
|
use of an owned buffer in an unchecked context is the author's
|
|
responsibility. Tightening the activation gate, or full linear
|
|
enforcement, is tracked separately (Issue #22 territory).
|
|
|
|
Storage at the LLVM-IR level is type-specialised: the Rust
|
|
intercept registered for `RawBuf` dispatches on the element type
|
|
at each call site and emits the appropriate `getelementptr` /
|
|
`load` / `store` instructions over an opaque `ptr` allocated via
|
|
`@ailang_rc_alloc`. No new C code; the existing RC machinery
|
|
handles allocation, drop, and copy-on-share.
|
|
|
|
### Series — the library extension
|
|
|
|
`Series a` is a bounded ring buffer with financial-style indexing
|
|
(index 0 = newest). It is a plain AILang ADT in a kernel-tier
|
|
`.ail` module. Source of truth:
|
|
`crates/ailang-kernel/src/series/source.ail` — the listing below
|
|
is that module with the per-item `(doc …)` strings elided for
|
|
readability:
|
|
|
|
```
|
|
(module series
|
|
(kernel)
|
|
|
|
(data Series (vars a)
|
|
(param-in (a Int Float)) ; Bool deferred (#61)
|
|
(ctor S (con RawBuf a) ; the storage (no mode: modes live on
|
|
; fn params/ret, not on ADT fields)
|
|
(con Int) ; lookback
|
|
(con Int) ; head index
|
|
(con Int) ; current count
|
|
(con Int))) ; total pushes ever
|
|
|
|
(fn new
|
|
(type (forall (vars a) (fn-type
|
|
(params (own (con Int)))
|
|
(ret (own (con Series a))))))
|
|
(params lookback)
|
|
(body
|
|
(term-ctor Series S
|
|
; element solved from the (con RawBuf a) ctor field — no type-arg
|
|
(new RawBuf lookback) lookback 0 0 0)))
|
|
|
|
(fn push
|
|
(type (forall (vars a) (fn-type
|
|
(params (own (con Series a)) (own a))
|
|
(ret (own (con Series a))))))
|
|
(params s v)
|
|
(body
|
|
(match s
|
|
(case (pat-ctor S buf lookback head count total)
|
|
(term-ctor Series S
|
|
(app RawBuf.set buf head v)
|
|
lookback
|
|
(app % (app + head 1) lookback)
|
|
(if (app lt count lookback) (app + count 1) count)
|
|
(app + total 1))))))
|
|
|
|
(fn at
|
|
(type (forall (vars a) (fn-type
|
|
(params (borrow (con Series a)) (own (con Int)))
|
|
(ret (own a)))))
|
|
(params s i)
|
|
(body
|
|
(match s
|
|
(case (pat-ctor S buf lookback head count total)
|
|
(app RawBuf.get buf
|
|
(app % (app + (app - (app - head 1) i) (app * lookback 2)) lookback))))))
|
|
|
|
(fn len
|
|
(type (forall (vars a) (fn-type
|
|
(params (borrow (con Series a)))
|
|
(ret (own (con Int))))))
|
|
(params s)
|
|
(body (match s (case (pat-ctor S buf lookback head count total) count))))
|
|
|
|
(fn total_count
|
|
(type (forall (vars a) (fn-type
|
|
(params (borrow (con Series a)))
|
|
(ret (own (con Int))))))
|
|
(params s)
|
|
(body (match s (case (pat-ctor S buf lookback head count total) total)))))
|
|
```
|
|
|
|
Push semantics: take Series by `own`, return a new Series with
|
|
the buffer mutated (via `RawBuf.set`) and the bookkeeping fields
|
|
updated. The match-and-rebuild pattern is the explicit linear
|
|
state-threading style. Under uniqueness inference, both the
|
|
RawBuf mutation and the Series ADT rebuild become in-place; the
|
|
caller-side `(let s_new (app Series.push s v) ...)` pattern
|
|
optimises to single-allocation, two-counter-update cost. Under
|
|
shared ownership, push allocates a new Series wrapper (~40 bytes
|
|
RC overhead) per call — the performance fallback that Issue #22
|
|
will narrow.
|
|
|
|
No `Series` effect. The mutation is mode-tracked. Caller
|
|
signatures do *not* gain a `[Series]` or `[RawBuf]` effect entry;
|
|
they only need the linear threading discipline.
|
|
|
|
`Series.at` uses financial-style indexing (0 = newest):
|
|
`buf_index = (head - 1 - i + 2*lookback) mod lookback`. UB if
|
|
`i >= count`; the caller checks via `Series.len` or
|
|
`Series.total_count`. The `+ 2*lookback` is a non-negative
|
|
adjustment so the modulo arithmetic stays well-defined for
|
|
small `head` values.
|
|
|
|
### Forward axis: SoA for records (already accommodated)
|
|
|
|
Extending Series to hold records (`Series {price: Float, volume: Int}`)
|
|
is purely a RawBuf change. The RawBuf intercept gains a
|
|
dispatch path for record element types — primitive types stay
|
|
flat (AoS), record types switch to struct-of-arrays internally
|
|
with per-field parallel storage. `RawBuf.get` for a record-typed
|
|
buffer materialises the record on demand from the parallel
|
|
slots; `RawBuf.set` distributes the record's fields across the
|
|
parallel slots. Series's AILang code does not change; the API
|
|
surface is identical.
|
|
|
|
The Series milestone scope does *not* include record element
|
|
types; that is a future axis. But the architecture
|
|
accommodates it without revisiting Series itself.
|
|
|
|
## Feature-acceptance argument
|
|
|
|
Series's three-clause feature-acceptance check is in the spec; the
|
|
summary: LLM authors naturally reach for a bounded ring buffer
|
|
for streaming workloads (clause 1 — the SMA worked example
|
|
above is the evidence); the type structurally eliminates a class
|
|
of off-by-one and warmup-handling bugs (clause 2); the bounded
|
|
push-only mutation surface — gated by uniqueness mode-tracking
|
|
on the owned `Series` value (not by an algebraic effect; see
|
|
§"Coexistence" below) — does not reintroduce the iterated-
|
|
mutable-state bug class that the `mut`/`var`/`assign` removal
|
|
addressed (clause 3 — see
|
|
`docs/specs/0052-kernel-extension-mechanics.md`'s clause-3
|
|
discussion).
|
|
|
|
The same three-clause check applies to *each future kernel
|
|
extension*. The whitepaper does not pre-justify Matrix or Decimal
|
|
or Time — each gets its own feature-acceptance gate when its spec
|
|
is written.
|
|
|
|
## Migration policy (pre-production frame)
|
|
|
|
AILang is pre-production. No external author depends on a
|
|
particular surface; no compiled artifact in the wild. The
|
|
implication for kernel-extensions: **when a new mechanism is
|
|
strictly better than an existing one for the use case it covers,
|
|
the existing one is retired or repositioned, not preserved
|
|
in parallel for compatibility.**
|
|
|
|
Concrete state after the mechanisms milestone closed (2026-05-28):
|
|
|
|
- Type-scoped namespacing makes `<module>.<TypeOrFn>` non-canonical
|
|
for type-associated operations. The example and fixture corpus
|
|
has been rewritten from `std_maybe.from_maybe`,
|
|
`std_pair.from_pair`, etc., to type-scoped form. The hash-pin
|
|
blast-radius audit at prep.1 plan time enumerated the affected
|
|
pin files; only `crates/ailang-surface/tests/prelude_module_hash_pin.rs`
|
|
needed refresh in this milestone (at prep.3, when prelude
|
|
gained `(kernel)`).
|
|
|
|
- The pre-existing `BareCrossModuleTypeRef` /
|
|
`BadCrossModuleTypeRef` diagnostics are repurposed: what they
|
|
considered "bad" before (a bare type ref to a foreign module's
|
|
type) is still bad when the type is not in scope, but the
|
|
*correct* form is now type-scoped (when feasible) rather than
|
|
module-qualified.
|
|
|
|
- The prelude module carries `kernel: true`. The previously
|
|
hardcoded prelude-name paths in `crates/ailang-surface/src/loader.rs`
|
|
(the `&["prelude"]` literal) and the matching reservation +
|
|
contract docs in `crates/ailang-core/src/workspace.rs` have
|
|
been replaced by a generic `modules.values().filter(|m| m.kernel)`
|
|
derivation. Consumer-observable behaviour for prelude is
|
|
unchanged (the 12 free fns remain callable bare in every
|
|
consumer — `crates/ail/tests/prelude_free_fns.rs` is the
|
|
regression pin); the code path no longer hardcodes any module
|
|
name as special.
|
|
|
|
- Codegen intercepts: the compiler-supplied implementations of the
|
|
prelude's primitive Eq/Ord/Float operations live in a registry,
|
|
`crates/ailang-codegen/src/intercepts.rs::INTERCEPTS`. A
|
|
kernel-tier or prelude definition whose body is the `(intrinsic)`
|
|
marker (`Term::Intrinsic`) declares membership in that registry;
|
|
codegen routes it through `intercepts::lookup` on its mangled
|
|
name. The pairing is locked by
|
|
`intercepts_bijection_with_intrinsic_markers`: every intrinsic
|
|
marker reachable in the loaded workspace resolves to a registry
|
|
entry, and every registry entry not on the optimisation-only
|
|
allowlist has a marker. The registry also carries an
|
|
optimisation-only class — entries that intercept the
|
|
monomorphised `__Int` specialisation of a real-bodied polymorphic
|
|
free fn (`lt/le/gt/ge/ne`) for a faster direct `icmp`; those have
|
|
a real source body and no marker.
|
|
|
|
## Coexistence with existing mechanisms
|
|
|
|
The mechanisms in this whitepaper interact with several
|
|
pre-existing parts of the language. Each interaction is named
|
|
here so the spec can quote the position:
|
|
|
|
- **Classes / method dispatch.** Orthogonal. Type-scoped
|
|
namespacing accesses *top-level defs* in a type's home module;
|
|
class-method dispatch (see [method dispatch](../contracts/0016-method-dispatch.md))
|
|
resolves *class method calls* by type-driven instance lookup.
|
|
Both can coexist on the same type — e.g. `Series` could
|
|
someday have a `Show` instance (class method `show` dispatches
|
|
via the instance) and a `Series.dump` free-fn def (accessed
|
|
via type-scope). Both mechanisms remain.
|
|
|
|
- **Algebraic effects.** Not extended by Series. Mutation
|
|
discipline lives in the uniqueness/mode system (see
|
|
`(own Series)` in caller signatures); the algebraic-effects
|
|
set is unchanged.
|
|
|
|
- **RC + uniqueness.** Series values are RC-managed like any
|
|
heap value; drop is via a kernel-supplied `@ailang_series_drop`.
|
|
Future Uniqueness inference (Gitea #22) can in principle
|
|
recognise unique Series and elide RC ops on push — but the
|
|
baseline does not depend on that.
|
|
|
|
- **Heap-Str ABI.** The Series runtime borrows the heap-Str
|
|
RC-pointer-to-opaque-struct pattern (see
|
|
[str-abi](../contracts/0011-str-abi.md)). Same pattern: opaque
|
|
`ptr` from the compiler's view; dedicated `_new`, `_drop`,
|
|
and operation symbols in C; RC header in the struct prefix.
|
|
|
|
- **Term::Ctor + pattern matching.** Unchanged. `term-ctor`
|
|
and `pat-ctor` keep their roles for named-ctor ADTs.
|
|
|
|
- **`term-ctor` vs `new`.** Different constructs for different
|
|
needs. The choice point for a hypothetical hybrid (e.g.
|
|
"every named ctor implicitly defines a `new` fn") is
|
|
out of scope for this whitepaper — the two coexist by
|
|
design.
|
|
|
|
## Forward axes
|
|
|
|
This whitepaper does not commit to any future kernel extension.
|
|
The shape it enables — domain-specific types as plugins — is
|
|
intended to make a future Matrix, Decimal, Time, etc., a
|
|
self-contained crate-level proposal each gated by its own
|
|
feature-acceptance and brainstorm pass. The plugin contract
|
|
above is the only commitment.
|
|
|
|
## Cross-references
|
|
|
|
- **Feature-acceptance gate** applied to each kernel extension:
|
|
[feature-acceptance](../contracts/0004-feature-acceptance.md).
|
|
- **Method dispatch** (orthogonal to type-scoped namespacing):
|
|
[method-dispatch](../contracts/0016-method-dispatch.md).
|
|
- **Honesty rule** (this whitepaper's STATUS contract):
|
|
[honesty-rule](../contracts/0007-honesty-rule.md).
|
|
- **Reference design** for Series storage layout:
|
|
`/home/brummel/dev/RustAst/src/ast/rtl/series/` (external Rust
|
|
project; not in this repo).
|
|
- **Per-milestone specs:** `docs/specs/0052-kernel-extension-mechanics.md`
|
|
(prep milestone); future `docs/specs/YYYY-MM-DD-series.md`
|
|
(Series milestone, written after prep closes).
|