spec: 24-show-print — post-22 prelude Show + print rewire
Milestone 24 closes the Post-22 Prelude roadmap entry's second half. Architecture: `class Show a where show : (a borrow) -> Str`, four primitive instances (Int/Bool/Str/Float — Float included because float_to_str is semantically unproblematic, unlike Eq/Ord's IEEE-754 issues), and `print : forall a. Show a => (a borrow) -> () !IO` as a polymorphic free fn following 23.5's `ne/lt`/etc. shape. Two new runtime primitives (`bool_to_str`, `str_clone`) let Show Bool and Show Str honour the uniform `(a borrow) -> Str Own` signature without codegen intercept. Three iters: 24.1 (runtime + codegen for the two new primitives), 24.2 (class + 4 instances in prelude.ail.json + DESIGN.md anchor), 24.3 (print free fn + positive/user-ADT/negative E2E + DESIGN.md sync). io/print_int|bool|float STAY this milestone — redundancy with `print` ratified as transitional per the 23-spec precedent for ==/eq. Corpus migration (86 fixtures) queued as separate P2 follow-up. Grounding-check PASS: all 12 enumerated load-bearing assumptions plus two additional implicit claims ratified by currently-green named tests (eob.1 RC-discipline tests anchor 24.1's critical group; milestone-23 mono unification anchors 24.2/24.3's group).
This commit is contained in:
@@ -0,0 +1,650 @@
|
||||
# 24 — Show + print rewire — Design Spec
|
||||
|
||||
**Date:** 2026-05-12
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Close the prelude story opened by milestone 23 (Eq/Ord) by shipping:
|
||||
|
||||
1. The `Show` typeclass with single method `show : (a borrow) -> Str`.
|
||||
2. Four primitive instances: `Show Int`, `Show Bool`, `Show Str`,
|
||||
`Show Float`.
|
||||
3. A polymorphic free fn `print : forall a. Show a => (a borrow) -> () !IO`
|
||||
that routes through `show` and `io/print_str`, replacing the
|
||||
ad-hoc per-type print idiom for new code.
|
||||
4. Two new runtime primitives that let `Show Bool` and `Show Str`
|
||||
honour the uniform `(a borrow) -> Str Own` signature without
|
||||
special-casing the codegen pipeline.
|
||||
|
||||
The milestone is the second and final half of the original
|
||||
"Post-22 Prelude" roadmap entry. The first half (Eq/Ord) shipped as
|
||||
milestone 23. The two halves were split because `Show` had a hard
|
||||
dependency on the heap-`Str` ABI (`int_to_str` / `float_to_str` had
|
||||
to allocate heap-`Str` slabs at runtime), which itself was a
|
||||
substantively separate milestone. That dependency closed in the
|
||||
heap-`Str` ABI milestone (`hs.1`–`hs.4` plus `eob.1`, ratified at
|
||||
`audit-eob` on 2026-05-12). `int_to_str` / `float_to_str` are now
|
||||
fully wired and RC-disciplined, removing the only barrier.
|
||||
|
||||
Existing per-type effect-ops `io/print_int` / `io/print_bool` /
|
||||
`io/print_float` STAY in this milestone. The redundancy between
|
||||
`print x` and `io/print_int x` for `x : Int` is **ratified as
|
||||
transitional**, mirroring the same call milestone 23 made for `==`
|
||||
vs. `eq`. Retiring the per-type effect-ops and migrating the
|
||||
example corpus (86 fixtures) is queued as a separate P2 follow-up;
|
||||
this milestone is the architecture-shipping milestone, not the
|
||||
migration milestone.
|
||||
|
||||
## Architecture
|
||||
|
||||
Three artefacts, in dependency order.
|
||||
|
||||
### 1. Two new runtime primitives
|
||||
|
||||
`runtime/str.c` gains two functions paralleling the existing
|
||||
`ailang_int_to_str` and `ailang_float_to_str`:
|
||||
|
||||
- `ailang_bool_to_str(int1_t b) -> heap_str_ptr` — returns a freshly
|
||||
allocated heap-Str slab containing either `"true"` or `"false"`
|
||||
(5 or 6 bytes inclusive of trailing NUL). The slab is allocated
|
||||
via `ailang_rc_alloc` with `rc_header` at `payload - 8`, exactly
|
||||
like `int_to_str`. Always heap-allocates; never returns a
|
||||
static-Str pointer. The allocation cost is paid every `show True`
|
||||
/ `show False` call; the alternative (schema-`if` with two
|
||||
static-Str literals) is deferred as an open commitment because
|
||||
phi-of-static-Str through the drop-elision pipeline is not
|
||||
load-bearing-ratified today.
|
||||
- `ailang_str_clone(const heap_str_ptr src) -> heap_str_ptr` —
|
||||
reads `i64 len` from offset 0 of the source slab and allocates a
|
||||
fresh heap-Str slab of the same length, memcpy's `len + 1` bytes
|
||||
(payload + trailing NUL) from source to destination, and returns
|
||||
the new slab pointer. Works uniformly on both static-Str and
|
||||
heap-Str inputs because the consumer ABI is identical (see
|
||||
DESIGN.md §"Str ABI"); only the `len` field at offset 0 plus the
|
||||
bytes plus the NUL are consulted, never the (absent for
|
||||
static-Str) `rc_header` of the source.
|
||||
|
||||
Both new symbols install in `crates/ailang-check/src/builtins.rs`
|
||||
alongside `int_to_str` / `float_to_str`:
|
||||
|
||||
- `bool_to_str : (Bool) -> Str` with `ret_mode: Own`.
|
||||
- `str_clone : (Str borrow) -> Str` with `ret_mode: Own`.
|
||||
|
||||
Both lower in `crates/ailang-codegen/src/lib.rs::Emitter::lower_app`
|
||||
via new arms paralleling the existing `int_to_str` and
|
||||
`float_to_str` arms (extern declarations in the IR header preamble,
|
||||
direct call emission, `Position::Consume` for the result let-binder
|
||||
per eob.1's effect-op-Borrow / let-binder-Own discipline).
|
||||
|
||||
The `is_static_callee` whitelist in `crates/ailang-codegen/src/synth.rs`
|
||||
extends to include both new names.
|
||||
|
||||
### 2. `Show` typeclass + four primitive instances
|
||||
|
||||
`examples/prelude.ail.json` gains five new top-level defs:
|
||||
|
||||
```jsonc
|
||||
// class
|
||||
{ "kind": "class",
|
||||
"name": "Show",
|
||||
"param": "a",
|
||||
"methods": [
|
||||
{ "name": "show",
|
||||
"type": {
|
||||
"k": "fn",
|
||||
"params": [{ "k": "var", "name": "a" }],
|
||||
"param_modes": ["borrow"],
|
||||
"ret": { "k": "con", "name": "Str" },
|
||||
"effects": []
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
// instance Show Int: body invokes int_to_str
|
||||
// instance Show Bool: body invokes bool_to_str
|
||||
// instance Show Str: body invokes str_clone
|
||||
// instance Show Float: body invokes float_to_str
|
||||
```
|
||||
|
||||
Each instance body is a single-application lambda
|
||||
`\x -> <primitive_to_str> x`. No codegen intercept (mirror of
|
||||
`try_emit_primitive_instance_body` from Eq/Ord) is required because
|
||||
the four primitives are themselves first-class lowered functions —
|
||||
unlike Eq/Bool/Str whose `==` bodies needed `try_emit_primitive_instance_body`
|
||||
to redirect to the appropriate `icmp` or `@ail_str_eq` lowering. The
|
||||
mono pass synthesises `show__Int`, `show__Bool`, `show__Str`,
|
||||
`show__Float`; each body is a direct call to the corresponding
|
||||
primitive.
|
||||
|
||||
Float **is** included in the Show prelude — unlike Eq/Ord which
|
||||
explicitly excluded Float because IEEE-754 makes structural equality
|
||||
and total ordering semantically dubious. Producing a textual
|
||||
representation of a Float is well-defined modulo the NaN spelling
|
||||
caveat in DESIGN.md §"Float semantics" (`printf("%g", nan)` may emit
|
||||
`nan` / `-nan` / `NaN`); this caveat is acceptable for a
|
||||
human-readable Show.
|
||||
|
||||
### 3. `print` polymorphic free fn
|
||||
|
||||
`examples/prelude.ail.json` also gains a sixth new top-level def:
|
||||
|
||||
```jsonc
|
||||
{ "kind": "fn",
|
||||
"name": "print",
|
||||
"type": {
|
||||
"k": "forall",
|
||||
"vars": ["a"],
|
||||
"constraints": [{ "class": "Show", "type": { "k": "var", "name": "a" } }],
|
||||
"body": {
|
||||
"k": "fn",
|
||||
"params": [{ "k": "var", "name": "a" }],
|
||||
"param_modes": ["borrow"],
|
||||
"ret": { "k": "con", "name": "Unit" },
|
||||
"effects": ["IO"]
|
||||
}
|
||||
},
|
||||
"params": ["x"],
|
||||
"body": {
|
||||
"t": "let",
|
||||
"name": "s",
|
||||
"value": { "t": "app", "fn": { "t": "var", "name": "show" }, "args": [{ "t": "var", "name": "x" }] },
|
||||
"body": { "t": "do", "op": "io/print_str", "args": [{ "t": "var", "name": "s" }] }
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
The let-binder for `show x` is **explicit**, not implicit. This is
|
||||
load-bearing for the heap-Str RC discipline: the Own heap-Str
|
||||
returned by `show x` (for Int/Bool/Str/Float, every instance allocates)
|
||||
needs a let-binder so that
|
||||
`drop_symbol_for_binder` fires the heap-Str drop at scope close —
|
||||
the Str carve-out path introduced in `eob.1`. Without the let-binder,
|
||||
the heap-Str slab from `show x` would not be RC-tracked at any
|
||||
binder and the slab would leak (the same failure mode the eob.1 RED
|
||||
tests pinned).
|
||||
|
||||
`print` is a free fn, not a class method. Two reasons:
|
||||
|
||||
- The body is identical for every `a : Show a` — no per-instance
|
||||
variation. The per-instance dispatch happens **inside** `show x`,
|
||||
not in `print`'s body. A class method with an identical body for
|
||||
every instance would be redundant.
|
||||
- It matches Haskell's Prelude convention (`print :: Show a => a -> IO ()`
|
||||
is a free fn, not a class method) and the milestone 23 free-fn
|
||||
pattern (`ne`/`lt`/`le`/`gt`/`ge`).
|
||||
|
||||
The mono pass (`crates/ailang-check/src/mono.rs`, unified in 23.4)
|
||||
handles `print` exactly as it handles `ne`: free-fn entry, rigid-var
|
||||
substitution `a → Int` (or whichever concrete type), body walker
|
||||
sees the nested `show` call at concrete type, schedules `show__Int`
|
||||
in the same fixpoint round, the synthesised `print__Int` body
|
||||
references `show__Int` directly.
|
||||
|
||||
## Components (iterations)
|
||||
|
||||
| Iter | Status | Scope |
|
||||
|------|--------|-------|
|
||||
| **24.1** | upcoming | **Runtime + codegen for two new primitives.** `runtime/str.c` gains `ailang_bool_to_str` and `ailang_str_clone`. `crates/ailang-check/src/builtins.rs` installs `bool_to_str : (Bool) -> Str` and `str_clone : (Str borrow) -> Str`, both with `ret_mode: Own`. `crates/ailang-codegen/src/lib.rs::Emitter::lower_app` gains two new arms emitting direct calls to `@ailang_bool_to_str` and `@ailang_str_clone`, plus extern declarations in the IR header preamble. `crates/ailang-codegen/src/synth.rs::is_static_callee` whitelist extends. RC-stats E2E tests pin `allocs == 1, frees == 1, live == 0` for both primitives. IR-shape pins for the two extern declarations and the two call emissions. |
|
||||
| **24.2** | upcoming | **`class Show` + 4 primitive instances in prelude.** `examples/prelude.ail.json` gains `class Show a where show : (a borrow) -> Str` and four `instance Show <T>` defs (Int/Bool/Str/Float), each with a single-application lambda body invoking the corresponding `*_to_str` primitive. Round-trip test confirms prelude.ail.json parses + canonicalises bit-stable. Mono synthesis test confirms `show__Int`, `show__Bool`, `show__Str`, `show__Float` Def::Fn entries are produced. DESIGN.md §"Prelude (built-in) classes" amended to include Show with the four instances. |
|
||||
| **24.3** | upcoming | **`print` polymorphic free fn + E2E + DESIGN.md sync.** `examples/prelude.ail.json` gains `fn print : forall a. Show a => (a borrow) -> () !IO` with body `\x -> let s = show x in do io/print_str s`. E2E fixtures: (a) positive — `do print 42`, `do print True`, `do print "hello"`, `do print 3.14` produce expected stdout; (b) user-ADT — `data IntBox = MkIntBox Int` + `instance Show IntBox where show x = match x with MkIntBox n -> int_to_str n` + `print (MkIntBox 7)` produces stdout `"7"`; (c) negative — `print f` where `f : Int -> Int` fires `NoInstance Show <fn-type>` at typecheck with a Show-aware diagnostic. DESIGN.md §"Prelude (built-in) classes" amended to include `print`; §"Float semantics" gains a paragraph linking Show Float (via `float_to_str`) to the existing NaN-spelling caveat. Roadmap P1 "Post-22 Prelude" entry flips to `[x]`; new P2 entry added: "retire `io/print_int|bool|float` effect-ops + migrate example corpus to `print`". |
|
||||
|
||||
The milestone closes with the standard `audit` pipeline (architect
|
||||
drift review + three bench scripts).
|
||||
|
||||
## Data flow
|
||||
|
||||
Two trajectories show the routing at work.
|
||||
|
||||
### `print 42` at type `Int`
|
||||
|
||||
1. **Typecheck.** `print` resolves to the polymorphic free fn with
|
||||
`forall a. Show a => (a borrow) -> () !IO`. Bare-name lookup
|
||||
reaches the prelude via `env.module_globals` fall-through
|
||||
(prep1 from 23.4-prep). Constraint `Show Int` discharged against
|
||||
the registry entry for `instance Show Int`.
|
||||
2. **Mono (free-fn entry).** Body taken directly from `Def::Fn.body`,
|
||||
rigid-var subst `a → Int`. The body walker detects the nested
|
||||
`show x` call at concrete `Int` and schedules `show__Int` in the
|
||||
same fixpoint round. `show__Int` synthesises from the
|
||||
`instance Show Int` body (class-method entry,
|
||||
`Registry::entries[(Show, Int)]` lookup). The synthesised
|
||||
`show__Int` body is `\x -> int_to_str x`. The synthesised
|
||||
`print__Int` body is `\x -> let s = show__Int x in do io/print_str s`.
|
||||
3. **Codegen.** `print__Int` lowers as any monomorphic fn. The
|
||||
nested `show__Int x` is a direct call returning Own heap-Str;
|
||||
the let-binder `s` is RC-tracked at scope close per the eob.1
|
||||
Str carve-out in `drop_symbol_for_binder`. `do io/print_str s`
|
||||
walks `s` as `Position::Borrow` (eob.1's effect-op arg rule);
|
||||
the let-binder's drop fires after the effect-op call returns,
|
||||
emitting `@ailang_rc_dec(s_ptr)` which decrements the heap-Str's
|
||||
rc_header to zero and frees the slab. Stdout: `"42\n"`.
|
||||
|
||||
### `print 3.14` at type `Float`
|
||||
|
||||
Identical to the above with `a → Float`, `Show Float`, `show__Float`,
|
||||
`int_to_str` replaced by `float_to_str`. The NaN-spelling caveat
|
||||
applies if the Float happens to be NaN: the rendered output follows
|
||||
libc's `%g` formatting, identical to `io/print_float`. Stdout for
|
||||
`3.14`: depends on libc but typically `"3.14\n"`; for `0.0 / 0.0`:
|
||||
typically `"nan\n"` or `"-nan\n"`.
|
||||
|
||||
### `print x` at user type `IntBox` with `instance Show IntBox`
|
||||
|
||||
1. **Typecheck.** `Show IntBox` discharged against the registry
|
||||
entry for `instance Show IntBox`.
|
||||
2. **Mono.** `print__IntBox` synthesises with body
|
||||
`\x -> let s = show__IntBox x in do io/print_str s`. `show__IntBox`
|
||||
synthesises from the instance body (whatever the user wrote, e.g.
|
||||
`\x -> match x with MkIntBox n -> int_to_str n`).
|
||||
3. **Codegen.** Lowers normally; ADT-pattern-match plus inner
|
||||
`int_to_str` call produce a heap-Str; outer let-binder drops at
|
||||
scope close.
|
||||
|
||||
## Error handling
|
||||
|
||||
- **`NoInstance Show <T>`** — fired at typecheck when `print` is
|
||||
called on a type without a `Show` instance (most commonly a
|
||||
function type, or a user type the author forgot to give an
|
||||
instance for). Diagnostic must cross-reference DESIGN.md
|
||||
§"Prelude (built-in) classes" so the LLM-author immediately learns
|
||||
which types ship with built-in Show instances.
|
||||
|
||||
- **`NoInstance Show <UserType>`** — re-uses the existing 22-era
|
||||
diagnostic path; no new code shape.
|
||||
|
||||
- **`OrphanInstance Show <T>`** — Decision 11 coherence rule
|
||||
unchanged. The four primitive instances ship in the prelude
|
||||
(`Show`'s defining module = `Int`/`Bool`/`Str`/`Float`'s defining
|
||||
module = prelude module; non-orphan by construction). User-side
|
||||
`instance Show <UserType>` MUST live in the user type's defining
|
||||
module or in the prelude module (the latter is not possible for
|
||||
user types since the prelude is read-only), which constrains user
|
||||
instances to the user-type's defining module.
|
||||
|
||||
- **`CheckError::Internal` from mono** — if `Show`-specialisation
|
||||
fails internally (e.g. the body walker fails to schedule
|
||||
`show__T` when synthesising `print__T`), this is a caller-contract
|
||||
violation per the existing convention in `mono.rs::synthesise_mono_fn`.
|
||||
Mirrors 23.4's free-fn-entry error handling.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
### 24.1 — runtime + codegen for `bool_to_str` + `str_clone`
|
||||
|
||||
- **Unit: each primitive lowers to expected IR.** Two new IR-shape
|
||||
pins in `crates/ailang-codegen/src/lib.rs::tests`:
|
||||
- `bool_to_str_emits_call_to_ailang_bool_to_str` — fixture
|
||||
`let s = bool_to_str true in do io/print_str s`; assert IR body
|
||||
contains `call ptr @ailang_bool_to_str(i1 1)` and
|
||||
`declare ptr @ailang_bool_to_str(i1)`.
|
||||
- `str_clone_emits_call_to_ailang_str_clone` — fixture
|
||||
`let s = str_clone "hi" in do io/print_str s`; assert IR body
|
||||
contains `call ptr @ailang_str_clone(ptr ...)` and
|
||||
`declare ptr @ailang_str_clone(ptr)`.
|
||||
|
||||
- **E2E RC-stats (two tests in `crates/ailang-codegen/tests/e2e.rs`):**
|
||||
- `bool_to_str_drop_balances_rc_stats` — fixture
|
||||
`let s = bool_to_str true in do io/print_str s`. Stdout
|
||||
`"true\n"`. RC stats: `allocs == 1, frees == 1, live == 0`.
|
||||
- `str_clone_drop_balances_rc_stats` — fixture
|
||||
`let s = str_clone "hello" in do io/print_str s`. Stdout
|
||||
`"hello\n"`. RC stats: `allocs == 1, frees == 1, live == 0`.
|
||||
|
||||
- **E2E stdout-smoke (two tests):**
|
||||
- `bool_to_str_emits_true_or_false` — both branches:
|
||||
`let s = bool_to_str true in do io/print_str s` → `"true\n"`;
|
||||
same with `false` → `"false\n"`.
|
||||
- `str_clone_emits_input_bytes` — `str_clone "world"` →
|
||||
stdout `"world\n"`. Confirms memcpy semantics, not just the
|
||||
pointer.
|
||||
|
||||
- **Cross-realisation test for `str_clone`:** clone a heap-Str
|
||||
(output of `int_to_str 42`) AND a static-Str (literal `"abc"`).
|
||||
Both produce heap-Str outputs with correct bytes. RC discipline
|
||||
green in both cases. Pins the "uniform consumer ABI" claim from
|
||||
DESIGN.md §"Str ABI".
|
||||
|
||||
- **Linker / build hygiene:** `cargo test --workspace` green. The
|
||||
`__attribute__((weak))` on `ailang_rc_alloc` extern (hs.3 pattern)
|
||||
is unchanged — `rc.c` is unconditionally linked post-eob.1, so
|
||||
the weak symbol is a documented no-op.
|
||||
|
||||
### 24.2 — `class Show` + 4 instances
|
||||
|
||||
- **Round-trip:** `examples/prelude.ail.json` parses + canonicalises
|
||||
bit-stable after the four new defs land. The existing prelude
|
||||
hash-stability test from milestone 23 stays green (the prelude's
|
||||
pre-existing defs — Ordering, Eq, Ord, instances, ne/lt/le/gt/ge —
|
||||
are unaffected).
|
||||
|
||||
- **Mono synthesis (unit test in `crates/ailang-check/src/mono.rs::tests`):**
|
||||
for a fixture that calls `show 1`, `show True`, `show "x"`, and
|
||||
`show 1.5`, assert that the post-mono workspace contains
|
||||
`show__Int`, `show__Bool`, `show__Str`, `show__Float` as `Def::Fn`
|
||||
entries. Bodies are direct calls to the corresponding primitives.
|
||||
|
||||
- **Hash stability of existing mono symbols:** `eq__Int`,
|
||||
`compare__Str`, and the four other class-method mono symbols from
|
||||
milestone 23 must produce identical bodies (and therefore
|
||||
identical hashes) under the unified pass after the Show defs are
|
||||
added. Pin test in the style of
|
||||
`crates/ailang-core/src/hash.rs::ct4_migrated_fixtures_have_canonical_form_hashes`.
|
||||
|
||||
- **Round-trip of new fixtures** — every fixture authored under 24.2
|
||||
passes Form-A parser + canonicaliser bit-stable.
|
||||
|
||||
### 24.3 — `print` polymorphic free fn + E2E
|
||||
|
||||
- **Positive E2E (`examples/show_print_smoke.ail.json`):** a single
|
||||
fixture exercises all four primitives:
|
||||
```
|
||||
fn main = do
|
||||
print 42 -- "42\n"
|
||||
print true -- "true\n"
|
||||
print "hello" -- "hello\n"
|
||||
print 3.14 -- "3.14\n" (libc-dependent)
|
||||
```
|
||||
Test asserts compile, run, expected stdout (the Float line uses
|
||||
a non-NaN, non-inf value where libc rendering is stable across
|
||||
versions — `3.14`'s `%g` rendering is `"3.14"` on every libc this
|
||||
project targets).
|
||||
|
||||
- **User-ADT E2E (`examples/show_user_adt.ail.json`):**
|
||||
```
|
||||
data IntBox = MkIntBox Int
|
||||
instance Show IntBox where
|
||||
show = \x -> match x with MkIntBox n -> int_to_str n
|
||||
fn main = do print (MkIntBox 7)
|
||||
```
|
||||
Stdout `"7\n"`. Confirms the mono pass handles user-defined Show
|
||||
instances and that `print` composes with them.
|
||||
|
||||
- **Negative E2E (`examples/show_no_instance.ail.json`):**
|
||||
```
|
||||
fn main = do print id -- id : forall a. a -> a, no Show instance
|
||||
```
|
||||
Typecheck rejects with `NoInstance Show <fn-type>`. The exact
|
||||
diagnostic wording is named as an Open commitment below
|
||||
("Negative-test diagnostic wording"); the gold-standard test pins
|
||||
the message verbatim after the implementer drafts it.
|
||||
|
||||
- **Mono symbol IR-shape pin:** `crates/ailang-check/src/mono.rs::tests`
|
||||
asserts `print__Int` body desugars to
|
||||
`\x -> let s = show__Int x in do io/print_str s` post-mono. Confirms
|
||||
the let-binder is preserved (not optimised away — load-bearing for
|
||||
the heap-Str RC discipline).
|
||||
|
||||
- **Round-trip of new fixtures.**
|
||||
|
||||
- **Bench regression check** at milestone close: the three bench
|
||||
scripts exit 0 or audit-ratified per audit-skill convention.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
The milestone closes when:
|
||||
|
||||
1. **24.1 has landed:** `runtime/str.c` defines `ailang_bool_to_str`
|
||||
and `ailang_str_clone`. `crates/ailang-check/src/builtins.rs`
|
||||
installs both signatures with `ret_mode: Own`.
|
||||
`crates/ailang-codegen/src/lib.rs::Emitter::lower_app` emits direct
|
||||
calls plus extern declarations. RC-stats E2E pins balance.
|
||||
|
||||
2. **24.2 has landed:** `examples/prelude.ail.json` contains
|
||||
`class Show a where show : (a borrow) -> Str` and four primitive
|
||||
instances (Int/Bool/Str/Float). The mono pass synthesises
|
||||
`show__Int`, `show__Bool`, `show__Str`, `show__Float`. DESIGN.md
|
||||
§"Prelude (built-in) classes" amended to include Show with the
|
||||
four instances.
|
||||
|
||||
3. **24.3 has landed:** `examples/prelude.ail.json` contains
|
||||
`fn print : forall a. Show a => (a borrow) -> () !IO` with the
|
||||
explicit-let body shape. The mono pass synthesises `print__Int`,
|
||||
`print__Bool`, `print__Str`, `print__Float` for each call site at
|
||||
a primitive type, plus `print__<UserType>` for each user-instance
|
||||
call site. Positive / user-ADT / negative E2E green. DESIGN.md
|
||||
§"Prelude (built-in) classes" lists `print` as the polymorphic
|
||||
helper; §"Float semantics" gains the Show Float NaN-spelling
|
||||
cross-reference paragraph.
|
||||
|
||||
4. **Tests pass:** `cargo test --workspace` green; existing milestone
|
||||
23 prelude fixtures (`ne`/`lt`/`le`/`gt`/`ge` E2E) unchanged;
|
||||
existing typeclass fixtures (`eq__Int`, `compare__Str`, etc.)
|
||||
hash-stable.
|
||||
|
||||
5. **Bench regression ratified:** `bench/check.py && bench/compile_check.py && bench/cross_lang.py`
|
||||
exit 0 or audit-ratified with journal entry.
|
||||
|
||||
6. **Roadmap update:** P1 "Post-22 Prelude — Show + print rewire"
|
||||
entry flips to `[x]`. New P2 entry: "Retire `io/print_int` /
|
||||
`io/print_bool` / `io/print_float` effect-ops + migrate example
|
||||
corpus to `print`". A user runs the bulk text substitution
|
||||
`do io/print_<T> x` → `do print x` across `examples/*.ail.json`
|
||||
(86 files affected), and the per-type ops are deleted from
|
||||
`builtins.rs` / `lib.rs` codegen arms / runtime C glue.
|
||||
|
||||
## Out of scope (deferred, with substantive rationale)
|
||||
|
||||
- **Retiring `io/print_int` / `io/print_bool` / `io/print_float`.**
|
||||
Queued as P2 follow-up. The architecture-shipping milestone and
|
||||
the corpus-migration milestone are kept separate so the migration
|
||||
is one mechanical pass against a frozen architecture, not a
|
||||
moving target. Same call milestone 23 made for the
|
||||
`==` / `eq`, `<` / `lt` redundancy.
|
||||
|
||||
- **`io/print_str` retirement.** Stays. Load-bearing inside `print`'s
|
||||
body (`do io/print_str s`); cannot be retired without an alternate
|
||||
primitive output path. Also stays as a directly-callable surface
|
||||
for Str-typed values where the LLM-author wants to bypass Show
|
||||
(e.g. when the Str is already in hand and `show__Str`'s
|
||||
`str_clone`-allocation is wasteful).
|
||||
|
||||
- **`bool_to_str` as schema-`if`.** The body `\x -> if x then "true" else "false"`
|
||||
is schematically valid but requires phi-of-static-Str to flow
|
||||
cleanly through the drop-elision pipeline (DESIGN.md §"Str ABI"
|
||||
codegen-level static-Str elision). The phi case is not
|
||||
load-bearing-ratified today; the safe always-correct
|
||||
`bool_to_str` primitive avoids the question. Open commitment:
|
||||
if a future codegen iter ratifies phi-of-static-Str drop-elision,
|
||||
swap `show__Bool` body to the schema-`if` form and retire
|
||||
`bool_to_str`.
|
||||
|
||||
- **`str_clone` as rc_header bump.** For heap-Str inputs, `str_clone`
|
||||
could rc_inc the existing slab instead of allocating a fresh
|
||||
copy. This requires the implementation to distinguish heap-Str
|
||||
from static-Str at runtime, which the codebase deliberately does
|
||||
NOT support post-hs.2 (the UINT64_MAX sentinel was dropped in
|
||||
favour of codegen-time elision). Open commitment for a future
|
||||
iter: if runtime tagging is reintroduced for a different reason,
|
||||
`str_clone` can become an rc_inc on heap-Str / no-op-with-fresh-
|
||||
alloc on static-Str hybrid. For now: always-allocate, always-copy.
|
||||
|
||||
- **`Show Ordering` instance.** The prelude's `Ordering` ADT has
|
||||
three constructors (LT/EQ/GT). Shipping `Show Ordering` would
|
||||
add a user-friendly pretty-print but no concrete demand exists
|
||||
and the design-by-default in this milestone is "instances ship
|
||||
for types LLM authors actually print". User can declare their
|
||||
own `instance Show Ordering` if they want it.
|
||||
|
||||
- **`Show` for ADTs via `deriving`.** No auto-derivation. The
|
||||
`instance Show <UserType>` body is hand-written per instance.
|
||||
Auto-derivation is a substantive feature in its own right
|
||||
(canonical-form choices, recursive descent, list / tuple Show
|
||||
bodies) and out of scope here.
|
||||
|
||||
- **Higher-kinded `Show` (`Show [a]`, `Show (Maybe a)`).** Decision
|
||||
11 axis 5 explicitly excludes higher-kinded class params. The
|
||||
LLM-natural pattern is per-type instances (`Show [Int]` as a
|
||||
monomorphic instance, hand-written). Same constraint as Eq/Ord.
|
||||
|
||||
- **`print` with newline-free variant (`putStr` / `print_no_newline`).**
|
||||
`io/print_str` calls `@puts` which appends a newline. Every
|
||||
`print x` therefore ends in `\n`. A newline-suppressed variant is
|
||||
a separate feature; deferred until a concrete LLM-author pattern
|
||||
demands it.
|
||||
|
||||
- **Operator routing through `Show` (`show` invoked as `<<` or
|
||||
similar).** No commitment. AILang does not have a Haskell-style
|
||||
monadic operator surface and adding one to invoke `show`
|
||||
implicitly would re-open the ergonomics question Decision 6
|
||||
closed in favour of explicit `do` blocks.
|
||||
|
||||
## Open commitments (24.1 / 24.2 / 24.3 implementer)
|
||||
|
||||
- **`bool_to_str` runtime body.** The 4-byte slab `"true"` and
|
||||
5-byte slab `"false"` can either be heap-allocated per call
|
||||
(current spec) or cached as module-level static slabs the
|
||||
function returns by-pointer. The cached variant is faster but
|
||||
re-introduces the same "static-Str-without-sentinel" question
|
||||
the project deliberately avoided. Implementer ships the
|
||||
always-heap-allocate variant unless a clear path through the
|
||||
drop-elision pipeline appears.
|
||||
|
||||
- **`str_clone` byte count.** The naive memcpy copies `len + 1`
|
||||
bytes (payload + trailing NUL). The implementation may choose to
|
||||
recompute the NUL via `strncpy`-style code instead of trusting
|
||||
the trailing NUL in the source; either is correct, both are
|
||||
acceptable as long as the result slab is valid UTF-8-or-bytes
|
||||
per the source's contract.
|
||||
|
||||
- **Negative-test diagnostic wording.** Implementer drafts the
|
||||
one-line Show-aware message for `NoInstance Show <T>`;
|
||||
orchestrator reviews in spec-compliance phase.
|
||||
|
||||
- **Implicit-let vs. explicit-let in `print`'s body.** The spec
|
||||
prescribes the explicit-let form
|
||||
`\x -> let s = show x in do io/print_str s`. If the AILang
|
||||
desugarer would automatically introduce a let-binder for any
|
||||
Term::App in effect-op-arg position, the explicit-let could be
|
||||
dropped from the source form. Implementer verifies the
|
||||
desugarer's behaviour during 24.3 Task 1; if implicit-let is
|
||||
the realised semantics, the prelude source form may be the
|
||||
more compact `\x -> do io/print_str (show x)`. The
|
||||
load-bearing property is "the heap-Str returned by `show x` has
|
||||
a tracked let-binder when entering the effect-op call site";
|
||||
whether the let-binder is sourced from the prelude form or
|
||||
desugar-introduced is a surface-level choice with identical
|
||||
semantics post-checker.
|
||||
|
||||
- **Show instance for the `Unit` type / Tuples / Lists.** Out of
|
||||
scope per "instances for types LLM authors actually print" — but
|
||||
if 24.3's user-ADT E2E surfaces a recurring shape (e.g. printing
|
||||
a Tuple inside the `IntBox` test), the implementer may queue a
|
||||
P3 idea entry without expanding the milestone scope.
|
||||
|
||||
## Known costs
|
||||
|
||||
- **24.1 runtime + codegen:** estimated +30 LOC in `runtime/str.c`
|
||||
(two new functions, ~15 LOC each), +20 LOC in
|
||||
`crates/ailang-check/src/builtins.rs` (two new signature
|
||||
installations parallel to the existing `int_to_str` /
|
||||
`float_to_str` blocks), +30 LOC in
|
||||
`crates/ailang-codegen/src/lib.rs` (two new arms in `lower_app`
|
||||
+ two extern declarations in the IR header preamble), +2 LOC in
|
||||
`crates/ailang-codegen/src/synth.rs::is_static_callee`.
|
||||
|
||||
- **24.2 prelude additions:** `examples/prelude.ail.json` +40–50
|
||||
lines (one class + four instances, JSON shape parallel to Eq
|
||||
Int/Bool/Str). DESIGN.md amendment ~10 lines.
|
||||
|
||||
- **24.3 prelude additions + tests:** `examples/prelude.ail.json`
|
||||
+30 lines (one polymorphic free fn with constraint signature
|
||||
and let-bound body). Three new E2E `.ail.json` fixtures, ~40
|
||||
lines JSON each. Diagnostic test ~20 lines Rust. DESIGN.md
|
||||
amendments ~20 lines (Prelude classes + Float semantics
|
||||
cross-reference).
|
||||
|
||||
- **Net code reduction:** none. This milestone is additive.
|
||||
Reduction comes later in the P2 follow-up (retiring three
|
||||
builtin effect-ops + three codegen arms + three runtime glue
|
||||
functions, estimated ~−150 LOC).
|
||||
|
||||
- **Compile-time shift:** the mono pass gains four new instance-method
|
||||
synthesis targets (`show__Int|Bool|Str|Float`) plus one new free-fn
|
||||
target (`print`) per call site. The shift is bounded — additive
|
||||
per call site, no new fixpoint depth — and is expected to be
|
||||
within bench tolerance. Quantified by `bench/compile_check.py`
|
||||
post-24.3; audit-ratified or rebaselined.
|
||||
|
||||
- **Runtime cost on `print x`:**
|
||||
- For `x : Int` — one `int_to_str` allocation (~3–20 bytes per
|
||||
Int depending on magnitude) plus one rc_dec at scope close.
|
||||
- For `x : Bool` — one `bool_to_str` allocation (5 or 6 bytes)
|
||||
plus one rc_dec.
|
||||
- For `x : Str` — one `str_clone` allocation + memcpy plus one
|
||||
rc_dec. **Strictly worse** than `do io/print_str x`. The
|
||||
redundancy is acknowledged; LLM-author has the recourse to
|
||||
bypass `print` for Str-typed values.
|
||||
- For `x : Float` — one `float_to_str` allocation plus one rc_dec.
|
||||
|
||||
## Load-bearing assumptions about current behaviour
|
||||
|
||||
Surfaced explicitly so the Step 7.5 grounding-check agent has a
|
||||
canonical list to ratify. Each assumption is something this spec
|
||||
relies on as currently-true.
|
||||
|
||||
1. `crates/ailang-check/src/mono.rs::monomorphise_workspace` is the
|
||||
single specialiser for both class methods and polymorphic free
|
||||
fns (per milestone 23.4 unification), and it handles transitive
|
||||
specialisation across nested calls in one fixpoint loop.
|
||||
|
||||
2. `int_to_str : (Int) -> Str` and `float_to_str : (Float) -> Str`
|
||||
are installed in `builtins.rs` with `ret_mode: Own`, lowered in
|
||||
`Emitter::lower_app` via direct extern calls to
|
||||
`@ailang_int_to_str` / `@ailang_float_to_str`, and RC-disciplined
|
||||
end-to-end (allocs == frees, live == 0) per eob.1.
|
||||
|
||||
3. `io/print_str` lowers to `@puts(ptr)` and accepts any Str
|
||||
realisation (static-Str at `@.str_*` LLVM globals OR heap-Str
|
||||
allocated by `int_to_str` / `float_to_str` / the new primitives)
|
||||
via a consumer ABI of `i64 len` at offset 0 followed by the
|
||||
bytes plus a trailing NUL (DESIGN.md §"Str ABI").
|
||||
|
||||
4. Effect-op args walk in `Position::Borrow` per eob.1
|
||||
(`uniqueness.rs:289` + `linearity.rs`'s effect-op-arg arm); the
|
||||
let-binder for the Own heap-Str returned by `show x` fires its
|
||||
drop at scope close.
|
||||
|
||||
5. `drop_symbol_for_binder` has a Str carve-out (eob.1) that emits
|
||||
the correct rc-dec call for a Str let-binder regardless of
|
||||
whether the underlying realisation is heap-Str or static-Str
|
||||
(codegen-time elision ensures static-Str pointers do not reach
|
||||
`ailang_rc_dec`).
|
||||
|
||||
6. `Type::Forall` with `constraints` round-trips bit-stable through
|
||||
the Form-A parser + canonicaliser + printer (22b.4a.4.5 work,
|
||||
ratified by milestone 23's prelude fixtures `ne`/`lt`/`le`/etc.
|
||||
which all carry `Eq` or `Ord` constraints).
|
||||
|
||||
7. The Form-A `ClassDef` and `InstanceDef` schema shapes (DESIGN.md
|
||||
line 1512–1547) round-trip; the existing `class Eq` / `class Ord`
|
||||
defs in `examples/prelude.ail.json` are the load-bearing proof.
|
||||
|
||||
8. `ailang_rc_alloc(size_t)` is the heap-Str slab allocator,
|
||||
unconditionally linked post-eob.1 (the `__attribute__((weak))`
|
||||
on str.c's extern declaration is a documented no-op).
|
||||
|
||||
9. The mono pass's body walker (`mono.rs::collect_mono_targets`)
|
||||
schedules targets for both class-method residuals AND
|
||||
polymorphic free-fn calls with fully-concrete substitutions, in
|
||||
one pass, transitively (the `cmp_max_smoke` proof from 23.4).
|
||||
|
||||
10. `NoInstance` diagnostics already cross-reference the responsible
|
||||
class (per 22 milestone error-handling) and accept additional
|
||||
cross-references via the existing diagnostic-message
|
||||
infrastructure; adding a Show-aware variant is a content edit,
|
||||
not an infrastructure extension.
|
||||
|
||||
11. The canonical-form layer (per
|
||||
`docs/specs/2026-05-10-canonical-type-names.md`) treats mono
|
||||
Defs as post-typecheck artefacts not in
|
||||
`CheckedModule.symbols`, so adding `show__T` and `print__T`
|
||||
symbols does not affect surface-level hash pins. The four
|
||||
primitive instance type names (Int/Bool/Str/Float) are
|
||||
canonical (Decision 11's mono-symbol naming uses surface name
|
||||
for primitives).
|
||||
|
||||
12. `examples/prelude.ail.json` is the auto-loaded prelude per
|
||||
23.1's `check_workspace` extension; new defs added to it are
|
||||
visible to every workspace without an explicit `import`.
|
||||
Reference in New Issue
Block a user