diff --git a/docs/specs/2026-05-10-floats.md b/docs/specs/2026-05-10-floats.md index 194de51..b6dc1f7 100644 --- a/docs/specs/2026-05-10-floats.md +++ b/docs/specs/2026-05-10-floats.md @@ -101,54 +101,121 @@ Negative float literals follow today's negative-int rule digit as part of a numeric token), so `-1.5` lexes as a single `Tok::Float`. -### A3 — Builtin operators: no overloading, explicit f-prefix +### A3 — Builtin operators: polymorphic over `{Int, Float}` via codegen-dispatch -| Domain | Int (existing) | Float (new) | +The arithmetic and comparison operators that today are +monomorphic-Int (`+`, `-`, `*`, `/`, `<`, `<=`, `>`, `>=`) are +**widened to polymorphic** with the same shape and dispatch +mechanism the existing `==` / `!=` already use: + +``` ++ : forall a. (a, a) -> a -- Int|Float; reject otherwise +- : forall a. (a, a) -> a -- Int|Float +* : forall a. (a, a) -> a -- Int|Float +/ : forall a. (a, a) -> a -- Int|Float +< : forall a. (a, a) -> Bool -- Int|Float +<= : forall a. (a, a) -> Bool -- Int|Float +> : forall a. (a, a) -> Bool -- Int|Float +>= : forall a. (a, a) -> Bool -- Int|Float +== : forall a. (a, a) -> Bool -- existing; Float arm added +!= : forall a. (a, a) -> Bool -- existing; Float arm added +% : (Int, Int) -> Int -- stays monomorphic (no fmod yet) +``` + +Codegen dispatches on the resolved argument type at the call +site, parallel to today's `==` path (`crates/ailang-codegen/src/ +lib.rs:2244-2266`): + +| Op | Int arm | Float arm | |---|---|---| -| Arithmetic | `+ - * / %` | `fadd fsub fmul fdiv fneg` | -| Equality | `== !=` (polymorphic, codegen-dispatched) | (same — codegen arm extended) | -| Ordering | `< <= > >=` (Int-only) | `flt fle fgt fge` | +| `+` | `add i64` | `fadd double` | +| `-` | `sub i64` | `fsub double` | +| `*` | `mul i64` | `fmul double` | +| `/` | `sdiv i64` | `fdiv double` | +| `==` | existing `icmp eq i64` / `i1` / `@strcmp` / `i1 1` | `fcmp oeq double` | +| `!=` | derived from `==` | `fcmp one double` | +| `<` | `icmp slt i64` | `fcmp olt double` | +| `<=` | `icmp sle i64` | `fcmp ole double` | +| `>` | `icmp sgt i64` | `fcmp ogt double` | +| `>=` | `icmp sge i64` | `fcmp oge double` | + +Non-{Int,Float} resolutions for `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` +get rejected at codegen with the same diagnostic shape the `==` +path uses today (`"+ not supported for type X"`). The reject +keeps the polymorphism honest — there is no silent fallback, +no string-concatenation-via-`+`, no boolean-arithmetic-via-`+`. Rationale: -- AILang already rejects operator overloading - (`docs/DESIGN.md` "Feature-acceptance criterion"). A - polymorphic `+ : forall a. (a, a) -> a` would either need - ad-hoc constraints (the typeclass story, out of scope here) or - a hard-coded Int|Float type spec-case in the typechecker. Both - cost more than two-name disambiguation. -- The `==`/`!=` codegen-dispatch path already exists - (`crates/ailang-check/src/builtins.rs:78`, - `crates/ailang-codegen/src/lib.rs:2244-2266`). Extending the - arm is one branch addition; introducing `feq`/`fne` would be a - duplication of an already-polymorphic site for no semantic - gain. IEEE-conformant `==` (NaN == NaN ⇒ false) falls out of - LLVM `fcmp oeq` directly. -- `<`/`<=`/`>`/`>=` on Int are monomorphic today, so widening - them to polymorphic-Int|Float would require a *new* dispatch - path. Cheaper and more honest to add `flt`/`fle`/`fgt`/`fge` - alongside. -- `fmod` is **excluded** for this milestone. IEEE 754-2008 - remainder semantics (`fmod` vs `remainder`) are subtle enough - to deserve their own decision; not blocking the milestone on - it. +- **Mainstream alignment.** Every LLM-relevant programming + language (Rust, Java, C, Python, JavaScript, Haskell, Swift, + OCaml-via-typeclass-like-extension) accepts `1.5 + 2.5`. An + AILang where the LLM-author has to write `(fadd 1.5 2.5)` is + a high-friction first-try-error surface. The user-facing + decision (this conversation, 2026-05-10) chose Mainstream + alignment over the explicit-naming purity of an earlier draft. +- **Precedent already in tree.** The `==` builtin is + `forall a. (a, a) -> Bool` with a hardcoded Int|Bool|Str|Unit + codegen dispatch and explicit reject for ADT/Fn equality + (`builtins.rs:75-77`). The widening of `+`/`-`/etc. uses the + *same* mechanism — no new architectural surface, just more + arms in the existing dispatch helper. +- **Typeclass migration story.** When typeclasses ship + (Post-22 Prelude + 22c), the hardcoded `Int|Float` spec-case + in the typechecker can be cleanly replaced by a `Num a` + constraint. Surface (`(+ 1.5 2.5)`) does not change. The + spec-case is transitional, not load-bearing. +- **`%` stays monomorphic.** IEEE `frem` (LLVM op for `fmod`) + has subtle semantics (sign-of-result-follows-dividend, + ±0 / ±Inf edge cases) that deserve their own decision; out + of scope for this milestone. -Builtin signatures (added to -`crates/ailang-check/src/builtins.rs::install`): +Other new builtins: ``` -fadd : (Float, Float) -> Float -fsub : (Float, Float) -> Float -fmul : (Float, Float) -> Float -fdiv : (Float, Float) -> Float -fneg : (Float) -> Float -flt : (Float, Float) -> Bool -fle : (Float, Float) -> Bool -fgt : (Float, Float) -> Bool -fge : (Float, Float) -> Bool +neg : forall a. (a) -> a -- Int|Float; reject otherwise int_to_float : (Int) -> Float float_to_int_truncate : (Float) -> Int float_to_str : (Float) -> Str +is_nan : (Float) -> Bool -- LLVM `fcmp uno double %x, %x` +``` + +The unary `neg` is widened the same way arithmetic ops are +(today there is no `neg` builtin — unary minus is desugared from +the surface lexer's `-` rule into a literal or via +`(- 0 x)`-style desugar; the spec adds an explicit `neg` so +Float negation has a name without the `(- 0.0 x)` workaround, +which is wrong for `-0.0`). The plan picks the desugar/builtin +boundary. + +New builtin float constants (always-in-scope `Term::Var` +references, parallel to today's `__unreachable__`): + +``` +nan : Float -- bits 7ff8000000000000 (canonical quiet NaN) +inf : Float -- bits 7ff0000000000000 +neg_inf : Float -- bits fff0000000000000 +``` + +Rationale for the constants: + +- Every Mainstream language exposes them (`f64::NAN`, + `Double.NaN`, `float('nan')`, `NaN`, `Double.nan`). + Withholding them while shipping the IEEE-conformant + semantics that *make them necessary* is a pointless friction. +- Hex bits via Form-A still works as the ground truth, but + surface-level `(var nan)` lets the LLM-author write code that + reads like every other language's float code. +- Names are lowercase (`nan`, not `NaN`) so they're regular + identifiers, no surface-lex special-case. `neg_inf` instead + of `-inf` because `-` cannot start a value identifier (the + surface-lex `-` rule applies to numeric literals + only). + +Effect ops (added): + +``` +io/print_float : (Float) -> Unit !IO -- new ``` ### A4 — Conversions: total, foot-gun-free @@ -269,37 +336,66 @@ the plan for iteration boundaries. - `lib.rs` (4457 LoC) — `Literal::Float` is well-typed at `Type::float()`. Add the one-arm extension to whatever `Term::Lit` typing helper exists. -- `builtins.rs` (183 LoC) — install all twelve new entries (per - A3). Extend `list()` accordingly so `ail builtins` reflects - them. The `==` polymorphic entry needs no change here — the - signature stays `forall a. (a, a) -> Bool`; the codegen - side (below) handles the new Float arm. +- `builtins.rs` (183 LoC) — three classes of change: + 1. **Widen** the existing arithmetic and comparison entries + `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` from monomorphic Int to + `forall a. (a, a) -> a` (or `... -> Bool`) — same shape + as today's `==` entry. Existing `==`/`!=` entries + unchanged in signature; their dispatch arm gets extended + codegen-side. + 2. **Install** the new builtins: `neg` (polymorphic), + `int_to_float`, `float_to_int_truncate`, `float_to_str`, + `is_nan`, plus the three constants `nan`, `inf`, + `neg_inf` (each a `Term::Var`-resolvable global at + `Type::float()`, parallel to `__unreachable__`). + 3. **Install** the new effect op `io/print_float`. + + Extend `list()` accordingly so `ail builtins` reflects every + added entry. The `list()` strings serve as the LLM-author's + contract — they must be accurate after this iteration. ### `crates/ailang-codegen/` -- `lib.rs` (2877 LoC) — six new lowering paths: +- `lib.rs` (2877 LoC) — six lowering changes: 1. **Float literal** (`Literal::Float { bits }`) → emit `double` constant via LLVM hex-float syntax `0x1p+0`-style or via `bitcast i64 0x... to double`. Sites: every place `Literal::Int { value }` is matched today (lines 918, 1215). - 2. **Arithmetic builtins** `fadd/fsub/fmul/fdiv/fneg` → - LLVM `fadd double`, `fsub double`, `fmul double`, - `fdiv double`, `fneg double`. Site: parallel to the - `t_add` / `+` lowering (line 1745 region). - 3. **Comparison builtins** `flt/fle/fgt/fge` → LLVM - `fcmp olt`, `fcmp ole`, `fcmp ogt`, `fcmp oge` - (ordered, so NaN compares yield `false`). + 2. **Widen arithmetic dispatch.** `+`/`-`/`*`/`/` are + today lowered as monomorphic Int instructions + (line 1745 region). Convert the lowering site into a + type-dispatched helper analogous to the existing `==` + dispatch (`lib.rs:2244-2266`): Int arm emits + `add/sub/mul/sdiv i64`, Float arm emits + `fadd/fsub/fmul/fdiv double`, anything else fails with + `" not supported for type X"`. + 3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=` get the + same treatment: Int arm `icmp s{lt,le,gt,ge} i64`, Float + arm `fcmp o{lt,le,gt,ge} double`, reject otherwise. 4. **`==` / `!=` Float arm** in the existing dispatch (line 2263 region) → `fcmp oeq` / `fcmp one` for the - `Float` case. Add the case alongside the existing - `"Int"` / `"Bool"` / `"Str"` / `"Unit"` arms. - 5. **Conversions** `int_to_float` → `sitofp i64 to double`; - `float_to_int_truncate` → `call double @llvm.fptosi.sat.i64` - (or the legalised equivalent). - 6. **`io/print_float`** effect-op lowering parallel to - `io/print_int` (line 2150 region) → call into runtime C - glue. + `Float` case, alongside the existing arms. + 5. **`neg` polymorphic** — Int arm `sub i64 0, %x`, Float + arm `fneg double %x` (correct for `-0.0`, unlike a + hypothetical `(- 0.0 x)` desugar). Reject other types. + 6. **Conversions and IO**: + - `int_to_float` → `sitofp i64 ... to double`. + - `float_to_int_truncate` → `@llvm.fptosi.sat.i64.f64` + intrinsic (or the legalised cast sequence if the + target backend doesn't expose it directly). + - `is_nan` → `fcmp uno double %x, %x` (returns `i1`, + which already coerces to AILang `Bool`). + - `float_to_str` → call into runtime C glue + `@ail_float_to_str`. + - `io/print_float` → parallel to `io/print_int` + (line 2150 region) → call into runtime C glue + `@ail_print_float`. + 7. **Float constants** `nan`/`inf`/`neg_inf` lower as + `Term::Var` references resolving to compile-time `double` + constants (the codegen path that resolves `Var "x"` to + the SSA value of a global gets a builtin-constant arm, + same way `__unreachable__` resolves to `unreachable`). - ADT / container layout — `double` is 8 bytes, fits the existing 8-byte slot used for `i64` and `ptr`. **No layout change.** Confirm this by inspecting how `List` lowers @@ -315,13 +411,21 @@ the plan for iteration boundaries. ### `runtime/` - New file `runtime/print_float.c` (or extend an existing C - file) — `void ail_print_float(double v)` that writes the - shortest round-trippable decimal followed by a newline. We - vendor a small `ryu`-style implementation, or — if simpler — - use `printf("%.17g\n", v)` for the milestone and revisit if - the redundancy is a problem. -- The RC runtime (`rc.c`, `bump.c`) is **not touched**. Float - is a value type with no heap allocation per literal. + file) — two functions: + - `void ail_print_float(double v)` — write shortest + round-trippable decimal + newline. + - `const char *ail_float_to_str(double v)` — return a + heap-allocated AILang `Str` of the shortest + round-trippable decimal (no newline). Refcounted as any + other `Str` in the runtime. + + Implementation: vendor a small `ryu`-style routine, or — if + simpler — use `snprintf("%.17g", v)` for the milestone and + revisit if the redundancy is a problem. Plan-time call. +- The RC runtime (`rc.c`, `bump.c`) is **not touched** by the + Float value path itself. Float is a value type with no heap + allocation per literal. The `ail_float_to_str` glue allocates + a `Str`, but uses the existing `Str` runtime path. ### `crates/ail/` (CLI) @@ -437,20 +541,20 @@ fixes the *property set* that must be covered. ### IEEE-conformance properties -- `(fadd 0.1 0.2)` produces the exact `bits` of +- `(+ 0.1 0.2)` produces the exact `bits` of `0.1_f64 + 0.2_f64` (i.e. `bits == 0x3fd3333333333334`, not `0x3fd3333333333333`). A single `fadd` cannot be FMA-contracted (no `c` operand to absorb), so the result is bit-stable per A5. -- `==` on the same NaN bit pattern (passed in as a Float literal) - returns `false`. `!=` on the same NaN literal returns `true`. -- `flt`, `fle`, `fgt`, `fge` all return `false` when either - argument is NaN (ordered comparisons). -- `(fdiv 1.0 0.0)` produces `+inf` (bits `7ff0000000000000`); - `(fdiv -1.0 0.0)` produces `-inf` (bits `fff0000000000000`); - `(fdiv 0.0 0.0)` produces *some* NaN (test asserts - `(fne result result) == true` per IEEE NaN-detection idiom, - **not** specific NaN bits — A5 leaves the qNaN payload - unspecified). +- `(== nan nan)` returns `false`. `(!= nan nan)` returns `true`. +- `<`, `<=`, `>`, `>=` all return `false` when either + argument is NaN (ordered comparisons via `fcmp o*`). +- `(/ 1.0 0.0)` produces `+inf` (bits `7ff0000000000000`); + `(/ -1.0 0.0)` produces `-inf` (bits `fff0000000000000`); + `(/ 0.0 0.0)` produces *some* NaN (test asserts + `(is_nan result) == true`, **not** specific NaN bits — + A5 leaves the qNaN payload unspecified). +- `(is_nan nan) == true`. `(is_nan 1.0) == false`. + `(is_nan inf) == false`. `(is_nan neg_inf) == false`. - `+0.0` and `-0.0` hash distinctly in Form-A but compare equal via `==`. @@ -491,8 +595,14 @@ The milestone is closeable when **all** of the following hold: 2. `Literal::Float { bits: u64 }` is serialised as `{"bits":"<16-hex>","kind":"float"}` in canonical JSON. The round-trip test passes. -3. The twelve new builtins (per A3) appear in - `ail builtins` output. +3. `ail builtins` output reflects: + (a) widened signatures for `+`, `-`, `*`, `/`, `<`, `<=`, + `>`, `>=` (now `forall a. (a, a) -> a` / + `forall a. (a, a) -> Bool`); + (b) new builtins: `neg`, `int_to_float`, + `float_to_int_truncate`, `float_to_str`, `is_nan`; + (c) new constants: `nan`, `inf`, `neg_inf`; + (d) new effect op: `io/print_float`. 4. `examples/floats.ail.json` builds, runs, and produces the expected stdout (printed floats round-trip the literal forms). @@ -519,15 +629,12 @@ Out of scope, explicitly: gets `Show` in the next milestone; `Eq` and `Ord` will *intentionally* not exist for `Float` because of A5 + user-fixed constraint #2.) -- Polymorphic numeric class (`Num`). +- Polymorphic numeric class (`Num`). The hardcoded + `{Int, Float}` spec-case in the typechecker is transitional + scaffolding; replaced by a proper `Num a` constraint when + typeclass machinery picks up arithmetic in 22c. - `f32`. -- `fmod` / IEEE-`remainder`. -- NaN-detection builtin (`is_nan`); NaN-construction builtin. - Workaround in scope: `(fne x x)` is `true` iff `x` is NaN - (the canonical IEEE NaN test). Documented in - §"Float semantics". -- `Float.nan` / `Float.infinity` named constants — these come - with the eventual Float stdlib, not the primitive milestone. +- `fmod` / IEEE-`remainder`. `%` stays Int-only this milestone. - `print` rewiring through `Show.show` — that is Post-22 Prelude. - Pattern-matching on Float literals (`Pattern::Lit { lit: @@ -540,25 +647,40 @@ Out of scope, explicitly: IEEE-`==` semantics, which the LLM-author has to remember. Either way: this milestone explicitly does NOT introduce a Float-pattern *idiom* — the documented way to discriminate - Floats is via the comparison builtins (`flt`/`fle`/...) and - the NaN-detection idiom `(fne x x)`. + Floats is via the comparison operators (`<`/`>`/...) and + `(is_nan x)`. ## Notes for the plan The plan should sequence iterations roughly: - **Iteration 1**: AST + canonical + primitives (the schema - layer). Pure schema, RED-first by canonical-bytes test. + layer). Pure schema, RED-first by canonical-bytes test for + `Literal::Float`. - **Iteration 2**: Surface lex + parse + print round-trip. RED-first by `lex(print(L)) == L` property. -- **Iteration 3**: Type + builtins install. RED-first by - typecheck unit test on `(fadd 1.0 2.0) : Float`. -- **Iteration 4**: Codegen (literal + arithmetic + comparison + - conversion + IO). RED-first by E2E - `examples/floats.ail.json`. +- **Iteration 3**: Type + builtins install. Two distinct + sub-tasks: + (a) **widen** existing `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` to + polymorphic; **don't break** existing Int-only fixtures; + (b) install new builtins (`neg`, conversions, `is_nan`, + constants) and `io/print_float`. + RED-first by typecheck unit test on `(+ 1.0 2.0) : Float` + AND `(+ 1 2) : Int` (regression). +- **Iteration 4**: Codegen widening + Float lowering paths. + Same widen-vs-add split as iteration 3 — codegen for + `+`/`-`/`*`/`/` becomes type-dispatched, plus Float arms for + comparison, conversion, IO, and constants. RED-first by E2E + `examples/floats.ail.json` AND existing Int E2E fixtures + staying GREEN (regression gate). - **Iteration 5**: Prose + DESIGN.md + drift-test extension + rustdoc. +Note the regression-gate emphasis on iterations 3 and 4: this +milestone *widens* operators that are today monomorphic. Every +existing Int-using fixture must keep working bit-identical. +The plan should pin a "no Int regression" property explicitly. + Iteration boundaries are the plan's call. The five-cluster shape above is the spec's scope estimate, not a binding sequence.