AILang/docs/specs/0049-operator-routing-eq-ord.md

Operator routing through Eq / Ord — Design Spec

Date: 2026-05-20 Status: Draft — awaiting user spec review Authors: Brummel (orchestrator) + Claude

Resolves Gitea #1. Realises the "P2 follow-up" called out in examples/prelude.ail:9 — routing the surface comparator names through the prelude.Eq / prelude.Ord classes instead of the hard-coded built-in comparator table.

Goal

Today AILang has two parallel paths for comparison:

• Built-in operators ==, !=, <, <=, >, >= — special- cased in codegen with hardcoded polymorphism over fixed primitive type sets (== over {Int, Bool, Str, Unit, Float}; the other five over {Int, Float}). User ADTs are rejected at codegen with a generic error.
• Typeclass methods prelude.Eq.eq and prelude.Ord.compare with instances for {Int, Bool, Str}, plus the polymorphic free- fn helpers ne/lt/le/gt/ge. Float and Unit have no Eq/Ord instance by design (Float: partial orderability per float-semantics; Unit: oversight that today's (app == () ()) builtin path hides).

The two paths are redundant — instance Eq Int body literally calls (app == x y), so the class layer today delegates back to the builtin. The redundancy is structurally observable: every release pays the cost of maintaining both. User ADTs cannot participate in == at all, even when the LLM-author has written instance Eq Point — the operator is sealed at the primitive types.

After this milestone, the LLM-author writes (app eq p1 p2) for user types and gets the natural typeclass-dispatched behaviour; ==/!=/</<=/>/>= as identifiers are gone from the language; Float comparison is named explicitly via float_eq / float_lt / etc. (no IEEE-NaN-bug-class smuggled in via a polymorphic eq).

Architecture

Three layers shift in lockstep:

Surface / parser: unchanged. The Form-A tokens == / != / < / <= / > / >= remain legal identifier strings at the parser level — there is no syntactic change. They are simply not recognised at typecheck or codegen.

Typechecker: the entries for == / != / < / <= / > / >= in the builtin signature table (crates/ailang-check/src/builtins.rs::install — comparator loop at lines 96-98, polymorphic == Forall block at lines 109-125, list-side mirror at lines 303-308) are removed. Surface use of these names resolves like any other unknown identifier — first via the class-method-dispatch index per method-dispatch, which finds no candidate (the method name is eq, not ==), then via fn lookup, which also finds none, then fails with the standard unknown variable diagnostic. The diagnostic does NOT special-case the comparator names with a "did you mean eq?" hint — the milestone is a clean break, not a transition aid; AILang has no external users requiring migration.

All (app eq …) / (app compare …) / (app ne …) / (app lt …) / etc. resolve through the existing class-method-dispatch machinery documented in method-dispatch. No new dispatch rule.

Codegen: try_emit_primitive_instance_body in crates/ailang-codegen/src/lib.rs (the intercept already used for eq__Str, compare__Int, compare__Bool, compare__Str) gains three new arms — eq__Int, eq__Bool, eq__Unit. Every primitive instance body emitted via this intercept carries an alwaysinline attribute on the generated LLVM function so the -O0 build path collapses the trivial body to its single icmp/fcmp/call instruction at every use site, matching today's direct-emit IR shape under -O0 as well as -O2.

Six new prelude free functions ship for Float comparison: float_eq, float_ne, float_lt, float_le, float_gt, float_ge, each Float -> Float -> Bool without a class constraint. Their bodies are intercept-lowered to the corresponding fcmp instruction (oeq / une / olt / ole / ogt / oge), preserving the bit-exact IEEE semantics float-semantics guarantees today for == / < etc. on Float — the guarantee is transferred from the deleted operator names to the named Float fns.

The lit-pattern desugar in crates/ailang-core/src/desugar.rs::build_eq (line 1099) rewrites (pat-lit "hi") to (if (eq sv "hi") body fall_k) instead of the current (if (== sv "hi") body fall_k) — the literal symbol Term::Var { name: "==" } at line 1109 becomes name: "eq". This is the single live ==-emitting desugar site; everything else mechanically migrates as fixture or test-scaffold work, not as desugar-pass changes. This is the non-obvious mechanical follow: lit patterns inherit equality dispatch by construction.

Concrete code shapes

The LLM-author program this milestone enables

(module eq_user_adt_smoke
  (data Point
    (ctor Point (con Int) (con Int)))
  (instance
    (class prelude.Eq)
    (type (con Point))
    (method eq
      (body (lam (params (typed p1 (con Point)) (typed p2 (con Point))) (ret (con Bool))
        (body (match p1
          (case (pat-ctor Point a1 b1)
            (match p2
              (case (pat-ctor Point a2 b2)
                (if (app eq a1 a2)
                    (app eq b1 b2)
                    false))))))))))
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (let p1 (term-ctor Point 1 2)
      (let p2 (term-ctor Point 1 2)
      (let p3 (term-ctor Point 1 3)
        (seq (app print (app eq p1 p2))
             (app print (app eq p1 p3)))))))))

Expected stdout: true\nfalse\n. This is the feature-acceptance clause-1 evidence: the LLM-natural form that is structurally impossible to write today. Today (app == p1 p2) is rejected at codegen (Point is not in the polymorphic == type set); (app eq p1 p2) fires NoInstance Eq Point even after the author writes the instance, because the body's nested (app eq a1 a2) on Int delegates to (app == x y) which then has to thread back via the polymorphic-== mechanism — the chain works but the author gets the same outcome as writing == directly, no gain.

After this milestone, both the outer (app eq p1 p2) and the nested (app eq a1 a2) resolve via the canonical class-dispatch path: the outer to eq_user_adt_smoke.eq__Point (the user instance), the nested to prelude.eq__Int (the primitive instance, intercept-lowered to icmp eq i64 and inlined back to the call site).

The Klausel-3 discriminator (must fail at typecheck)

(module eq_float_must_fail
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body (app print (app eq 1.5 1.5)))))

Must produce a typecheck-time diagnostic — NoInstance Eq Float with a follow-up sentence Float has no Eq instance by design (partial orderability per design/contracts/0005-float-semantics.md); use float_eq for explicit IEEE-aware comparison. The diagnostic is the existing NoInstance channel; the Float-aware addendum is the existing Float-specific hint in crates/ailang-check/src/lib.rs around line 860 (which already special-cases Eq/Ord-at-Float diagnostics), extended to name float_eq / float_lt as the explicit alternative.

The Float-with-named-fn happy path

(module float_compare_smoke
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (seq (app print (app float_eq 1.5 1.5))
      (seq (app print (app float_lt 1.0 2.0))
           (app print (app float_eq 1.0 0.0)))))))

Expected stdout: true\ntrue\nfalse\n. Demonstrates that Float comparison remains available via the named-fn route. The implementation lowers each float_* call to a single fcmp instruction via the intercept mechanism — IR-byte-equivalent to today's (app == 1.5 1.5) after the operator name is removed.

Migration pattern for existing fixtures

; examples/eq_demo.ail (current)
(seq (app print (app == 5 5))
(seq (app print (app == true false))
     (app print (app == "hi" "hi"))))

; examples/eq_demo.ail (after this milestone)
(seq (app print (app eq 5 5))
(seq (app print (app eq true false))
     (app print (app eq "hi" "hi"))))

≈10 fixtures under examples/ use one or more of the deleted operator names. Each migrates to the corresponding class-method or named-fn (Float case): == → eq, != → ne, < → lt, <= → le, > → gt, >= → ge. The Float-operator uses in bench_compute_collatz.ail (and any other Float-touching bench fixture) migrate to float_lt / float_eq / etc. The exact fixture list is enumerated by the planner via grep -rln '(app == \|(app != \|(app < \|(app <= \|(app > \|(app >=' examples/.

Implementation shape (secondary — supporting detail)

The load-bearing code changes (planner derives exact paths/line numbers; this section establishes shape):

crates/ailang-codegen/src/synth.rs::builtin_binop_typed — the comparator arms vanish:

// Before — 10 arms for ==/!=/</<=/>/>= over Int+Float
match (name, is_int, is_float) {
    ("+", true, _) => Some(("add", "i64", "i64")),
    ("+", _, true) => Some(("fadd", "double", "double")),
    // ... arithmetic ...
    ("!=", true, _) => Some(("icmp ne", "i64", "i1")),
    ("<",  true, _) => Some(("icmp slt", "i64", "i1")),
    ("<=", true, _) => Some(("icmp sle", "i64", "i1")),
    (">",  true, _) => Some(("icmp sgt", "i64", "i1")),
    (">=", true, _) => Some(("icmp sge", "i64", "i1")),
    ("!=", _, true) => Some(("fcmp une", "double", "i1")),
    ("<",  _, true) => Some(("fcmp olt", "double", "i1")),
    ("<=", _, true) => Some(("fcmp ole", "double", "i1")),
    (">",  _, true) => Some(("fcmp ogt", "double", "i1")),
    (">=", _, true) => Some(("fcmp oge", "double", "i1")),
    _ => None,
}

// After — arithmetic only
match (name, is_int, is_float) {
    ("+", true, _) => Some(("add", "i64", "i64")),
    ("+", _, true) => Some(("fadd", "double", "double")),
    ("-", true, _) => Some(("sub", "i64", "i64")),
    ("-", _, true) => Some(("fsub", "double", "double")),
    ("*", true, _) => Some(("mul", "i64", "i64")),
    ("*", _, true) => Some(("fmul", "double", "double")),
    ("/", true, _) => Some(("sdiv", "i64", "i64")),
    ("/", _, true) => Some(("fdiv", "double", "double")),
    ("%", true, _) => Some(("srem", "i64", "i64")),
    _ => None,
}

crates/ailang-codegen/src/lib.rs — the ==-polymorphic-dispatch special case (lib.rs around 2947 plus the Int/Bool/Str/Unit matching) is gone; replaced by try_emit_primitive_instance_body arms for the new symbol set:

// New arms in try_emit_primitive_instance_body's match
match instance_key {
    "eq__Int"  => emit_icmp_eq("i64"),     // new
    "eq__Bool" => emit_icmp_eq("i1"),      // new
    "eq__Unit" => emit_const_i1_true(),    // new
    "eq__Str"  => /* existing — @ail_str_eq */,
    "compare__Int" | "compare__Bool" | "compare__Str" => /* existing */,
    // 6 new Float-named-fn arms
    "float_eq" => emit_fcmp("oeq", "double"),
    "float_ne" => emit_fcmp("une", "double"),
    "float_lt" => emit_fcmp("olt", "double"),
    "float_le" => emit_fcmp("ole", "double"),
    "float_gt" => emit_fcmp("ogt", "double"),
    "float_ge" => emit_fcmp("oge", "double"),
    _ => return None,
}

Each emit_* helper adds attributes #N = { alwaysinline … } to the generated function header so the -O0 build path inlines the single-instruction body at every call site, matching today's direct-emit shape.

examples/prelude.ail — three additions, three rewrites:

; New: Eq Unit instance (preserves today's `==`-on-Unit capability).
(instance
  (class Eq)
  (type (con Unit))
  (doc "Eq Unit. Body is constant true — Unit is single-inhabitant
        so all values compare equal. Lowered via
        try_emit_primitive_instance_body::eq__Unit to `ret i1 1`.")
  (method eq
    (body (lam (params (typed x a) (typed y a)) (ret (con Bool))
            (body true)))))

; Eq Int — body becomes a placeholder (lambda returning false);
; codegen intercept overrides to icmp eq i64. Matches Ord Int's
; existing placeholder pattern.
(instance
  (class Eq)
  (type (con Int))
  (doc "Eq Int. Body is placeholder for round-trip stability;
        codegen intercept emits `icmp eq i64` with alwaysinline.")
  (method eq
    (body (lam (params (typed x a) (typed y a)) (ret (con Bool))
            (body false)))))

; Eq Bool — same placeholder shape.
; Eq Str — body unchanged in shape (already placeholder-style),
;   intercept already exists.

; New Float-fns: six entries.
(fn float_eq
  (doc "IEEE-aware Float equality. `float_eq x y` returns true iff
        both operands are non-NaN and bit-equal. Lowered to
        `fcmp oeq double`. Replaces the milestone-deleted `(app == x y)`
        on Float.")
  (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
  (params x y)
  (body (lam (params (typed x (con Float)) (typed y (con Float))) (ret (con Bool))
          (body false))))
; ... float_ne / float_lt / float_le / float_gt / float_ge analogous.

; Line-9 comment on `class Eq` (the "P2 follow-up" note) is removed —
; routing-through-Eq.eq is no longer follow-up, it's the present.

Components

The milestone touches seven layers, all in one cohesive iter:

1. Typechecker builtin table (crates/ailang-check/src/builtins.rs) — six operator-name entries removed (install lines 96-98 + 109-125); list-side mirror at lines 303-308 trimmed; the in- source mod tests helpers eq_app and the polymorphic-== regression tests (lib.rs:6092, lib.rs:6220 — both inside #[cfg(test)]) migrate to the eq symbol so the test suite stays green over the new dispatch path.

2. Codegen builtin binop table (crates/ailang-codegen/src/synth.rs) — ten comparator arms removed from builtin_binop_typed; the table reduces to the arithmetic core.

3. Codegen primitive-instance intercept (crates/ailang-codegen/src/lib.rs) — try_emit_primitive_instance_body gains three Eq arms (eq__Int, eq__Bool, eq__Unit) and six Float-fn arms (float_eq/float_ne/float_lt/float_le/float_gt/ float_ge); each generated function header carries alwaysinline. The existing ==-polymorphic-dispatch lowering (lib.rs around 2947, the Int/Bool/Str/Unit/Float matching for ==) is deleted.

4. Lit-pattern desugar (crates/ailang-core/src/desugar.rs) — build_eq (line 1099) substitutes eq for == in the generated (if … body fall_k) form. This is the only live desugar-pass change. Float-pattern rejection per float-semantics.md is unaffected (still hard-rejected at typecheck, before desugar runs).

   In-source test scaffolds in the same file (desugar.rs:2414, inside #[cfg(test)] mod tests) and in crates/ailang-check/src/lib.rs (lines 6092 and 6220, also #[cfg(test)]) construct hand-built Term::Var { name: "==" } in AST literals to drive ==-specific assertions; these migrate to name: "eq" alongside the production change. Counted as test-scaffold migration, not desugar-pass work.

5. Prelude module (examples/prelude.ail) — adds instance Eq Unit; rewrites Eq Int / Eq Bool bodies to placeholder pattern (codegen intercept does the work); adds six float_* free fns; removes the "P2 follow-up" comment on class Eq. Prelude module hash will shift; the hash pin in crates/ailang-surface/tests/prelude_module_hash_pin.rs regenerates as part of the iter.

6. Fixture migration — ≈10 files under examples/ rewritten from operator-form to method-form. The planner enumerates the exact set via grep and assigns it as a discrete task.

7. Contracts — three updates:

   • design/contracts/0005-float-semantics.md lines 10-14: the guarantees about +/-/etc. and ==/</!= lowering to single LLVM instructions are retained for arithmetic but transferred from ==/</!= to float_eq/float_lt/float_ne/etc. for the comparison set. The NaN-spelling caveat is unchanged.
   • design/contracts/0017-prelude-classes.md: instance list extends with Eq Unit; a new paragraph documents the six float_* fns as the Float-comparison surface; the Float-no-Eq/Ord clause gains a → use float_eq cross-reference.
   • design/contracts/0013-typeclasses.md: no change. Class schema, dispatch rule, and diagnostics are stable; the milestone only activates existing machinery for eq/compare over more types.

Data flow

A surface (app eq p1 p2) flows through the existing pipeline:

1. Parse — Term::App { fn: Var "eq", args: [p1, p2] }. No change from today.
2. Typecheck — class-method-dispatch (per design/contracts/0016-method-dispatch.md) consults method_to_candidate_classes["eq"] → {prelude.Eq}. Singleton class survivor; type-driven filter against the workspace registry for the resolved type:
   • p1, p2 : Int → prelude.eq__Int
   • p1, p2 : Point → eq_user_adt_smoke.eq__Point
   • p1, p2 : Float → no instance → NoInstance Eq Float with Float-aware hint pointing at float_eq.
3. Mono — synth produces the instance-body symbol (existing pass; per design/contracts/0013-typeclasses.md invariants 1-3).
4. Codegen — emits a call to the resolved instance fn. For primitive instances, the body is intercept-lowered to a single icmp/fcmp/call; alwaysinline attribute ensures the call folds at every use site under -O0 as well as -O2. For user-ADT instances, codegen emits the full lambda body normally; the call to the instance fn is normal (no intercept).

The data-flow is conceptually identical to today's show / compare paths — the milestone unifies eq into the same shape.

Error handling

Three diagnostic situations:

NoInstance Eq Float / NoInstance Ord Float — fires at typecheck for any (app eq …) or (app compare …) (or ne/lt/le/gt/ge) on Float. The existing Float-aware addendum (lib.rs:860-873) is extended:

Eq has no instance at Float — Float has no Eq/Ord instance by
design (partial orderability per design/contracts/0005-float-semantics.md);
use float_eq for explicit IEEE-aware comparison.

compare/Ord use case names float_lt / float_compare (the latter doesn't ship as a fn — compare returns Ordering, no Float equivalent — so the hint says "use float_lt / float_eq for explicit IEEE-aware comparison").

NoInstance Eq <UserType> — fires when the LLM-author calls (app eq p1 p2) on a user type without having written the instance. Standard NoInstance channel; no special-case wording. The author writes instance Eq <UserType> by hand (no deriving).

unknown variable: == (et al.) — fires when the LLM-author writes (app == 5 5) after the milestone. The diagnostic does NOT carry a "did you mean eq?" hint. This is a clean break, not a transition; AILang has no external users to migrate. The lack of hint is documented in the prelude-classes.md contract update ("comparator-operator names are not part of the language").

Testing strategy

Five test artefacts, all in crates/ail/tests/:

1. eq_user_adt_smoke_e2e.rs — drives the north-star fixture examples/eq_user_adt_smoke.ail through ail build + binary execution; asserts stdout "true\nfalse\n". This is the milestone-defining E2E. Protects: user-ADT-Eq path works end-to- end, including cross-module reference from user-instance body to prelude.eq__Int.
2. eq_float_must_fail_pin.rs — drives the must-fail fixture examples/eq_float_must_fail.ail; asserts ail check exits non-zero with stderr containing NoInstance Eq Float AND float_eq. Protects: the Klausel-3 discriminator stays discriminative; Float-aware diagnostic stays informative.
3. float_compare_smoke_e2e.rs — drives the Float-named-fn fixture; asserts stdout "true\ntrue\nfalse\n". Protects: the six float_* fns lower correctly to fcmp; replacement surface for the deleted Float operators stays functional.
4. operator_names_unbound_pin.rs — drives a minimal fixture (app == 5 5); asserts ail check exits non-zero with stderr containing unknown variable: ==. Protects: the operator-name removal is durable; no codegen path silently re-introduces them.
5. prelude_eq_alwaysinline_ir_pin.rs — compiles (app eq 5 5) with --emit-ir --opt=O0; asserts the resulting IR contains either icmp eq i64 directly at the call site OR the alwaysinline attribute on @prelude_eq__Int such that the inliner is guaranteed to fold under -O2. Protects: the alwaysinline mitigation is wired (not silently dropped); the bench-gate risk is structurally bounded.

Plus: the bench corpus (latency + throughput + cross-lang) runs as the acceptance gate. The expectation is 0/0/0 regressions; if regressions appear, the alwaysinline-mitigation needs investigation (likely codegen-bug) or the spec needs revisiting toward α (call-site intercept).

Existing tests stay green by virtue of the fixture migration — every ==/</etc. in test fixtures is rewritten alongside the language change. The lit-pattern regression suite (if exists in crates/ailang-check/tests/ per planner-recon) exercises (case (pat-lit "hi") …) paths after the desugar rewrites to eq; these stay green provided the desugar is updated correctly.

Acceptance criteria

The milestone ships when all of the following hold:

1. cargo test --workspace --quiet — all binaries 0 failed.
2. examples/eq_user_adt_smoke.ail exists and builds and runs and prints "true\nfalse\n"; the corresponding E2E is green.
3. examples/eq_float_must_fail.ail exists and ail check rejects it with NoInstance Eq Float and a float_eq hint.
4. examples/float_compare_smoke.ail exists and runs and prints "true\ntrue\nfalse\n".
5. grep -rn '"=="\|"<"\|"<="\|">"\|">="\|"!="' crates/ailang-check/src/builtins.rs crates/ailang-codegen/src/synth.rs crates/ailang-codegen/src/lib.rs crates/ailang-core/src/desugar.rs returns matches only in comment / doc context, not as live env.globals.insert(...), Type::Var { name: "==" }, or Some((..., "...)) table entries. Documentation comments referring historically to the removed names are permitted only in commit-bodies and contract-history sections, not as live code paths.
6. grep -rln '(app == \|(app != \|(app < \|(app <= \|(app > \|(app >=' examples/ returns zero matches (full fixture migration complete).
7. examples/prelude.ail contains instance Eq Unit and the six float_* fns; the line-9 "P2 follow-up" comment on class Eq is removed.
8. bench/check.py exit 0; bench/compile_check.py exit 0; bench/cross_lang.py exit 0 (full bench-corpus green against the post-milestone baseline regenerated by the iter).
9. design/contracts/0005-float-semantics.md updated to name float_eq / float_lt / float_ne / etc. as the comparison guarantees (comparison guarantees on ==/</!= removed; arithmetic guarantees on +/-/*// unchanged).
10. design/contracts/0017-prelude-classes.md updated: Eq Unit in the instance list; new section on the six Float-named comparison fns; the Float-no-Eq/Ord clause carries a → use float_eq cross-reference.
11. Closes Gitea #1 via the iter-commit closes #1 trailer.

Out of scope (tracked separately):

• Deriving for Eq/Ord — typeclasses.md:177 "No deriving" stands. LLM-author writes instance bodies by hand. If deriving becomes a real friction point post-milestone, that is its own spec (likely tied to Gitea #2 "22c typeclass corpus expansion").
• Parameterised-ADT instances (instance Eq (List a), etc.) — requires multi-parameter-class / constraint-propagation infrastructure, part of Gitea #2.
• Eq / Ord for the Ordering ADT itself — no use case; Ordering is consumed via match, not compared.
• and / or as Builtins — north-star fixture uses (if … … false) for short-circuit conjunction. Adding and / or as separate fns or operators is a separate concern; no forcing here.