spec: 24-show-print post-mq re-derive (24.2 + 24.3)
Re-derives the deferred iters 24.2 (class Show + 4 prim instances)
and 24.3 (print free fn + E2E) against the post-mq architecture.
Iter 24.1 shipped at f38bad8 and is unchanged. The supersedes-note
in the spec frontmatter explains the relation to the predecessor at
docs/specs/2026-05-12-24-show-print.md.
Substantive deltas vs. predecessor:
- Dispatch routing through the mq.2/.3 5-step rule; constraint-driven
filter (mq.tidy T1) is load-bearing for show calls inside print's
body.
- 24.2 grows to include the 22b-Show -> TShow/tshow migration
(~14 fixtures + 2 Rust test files) to eliminate post-prelude.Show
ambiguity, analogous to the existing TEq/TOrd convention.
Grounding-check PASS (re-dispatched after two LBA path corrections;
12 load-bearing assumptions all ratified).
This commit is contained in:
@@ -0,0 +1,616 @@
|
|||||||
|
# 24 — Show + print rewire (post-mq re-derive) — Design Spec
|
||||||
|
|
||||||
|
**Date:** 2026-05-13
|
||||||
|
**Status:** Draft — awaiting user spec review
|
||||||
|
**Authors:** Brummel (orchestrator) + Claude
|
||||||
|
**Supersedes:** `docs/specs/2026-05-12-24-show-print.md` for iters 24.2 +
|
||||||
|
24.3 only. The earlier spec stays as historical context for the
|
||||||
|
deferral rationale; iter 24.1 shipped against the earlier spec at
|
||||||
|
`f38bad8` and is unchanged. This document re-derives 24.2 + 24.3 from
|
||||||
|
scratch against the post-`mq` architecture (commits `0eb3323` mq.1 →
|
||||||
|
`2e6a4ca` mq.2 → `99d3968` mq.3 → `1b6cbcb` mq.tidy).
|
||||||
|
|
||||||
|
## Goal
|
||||||
|
|
||||||
|
Close the prelude story opened by milestone 23 (Eq/Ord) by shipping:
|
||||||
|
|
||||||
|
1. The `Show` typeclass with single method `show : (a borrow) -> Str`
|
||||||
|
in the prelude module.
|
||||||
|
2. Four primitive instances: `prelude.Show Int`, `prelude.Show Bool`,
|
||||||
|
`prelude.Show Str`, `prelude.Show Float`.
|
||||||
|
3. A polymorphic free fn `print : forall a. Show a => (a borrow) -> () !IO`
|
||||||
|
in the prelude module that routes through `show` and `io/print_str`,
|
||||||
|
replacing the ad-hoc per-type print idiom for new code.
|
||||||
|
|
||||||
|
The runtime + codegen primitives `bool_to_str` and `str_clone` already
|
||||||
|
shipped in iter 24.1 at `f38bad8`. No runtime work in this re-derive.
|
||||||
|
|
||||||
|
Existing per-type effect-ops `io/print_int|bool|float` STAY. Retiring
|
||||||
|
them and migrating the example corpus (~86 fixtures) is queued as a
|
||||||
|
separate P2 follow-up, unchanged from the original spec.
|
||||||
|
|
||||||
|
The post-mq architecture changes two things compared to the original
|
||||||
|
spec:
|
||||||
|
|
||||||
|
- **Dispatch routing.** mq.2 / mq.3 installed type-driven method
|
||||||
|
dispatch with a 5-step rule (qualifier → singleton → type-driven
|
||||||
|
filter → constraint-driven filter → Multi). The original spec
|
||||||
|
predicated routing on a workspace-global `MethodNameCollision`
|
||||||
|
pre-pass that has been retired. The new dispatch routes `show` calls
|
||||||
|
inside `print`'s body via the constraint-driven filter (Step 4 of
|
||||||
|
the dispatch rule) — `Show a` in `print`'s declared constraints
|
||||||
|
pins the candidate class to `prelude.Show`.
|
||||||
|
|
||||||
|
- **Existing fixture corpus collides at the class name "Show".** Pre-mq,
|
||||||
|
user-side `class Show` declarations in 14 test fixtures
|
||||||
|
(`examples/test_22b{1,2,3}_*.ail.json`) were the only `Show` in their
|
||||||
|
workspaces. Post-mq, shipping `prelude.Show` makes those user-Show
|
||||||
|
classes coexist with the prelude one — and because the user-Show
|
||||||
|
methods carry the same method name (`show`), the same arg-type shape
|
||||||
|
(`(a) -> Str`), AND the same instance head-type for `Int`, the
|
||||||
|
type-driven filter (Step 3) cannot discriminate at bare call sites.
|
||||||
|
Every `show x` in those fixtures would become Multi-ambiguous and
|
||||||
|
require an explicit qualifier. Migration is part of iter 24.2; the
|
||||||
|
strategy is "rename to `TShow`/`tshow`", analogous to the existing
|
||||||
|
`TEq`/`teq`, `TOrd`/`tlt` test-internal class-name convention that
|
||||||
|
pre-empts identical collisions with `prelude.Eq` / `prelude.Ord`.
|
||||||
|
|
||||||
|
## Architecture
|
||||||
|
|
||||||
|
Three artefacts, in dependency order; iter 24.1 already shipped the
|
||||||
|
two runtime primitives.
|
||||||
|
|
||||||
|
### 1. `class Show` + four primitive instances in `prelude.ail.json`
|
||||||
|
|
||||||
|
The prelude module name is literally `"prelude"`. Per the mq.1
|
||||||
|
canonical-form rule, intra-prelude class refs are bare; cross-module
|
||||||
|
refs (from user instance / constraint defs) carry the
|
||||||
|
`"prelude.Show"` qualifier.
|
||||||
|
|
||||||
|
`examples/prelude.ail.json` gains five new top-level defs (one class +
|
||||||
|
four instances):
|
||||||
|
|
||||||
|
```jsonc
|
||||||
|
// class — same-module, bare name
|
||||||
|
{ "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 — same-module, bare class ref per mq.1 canonical-form
|
||||||
|
{ "kind": "instance",
|
||||||
|
"class": "Show", // bare per mq.1
|
||||||
|
"type": { "k": "con", "name": "Int" },
|
||||||
|
"methods": [
|
||||||
|
{ "name": "show",
|
||||||
|
"body": { "t": "lam",
|
||||||
|
"params": ["x"],
|
||||||
|
"body": { "t": "app",
|
||||||
|
"fn": { "t": "var", "name": "int_to_str" },
|
||||||
|
"args": [{ "t": "var", "name": "x" }] } } }
|
||||||
|
]
|
||||||
|
}
|
||||||
|
// 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 (no
|
||||||
|
`try_emit_primitive_instance_body`-style hook) is needed because the
|
||||||
|
four primitives are themselves first-class lowered functions. 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 Show — unlike Eq/Ord (which exclude 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`);
|
||||||
|
acceptable for a human-readable Show.
|
||||||
|
|
||||||
|
### 2. `print` polymorphic free fn
|
||||||
|
|
||||||
|
`examples/prelude.ail.json` gains a sixth new top-level def:
|
||||||
|
|
||||||
|
```jsonc
|
||||||
|
{ "kind": "fn",
|
||||||
|
"name": "print",
|
||||||
|
"type": {
|
||||||
|
"k": "forall",
|
||||||
|
"vars": ["a"],
|
||||||
|
"constraints": [
|
||||||
|
{ "class": "Show", // bare per mq.1
|
||||||
|
"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**. Load-bearing for the
|
||||||
|
heap-Str RC discipline: the Own heap-Str returned by `show x` (every
|
||||||
|
instance allocates) needs a let-binder so `drop_symbol_for_binder`
|
||||||
|
fires the heap-Str drop at scope close via the Str carve-out
|
||||||
|
introduced in `eob.1`. The original spec marked implicit-vs-explicit
|
||||||
|
as an open commitment for the 24.3 implementer; this re-derive keeps
|
||||||
|
the same open commitment — if the desugarer auto-introduces a
|
||||||
|
let-binder for `Term::App` in effect-op-arg position, the source form
|
||||||
|
may be `\x -> do io/print_str (show x)` with identical post-checker
|
||||||
|
semantics.
|
||||||
|
|
||||||
|
`print` is a free fn, not a class method. Two reasons (unchanged from
|
||||||
|
the original spec):
|
||||||
|
|
||||||
|
- The body is identical for every `a : Show a` — no per-instance
|
||||||
|
variation. 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) and milestone 23's free-fn pattern (`ne`/`lt`/`le`/`gt`/`ge`).
|
||||||
|
|
||||||
|
### 3. Dispatch routing through the mq mechanism
|
||||||
|
|
||||||
|
Inside `print`'s body the call is `show x`. Bare method name; the
|
||||||
|
post-mq dispatcher (`resolve_method_dispatch` at synth time,
|
||||||
|
`refine_multi_candidate_residual` at discharge time) applies the
|
||||||
|
5-step rule:
|
||||||
|
|
||||||
|
1. **Qualifier** — none (bare).
|
||||||
|
2. **Singleton** — `Env.method_to_candidate_classes["show"]` is a
|
||||||
|
workspace-global index. Post-24.2-migration, no user class ships a
|
||||||
|
`show` method (the 22b corpus is renamed to `tshow`); the only
|
||||||
|
class with `show` is `prelude.Show`. So the candidate set for `show`
|
||||||
|
reduces to `{prelude.Show}` workspace-globally and Step-2 singleton
|
||||||
|
resolves directly — Steps 3-4 are not exercised for the bare `show`
|
||||||
|
inside `print`'s body. The constraint-driven filter (below) becomes
|
||||||
|
the load-bearing narrower only if a downstream user later
|
||||||
|
re-introduces their own `class Show` with a separate `show` method.
|
||||||
|
3. **Type-driven filter** — narrows by which candidate classes have a
|
||||||
|
registry entry for the residual type (`Show Int` instance check
|
||||||
|
for `print 42`).
|
||||||
|
4. **Constraint-driven filter** — `print`'s declared constraint
|
||||||
|
`Show a` is the load-bearing narrower. At the call site
|
||||||
|
`show x` inside `print`'s body, `x : a` rigid, and the rigid-var
|
||||||
|
filter installed by mq.tidy's T1 checks
|
||||||
|
`dc.class == c && constraint_type_matches(dc.type_, residual.type_)`.
|
||||||
|
The residual is `Show a` (the rigid type-var), `print`'s declared
|
||||||
|
constraint is `Show a`; both match → `prelude.Show` is the unique
|
||||||
|
resolved class.
|
||||||
|
5. **Multi** — not reached.
|
||||||
|
|
||||||
|
At the *outer* user call site `do print 42`, the dispatch on `print`
|
||||||
|
itself is by name (free fn, single global symbol) and the constraint
|
||||||
|
`Show Int` is discharged against the workspace registry which contains
|
||||||
|
`prelude.Show Int`. The dispatcher's behaviour mirrors milestone 23's
|
||||||
|
`ne`/`lt`/`le`/`gt`/`ge` at the same level.
|
||||||
|
|
||||||
|
### 4. Migration of 22b-Show user-class fixtures
|
||||||
|
|
||||||
|
Pre-mq, 14 test fixtures under `examples/test_22b{1,2,3}_*.ail.json`
|
||||||
|
declare a user-side `class Show {methods: ["show"]}` with arg-type
|
||||||
|
shape `(a) -> Str`. Pre-mq, these were the only `Show` in their
|
||||||
|
workspaces. Post-`prelude.Show` shipping, the prelude is auto-loaded
|
||||||
|
into every workspace per 23.1's `check_workspace` extension, so every
|
||||||
|
22b fixture now has TWO classes named `Show`: `prelude.Show` and (e.g.)
|
||||||
|
`test_22b1_dup_classmod.Show`. Both ship `(Int) -> Str` instances; the
|
||||||
|
type-driven filter cannot discriminate at bare `show x` call sites.
|
||||||
|
|
||||||
|
Strategy: **rename user-Show → TShow, user-show → tshow**, analogous
|
||||||
|
to the existing `TEq`/`teq` (vs. `prelude.Eq`/`eq`) and `TOrd`/`tlt`
|
||||||
|
(vs. `prelude.Ord`/`lt`) convention. The fixtures' intent is
|
||||||
|
unchanged (they test class-mechanism: orphan detection, dup detection,
|
||||||
|
xmod instances, missing-constraint diagnostics) — only the literal
|
||||||
|
class and method name change.
|
||||||
|
|
||||||
|
Mechanical scope:
|
||||||
|
|
||||||
|
- ~14 fixture `.ail.json` files: `"name": "Show"` → `"name": "TShow"`,
|
||||||
|
`"name": "show"` → `"name": "tshow"`, `"class": "Show"` →
|
||||||
|
`"class": "TShow"`, `"class": "<modname>.Show"` →
|
||||||
|
`"class": "<modname>.TShow"`, fn-body `"name": "show"` →
|
||||||
|
`"name": "tshow"`. Both `Show`-the-class and `show`-the-method get
|
||||||
|
renamed.
|
||||||
|
- 2 Rust test files: `crates/ail/tests/typeclass_22b2.rs` (30
|
||||||
|
Show/show occurrences) + `crates/ail/tests/typeclass_22b3.rs` (49).
|
||||||
|
Replace `"Show"` → `"TShow"` and `"show"` → `"tshow"` in expected
|
||||||
|
diagnostic strings.
|
||||||
|
|
||||||
|
The migration is a single mechanical pass within iter 24.2. Aborted-
|
||||||
|
attempt risk is low because the change is purely string substitution
|
||||||
|
(no semantic shift).
|
||||||
|
|
||||||
|
`mq3_two_show_*` and `mq3_class_eq_vs_fn_eq*` fixtures (created during
|
||||||
|
mq.3) intentionally do NOT migrate. They simulate the
|
||||||
|
two-Show-coexisting and class-vs-fn-collision shapes that are now
|
||||||
|
fully supported by the post-mq dispatcher; renaming them away would
|
||||||
|
defeat their purpose. These fixtures' Show classes are
|
||||||
|
`mq3_two_show_ambiguous_a.Show` and `mq3_two_show_ambiguous_b.Show`,
|
||||||
|
not user-Show analogues of prelude.Show.
|
||||||
|
|
||||||
|
After 24.2 lands, the workspace fixture corpus has zero ambiguous
|
||||||
|
bare-`show` call sites: every `show x` resolves either to `prelude.Show`
|
||||||
|
(via constraint-driven filter at user call sites with `Show Int`-style
|
||||||
|
constraints OR via instance singleton when only prelude.Show ships
|
||||||
|
Show-T for the residual T) or to `prelude.show` / `tshow` /
|
||||||
|
`mq3_*.Show.show` per their explicit qualifiers.
|
||||||
|
|
||||||
|
## Components (iterations)
|
||||||
|
|
||||||
|
| Iter | Status | Scope |
|
||||||
|
|------|--------|-------|
|
||||||
|
| **24.1** | shipped (`f38bad8`) | Runtime + codegen for `bool_to_str` + `str_clone`. Unchanged from original spec. |
|
||||||
|
| **24.2** | upcoming | **`class Show` + 4 primitive instances in prelude.** Plus the **22b-Show → TShow/tshow migration**. `examples/prelude.ail.json` gains `class Show a where show : (a borrow) -> Str` and four `instance Show <T>` defs (Int/Bool/Str/Float). ~14 `examples/test_22b*_*.ail.json` fixtures and 2 `crates/ail/tests/typeclass_22b{2,3}.rs` files migrate. DESIGN.md §"Prelude (built-in) classes" amended. Round-trip + mono-synthesis + hash-stability tests; full `cargo test --workspace` green. |
|
||||||
|
| **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`. Three new E2E fixtures (positive 4-prim, user-ADT, negative NoInstance). DESIGN.md §"Prelude (built-in) classes" amended to include `print`; §"Float semantics" gains the Show-Float NaN-spelling cross-reference paragraph. Roadmap P1 "Post-22 Prelude" entry flips to `[x]`; new P2 entry: "retire `io/print_int|bool|float` effect-ops + migrate example corpus to `print`". |
|
||||||
|
|
||||||
|
The milestone closes with the standard `audit` pipeline.
|
||||||
|
|
||||||
|
## Data flow
|
||||||
|
|
||||||
|
Two trajectories show the routing at work.
|
||||||
|
|
||||||
|
### `print 42` at type `Int` (user workspace)
|
||||||
|
|
||||||
|
1. **Typecheck of user call site.** `print` resolves to the
|
||||||
|
polymorphic free fn at `prelude.print` via the existing free-fn
|
||||||
|
global-lookup path (prep1 from 23.4). Constraint `Show Int`
|
||||||
|
discharged against `prelude.Show Int` (singleton registry hit).
|
||||||
|
2. **Mono of `print__Int`.** Body taken 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 `instance prelude.Show Int`'s
|
||||||
|
body (`\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 eob.1's Str
|
||||||
|
carve-out. `do io/print_str s` walks `s` as `Position::Borrow`; the
|
||||||
|
let-binder's drop fires after the effect-op call returns, emitting
|
||||||
|
`@ailang_rc_dec(s_ptr)`. Stdout: `"42\n"`.
|
||||||
|
|
||||||
|
### `print x` at user type `IntBox` with `instance prelude.Show IntBox`
|
||||||
|
|
||||||
|
1. **Typecheck.** User declares `data IntBox = MkIntBox Int` and
|
||||||
|
`instance prelude.Show IntBox` (cross-module class ref per
|
||||||
|
mq.1 — the instance lives in the user-type's defining module per
|
||||||
|
Decision 11 coherence). Constraint `prelude.Show IntBox` discharged
|
||||||
|
against the user-module registry entry.
|
||||||
|
2. **Mono.** `print__IntBox` synthesises with body
|
||||||
|
`\x -> let s = show__IntBox x in do io/print_str s`. `show__IntBox`
|
||||||
|
synthesises from the user instance body (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). The
|
||||||
|
diagnostic must cross-reference DESIGN.md §"Prelude (built-in)
|
||||||
|
classes" so the LLM-author immediately learns which types ship with
|
||||||
|
built-in Show. Re-uses the existing 22-era diagnostic
|
||||||
|
infrastructure; only content edit.
|
||||||
|
|
||||||
|
- **Class qualifier ambiguity at a user call site** — does NOT fire in
|
||||||
|
this milestone because the 22b-migration eliminates all current
|
||||||
|
ambiguous `show` call sites. Post-milestone, if a downstream user
|
||||||
|
declares their own `class Show` AND ships an instance whose head-type
|
||||||
|
collides with a prelude.Show instance head-type, the existing mq.3
|
||||||
|
`MultiClassUnresolved` diagnostic fires (already pinned by
|
||||||
|
`examples/mq3_two_show_ambiguous*.ail.json`). No new diagnostic
|
||||||
|
shape.
|
||||||
|
|
||||||
|
- **`OrphanInstance Show <UserType>`** — Decision 11 coherence rule
|
||||||
|
unchanged. User-side `instance prelude.Show <UserType>` MUST live in
|
||||||
|
the user-type's defining module (the prelude is read-only).
|
||||||
|
|
||||||
|
- **`CheckError::Internal` from mono** — if Show-specialisation fails
|
||||||
|
internally, this is a caller-contract violation per the existing
|
||||||
|
`mono.rs::synthesise_mono_fn` convention. Mirrors 23.4's free-fn
|
||||||
|
error handling.
|
||||||
|
|
||||||
|
## Testing strategy
|
||||||
|
|
||||||
|
### 24.2 — class Show + 4 instances + 22b migration
|
||||||
|
|
||||||
|
- **Round-trip:** `examples/prelude.ail.json` parses + canonicalises
|
||||||
|
bit-stable after the five new defs land. The existing prelude
|
||||||
|
hash-stability test from milestone 23 stays green (pre-existing
|
||||||
|
Ordering/Eq/Ord/instances/`ne`/`lt`/`le`/`gt`/`ge` unaffected).
|
||||||
|
|
||||||
|
- **Mono synthesis** (unit test in
|
||||||
|
`crates/ailang-check/src/mono.rs::tests`): for a fixture calling
|
||||||
|
`show 1`, `show True`, `show "x"`, `show 1.5`, assert 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.
|
||||||
|
|
||||||
|
- **Dispatch via constraint-driven filter pin** (unit test in
|
||||||
|
`crates/ailang-check/src/lib.rs::tests`, building on the existing
|
||||||
|
`method_dispatch_pin.rs` style): for a workspace with `prelude.Show`
|
||||||
|
loaded and a user `class TShow {tshow}` declared in a user module,
|
||||||
|
assert that `show x` (bare) routes to `prelude.Show` and `tshow x`
|
||||||
|
(bare) routes to user `TShow`. Each method name has exactly one
|
||||||
|
candidate class globally, so Step-2 singleton resolves without
|
||||||
|
needing Steps 3-4. The pin covers the post-22b-migration steady
|
||||||
|
state where user fixtures pick non-`Show` class names.
|
||||||
|
|
||||||
|
- **Hash stability of existing mono symbols:** `eq__Int`,
|
||||||
|
`compare__Str`, and the other class-method mono symbols from
|
||||||
|
milestone 23 must produce identical bodies (and identical hashes)
|
||||||
|
under the unified pass after Show defs are added. Pin in the style
|
||||||
|
of `crates/ailang-core/src/hash.rs`'s milestone-23 fixtures.
|
||||||
|
|
||||||
|
- **22b-migration regression check** — `cargo test -p ail
|
||||||
|
--test typeclass_22b2 --test typeclass_22b3` passes after the
|
||||||
|
rename. Each migrated fixture parses + canonicalises bit-stable.
|
||||||
|
|
||||||
|
### 24.3 — print polymorphic free fn + E2E
|
||||||
|
|
||||||
|
- **Positive E2E (`examples/show_print_smoke.ail.json`):** 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)
|
||||||
|
```
|
||||||
|
Asserts compile, run, expected stdout. The Float line uses
|
||||||
|
`3.14` whose `%g` rendering is stable across all targeted libc
|
||||||
|
versions.
|
||||||
|
|
||||||
|
- **User-ADT E2E (`examples/show_user_adt.ail.json`):**
|
||||||
|
```
|
||||||
|
data IntBox = MkIntBox Int
|
||||||
|
instance prelude.Show IntBox where
|
||||||
|
show = \x -> match x with MkIntBox n -> int_to_str n
|
||||||
|
fn main = do print (MkIntBox 7)
|
||||||
|
```
|
||||||
|
Stdout `"7\n"`. Confirms mono handles user-defined `prelude.Show`
|
||||||
|
instances and that `print` composes with them. The qualifier
|
||||||
|
`prelude.Show` is canonical-form per mq.1 (cross-module class ref
|
||||||
|
from a user-defining module).
|
||||||
|
|
||||||
|
- **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>`. Diagnostic
|
||||||
|
wording finalised by the implementer; gold-standard test pins
|
||||||
|
the message verbatim post-draft (open commitment carries forward
|
||||||
|
from original spec).
|
||||||
|
|
||||||
|
- **Mono symbol IR-shape pin:** 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** — every E2E fixture parses +
|
||||||
|
canonicalises bit-stable.
|
||||||
|
|
||||||
|
- **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.2 has landed:** `examples/prelude.ail.json` contains
|
||||||
|
`class Show a where show : (a borrow) -> Str` (bare class name,
|
||||||
|
bare method name, intra-prelude canonical form) and four primitive
|
||||||
|
instances Int/Bool/Str/Float. The mono pass synthesises
|
||||||
|
`show__Int|Bool|Str|Float`. The 22b-Show fixture corpus is migrated
|
||||||
|
to `TShow`/`tshow`; `cargo test --workspace` green. DESIGN.md
|
||||||
|
§"Prelude (built-in) classes" amended to include Show with the four
|
||||||
|
instances.
|
||||||
|
|
||||||
|
2. **24.3 has landed:** `examples/prelude.ail.json` contains
|
||||||
|
`fn print : forall a. Show a => (a borrow) -> () !IO` with the
|
||||||
|
explicit-let body (or implicit-let if the implementer ratifies the
|
||||||
|
surface-form simplification per Open Commitment carryforward). The
|
||||||
|
mono pass synthesises `print__Int|Bool|Str|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.
|
||||||
|
|
||||||
|
3. **Tests pass:** `cargo test --workspace` green; existing milestone
|
||||||
|
23 prelude fixtures (`ne`/`lt`/`le`/`gt`/`ge` E2E) unchanged; mq.3
|
||||||
|
E2E fixtures (`mq3_two_show_*`, `mq3_class_eq_vs_fn_eq*`)
|
||||||
|
unchanged.
|
||||||
|
|
||||||
|
4. **Bench regression ratified:** `bench/check.py && bench/compile_check.py && bench/cross_lang.py`
|
||||||
|
exit 0 or audit-ratified with journal entry.
|
||||||
|
|
||||||
|
5. **Roadmap update:** P1 "Post-22 Prelude — Show + print rewire"
|
||||||
|
entry flips to `[x]`. New P2 entry: "Retire `io/print_int|bool|float`
|
||||||
|
effect-ops + migrate example corpus to `print`".
|
||||||
|
|
||||||
|
## Out of scope (deferred, with substantive rationale)
|
||||||
|
|
||||||
|
Unchanged from the original spec; condensed summary:
|
||||||
|
|
||||||
|
- **Retiring `io/print_int|bool|float`.** Queued P2; same call as
|
||||||
|
milestone 23 made for `==` / `eq`.
|
||||||
|
- **`io/print_str` retirement.** Stays — load-bearing inside `print`,
|
||||||
|
plus useful as a bypass when an Str is already in hand.
|
||||||
|
- **`bool_to_str` as schema-`if`.** Stays as runtime primitive;
|
||||||
|
phi-of-static-Str through drop-elision is not ratified.
|
||||||
|
- **`str_clone` as rc_header bump.** Stays as always-copy; runtime
|
||||||
|
static-Str/heap-Str tagging is deliberately not supported post-hs.2.
|
||||||
|
- **`Show Ordering` instance.** No demand; user can declare.
|
||||||
|
- **`Show` for ADTs via `deriving`.** No auto-derivation; substantive
|
||||||
|
feature in its own right.
|
||||||
|
- **Higher-kinded Show (`Show [a]`).** Decision 11 axis 5 excludes
|
||||||
|
higher-kinded class params; LLM-natural pattern is per-type
|
||||||
|
instances.
|
||||||
|
- **`print` newline-free variant.** Deferred until a concrete
|
||||||
|
LLM-author pattern demands it.
|
||||||
|
- **Operator routing through `Show`.** No commitment; AILang has no
|
||||||
|
Haskell-style monadic operator surface.
|
||||||
|
|
||||||
|
## Open commitments (24.2 / 24.3 implementer)
|
||||||
|
|
||||||
|
- **`print` implicit-let vs. explicit-let** — implementer verifies the
|
||||||
|
desugarer's behaviour during 24.3 Task 1; if implicit-let is the
|
||||||
|
realised semantics for `Term::App` in effect-op-arg position, the
|
||||||
|
prelude source form may use the more compact
|
||||||
|
`\x -> do io/print_str (show x)`. Load-bearing property: "the
|
||||||
|
heap-Str returned by `show x` has a tracked let-binder when entering
|
||||||
|
the effect-op call site"; sourcing is surface-level.
|
||||||
|
|
||||||
|
- **Negative-test diagnostic wording.** Implementer drafts the
|
||||||
|
Show-aware `NoInstance Show <T>` message; orchestrator reviews in
|
||||||
|
spec-compliance phase.
|
||||||
|
|
||||||
|
- **22b-migration mechanical-pass scope.** Implementer verifies during
|
||||||
|
24.2 Task 1 that the rename target set is exactly the 14 fixtures
|
||||||
|
surfaced by `grep -l '"name": "Show"' examples/test_22b*_*.ail.json`
|
||||||
|
plus the two `typeclass_22b{2,3}.rs` files. If a 22b fixture turns
|
||||||
|
out to use `Show` as part of a substring (e.g. inside an ADT
|
||||||
|
constructor name like `"ShowValue"`), the implementer flags and
|
||||||
|
spot-checks rather than blindly sed-ing. (Quick visual scan above
|
||||||
|
shows only class names + method names + cross-module class refs;
|
||||||
|
no constructor-name false positives.)
|
||||||
|
|
||||||
|
- **mq3 fixture preservation.** The 7 `mq3_*` fixtures created in
|
||||||
|
mq.3 INTENTIONALLY do NOT migrate. Implementer confirms they stay
|
||||||
|
unchanged and continue to pin two-Show-coexisting and
|
||||||
|
class-vs-fn-collision behaviour.
|
||||||
|
|
||||||
|
## Known costs
|
||||||
|
|
||||||
|
- **24.2 prelude additions:** `examples/prelude.ail.json` +40–50 lines
|
||||||
|
(one class + four instances, JSON shape parallel to existing Eq
|
||||||
|
Int/Bool/Str instances). DESIGN.md amendment ~10 lines.
|
||||||
|
|
||||||
|
- **24.2 22b-migration:** ~14 `.ail.json` files (~3-5 string subs
|
||||||
|
each), 2 Rust test files (~80 string subs total). Net LOC change
|
||||||
|
zero (pure rename); review-burden non-trivial because of fixture
|
||||||
|
count.
|
||||||
|
|
||||||
|
- **24.3 prelude additions + tests:** `examples/prelude.ail.json` +30
|
||||||
|
lines (one polymorphic free fn). Three new E2E `.ail.json` fixtures,
|
||||||
|
~40 lines each. Diagnostic test ~20 lines Rust. DESIGN.md amendments
|
||||||
|
~20 lines.
|
||||||
|
|
||||||
|
- **Net code reduction:** none. Additive milestone. Reduction comes in
|
||||||
|
the P2 follow-up (~−150 LOC retiring the three per-type effect-ops).
|
||||||
|
|
||||||
|
- **Compile-time shift:** mono pass gains four instance-method
|
||||||
|
synthesis targets plus one free-fn target per call site. Bounded,
|
||||||
|
expected within bench tolerance; audit-ratified post-24.3.
|
||||||
|
|
||||||
|
- **Runtime cost on `print x`:**
|
||||||
|
- `x : Int` — one `int_to_str` alloc (~3-20 bytes) + rc_dec.
|
||||||
|
- `x : Bool` — one `bool_to_str` alloc (5-6 bytes) + rc_dec.
|
||||||
|
- `x : Str` — one `str_clone` alloc + memcpy + rc_dec. **Strictly
|
||||||
|
worse** than `do io/print_str x`; redundancy acknowledged.
|
||||||
|
- `x : Float` — one `float_to_str` alloc + rc_dec.
|
||||||
|
|
||||||
|
## Load-bearing assumptions about current behaviour
|
||||||
|
|
||||||
|
Each assumption is something this spec relies on as currently-true.
|
||||||
|
|
||||||
|
1. **mq.2/.3 dispatcher.** `crates/ailang-check/src/lib.rs::resolve_method_dispatch`
|
||||||
|
implements the 5-step rule (qualifier → singleton → type-driven
|
||||||
|
filter → constraint-driven filter → Multi). `refine_multi_candidate_residual`
|
||||||
|
applies the discharge-time refinement with the rigid-var
|
||||||
|
type-unification leg added by mq.tidy T1. Bare method names route
|
||||||
|
correctly through both call sites. Pinned by
|
||||||
|
`crates/ailang-check/tests/method_dispatch_pin.rs`.
|
||||||
|
|
||||||
|
2. **Inverse method index.** `Env.method_to_candidate_classes` is
|
||||||
|
populated workspace-globally and is the authoritative source for
|
||||||
|
"which classes declare method M". Pinned by
|
||||||
|
`crates/ailang-check/tests/method_collision_pin.rs`.
|
||||||
|
|
||||||
|
3. **`class_methods` tuple-keyed.** `class_methods` is keyed by
|
||||||
|
`(QualifiedClass, MethodName)` post-mq.3 retirement of the global
|
||||||
|
pre-pass; two classes can declare the same method name without
|
||||||
|
collision. Pinned by `mq3_class_method_shadowed_by_fn_warning_fires`
|
||||||
|
and `crates/ail/tests/mq3_multi_class_e2e.rs`.
|
||||||
|
|
||||||
|
4. **mq.1 canonical-form for class refs.** Class refs in
|
||||||
|
`InstanceDef.class`, `Constraint.class`, `SuperclassRef.superclass`,
|
||||||
|
and `Type::Con.name` follow: bare for same-module, `<module>.<Class>`
|
||||||
|
for cross-module. Pinned by the in-crate `bare_cross_module_class_ref_fires`
|
||||||
|
and `bad_cross_module_class_ref_fires` tests in
|
||||||
|
`crates/ailang-core/src/workspace.rs` (the `#[cfg(test)] mod tests`
|
||||||
|
block around lines 2783-2860) plus the on-disk mq.1 fixture corpus
|
||||||
|
(`examples/mq1_xmod_constraint_class{,_dep}.ail.json`).
|
||||||
|
|
||||||
|
5. **`int_to_str`, `float_to_str`, `bool_to_str`, `str_clone`** —
|
||||||
|
installed in `builtins.rs` with `ret_mode: Own`, lowered in
|
||||||
|
`Emitter::lower_app` via direct extern calls, RC-disciplined
|
||||||
|
end-to-end. The latter two shipped in 24.1 at `f38bad8`. Pinned by
|
||||||
|
`crates/ail/tests/e2e.rs::{int,bool,str_clone}_*_drop_balances_rc_stats`
|
||||||
|
plus the builtins-side signature-install tests in
|
||||||
|
`crates/ailang-check/src/builtins.rs`'s `#[cfg(test)] mod tests`.
|
||||||
|
|
||||||
|
6. **`io/print_str`** lowers to `@puts(ptr)` and accepts any Str
|
||||||
|
realisation via the heap-Str-compatible consumer ABI per
|
||||||
|
DESIGN.md §"Str ABI". Effect-op args walk in `Position::Borrow`
|
||||||
|
per eob.1.
|
||||||
|
|
||||||
|
7. **`drop_symbol_for_binder` Str carve-out.** Emits the correct
|
||||||
|
rc-dec for Str let-binders regardless of static-Str / heap-Str
|
||||||
|
underlying realisation; codegen-time elision ensures static-Str
|
||||||
|
pointers do not reach `ailang_rc_dec`.
|
||||||
|
|
||||||
|
8. **`Type::Forall` round-trip.** Form-A parser + canonicaliser +
|
||||||
|
printer round-trip `Type::Forall` with `constraints` bit-stable.
|
||||||
|
Pinned by milestone 23's `ne`/`lt`/`le`/`gt`/`ge` prelude entries.
|
||||||
|
|
||||||
|
9. **Mono pass body walker.** `mono.rs::collect_mono_targets`
|
||||||
|
schedules targets for both class-method residuals and polymorphic
|
||||||
|
free-fn calls in one fixpoint pass; pinned by 23.4's
|
||||||
|
`cmp_max_smoke` proof.
|
||||||
|
|
||||||
|
10. **Auto-loaded prelude.** `examples/prelude.ail.json` is auto-loaded
|
||||||
|
per 23.1's `check_workspace` extension; new prelude defs are
|
||||||
|
visible to every workspace without explicit `import`. The
|
||||||
|
pre-existing `"prelude" is reserved` loader-side error confirms
|
||||||
|
auto-injection.
|
||||||
|
|
||||||
|
11. **22b user-Show fixtures structurally identical.** All 14
|
||||||
|
target fixtures declare `class Show {methods: ["show"]}` with
|
||||||
|
`(a) -> Str` signature, and any instance declarations
|
||||||
|
use type-shape that collides with prelude.Show's at the
|
||||||
|
type-driven filter level. Empirical grep above ratifies the
|
||||||
|
structural-identity assumption.
|
||||||
|
|
||||||
|
12. **mq3 fixtures intentionally exercise multi-Show.** `mq3_two_show_*`
|
||||||
|
and `mq3_class_eq_vs_fn_eq*` fixtures use Show class names in
|
||||||
|
their own modules deliberately to exercise post-mq dispatch; they
|
||||||
|
do NOT migrate in 24.2.
|
||||||
Reference in New Issue
Block a user