Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

fieldtest: floats — 4 examples, 6 findings (1 bug, 1 friction, 1 spec_gap, 3 working)

Browse Source
This commit is contained in:
Brummel
2026-05-10 16:57:38 +02:00
parent 741f3bbf08
commit 2052f4dfcc
9 changed files with 497 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/specs/2026-05-10-fieldtest-floats.md
+307
View File
@@ -0,0 +1,307 @@
# Fieldtest — Floats milestone — 2026-05-10
**Status:** Draft — awaiting orchestrator triage
**Author:** ailang-fieldtester (dispatched by skills/fieldtest)
## Scope
The Floats milestone (closed 2026-05-10) added `Float` as a fourth
zero-arity primitive type (IEEE-754 binary64). Surface accepts
`1.5`, `1.5e3`, `1e10`, `-1.5`. Operators `+`/`-`/`*`/`/` and
`<`/`<=`/`>`/`>=`/`!=`/`==` widened to polymorphic over `{Int,Float}`
via codegen-dispatch. New builtins: `neg` (poly), `int_to_float`,
`float_to_int_truncate`, `is_nan`. Constants `nan`, `inf`,
`neg_inf` (bit-pattern globals). New effect op `io/print_float`.
`float_to_str` is type-installed but codegen-deferred. Per
DESIGN.md §"Float semantics", `Pattern::Lit::Float` is supposed
to be hard-rejected at typecheck via `CheckError::FloatPatternNotAllowed`.
## Examples
### `examples/fieldtest/floats_1_newton_sqrt.ailx` — Newton's method for √2
- 20-step Newton iteration `x' = 0.5 * (x + N/x)` for `N = 2.0`,
printed via `io/print_float`.
- Exercises Float literals (`0.5`, `2.0`), polymorphic `*` and `+`
and `/` and `==` and `-` (the loop counter is `Int`), tail-
recursive `Float`-typed accumulator, `io/print_float`.
- **Outcome:** typechecks, builds, runs first try. stdout: `1.41421`
(matches `sqrt(2)` to 5 decimals — the IEEE-conformant truncated
`%g` printf).
### `examples/fieldtest/floats_2_average_int_list.ailx` — mean of an Int list as Float
- Sum and count an `IntList` with two tail-recursive accumulators,
then promote both to `Float` via `int_to_float` and divide.
- Exercises `int_to_float` at both numerator and denominator (the
natural shape — neither operand can be left as `Int` because `+`,
`-`, `*`, `/` reject mixed-type args).
- **Outcome:** typechecks, builds, runs first try. stdout: `3.2`
(sum 16 / count 5 = exact 3.2 since 5 is a power of 5 not
representable in binary, but the printer lands on the
shortest-decimal that round-trips).
### `examples/fieldtest/floats_3_safe_division.ailx` — IEEE division + `is_nan`
- Three division cases: `6.0/3.0` (normal), `1.0/0.0` (+Inf),
`0.0/0.0` (NaN). For each, `classify` returns `-1` if the value is
NaN (via `is_nan`), `0` if infinite (via comparison against
`1.0e308` and `-1.0e308`), `1` otherwise.
- Exercises `is_nan`, polymorphic `>`, `<`, large literal
exponents, `io/print_float` on Inf/NaN values, and the IEEE
`0.0/0.0 = NaN` semantics.
- **Outcome:** typechecks, builds, runs first try (after a paren-
count typo fix). stdout:
```
2
1
inf
0
-nan
-1
```
Three observations from the actual stdout vs. the expected:
1. `6.0/3.0` printed as `2`, not `2.0` (see finding F1).
2. NaN printed as `-nan` (the platform's qNaN sign-bit
representation).
3. `is_nan` correctly returned `true` for the `0.0/0.0` result
and `false` for `1.0/0.0`.
### `examples/fieldtest/floats_4_float_to_str_reach.ailx` — reach for `float_to_str`
- `(do io/print_str (app float_to_str 3.14))` — the natural
reach: an LLM-author who finds `float_to_str : (Float) -> Str`
in `ail builtins` will write this, expecting a `Str`-printable
Float.
- **Outcome:** `ail check` succeeds (typechecks fine). `ail build`
fails with the structured codegen-deferred error — the diagnostic
is excellent, see finding F2.
## Findings
### [bug] B1 — `Pattern::Lit::Float` is NOT rejected at typecheck (DESIGN.md says it must be)
DESIGN.md §"Float semantics" (lines 2076-2081):
> **Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard-
> rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
> semantics make Float patterns semantically dubious — NaN never
> matches via IEEE-`==`, and bit-exact equality is rarely what an
> LLM-author wants. Use ordering operators (`<`, `>`, ...) and
> `is_nan` to discriminate Floats.
JOURNAL Floats.3 (line 13559-13560):
> `Pattern::Lit::Float` typecheck-rejected via new
> `CheckError::FloatPatternNotAllowed`.
Floats.5 milestone-close JOURNAL repeats the claim. But probing
with this fixture (saved at `/tmp/probe_pat_float.ailx`, not
committed; reproduced below):
```
(module probe_pat_float
(fn classify
(type (fn-type (params (con Float)) (ret (con Int))))
(params x)
(body
(match x
(case (pat-lit 0.0) 1)
(case _ 0))))
(fn main
(type (fn-type (params) (ret (con Unit)) (effects IO)))
(params)
(body (do io/print_int (app classify 0.0)))))
```
`ail check` reports `ok (2 symbols across 1 modules)`. `ail build`
succeeds. The compiled binary returns `1` for `classify(0.0)` —
the Float pattern *runs*. Multi-arm probe confirms IEEE semantics:
NaN does not match `0.0` (yields the `_` branch), `-0.0` (via
`(neg 0.0)`) DOES match `(pat-lit 0.0)` (yields `1`). So the
underlying behaviour is "option (b)" from the spec's out-of-scope
note (Floats spec line 729-731) — Float patterns work with
IEEE-`==` semantics, despite DESIGN.md and JOURNAL both promising
the option-(a) hard-reject.
- **Repro:** the four-line probe above; check exits 0 instead
of error.
- **Recommended action:** `debug` — RED-first test that
`(case (pat-lit 0.0) ...)` produces
`CheckError::FloatPatternNotAllowed`, then implement the missing
reject path in `crates/ailang-check/`. Alternative: if the team
decides option (b) (silent Float-pattern with IEEE-`==`) is
actually the right semantics on reflection, then DESIGN.md and
JOURNAL must be amended — but this is a substantive design
reversal and should go through `brainstorm`, not be silently
papered over.
### [working] W1 — `float_to_str` deferred-codegen diagnostic is excellent
Diagnostic from `ail build` on example 4:
```
Error: module `floats_4_float_to_str_reach`: def `main`: internal:
`float_to_str` codegen lowering is not yet implemented (requires
dynamic Str allocation in the runtime)
```
This is the gold-standard form for an LLM-author-facing diagnostic:
- **Names the builtin** that triggered the error (`float_to_str`).
- **Names the failure layer** (codegen, not typecheck — so the LLM
knows the type signature is correct and not to second-guess it).
- **Names the underlying blocker** (dynamic Str allocation) so the
LLM can decide whether to wait for the future milestone or work
around (no current workaround: there's no other Float→Str path).
The reach itself (looking at `ail builtins`, finding
`float_to_str : (Float) -> Str`, writing
`(do io/print_str (app float_to_str 3.14))`) was natural — exactly
the shape an LLM produces for "print this Float as a labeled
string". The deferred-codegen state is communicated cleanly enough
that the LLM gets a useful signal without reaching for the source.
- **Recommended action:** `carry-on`. This is the model for how
other "type-installed but codegen-deferred" features should
diagnose themselves.
### [working] W2 — DESIGN.md §"Float semantics" is sufficient to guide the natural-reach for `is_nan`
DESIGN.md line 2034-2037:
> - `is_nan` (`fcmp uno double %x, %x`) returns `true` iff `x` is
> NaN. Bit-pattern-based NaN detection without dependence on the
> payload bits.
Plus line 2079-2081:
> Use ordering operators (`<`, `>`, ...) and `is_nan` to
> discriminate Floats.
Reading these alone (no compiler peek), an LLM-author writing
example 3 reaches for `is_nan` directly, never considers the
ill-fated `(== x x)` form, and produces a working classifier.
The `nan` / `inf` / `neg_inf` constants are also discoverable
from the same section (line 2135-2137), and `ail builtins`
confirms them as bare-value globals — they were used as test
inputs in the iteration of example 3, where the same probe
showed they propagate correctly through `is_nan`, `<`, `>`.
- **Recommended action:** `carry-on`.
### [friction] F1 — `io/print_float` strips trailing `.0`, making float output indistinguishable from int output
Example 3 stdout includes `2` for `(/ 6.0 3.0)`, not `2.0`. The
spec/JOURNAL describes the printer as "shortest round-trippable
decimal" (Floats.2 entry, line 13548-13549) but that property
applies to the surface printer (`Literal::Float` → surface
`"2.0"`). The runtime path `io/print_float` lowers via
`printf("%g\n", v)` (Floats.4 entry, line 13571), and `%g` strips
trailing zeros and the trailing decimal point.
Consequences:
1. The stdout of `io/print_float v` for an integer-valued `v` is
indistinguishable from `io/print_int (float_to_int_truncate v)`.
For an LLM author writing a test that asserts on stdout, the
round-trip property "the text I see is unambiguously a Float"
silently breaks.
2. The asymmetry between the surface printer (always emits `.0`)
and the runtime printer (sometimes doesn't) is a hidden
contract the LLM-author has to learn from running the program,
not from DESIGN.md.
The deeper issue: DESIGN.md says nothing about the format of
`io/print_float` output. It is silent on whether the contract is
"shortest round-trippable" (matching the surface printer) or
"`%g`-style". An LLM-author who writes a test asserting `2.0` in
stdout has no DESIGN.md anchor to consult; running the test is
the only way to find out.
- **Recommended action:** `plan` (tidy iteration). Either (a)
switch `io/print_float` to a shortest-round-trippable format
(matches the surface printer, removes the asymmetry, makes
`print_float` output unambiguous as a Float), or (b) document
the `%g`-style format explicitly in DESIGN.md §"Float
semantics" so the contract is at least nameable. Option (a) is
the LLM-utility-aligned choice: the LLM-author benefit from
unambiguous output exceeds the cost of a more verbose format
string for integer-valued Floats. (Note: `float_to_str`,
when it ships its codegen, faces the *same* design choice —
pinning the format on `io/print_float` first preserves the
freedom to make `float_to_str` match.)
### [spec_gap] G1 — DESIGN.md is silent on the NaN sign-bit / payload visible to `io/print_float`
Example 3 stdout shows `-nan` for `(/ 0.0 0.0)`. DESIGN.md line
2057-2060 explicitly leaves the NaN payload unspecified:
> The exact NaN bit pattern produced by an op. Any quiet NaN bit
> pattern is conformant; `0.0 / 0.0` may produce
> `0x7ff8000000000000` on one target and a different qNaN on
> another.
The reading taken: since the payload (and sign bit) of the qNaN
produced by `0.0/0.0` is unspecified, the *printed form* of that
qNaN is also unspecified. The compiler's `printf("%g\n", v)`
exposes the sign bit (`-nan` vs `nan`) — that's a downstream
consequence of "NaN bit pattern unspecified".
The other plausible reading: DESIGN.md guarantees the constant
`nan` (line 2135) has bits `7ff8000000000000` (no sign bit set, so
prints as `nan`), AND that `is_nan` correctly identifies any qNaN
regardless of sign — but does NOT promise that the printed form
of an op-produced NaN is normalised to `nan` (no sign).
The picked reading (current behaviour) is internally consistent
with A5's "NaN payload unspecified". But an LLM-author who reads
DESIGN.md, sees the `nan` constant prints as `nan`, and assumes
all NaN values print the same way will be surprised by `-nan` on
ops that produce NaN. **Both readings are equally plausible from
the text.**
- **Recommended action:** `tighten DESIGN.md`. One additional
sentence in §"Float semantics" Unspecified-list: "The textual
form of a NaN value emitted by `io/print_float` follows
`printf("%g")` and may include a sign bit (`-nan`); `is_nan` is
the only reliable NaN test." Or, if the team prefers a
guarantee, normalise NaN printing in the runtime to `nan` and
add the corresponding Guaranteed-list entry. Either pin
removes the ambiguity.
### [working] W3 — Mixed `Int + Float` produces a clear, actionable diagnostic
Probe (`/tmp/probe_mixed.ailx`):
```
(do io/print_float (app + 1 1.5))
```
`ail check` reports:
```
error: [type-mismatch] main: type mismatch: expected Int, got Float
```
The diagnostic doesn't *suggest* `int_to_float`, but the LLM-author
reading "expected Int, got Float" will think "I need to coerce
the Int" and either (a) write `1.0` instead of `1` (the natural
fix here) or (b) reach for `int_to_float`. Both work. The
diagnostic doesn't lie about the type system: `+ : forall a. (a, a)
-> a` unifies under one type variable; mixing rejects.
- **Recommended action:** `carry-on`. A future polish iteration
could add a "did you mean to coerce one side?" hint, but for
the milestone scope the diagnostic is sufficient.
## Recommendation summary
| Finding | Class | Action |
|---|---|---|
| B1 — Pattern::Lit::Float not rejected | bug | `debug` — RED test pinning the missing `CheckError::FloatPatternNotAllowed`, then fix in `crates/ailang-check/`. Alternative: if option (b) is now preferred, run `brainstorm` to amend DESIGN.md and JOURNAL. |
| W1 — `float_to_str` deferred-codegen diagnostic | working | carry-on |
| W2 — `is_nan` discoverability | working | carry-on |
| F1 — `io/print_float` strips `.0` | friction | `plan` (tidy iteration) — switch to shortest-round-trippable, or document `%g` contract in DESIGN.md |
| G1 — NaN sign-bit print form unspecified | spec_gap | `tighten DESIGN.md` — one sentence in Unspecified-list, OR runtime normalisation + Guaranteed-list addition |
| W3 — mixed Int+Float diagnostic | working | carry-on |