From 5e5b0e1484c0066f46016df4c195405fdb56db61 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 10:56:01 +0200 Subject: [PATCH] docs(design): bring models/0007 worked examples onto the shipped surface (refs #7) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The raw-buf milestone fieldtest (spec 0066) surfaced a spec_gap: the kernel-extensions whitepaper teaches RawBuf surface syntax through its §Series worked examples, but those examples were written before three downstream surface decisions landed and never caught up — so an LLM author who pattern-matches them writes programs that fail to parse. Three drift classes, all verified against the HEAD parser: - fn-type slots carried no mode. Post-#55 every value slot needs an explicit `(own …)` / `(borrow …)` (the bare_slot_reject contract). - `(new RawBuf lookback)` omitted the element type. Post-#51 the form is `(new RawBuf (con T) )`; the whitepaper's own spec line (§"allocates") already documents `(new RawBuf (con T) (size: Int))`. - parametrised kernel types were spelled bare `(Series a)` / `(Series (con Float))`, contradicting the whitepaper's OWN prose (`(con Series (con Float))` at the §mechanisms section). Wrapped in `(con …)` to match the documented canonical form. - `len` / `total_count` carried no `(type …)` at all; completed from the obvious neighbour signatures (`borrow (con Series a) → own Int`). Scope is deliberately surface-syntax only. The §Series listing stays a forward-looking sketch of the still-pending library-extension milestone (STATUS header; "not in today's AILang" at the sma_demo block). Its full cross-module compile-verification remains assigned to the Series milestone per spec 0059 — these edits do not claim it compiles today (it leans on kernel-tier polymorphism that is not yet authorable), only that its surface syntax now matches what RawBuf authors must actually write. --- design/models/0007-kernel-extensions.md | 36 ++++++++++++++----------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index 1464326..922cd43 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -58,8 +58,8 @@ moving average over a stream of float values, window size 3": (fn sum_window_step (type (fn-type - (params (borrow (Series (con Float))) (con Int) (con Int) (con Float)) - (ret (con Float)))) + (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) @@ -70,8 +70,8 @@ moving average over a stream of float values, window size 3": (fn emit_if_full (type (fn-type - (params (borrow (Series (con Float))) (con Int)) - (ret (con Unit)) (effects IO))) + (params (borrow (con Series (con Float))) (own (con Int))) + (ret (own (con Unit))) (effects IO))) (params s n) (body (if (app >= (app Series.total_count s) n) @@ -82,8 +82,8 @@ moving average over a stream of float values, window size 3": (fn run_stream (type (fn-type - (params (own (Series (con Float))) (con Int) (con FloatList)) - (ret (con Unit)) (effects IO))) + (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 @@ -94,7 +94,7 @@ moving average over a stream of float values, window size 3": (tail-app run_stream s_new n rest))))))) (fn main - (type (fn-type (params) (ret (con Unit)) (effects IO))) + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) (params) (body (let s (new Series (con Float) 3) @@ -117,7 +117,7 @@ maps onto one of the four mechanisms this whitepaper defines: construct*. - `(app Series.at s i)`, `(app Series.total_count s)`, `(app Series.push s v)` — *type-scoped namespacing*. -- The `(own (Series ...))` mode on `run_stream` plus the linear +- 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 @@ -453,17 +453,17 @@ handles allocation, drop, and copy-on-share. (fn new (type (fn-type - (params (con Int)) - (ret (own (Series a))))) + (params (own (con Int))) + (ret (own (con Series a))))) (params lookback) (body (term-ctor Series S - (new RawBuf lookback) lookback 0 0 0))) + (new RawBuf (con a) lookback) lookback 0 0 0))) (fn push (type (fn-type - (params (own (Series a)) (con a)) - (ret (own (Series a))))) + (params (own (con Series a)) (own (con a))) + (ret (own (con Series a))))) (params s v) (body (match s @@ -477,8 +477,8 @@ handles allocation, drop, and copy-on-share. (fn at (type (fn-type - (params (borrow (Series a)) (con Int)) - (ret (con a)))) + (params (borrow (con Series a)) (own (con Int))) + (ret (own (con a))))) (params s i) (body (match s @@ -487,10 +487,16 @@ handles allocation, drop, and copy-on-share. (app % (app + (app - head 1) (app + (app * lookback 2) i)) lookback)))))) (fn len + (type (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 (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))))) ```