From 080d294bc9e2dd6e8753c29dc1143014f1acab70 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 18:08:16 +0700 Subject: [PATCH] The lattice of conversions that cannot change the number --- FIX.org | 121 +++++++++++++++++++++++++++++++++++++++++++++++++++ lib/types.ml | 67 +++++++++++++++++++++++++--- 2 files changed, 183 insertions(+), 5 deletions(-) diff --git a/FIX.org b/FIX.org index 9cdda86..d65d942 100644 --- a/FIX.org +++ b/FIX.org @@ -2442,3 +2442,124 @@ failures were that row and the sixth was ~dev-trap-free-all~, so what is racy is ~trap_park~ itself and every row that calls it — which is exactly what the mechanism described there predicts. Per the sweep policy the ~@x86~ and ~@sanitize~ sweeps were not run here. +* Implicit widening, 2026-09-20 — "go with C" +Answers DISCUSS.org's *implicit numeric conversions with a warning flag, +instead of hard errors*. The ask there was a warn-instead-of-refuse mode; the +answer is narrower and needs no mode and no flag. + +*The decision.* Implicit numeric *widening* is legal — every conversion that +cannot change the number. *Narrowing stays a hard error everywhere*, with no +flag that turns it into a warning. Odin's position roughly; Rust's +no-conversions-at-all position is rejected, and so is C's, which is what +DISCUSS.org's ~-Wconversion~ middle ground would have reproduced. + +So there is no second type-checking mode, which was the objection in the note: +one predicate says which conversions exist, one helper inserts the ~Cast~ for +them, and everything else in the checker is unchanged. + +** The lattice +~Types.widens_to ~from ~into~ (lib/types.ml). One rule decides every row: a +conversion is admitted exactly when no value of the source can come out the +other side as a different number. + +| from | widens implicitly into | +|-------------+-------------------------------------------| +| ~i8~ | ~i16~ ~i32~ ~i64~ ~f32~ ~f64~ | +| ~i16~ | ~i32~ ~i64~ ~f32~ ~f64~ | +| ~i32~ | ~i64~ ~f64~ | +| ~i64~ | — (nothing) | +| ~u8~ | ~u16~ ~u32~ ~u64~ ~i16~ ~i32~ ~i64~ ~f32~ ~f64~ | +| ~u16~ | ~u32~ ~u64~ ~i32~ ~i64~ ~f32~ ~f64~ | +| ~u32~ | ~u64~ ~i64~ ~f64~ | +| ~u64~ | — (nothing) | +| ~f32~ | ~f64~ | +| ~f64~ | — (nothing) | + +Read off the rule, one clause at a time: + +- *Same signedness, strictly wider* — the uncontroversial half. +- *Unsigned into strictly wider signed* — ~u8~→~i16~, ~u32~→~i64~. Every + value of the source is a value of the target, so it is in. +- *Signed into unsigned* — never, at any width: the negatives have nowhere to + go. +- *Equal width across signedness* (~i32~→~u32~, ~u32~→~i32~) — never, for the + same reason. Half the range would have to move. +- *Integer into float, exact only.* An ~f64~ significand is 53 bits, so + everything 32 bits and under reaches it and ~i64~/~u64~ do not — 2^53+1 is + not an ~f64~. An ~f32~ significand is 24 bits, so only the 8- and 16-bit + integers reach it. Odin allows any integer into any float; this is the + tighter rule deliberately. A program that wants ~i64~→~f64~ writes ~(f64 x)~. + Loosening this later adds programs; tightening it later would break them, + which is why the loose version is not the one that landed. +- *~dyn~ is not in the lattice.* Crossing into and out of a box is + ~box~/~unbox~ and is untouched — in particular a ~dyn~ still only unboxes to + ~i64~/~f64~/~bool~, and a narrower want there is still the refusal + lib/check.ml's ~unbox~ has always given. +- *Containers are invariant.* A ~[i32]~ is not a ~[i64]~, a ~(Vec i32)~ is not + a ~(Vec i64)~, an ~[8 u8]~ is not an ~[8 u16]~. Widening rewrites a value + with a ~Cast~; there is no value to rewrite in a slice that does not own its + bytes, and rewriting a ~Vec~ would mean allocating a second one. +- ~bool~ and an ~Enum~ are not numbers and are not on the list. A keyword still + resolves against an enum and a bare integer still does not fit one. + +*Not expressed as a loosening of ~equal~ or ~fits~*, deliberately. +~widens_to~ is a separate predicate precisely so that admitting a conversion +is always paired with inserting the ~Cast~ that performs it. Had ~fits~ been +loosened, every site that accepts a value without rewriting it would hand the +backends a node whose type lies about the bits it holds. + +** Where it applies +~Check.expect~ (lib/check.ml) is the single place a wanted type meets a +produced one, so one arm there covers the whole surface: argument passing, +return position, ~let~ and ~defvar~ with an annotation, struct field +initialisers, ~Vec~ pushes, ~set!~, every C import's parameters. Nothing else +had to learn about widening except the binary operators, which have no +"wanted type" to meet. + +** The join rule for binary operators +Both operands of a binary operator have one type, and the old comment said +"there is no implicit widening, so one side has to decide it". The +decides-rule generalises rather than disappearing: + +1. *An expectation still wins, and it reaches the operands.* When the site + wants a type — ~(defn f [] i64 (+ a b))~ — that want is threaded into both + operands as before, and now widens them. The addition happens at ~i64~, not + at ~i32~ followed by a widened result. That is the better of the two and it + is only reachable by programs that did not compile before. +2. *Literals decide exactly as they did.* ~y_decides~ and ~needs_want~ are + untouched: a literal takes its width from the other operand, a float + literal outranks an integer one. ~(+ x 1)~ over a ~u64~ ~x~ still builds a + ~u64~ one, which is what keeps ~(let [h fnv-offset])~ with a ~u64~ + ~defconst~ meaning exactly what it meant. +3. *Otherwise the wider side decides* — ~Types.join~: whichever operand the + other widens into, with the loser wrapped in a ~Cast~ to it. ~(+ i32-var + i64-var)~ is ~i64~ and is newly legal. ~(min i8-var i16-var)~ is ~i16~. +4. *Equal-width cross-sign still refuses.* ~(+ i32-var u32-var)~ has no join — + neither widens into the other — and the message names the cast to write. + +~join~ is not a real lattice and is not meant to be: ~(i32, u32)~ has no +answer, and inventing ~i64~ for it would pick a type neither operand was +written at. + +*Folds are still folds.* ~(+ a b c)~ is ~((a + b) + c)~, so the join is +pairwise and left-to-right: the first pair settles a type and the third +operand is checked against it. ~(+ i8 i8 i64)~ therefore still refuses, where +~(+ i64 i8 i8)~ passes. Left to stand rather than joined across the whole +argument list, because changing that would change what ~(- a b c)~ means, not +only what it admits. + +*Shifts are carved out.* ~<<~ and ~>>~ do not take the plain join: the value +decides, and the count widens to the value's type. Under the general rule +~(<< u8-var i32-count)~ would widen the *value* to ~i32~ and the result type +and the wrap width would silently follow the count's declared type — and the +emitter's poison mask is keyed to the value's width. A count wider than the +value is refused and says so. + +** Const folding is unchanged +The ~defconst~ integer folder (lib/check.ml) folds literal arithmetic within +one type and does not walk through a ~Cast~ node. So a widened operand is not +a folded constant: ~(defconst n (+ small-i32-const big-i64-const))~ compiles +and computes at run time rather than folding, and an array length written that +way is refused as it was before. Kept as it is on purpose — the folder's job +is array lengths and it already covers the same-type arithmetic they are +written with. diff --git a/lib/types.ml b/lib/types.ml index 7c267a1..110bcaf 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -9,8 +9,11 @@ have to have it. That rejection lives in [Check]; this module only names the shape. *) -(* Machine integer types. Signedness and width are both part of the type — - there is no implicit widening anywhere, per plan.org. *) +(* Machine integer types. Signedness and width are both part of the type, and + two of them are the same type only when both halves match. A value may move + to a type that cannot lose it — see [widens_to] at the bottom of this file, + FIX.org 2026-09-20 — and never the other way: narrowing is written or it + does not happen. *) type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64 type fkind = F32 | F64 @@ -115,9 +118,13 @@ let ikind_name k = let fkind_name = function F32 -> "f32" | F64 -> "f64" -(* Structural equality is the whole story: no subtyping, no coercion between - machine types, no variance. Written out rather than using [=] so that adding - a case with a function or a mutable field cannot silently break it. *) +(* Structural equality is the whole story for *identity*: no subtyping, no + variance, and nothing here bends to admit a conversion. Implicit widening + (below) is deliberately not expressed as a loosening of this function or of + [fits] — it is a separate predicate that every caller must pair with a + [Cast] on the value, so a node's type never lies about the bits it holds. + Written out rather than using [=] so that adding a case with a function or + a mutable field cannot silently break it. *) let rec equal a b = match a, b with | Int x, Int y -> x = y @@ -202,3 +209,53 @@ let is_equatable = function String -> true | t -> is_comparable t place anything resembling subtyping exists. *) let fits ~expected ~actual = match actual with Never -> true | _ -> equal expected actual + +(* ── Implicit widening, FIX.org 2026-09-20 ──────────────────────────── + Which numeric types a value may move to without the program saying so. + One rule decides every entry: the conversion is admitted exactly when no + value of the source type can come out the other side as a different number. + Narrowing is not on this list and never will be — [(u32 x)] is how an i64 + becomes a u32, because that one can lose. + + Read out of that rule: + + - Same signedness, strictly wider: i8→i16→i32→i64, u8→u16→u32→u64. + - Unsigned into a strictly wider signed: u8→i16, u8/u16→i32, u8/u16/u32→i64. + Every u32 fits in an i64, so nothing is lost. The mirror never holds: + signed into unsigned drops the negatives, at any width. + - Equal width across signedness (i32→u32, u32→i32) is refused for the same + reason — one of the two halves of the range has nowhere to go. + - f32→f64. + - Integer into float only where the float's significand covers the integer + exactly: f64 has 53 bits, so i8/i16/i32/u8/u16/u32 reach it and i64/u64 do + not (2^53+1 is not an f64); f32 has 24, so only i8/i16/u8/u16 reach it. + Odin is looser here and lets any integer into any float. This is the + tighter rule on purpose: a program that wants the lossy one writes (f64 x) + and says so, and loosening later adds programs where tightening later + would break them. + + Nothing else participates. [Bool] is not a number, an [Enum] is its own type + whose whole point is that a bare integer does not fit it, [Dyn] crosses by + boxing and unboxing rather than by this, and a container is invariant: a + [Vec i32] is not a [Vec i64] and a [[i32]] is not a [[i64]], because the + elements would each have to be rewritten and a slice does not own its + bytes. *) +let widens_to ~(from : t) ~(into : t) = + match from, into with + | Int a, Int b -> + if signed a = signed b then bits b > bits a + else (not (signed a)) && signed b && bits b > bits a + | Float F32, Float F64 -> true + | Int a, Float b -> bits a <= (match b with F64 -> 32 | F32 -> 16) + | _ -> false + +(* The type a binary operator's two operands meet at: whichever of the pair the + other one widens into, and nothing otherwise. That is total and it is not a + real lattice — (i32, u32) has no answer here, and inventing i64 for it would + be picking a type neither operand was written at. Equal types answer + themselves, so a caller can use this without checking for that first. *) +let join a b = + if equal a b then Some a + else if widens_to ~from:a ~into:b then Some b + else if widens_to ~from:b ~into:a then Some a + else None