spec: 23 — Eq/Ord Prelude (Show + heap-Str ABI deferred to next milestone)
This commit is contained in:
@@ -0,0 +1,208 @@
|
||||
# 23 — Eq / Ord Prelude — Design Spec
|
||||
|
||||
**Date:** 2026-05-10
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Ship `Eq` and `Ord` typeclasses with primitive instances on `Int`,
|
||||
`Bool`, and `Str`. Add the `Ordering` ADT (`LT | EQ | GT`) and five
|
||||
free top-level utility functions (`ne`, `lt`, `le`, `gt`, `ge`)
|
||||
defined through the class methods. Establish the partial-Eq/Ord
|
||||
story for `Float` as a lived reality: `Float` has neither instance,
|
||||
so polymorphic `eq x y` / `compare x y` over a Float fires
|
||||
`NoInstance` at typecheck — exactly what DESIGN.md §"Float
|
||||
semantics" prescribes.
|
||||
|
||||
`Show`, operator routing, `print`-rewire, and the heap-Str ABI are
|
||||
**out of scope** here. Each is its own milestone with substantive
|
||||
reasons (see "Out of scope").
|
||||
|
||||
## Architecture
|
||||
|
||||
The milestone consumes the milestone-22 typeclass machinery
|
||||
unchanged: `class` / `instance` schema, monomorphiser-emitted
|
||||
`<method>__<typesurfacename>` symbols, instance-resolution at
|
||||
typecheck. Three new artefacts:
|
||||
|
||||
1. **A prelude AILang module** at `examples/prelude.ail.json` —
|
||||
author-canonical Form-A JSON containing the `Eq` and `Ord`
|
||||
class definitions, six instances (Eq + Ord on Int / Bool / Str),
|
||||
the `Ordering` ADT, and the five free utility functions.
|
||||
2. **Auto-loading of the prelude into every workspace** via a small
|
||||
change to `check_workspace` so the prelude module is reachable
|
||||
from any user module without an explicit `import`.
|
||||
3. **Two new C-runtime functions in `runtime/str.c`:**
|
||||
`ail_str_eq(a, b) -> bool` (byte-equality on existing constant-
|
||||
string layouts) and `ail_str_compare(a, b) -> i32` (lex
|
||||
comparison returning -1/0/+1). Both operate on existing
|
||||
constant-Str payloads; **no heap allocation, no RC interaction**.
|
||||
Codegen arms for `eq__Str` and `compare__Str` emit calls to
|
||||
these.
|
||||
|
||||
Instance bodies for the non-Str primitives lower to existing IR
|
||||
shapes: `eq__Int` to `icmp eq i64`, `eq__Bool` to `icmp eq i1`,
|
||||
`compare__Int` to a branch ladder constructing `LT` / `EQ` / `GT`
|
||||
ADT values per `icmp slt` / `icmp eq` results, `compare__Bool`
|
||||
similarly.
|
||||
|
||||
The existing primitive operators (`==`, `<`, `<=`, `>`, `>=`)
|
||||
remain primitive and per-type-routed at lowering, **unchanged from
|
||||
milestone 22**. Routing them through the class methods is the
|
||||
declared P2 follow-up; the redundancy between primitive `==` and
|
||||
class `eq x y` on Int/Bool/Str is acknowledged and ratified for
|
||||
this milestone as transitional.
|
||||
|
||||
## Components (iterations)
|
||||
|
||||
| Iter | Scope |
|
||||
|------|-------|
|
||||
| 23.1 | `Ordering` ADT (`data Ordering = LT | EQ | GT`) + prelude-module skeleton at `examples/prelude.ail.json` containing only the `Ordering` def. Wire `check_workspace` to auto-load this module. Codegen + match-lowering for `Ordering` exercised by a unit test that pattern-matches on each constructor and returns an Int. |
|
||||
| 23.2 | Add `class Eq a where eq : (a borrow, a borrow) -> Bool` + three instances (Eq Int, Eq Bool, Eq Str) to the prelude. New file `runtime/str.c` with `ail_str_eq`. Codegen arm for `eq__Str` emits `call zext i1 @ail_str_eq(...)`. Codegen unit tests for `eq__Int`, `eq__Bool`, `eq__Str`. |
|
||||
| 23.3 | Add `class Ord a extends Eq where compare : (a borrow, a borrow) -> Ordering` + three instances (Ord Int, Ord Bool, Ord Str). Extend `runtime/str.c` with `ail_str_compare`. Codegen arms for `compare__Int`, `compare__Bool`, `compare__Str`; each pattern-matches the underlying primitive comparison into the `Ordering` ADT. |
|
||||
| 23.4 | Five free top-level functions in the prelude: `ne : forall a. Eq a => (a borrow, a borrow) -> Bool` (body: `not (eq x y)`); `lt`, `le`, `gt`, `ge` with `forall a. Ord a =>` constraints, bodies pattern-matching `compare` against the right Ordering shape. |
|
||||
| 23.5 | E2E fixtures: (a) positive — a polymorphic helper `forall a. Ord a => (a borrow, a borrow) -> Bool` invoked at three primitive types, prints `true`/`false` per case; (b) negative — `eq f g` where `f, g : Float` typecheck-rejects with `NoInstance Eq Float` matching DESIGN.md §"Float semantics"; (c) user-ADT integration — `data IntBox = MkIntBox Int` + `instance Eq IntBox` + `instance Ord IntBox` + polymorphic helper monomorphises to the user instances. DESIGN.md amendment: §"Decision 11 / Prelude (built-in) classes" updated to reflect Eq/Ord arrival in milestone 23 (Show still deferred). Roadmap moves Post-22 Prelude entry from `[~]` to `[x]` for the Eq/Ord half; Show half stays as a new entry. |
|
||||
|
||||
## Data flow
|
||||
|
||||
Surface call `(eq x y)` with `x : Int` known from context:
|
||||
|
||||
1. **Typecheck.** `eq` resolves to `forall a. Eq a => (a, a) -> Bool`.
|
||||
Constraint solver matches `Eq Int` against the `instance Eq Int`
|
||||
in the auto-loaded prelude; constraint discharged.
|
||||
2. **Monomorphisation** (22b.3 path). Call rewritten to
|
||||
`eq__Int x y`. Symbol synthesised in the same way 22's
|
||||
user-class fixture synthesises `foo__IntBox`.
|
||||
3. **Codegen.** `eq__Int` lowers to a single `icmp eq i64 %x, %y`
|
||||
plus a `zext i1 i8` (Bool is i8 in AILang's runtime).
|
||||
|
||||
For Str the codegen arm is a single `call i1 @ail_str_eq(...)`
|
||||
into `runtime/str.c`. For `compare` on Int the arm is a branch
|
||||
ladder (`icmp slt` for LT-or-not, `icmp eq` for EQ-or-GT)
|
||||
returning the corresponding ADT-tag.
|
||||
|
||||
Polymorphic helpers (`fn cmp_max : forall a. Ord a => (a, a) -> a`)
|
||||
work the same way: the typeclass-elaboration in 22b.3 inserts the
|
||||
right monomorphised `compare__T` symbol per use site.
|
||||
|
||||
## Error handling
|
||||
|
||||
- **`NoInstance Eq Float` / `NoInstance Ord Float`** — fired at
|
||||
typecheck when class resolution selects Float. Diagnostic must
|
||||
cross-reference DESIGN.md §"Float semantics" so the LLM-author
|
||||
immediately learns the partial-Float story instead of guessing.
|
||||
- **`NoInstance Eq <UserType>` / `NoInstance Ord <UserType>`** —
|
||||
re-uses 22's existing diagnostic path. No new wiring.
|
||||
- **`OrphanInstance`** — Decision 11 unchanged. Prelude
|
||||
instances are non-orphan because both class and instance type
|
||||
live in the prelude module.
|
||||
- **Codegen-side errors are not expected** — the new arms (`eq__Str`,
|
||||
`compare__Str`) are uniformly-shaped lowerings and reuse
|
||||
established `lower_app` mechanics. If a fall-through emerges,
|
||||
it must be `CodegenError::Internal`-shaped (per the iter-4.4
|
||||
Floats fixup precedent), never `unimplemented!()` panic.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
- **Codegen unit tests** per primitive method: `eq__Int`,
|
||||
`eq__Bool`, `eq__Str`, `compare__Int`, `compare__Bool`,
|
||||
`compare__Str`. Each asserts the IR string contains the right
|
||||
intrinsic / call.
|
||||
- **Workspace tests** (`check_module` / `check_workspace` path):
|
||||
- `eq` and `compare` return correct `Bool` / `Ordering` on
|
||||
each primitive.
|
||||
- `ne`, `lt`, `le`, `gt`, `ge` agree with their primitive-
|
||||
operator counterparts on a small suite of known cases.
|
||||
- **Negative:** `eq` / `compare` over a Float typecheck-rejects
|
||||
with the right diagnostic message (gold-standard test that
|
||||
pins the message text, mirroring the Floats-milestone
|
||||
diagnostic style).
|
||||
- **E2E fixture** `examples/eq_ord_polymorphic.ail.json`:
|
||||
defines a polymorphic helper, calls it on three primitive
|
||||
types, prints the right output. Compiles and runs end-to-end.
|
||||
- **Round-trip:** the prelude module + every new fixture passes
|
||||
Form-A parser + canonicaliser bit-stable.
|
||||
- **Bench-regression check** at milestone close: the three bench
|
||||
scripts exit 0 with the prelude auto-loaded into every
|
||||
workspace. (Hypothesis: prelude-load adds a constant-time
|
||||
per-workspace overhead, no per-call regression. If a regression
|
||||
fires, audit dispatches `ailang-bencher`.)
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
1. Iters 23.1 → 23.5 JOURNAL entries committed.
|
||||
2. Workspace tests pass: all current tests + the new positive,
|
||||
negative, and user-ADT fixtures.
|
||||
3. `bench/check.py && bench/compile_check.py && bench/cross_lang.py`
|
||||
exit 0 (or any non-zero exit is ratified per audit-skill rules
|
||||
with a JOURNAL entry naming the iter that intentionally moved
|
||||
the metric).
|
||||
4. A polymorphic helper `forall a. Ord a => (a borrow, a borrow) -> Bool`
|
||||
compiles, monomorphises at three primitive types, runs, and
|
||||
prints the expected output for at least Int and Str.
|
||||
5. The same polymorphic helper called on a Float fires
|
||||
`NoInstance Ord Float` at typecheck with a Float-aware
|
||||
diagnostic message.
|
||||
6. DESIGN.md §"Decision 11 / Prelude (built-in) classes" amended
|
||||
to reflect Eq/Ord shipping in milestone 23. The "Milestone 22
|
||||
ships no built-in Prelude classes" wording stays as historical
|
||||
accuracy; a forward-pointing addendum names this milestone's
|
||||
delivery.
|
||||
|
||||
## Out of scope (deferred, with substantive rationale)
|
||||
|
||||
- **`Show` typeclass.** Defers behind a heap-Str-ABI milestone.
|
||||
`instance Show Int` needs `int_to_str` to allocate a heap-Str —
|
||||
a runtime primitive AILang does not have today (see Floats
|
||||
fieldtest's deferred `float_to_str`). Bundling Show with
|
||||
heap-Str ABI in this milestone would conflate two orthogonal
|
||||
axes (typeclass-instance shape vs. runtime-allocated-Str
|
||||
ABI). They run as separate milestones in sequence.
|
||||
- **Operator routing through `Eq` / `Ord`.** `==`, `<`, etc. stay
|
||||
primitive this milestone. Routing them through the class methods
|
||||
is the declared P2 todo, gated on bench rebaseline confirmation
|
||||
that the indirection does not tank latency. Without routing,
|
||||
surface `==` on Int and `eq x y` are redundant — this is
|
||||
acknowledged and ratified as transitional for one milestone.
|
||||
- **`print`-rewire through `Show.show`.** Same heap-Str
|
||||
dependency as `Show`.
|
||||
- **`Eq` / `Ord` on Float.** No instance per DESIGN.md §"Float
|
||||
semantics". A future iter that surfaces concrete LLM-author code
|
||||
benefiting from `Float` partial-comparators (signature
|
||||
`compare : Float -> Float -> Maybe Ordering`) opens a separate
|
||||
brainstorm.
|
||||
- **`deriving (Eq, Ord)` for user ADTs.** No auto-derivation; the
|
||||
user / LLM writes `instance Eq Foo where eq = ...` explicitly.
|
||||
Future milestone gated on Feature-acceptance.
|
||||
- **`Ordering` total-ordering instance** (`Ord Ordering`). Cute
|
||||
but no concrete demand. Skipped.
|
||||
|
||||
## Known costs
|
||||
|
||||
- ~30 LOC of new C in `runtime/str.c`.
|
||||
- ~60-80 lines of new AILang Form-A JSON in `examples/prelude.ail.json`
|
||||
(class defs + instances + free fns + Ordering ADT).
|
||||
- ~6 new codegen arms (eq__T, compare__T for T ∈ {Int, Bool, Str}).
|
||||
- Small `check_workspace` change for prelude auto-loading.
|
||||
- Transitional redundancy `==` (primitive) ↔ `eq` (class method)
|
||||
on Int/Bool/Str. Lifts in P2 routing milestone.
|
||||
- New typecheck arm for the Float-NoInstance gold-standard
|
||||
diagnostic message.
|
||||
|
||||
## Open commitments (23.1 → 23.5 implementer)
|
||||
|
||||
- **Prelude module path.** Spec commits to
|
||||
`examples/prelude.ail.json`. If the implementation surfaces a
|
||||
reason this is wrong (e.g. `examples/` is reserved for user-
|
||||
facing fixtures and a non-fixture path is more honest), the
|
||||
implementer raises it via `NEEDS_CONTEXT`; the orchestrator
|
||||
picks the new home. Default holds otherwise.
|
||||
- **Diagnostic text** for `NoInstance Eq Float` /
|
||||
`NoInstance Ord Float`. Implementer drafts a one-line
|
||||
Float-aware message; orchestrator reviews in spec compliance.
|
||||
- **`Bool` is `i8` or `i1` in IR?** AILang's Bool surface
|
||||
representation is `i8` in the runtime ABI. `eq__Bool` produces
|
||||
`icmp eq i8` + the call site is responsible for staying in i8
|
||||
Bool-conventions. Confirm against existing `==` Bool lowering
|
||||
in `lower_eq`.
|
||||
Reference in New Issue
Block a user