JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A written zero stands where a numeric type variable stands

Browse Source 
pos? over every numeric type from one definition was the motivating
example for milestone 5 and was the one thing the landed generics could
not write: (> x 0) refused with "expected t, found the integer literal
0", because int_literal had no arm for a want that is a type variable.

It has one now, and the bound is what makes it sound rather than
optimistic. Every type numeric? admits is an integer or a float, and an
untyped integer constant is usable at all of them, so there is no
instantiation of a numeric? variable at which the literal has no
meaning. Under a weaker bound there is -- ordered? admits an enum -- so
numeric? is what is asked for and the refusal names it.

The float literal is refused at a type variable even under numeric?,
and that asymmetry is the concrete arms' own: an integer constant is
usable where a float is wanted and a float literal is never usable
where an integer is wanted, so a body written with 0.5 has no meaning
at the integer half of its own bound. Refusing at the definition is
what the abstract pass is for; the alternative is a surprise at
whichever call site first asks for i32.

The node the abstract pass builds is never emitted. Each copy
re-checks the same form with the variable substituted, and that is
where the literal is built at the concrete width and range-checked --
so (+ x 300) is fine at i32 and a refusal at u8, and u8 is where it is
refused.
This commit is contained in:
Joseph Ferano 2026-09-20 20:21:41 +07:00
parent d737625a3f
commit 879a439951
4 changed files with 142 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
lib/check.ml
View File

@ -2701,8 +2701,10 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
let tail = ctx.tail in
ctx.tail <- false;
match e.Ast.e with
| Ast.Int n -> int_literal loc ~want n
| Ast.Byte b -> int_literal loc ~want ~default:Types.U8 (Int64.of_int b)
| Ast.Int n -> int_literal loc ~want ~preds:ctx.env.tvpreds n
| Ast.Byte b ->
int_literal loc ~want ~preds:ctx.env.tvpreds ~default:Types.U8
(Int64.of_int b)
(* The float literal's own dyn case, for the reason the integer's has one:
the ABI carries one width and the literal is built at it. f64 is already
what an unconstrained float literal defaults to, so this only has to stop
@ -2713,6 +2715,27 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
let k =
match want with
| Some (Types.Float k) -> k
(* A float literal at a type variable, refused even under [numeric?] —
the asymmetry with the integer literal above is deliberate and is the
same asymmetry the concrete arms already have. An untyped integer
constant is usable wherever a float is wanted; a float literal is
never usable where an integer is wanted (Odin's rule, stated at the
[Int] case). So [numeric?] admits integers, and a body written with a
float literal has no meaning at the integer half of its own bound.
Refusing here keeps that a refusal at the definition rather than one
that surprises whichever call site first instantiates at [i32]. *)
| Some (Types.Var v) ->
Loc.failk literal_at_want loc
"the float literal %g cannot stand where $%s is wanted: %s may be \
instantiated at an integer type, and a float literal is never \
usable where an integer is wanted. Write the constant as an \
integer literal — that one is admitted under {:where (numeric? \
$%s)} at every numeric type — or take the value as a parameter"
x v
(if declares ctx.env.tvpreds v "numeric?" then
Printf.sprintf "{:where (numeric? $%s)} admits integers too, so $%s" v v
else Printf.sprintf "$%s" v)
v
| Some other when other <> Types.Never ->
Loc.failk literal_at_want loc "expected %s, found the float literal %g"
(Types.to_string other) x
@ -3043,9 +3066,29 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
ctx.defer_block;
register_defer ctx loc forms
and int_literal loc ~want ?(default = Types.I32) n =
and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
match want with
| Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k))
(* An integer literal where a *type variable* is wanted: the abstract pass
over a generic body, checking [(> x 0)] or [(+ x 1)] with [x] at [$t].
It is admitted exactly when [$t] is declared [numeric?], and that bound is
what makes it sound rather than optimistic: every type [numeric?] admits
is an integer or a float, and an untyped integer constant is usable at all
of them — the same rule the [Float k] arm below encodes for a concrete
float. So there is no instantiation of a [numeric?] variable at which this
literal has no meaning, which is the promise the abstract pass exists to
make.
The node built here is never emitted. A generic body produces no code; the
instantiation re-checks the same form with [$t] substituted, and then the
[Int k] or [Float k] arm above builds the literal at the concrete type and
runs the range check. [I64] is the placeholder width and is chosen only so
that a value too wide for [I32] survives the abstract pass to be ranged at
the instantiation that actually has a type — [(defn f [x $t] $t (+ x 300))]
is fine at [i32] and a refusal at [u8], and [u8] is where it is refused. *)
| Some (Types.Var v) when declares preds v "numeric?" ->
mk loc (Types.Var v) (Tast.Int (n, Types.I64))
(* A literal in dyn position takes i64 and not the i32 an unconstrained one
defaults to. This is where "dyn integers are i64" stops being a statement
about the ABI and becomes one about the language: [(defvar x dyn 5)] holds
@ -3060,6 +3103,17 @@ and int_literal loc ~want ?(default = Types.I32) n =
Odin. A float literal is never usable where an integer is wanted. *)
| Some (Types.Float k) ->
mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
(* The same position without the bound. An unconstrained variable supports
only what every type supports, and holding a number is not that, so the
refusal names the bound that would admit it rather than reporting a type
mismatch the programmer cannot act on. *)
| Some (Types.Var v) ->
Loc.failk literal_at_want loc
"the integer literal %Ld cannot stand where $%s is wanted: an \
unconstrained type variable may be instantiated at a type that holds \
no number. Declare the bound — {:where (numeric? $%s)} — and the \
literal is admitted at every type $%s can then be"
n v v v
| Some other when other <> Types.Never ->
Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
(Types.to_string other) n

42
test/programs/generics.flan
View File

@ -50,6 +50,33 @@
{:where (ordered? $t)}
(min (max x lo) hi))
;; An integer *literal* where the type variable is wanted, which is what the
;; author's motivating family needs: one pos? over every numeric type rather
;; than one per width. The literal is admitted because {:where (numeric? $t)}
;; is declared, and the bound is what makes it sound rather than optimistic —
;; every type numeric? admits is an integer or a float, and an untyped integer
;; constant is usable at all of them, so there is no instantiation at which
;; this 0 has no meaning. Without the clause it is refused at the definition;
;; see the rejects in test_flan.ml.
;;
;; The literal is never emitted from here. The abstract pass builds a
;; placeholder and throws it away with the rest of the body; each copy
;; re-checks (> x 0) with $t substituted, and *that* is where the literal is
;; built at the concrete width and range-checked.
(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
(defn neg? [x $t] bool {:where (numeric? $t)} (< x 0))
(defn zero-p? [x $t] bool {:where (numeric? $t)} (= x 0))
;; The same literal in arithmetic rather than comparison, and answering $t
;; rather than bool, so the placeholder has to survive being the operand of a
;; Prim and being returned.
(defn next-after [x $t] $t {:where (numeric? $t)} (+ x 1))
;; The range check is the instantiation's and not the definition's: 300 is
;; fine at i32 and would be a refusal at u8, and u8 is where it is refused.
;; This one is only ever asked for at i32.
(defn plus-300 [x $t] $t {:where (numeric? $t)} (+ x 300))
;; Two variables, and the second is determined by its own argument.
(defn fst [a $t b $u] $t
(do b a))
@ -131,6 +158,21 @@
(println (clamp-to 0.5 1.0 9.0))
(println (fst 8 true))
;; The literal-at-a-type-variable family, at six numeric types from three
;; written bodies. i32, i64, u8, u16, f32 and f64 all reach the same 0 and
;; the same 1.
(println (pos? 3))
(println (neg? (i8 -3)))
(println (zero-p? (u8 0)))
(println (zero-p? 0.0))
(println (pos? (u16 1)))
(println (neg? (f32 -0.5)))
(println (next-after 3))
(println (next-after (i64 10)))
(println (next-after 2.5))
(println (next-after (u8 254)))
(println (plus-300 1))
(show 3)
(show 4.5)
(show "text")

11
test/test_acceptance.ml
View File

@ -2584,9 +2584,18 @@ let () =
scalar types because a default that is returned and one that is
discarded are two different lowerings, and the last pair — [2 0] — is
the same pair at a $t that owns storage, where each answer is a header
onto whichever of the two buffers the branch chose. *)
onto whichever of the two buffers the branch chose.
The six [true]s and the five numbers after the first [8] are the
literal-at-a-type-variable family: three written bodies — pos?/neg?/
zero-p?, next-after and plus-300 — reaching i8, u8, u16, i32, i64, f32
and f64. [255] is next-after at u8 and is the one that would say
whether the placeholder width the abstract pass builds had leaked into
a copy; [301] is plus-300 at i32, whose range check belongs to the copy
and not to the definition. *)
let generics_out =
"3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\
true\ntrue\ntrue\ntrue\ntrue\ntrue\n4\n11\n3.5\n255\n301\n\
3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n\
0\n-1\n2.5\n0\ntrue\nfalse\ntrue\n2\n0\n\
3\n3\n0\n21\n7\n3\n4.5\n"

33
test/test_flan.ml
View File

@ -4711,6 +4711,39 @@ let () =
accepts "and is accepted when it is"
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
(* ── A numeric literal where a type variable is wanted ──────────────
The author's motivating family — one pos? over every numeric type from
one definition — needs a written 0 to stand where $t stands. The bound
is what makes it sound: every type [numeric?] admits is an integer or a
float, and an untyped integer constant is usable at all of them, so
there is no instantiation of a [numeric?] variable at which the literal
has no meaning. That is the whole rule, and the four pins below are its
two halves and its one asymmetry. *)
accepts "an integer literal stands where a numeric? type variable is wanted"
"(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))";
accepts "and in arithmetic, answering the variable"
"(defn next [x $t] $t {:where (numeric? $t)} (+ x 1))";
(* [numeric?] is what admits it and nothing weaker does. [ordered?] admits
an enum, which holds no number, so a literal under it has an
instantiation at which it means nothing — and the refusal below is what
stops that reaching the call site. *)
rejects_check "an unconstrained type variable admits no literal"
~needle:"may be instantiated at a type that holds no number"
"(defn f [x $t] bool (> x 0))";
rejects_check "and ordered? is not the bound that admits one"
~needle:"Declare the bound"
"(defn f [x $t] bool {:where (ordered? $t)} (> x 0))";
(* The asymmetry, and it is the concrete arms' asymmetry rather than a new
one: an untyped integer constant is usable where a float is wanted, and
a float literal is never usable where an integer is wanted. [numeric?]
covers both halves of the numbers, so a body written with a float
literal has no meaning at the integer half of its own bound. Refused at
the definition, which is where the abstract pass promises refusals
arrive — not at whichever call site first asks for i32. *)
rejects_check "a float literal is refused at a type variable even under numeric?"
~needle:"may be instantiated at an integer type"
"(defn half [x $t] $t {:where (numeric? $t)} (* x 0.5))";
(* A map key that is a type variable has no hash and no equality to emit:
they are chosen from the concrete type, which does not exist yet. So the
map operations join print and println on the list of forms the abstract