diff --git a/docs/specs/2026-05-21-fieldtest-operator-routing-eq-ord.md b/docs/specs/2026-05-21-fieldtest-operator-routing-eq-ord.md new file mode 100644 index 0000000..9fef742 --- /dev/null +++ b/docs/specs/2026-05-21-fieldtest-operator-routing-eq-ord.md @@ -0,0 +1,241 @@ +# Fieldtest — operator-routing-eq-ord — 2026-05-21 + +**Status:** Draft — awaiting orchestrator triage +**Author:** ailang-fieldtester (dispatched by skills/fieldtest) + +## Scope + +The `operator-routing-eq-ord` milestone removed the surface comparator +names `==` / `!=` / `<` / `<=` / `>` / `>=` from the language. Equality +and ordering are now class methods that resolve via `prelude.Eq` / +`prelude.Ord` class-dispatch — `eq` / `ne` / `lt` / `le` / `gt` / `ge` / +`compare` over the primitive instances (Int, Bool, Str, Unit) plus any +user ADT with a hand-written instance. Float has no Eq/Ord instance by +design; the six monomorphic prelude fns `float_eq` / `float_ne` / +`float_lt` / `float_le` / `float_gt` / `float_ge` are the explicit +named-fn surface for IEEE-aware Float comparison, each lowered to a +single `fcmp` via the codegen intercept with `alwaysinline`. + +## Examples + +### `examples/fieldtest/eqord_1_fizzbuzz.ail` — FizzBuzz over [1..15] + +- **What it does:** classic FizzBuzz, dispatching equality on + `(app eq (app % n K) 0)` for K in {3, 5, 15}, plus the empty-string + guard `(app eq label "")`, plus a tail-recursive loop driver bounded + by `(app gt i stop)`. +- **Why it fits:** exercises the primitive Eq path at Int and Str + simultaneously, plus the Ord-class free helper `gt` at Int — the + three most-reached-for shapes in everyday integer code. +- **Outcome:** compiles, runs, matches expected stdout + (`1\n2\nFizz\n4\nBuzz\nFizz\n7\n8\nFizz\nBuzz\n11\nFizz\n13\n14\nFizzBuzz\n`). + +### `examples/fieldtest/eqord_2_rational_eq.ail` — Rational with hand-written Eq + +- **What it does:** defines `data Rational (ctor MkRational Int Int)`, + writes `instance prelude.Eq Rational` using cross-multiplication + (`a/b == c/d` iff `a*d == b*c`), drives four comparisons in `main`. +- **Why it fits:** Axis 2 north-star. The user-instance body's inner + `(app eq (app * a d) (app * b c))` dispatches to `prelude.eq__Int`, + while the outer `(app eq r1 r2)` from main dispatches to this + module's `eq__Rational`. End-to-end: user-instance → prelude class + method → primitive intercept. +- **Outcome:** compiles, runs, matches expected stdout + (`true\nfalse\ntrue\nfalse\n`). + +### `examples/fieldtest/eqord_3_newton_sqrt.ail` — Newton's method via float_lt / float_eq + +- **What it does:** Newton-Raphson iteration `x_{k+1} = (x_k + n/x_k) / 2` + to compute sqrt. Convergence loop guards on + `(app float_lt (app fabs (app - xnew x)) tol)`; pathological-zero + guard on `(app float_eq n 0.0)`. `fabs` implemented inline as + `if (app float_lt x 0.0) then -x else x`. +- **Why it fits:** Axis 3 north-star. Demonstrates the LLM-natural + shape of the Float-comparison named-fn family in numerical code. + Mirrors how Rust/Python/Swift guide users toward bespoke Float-aware + methods (`f64::abs`, `math.isclose`). +- **Outcome:** compiles, runs, matches expected stdout + (`2.0\n3.16228\n0.0\n1.0\n`). The Show Float rendering of + `3.16228` is libc-`%g`-shaped per `float-semantics.md` (the exact + IEEE-correct value 3.1622776601683795 truncates in the default + Show width). Acceptable. + +### `examples/fieldtest/eqord_4_float_ord_must_fail.ail` — Ord at Float rejection + +- **What it does:** single-statement program + `(app print (if (app lt 1.5 2.5) 1 0))`. Must fail at `ail check`. +- **Why it fits:** Axis 4 north-star. Verifies the diagnostic that + steers an LLM-author from the polymorphic `lt` (an Ord-class free + helper) toward the named-fn `float_lt` when the inferred operand + type is Float. +- **Outcome:** `ail check` exits 1 with stderr: + ``` + error: [no-instance] main: fn `main` calls `compare` requiring + `instance prelude.Ord Float`, but no such instance exists in the + workspace — Float has no Eq/Ord instance by design (partial + orderability per IEEE-754); use float_eq / float_lt (and siblings + float_ne / float_le / float_gt / float_ge) for explicit IEEE-aware + comparison. See design/contracts/float-semantics.md. + ``` + +### `examples/fieldtest/eqord_5_float_eq_must_fail.ail` — Eq at Float rejection (companion) + +- **What it does:** single-statement program + `(app print (if (app eq 1.5 1.5) 1 0))`. Must fail at `ail check`. +- **Why it fits:** Axis 4 companion. Verifies the Eq-class half of the + Float diagnostic. +- **Outcome:** `ail check` exits 1 with stderr substituting `Eq` for + `Ord` and `eq` for `compare`; rest of the addendum identical. + +## Findings + +### [working] Primitive Eq/Ord at Int/Bool/Str/Unit is friction-free + +- **Example(s):** eqord_1_fizzbuzz (Int eq, Str eq, Int gt), + eqord_2_rational_eq (Int eq inside ADT-instance body). +- **What happened:** every `(app eq …)` and `(app gt …)` call I + wrote compiled on first try, lowered correctly, and produced the + expected output. No friction in the surface shape, no diagnostic + needed. +- **Why it's `working`:** the milestone's central thesis (class-dispatch + is the surface for all comparison) holds — there is no second + thought during authoring about which spelling to use, and no + ambiguity about which primitive instance dispatches. The FizzBuzz + fixture is the natural form an LLM would emit on the prompt + "write FizzBuzz in AILang". +- **Recommended downstream action:** carry-on. Worth keeping the + fixtures around as regression protection against any future + re-introduction of operator-name surface. + +### [working] User-ADT Eq with nested primitive eq calls Just Works + +- **Example(s):** eqord_2_rational_eq. +- **What happened:** the `instance prelude.Eq Rational` body wrote + itself naturally — match both operands, cross-multiply, compare + with inner `(app eq …)` on Int. No coercion ceremony, no manual + qualifier on the inner call (the inner `eq` resolves through the + same class-dispatch as the outer, just at a different inferred + type). The end-to-end run produced the correct cross-multiplication + results. +- **Why it's `working`:** this is the milestone's clause-1 evidence — + the form was structurally impossible before the milestone (the old + built-in `==` rejected user ADTs at codegen with a generic error; + even after writing `instance Eq Point`, the inner `(app eq a1 a2)` + on Int would route via the dead polymorphic-`==` path with no + visible gain). Post-milestone, the LLM-author's mental model + ("classes do equality") matches the implementation surface 1:1. +- **Recommended downstream action:** carry-on. + +### [working] Float-comparison named-fn surface is LLM-natural + +- **Example(s):** eqord_3_newton_sqrt. +- **What happened:** writing `(app float_lt x 0.0)`, `(app float_eq n 0.0)`, + and `(app float_lt (app fabs …) tol)` felt entirely natural while + composing the Newton iteration. The named-fn surface is no more + verbose than the deleted operator surface (`(app < x 0.0)` was three + tokens, `(app float_lt x 0.0)` is three tokens), and the explicit + `float_` prefix is an active reminder during authoring that this is + an IEEE-partial operation rather than a structural-equality one. +- **Why it's `working`:** the spec's clause-3 framing — "the + NaN-comparison anti-pattern stays visible in code as `float_eq` + rather than hiding behind `eq`" — held up in practice. Newton's + method is exactly the kind of numerical code where mistaking + Float-eq for structural-eq would cause real bugs; the explicit + spelling made me pause and think about whether `float_eq n 0.0` was + the right zero-test (it is, because `-0.0 == 0.0` per IEEE, which + is the correct guard). +- **Recommended downstream action:** carry-on. + +### [working] NoInstance Eq/Ord Float diagnostic is informative and actionable + +- **Example(s):** eqord_4_float_ord_must_fail, eqord_5_float_eq_must_fail. +- **What happened:** both `ail check` invocations exit 1; both + diagnostics name the right class (`Eq` vs `Ord`), the right method + call site (`fn main calls eq` / `calls compare` — note the Ord + helper `lt` is reported via its desugar to `compare`), the named-fn + family `float_eq / float_lt (and siblings …)`, the IEEE-754 design + rationale, and the contract path + `design/contracts/float-semantics.md`. An LLM-author who hits this + diagnostic learns the entire replacement surface in one read. +- **Why it's `working`:** this is the milestone's clause-2 evidence — + the diagnostic carries enough information for an LLM that has only + the stderr to converge on the right call site without re-reading + the spec. Acceptance-criterion #3 ("Float-aware hint pointing at + `float_eq`") is comfortably met. +- **Recommended downstream action:** carry-on. The diagnostic is + the load-bearing surface for clean-break removal of the operator + names; protect it with the existing `eq_float_noinstance.rs` test. + +### [spec_gap] Spec's own example program uses bare `(class Eq)` but the language requires `(class prelude.Eq)` + +- **Example(s):** confirmed by a /tmp probe; my own + `eqord_2_rational_eq.ail` writes `(class prelude.Eq)` because I + copied the pattern from the existing `eq_ord_user_adt.ail`, not + from the spec. +- **What happened:** the design spec at + `docs/specs/2026-05-20-operator-routing-eq-ord.md:113` writes + `(class Eq)` (bare) in the §"Concrete code shapes" north-star + example program. An LLM-author who copies that pattern verbatim + hits the diagnostic: + ``` + error: [bare-cross-module-class-ref] module `…` contains bare class + name `Eq` that does not resolve to a local class; candidates from + imports: ["prelude.Eq"] + ``` + The diagnostic is excellent (lists the qualified candidate), but + the spec primed the wrong pattern. +- **Why it's `spec_gap`:** the milestone spec is the primary + reference for the milestone-defining surface; if the spec's own + example doesn't typecheck verbatim, then either the spec is wrong + (most likely) or bare class names are a feature the language should + in fact support (unlikely — qualified is the established style per + every existing fixture). The honest action is to update the spec's + example to use `(class prelude.Eq)`. This is one-line of doc + drift, but it is the highest-information reference an LLM-author + consults when picking up the milestone surface. +- **Recommended downstream action:** tighten the design ledger — fix + the example in `docs/specs/2026-05-20-operator-routing-eq-ord.md` + (lines 109-133) to use `(class prelude.Eq)`, and consider whether + the same drift exists in `design/contracts/prelude-classes.md` or + `design/models/typeclasses.md`. A single forward-fix doc commit. + +### [friction] `(app compare …)` at Float diagnostic does not acknowledge there is no `float_compare` + +- **Example(s):** /tmp probe writing + `(app compare 1.5 2.5)` inside a match-on-Ordering. +- **What happened:** the diagnostic is identical to the `(app lt …)` + diagnostic — names `float_eq / float_lt (and siblings …)`. None of + the suggested replacements give the three-way LT/EQ/GT result that + `compare` returns. An LLM-author who specifically reached for + `compare` because they want to drive an `Ordering`-match on Float + reads this diagnostic and is left guessing whether they should + pattern on `float_lt` + `float_eq` themselves to reconstruct the + three-way decision, or whether some other surface exists. +- **Why it's `friction`:** the spec at lines 433-436 acknowledged + this case explicitly ("`compare`/`Ord` use case names `float_lt` / + `float_compare` (the latter doesn't ship as a fn …) — so the hint + says 'use float_lt / float_eq for explicit IEEE-aware comparison'"). + So the absence of `float_compare` is deliberate. But the + diagnostic doesn't tell the author *that* — it just lists the + replacements without explaining the gap. A one-line addendum + ("note: there is no `float_compare` because IEEE-754 ordering is + partial; build the three-way decision from `float_lt` + `float_eq` + if you need it") would close the gap without changing any code + path. +- **Recommended downstream action:** plan a tidy iteration that + extends the float-aware diagnostic to differentiate on the called + method — when the call site is `compare`, append the + "no float_compare exists, build it from float_lt + float_eq" + sentence. Scoped to one branch in the diagnostic addendum, no + contract change. + +## Recommendation summary + +| Finding | Class | Action | +|---|---|---| +| Primitive Eq/Ord at Int/Bool/Str/Unit friction-free | working | carry-on | +| User-ADT Eq with nested primitive eq Just Works | working | carry-on | +| Float-comparison named-fn surface is LLM-natural | working | carry-on | +| NoInstance Eq/Ord Float diagnostic is informative | working | carry-on | +| Spec example uses bare `(class Eq)` but language needs `(class prelude.Eq)` | spec_gap | tighten the design ledger (doc fix) | +| `(app compare …)` at Float diagnostic doesn't name the missing `float_compare` | friction | plan a tidy iteration (diagnostic addendum) | diff --git a/examples/fieldtest/eqord_1_fizzbuzz.ail b/examples/fieldtest/eqord_1_fizzbuzz.ail new file mode 100644 index 0000000..73e1e33 --- /dev/null +++ b/examples/fieldtest/eqord_1_fizzbuzz.ail @@ -0,0 +1,73 @@ +; Fieldtest fixture — Axis 1: equality on primitive Int via `(app eq …)`. +; +; FizzBuzz over [1..15]: +; if n % 15 == 0 print "FizzBuzz" +; else if n % 3 == 0 print "Fizz" +; else if n % 5 == 0 print "Buzz" +; else print (show n) +; +; Equality dispatches through prelude.Eq.eq at Int (intercept arm +; eq__Int → `icmp eq i64`). Demonstrates the LLM-natural shape of +; `(app eq …)` on the primitive type that dominates most numerical +; code. +; +; Expected stdout (one per line): +; 1 +; 2 +; Fizz +; 4 +; Buzz +; Fizz +; 7 +; 8 +; Fizz +; Buzz +; 11 +; Fizz +; 13 +; 14 +; FizzBuzz + +(module eqord_1_fizzbuzz + + (fn classify + (doc "Return the FizzBuzz label for n, or the empty string if n is a plain number.") + (type + (fn-type + (params (con Int)) + (ret (con Str)))) + (params n) + (body + (if (app eq (app % n 15) 0) + "FizzBuzz" + (if (app eq (app % n 3) 0) + "Fizz" + (if (app eq (app % n 5) 0) + "Buzz" + ""))))) + + (fn emit_one + (doc "Print the FizzBuzz label or the number itself.") + (type (fn-type (params (con Int)) (ret (con Unit)) (effects IO))) + (params n) + (body + (let label (app classify n) + (if (app eq label "") + (app print n) + (app print label))))) + + (fn loop + (doc "Tail-recursive driver over [i..stop].") + (type (fn-type (params (con Int) (con Int)) (ret (con Unit)) (effects IO))) + (params i stop) + (body + (if (app gt i stop) + (lit-unit) + (seq + (app emit_one i) + (tail-app loop (app + i 1) stop))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (app loop 1 15)))) diff --git a/examples/fieldtest/eqord_2_rational_eq.ail b/examples/fieldtest/eqord_2_rational_eq.ail new file mode 100644 index 0000000..94254a1 --- /dev/null +++ b/examples/fieldtest/eqord_2_rational_eq.ail @@ -0,0 +1,56 @@ +; Fieldtest fixture — Axis 2: user-ADT Eq instance, hand-written. +; +; Rational numbers compared by cross-multiplication: +; a/b == c/d iff a*d == b*c +; (assumes positive denominators; the constructor enforces it.) +; +; The interesting bit for the milestone is the *nested* equality call +; inside the user instance body: the inner `(app eq (app * a d) (app * b c))` +; dispatches to prelude.eq__Int (the primitive instance, intercept- +; lowered to `icmp eq i64`), while the outer `(app eq r1 r2)` from main +; dispatches to this module's own `eq__Rational`. End-to-end the chain +; is: user-instance method → prelude class method → primitive intercept. +; +; Expected stdout (one per line): +; true ; 1/2 == 2/4 +; false ; 1/2 == 1/3 +; true ; 3/4 == 6/8 +; false ; 5/6 == 4/5 + +(module eqord_2_rational_eq + + (data Rational + (doc "Numerator + (positive) denominator. No normalisation.") + (ctor MkRational (con Int) (con Int))) + + (instance + (class prelude.Eq) + (type (con Rational)) + (doc "Cross-multiplication equality. Inner eq dispatches to prelude.eq__Int.") + (method eq + (body + (lam + (params (typed r1 (con Rational)) (typed r2 (con Rational))) + (ret (con Bool)) + (body + (match r1 + (case (pat-ctor MkRational a b) + (match r2 + (case (pat-ctor MkRational c d) + (app eq (app * a d) (app * b c))))))))))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let r_1_2 (term-ctor Rational MkRational 1 2) + (let r_2_4 (term-ctor Rational MkRational 2 4) + (let r_1_3 (term-ctor Rational MkRational 1 3) + (let r_3_4 (term-ctor Rational MkRational 3 4) + (let r_6_8 (term-ctor Rational MkRational 6 8) + (let r_5_6 (term-ctor Rational MkRational 5 6) + (let r_4_5 (term-ctor Rational MkRational 4 5) + (seq (app print (app eq r_1_2 r_2_4)) + (seq (app print (app eq r_1_2 r_1_3)) + (seq (app print (app eq r_3_4 r_6_8)) + (app print (app eq r_5_6 r_4_5))))))))))))))) diff --git a/examples/fieldtest/eqord_3_newton_sqrt.ail b/examples/fieldtest/eqord_3_newton_sqrt.ail new file mode 100644 index 0000000..62bdb4a --- /dev/null +++ b/examples/fieldtest/eqord_3_newton_sqrt.ail @@ -0,0 +1,61 @@ +; Fieldtest fixture — Axis 3: Float comparison via the named-fn surface. +; +; Newton's method for sqrt: iterate x_{k+1} = (x_k + n/x_k) / 2 until +; |x_{k+1} - x_k| < tol +; Reaches for `float_lt` (loop convergence) and `float_eq` (zero-arg +; guard against pathological 0.0 input). Also exercises Float +; arithmetic + Show Float via `print`. +; +; The interesting bit for the milestone is that there is no +; polymorphic `eq` / `lt` at Float — those would fail at typecheck +; with `NoInstance Eq Float`. The LLM-author has to reach for the +; named family `float_eq` / `float_lt` / `float_gt`. The shape mirrors +; how Rust's `f64::abs` / partial_cmp guides users toward bespoke +; Float-aware methods. +; +; abs implemented inline as `if x < 0 then -x else x` using float_lt. +; +; Expected stdout (one per line): +; 2 (sqrt 4.0) ; 2.0 +; ~3.16 (sqrt 10.0) ; 3.1622776601683795 — exact IEEE +; 0 (sqrt 0.0) ; 0.0, short-circuit +; 1 (sqrt 1.0) ; 1.0 + +(module eqord_3_newton_sqrt + + (fn fabs + (doc "Float absolute value via the named-fn comparison surface.") + (type (fn-type (params (con Float)) (ret (con Float)))) + (params x) + (body + (if (app float_lt x 0.0) + (app - 0.0 x) + x))) + + (fn iterate + (doc "Tail-recursive Newton iteration. Stops when |xnew - x| < tol.") + (type (fn-type (params (con Float) (con Float) (con Float)) (ret (con Float)))) + (params n x tol) + (body + (let xnew (app / (app + x (app / n x)) 2.0) + (if (app float_lt (app fabs (app - xnew x)) tol) + xnew + (tail-app iterate n xnew tol))))) + + (fn sqrt + (doc "sqrt n via Newton with initial guess 1.0 and tolerance 1e-10. Returns 0.0 for n == 0.0; assumes n >= 0.") + (type (fn-type (params (con Float)) (ret (con Float)))) + (params n) + (body + (if (app float_eq n 0.0) + 0.0 + (app iterate n 1.0 0.0000000001)))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (app print (app sqrt 4.0)) + (seq (app print (app sqrt 10.0)) + (seq (app print (app sqrt 0.0)) + (app print (app sqrt 1.0)))))))) diff --git a/examples/fieldtest/eqord_4_float_ord_must_fail.ail b/examples/fieldtest/eqord_4_float_ord_must_fail.ail new file mode 100644 index 0000000..0f7a634 --- /dev/null +++ b/examples/fieldtest/eqord_4_float_ord_must_fail.ail @@ -0,0 +1,23 @@ +; Fieldtest fixture — Axis 4: rejection diagnostic for Ord at Float. +; +; This fixture is the discriminator for whether the post-milestone +; NoInstance diagnostic steers an LLM-author who reached for a +; polymorphic Ord-helper at Float toward the `float_lt` named-fn +; replacement. +; +; Today (per spec §Error handling) the diagnostic at Eq Float says +; "use float_eq for explicit IEEE-aware comparison" +; The spec also promises the Ord variant says +; "use float_lt / float_eq for explicit IEEE-aware comparison" +; so an LLM-author seeing this fail learns the named-fn surface +; without needing to read the prelude. +; +; Expected behaviour: `ail check` exits non-zero. stderr contains: +; - NoInstance Ord Float (or similar Ord-at-Float wording) +; - the literal string `float_lt` somewhere in the addendum + +(module eqord_4_float_ord_must_fail + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (app print (if (app lt 1.5 2.5) 1 0))))) diff --git a/examples/fieldtest/eqord_5_float_eq_must_fail.ail b/examples/fieldtest/eqord_5_float_eq_must_fail.ail new file mode 100644 index 0000000..b00d2b3 --- /dev/null +++ b/examples/fieldtest/eqord_5_float_eq_must_fail.ail @@ -0,0 +1,16 @@ +; Fieldtest fixture — Axis 4 companion: rejection diagnostic for Eq at Float. +; +; Twin of eqord_4_float_ord_must_fail.ail for the Eq variant. +; Verifies the diagnostic produced when an LLM-author tries the +; polymorphic `eq` at Float — what the milestone spec calls the +; Klausel-3 discriminator. +; +; Expected behaviour: `ail check` exits non-zero. stderr contains: +; - `NoInstance` mention of `Eq` and `Float` +; - the literal string `float_eq` somewhere in the addendum + +(module eqord_5_float_eq_must_fail + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (app print (if (app eq 1.5 1.5) 1 0)))))