fieldtest: operator-routing-eq-ord — 5 examples, 6 findings (4 working, 1 friction, 1 spec_gap)
Post-audit field test of the operator-routing-eq-ord milestone (closed via5170b6a+4d45bc6). Five `.ail` Surface-form fixtures under `examples/fieldtest/` written by an LLM-author working strictly from the design/ ledger + public examples (no `crates/` / `runtime/` / `bench/` reads — Iron Law honoured): eqord_1_fizzbuzz.ail — FizzBuzz [1..15] via (app eq …) on Int+Str and (app gt …) on Int eqord_2_rational_eq.ail — data Rational + user-instance (class prelude.Eq) by cross-mult; inner Int-eq nested in instance body eqord_3_newton_sqrt.ail — Newton's method via float_lt (convergence + fabs) and float_eq (zero-guard) eqord_4_float_ord_must_fail.ail — (app lt 1.5 2.5) must reject at typecheck with float_lt hint eqord_5_float_eq_must_fail.ail — (app eq 1.5 1.5) must reject at typecheck with float_eq hint Findings: [working] x4 — primitive Eq/Ord at Int/Bool/Str/Unit; user-ADT Eq with nested primitive eq calls; Float named-fn surface (float_eq/float_lt/etc.); NoInstance Eq/Ord Float diagnostic with float_eq / float_lt addendum. The milestone's central thesis (class-dispatch is the only comparison surface; Float opts out via named fns) is LLM-natural — every (app eq …) / (app gt …) / (app float_lt …) call I wrote compiled on first try with no diagnostic friction. [spec_gap] x1 — `docs/specs/2026-05-20-operator-routing-eq-ord.md:113` north-star example writes bare `(class Eq)` where the language requires `(class prelude.Eq)`. An LLM-author who copies the spec verbatim hits `bare-cross-module-class-ref`. The milestone spec is the highest-information reference an LLM-author consults; the bare-vs-qualified drift mis-primes the pattern. Resolution: tighten-the-design-ledger — fix the spec example inline (separate follow-up commit). The existing `examples/eq_ord_user_adt.ail` already uses the qualified form, so the corpus is consistent; only the spec drifted. [friction] x1 — `(app compare 1.5 2.5)` at Float fires the same diagnostic as `(app lt …)` at Float, naming `float_eq / float_lt (and siblings)` as the alternative. But the alternatives don't return Ordering; an LLM-author who wanted three-way LT/EQ/GT can't satisfy that with float_lt + float_eq alone. The spec (lines 433-436) acknowledged this case in commentary — "no float_compare ships; build it from float_lt + float_eq if you need three-way" — but the diagnostic doesn't say so. Resolution: file as Gitea backlog issue for a follow-up tidy iteration (codegen-side: branch the Float-aware NoInstance addendum on the called method-name; the `compare` arm gets a one-sentence "no float_compare; build it from float_lt + float_eq if you need three-way" addendum). Status: clean — no bugs, no blockers, the milestone surface is solidly LLM-usable. Both non-working findings are tractable forward-fixes that don't disturb the milestone's core contracts. Spec: docs/specs/2026-05-21-fieldtest-operator-routing-eq-ord.md
This commit is contained in:
@@ -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))))
|
||||
@@ -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)))))))))))))))
|
||||
@@ -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))))))))
|
||||
@@ -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)))))
|
||||
@@ -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)))))
|
||||
Reference in New Issue
Block a user