integer? bounds the integer-only bodies, and abs is one generic
The fifth predicate: integer? admits every integer kind and no float, entails numeric? (and through it ordered? and equal?), and gates what only integers support — the bitwise fold asks for it, the shifts admit a bounded variable under it, and the float literal in an integer? body is refused in the bound's own words. The literal arm needed nothing: the entailment admits an integer constant under either bound. abs-i32 and abs-i64 collapse into one integer?-bounded generic whose i32/i64 copies even keep the old symbols; abs-f32/abs-f64 stay as the float spellings because the right float abs is a sign-bit clear no integer body spells, and (abs 1.5) now refuses naming the bound — the where clause is checked before the name-collision check, which used to answer that call with 'abs-f64 is already defined'. Mixed widths at one $t join at the wider type now, in either argument order — the author reversed the refuse-both rule on 2026-09-20. A joinless pair is deferred and re-asked against the final binding, so a later wider argument settles u32-vs-i32; u64-vs-i64 still refuses, and a container-bound variable still binds exactly. The out-widened arguments catch up through the ordinary Cast. Two review follow-ups folded in: a struct field's unknown-lowercase message stops suggesting a parameter vector it does not have, and the tyvar-at-dyn message says defgeneric/defmethod in words instead of a schematic that does not compile.
This commit is contained in:
parent
c20a4b90dc
commit
f71cc40bb5
108
FIX.org
108
FIX.org
@ -3789,3 +3789,111 @@ spec-memory.md's Generics section gained the three rules this lane decided —
|
||||
the literal under ~numeric?~, the widening boundary, and dyn — because the
|
||||
spike banner names that section and plan.org's Types as the current account,
|
||||
and all three are observable from a program.
|
||||
|
||||
* integer?, the collapsed abs, and the join, 2026-09-20
|
||||
The author's brief, verbatim in spirit: we want generic arithmetic as much as
|
||||
possible; we are failing if a function that can be generalized needs variants
|
||||
for different numerical types.
|
||||
|
||||
** integer?, the fifth predicate
|
||||
~numeric?~ was one type too wide for a family of bodies. It is the only bound
|
||||
that admits a written 0, and it admits f32 and f64 too — so an integer body
|
||||
under it was instantiated at the floats, where ~(if (< x 0) (- 0 x) x)~ is
|
||||
the wrong abs (a -0.0 comes back negative) and the bitwise operators, the
|
||||
shifts and an integer-only ~%~ mean nothing at all. ~integer?~ admits every
|
||||
integer kind, signed and unsigned, at every width, and refuses floats and
|
||||
everything else: ~Types.is_integer~, wired into ~predicate_names~,
|
||||
~pred_holds~ and the entailment table.
|
||||
|
||||
The entailments run one way. ~integer?~ entails ~numeric?~ — every integer is
|
||||
a number, so the arithmetic, the written 0 and the untyped integer literal
|
||||
all come with the one clause, through the same ~int_literal~ arm ~numeric?~
|
||||
uses — and through it ~ordered?~ and ~equal?~. The reverse does not exist,
|
||||
because it would let floats into ~bit-and~.
|
||||
|
||||
What it unlocked in the checker: the bitwise fold asks ~unconstrained~ for
|
||||
~integer?~ now instead of ~numeric?~ (so ~(bit-and x 1)~ in a ~numeric?~ body
|
||||
is refused at the *definition*, not from inside the generic's source at
|
||||
whichever call site first instantiated at a float), and the shifts admit an
|
||||
~integer?~-bounded variable where they refused every variable before. The
|
||||
float literal in an ~integer?~-bounded body gets the bound's own sentence:
|
||||
there is no instantiation at which it means anything. ~%~ stays ~numeric?~
|
||||
deliberately — a typed float ~(% x y)~ is fmod and always was
|
||||
(test/programs/math3.flan pins the four sign cases), and tightening it would
|
||||
be a semantics change this predicate does not ask for.
|
||||
|
||||
** abs, collapsed
|
||||
~abs-i32~ and ~abs-i64~ existed per width only because ~numeric?~ admitted
|
||||
floats. They are one ~(defn abs [x $t] $t {:where (integer? $t)} ...)~ now,
|
||||
answering at all six-and-more integer widths; the copies at i32 and i64 even
|
||||
keep the old symbols, since an instantiation mangles to ~abs-i32~ and
|
||||
~abs-i64~.
|
||||
|
||||
The decision between "integer? plus the float overloads" and "one numeric?
|
||||
generic with a float-safe body": there is no float-safe body to write. ~(max
|
||||
x (- 0 x))~ picks whichever zero sits in the wrong slot because -0.0 and 0.0
|
||||
compare equal, and the branch spelling hands -0.0 back unchanged. The right
|
||||
float abs is a sign-bit clear, which is libm's fabs and is already declared —
|
||||
~abs-f32~/~abs-f64~ stay as the float spellings, and ~(abs 1.5)~ is refused
|
||||
naming the bound. For that refusal to be the one a float caller sees,
|
||||
~instantiate~ now checks the ~where~ clause *before* the name-collision
|
||||
check; before the reorder, ~(abs 1.5)~ computed the sym ~abs-f64~ and died on
|
||||
"already defined — rename one of them", which is the wrong sentence with no
|
||||
fix in it.
|
||||
|
||||
Behaviour pinned identical: both signed minimums answer themselves (the
|
||||
negation wraps, as every two's-complement abs), unsigned is the identity,
|
||||
~(abs-f64 -0.0)~ is 0. test/programs/int-generic.flan, plus the math3 rows.
|
||||
|
||||
** The survey — what else numeric?-admits-floats was keeping per-width
|
||||
The prelude's remaining per-width families, each left with its reason:
|
||||
- ~sum-i32~/~sum-f32~ — the accumulator is a *different, wider* type than the
|
||||
element ("the type $t accumulates into" is a type-level function no
|
||||
predicate spells); their own comment already says so.
|
||||
- ~append-i64~/~append-f64~ — two different runtime primitives.
|
||||
- ~parse-i64~/~parse-f64~ — the variable would appear only in the return
|
||||
type, which no argument determines and no syntax names.
|
||||
- ~rand-i32-range~/~rand-f32-range~ — two different algorithms (Lemire
|
||||
rejection vs. scale), not one body twice.
|
||||
- ~sign-f32~ — its integer twin would write -1, which has no meaning at the
|
||||
unsigned half of ~integer?~; a bound spelling "signed" does not exist and
|
||||
is not asked for.
|
||||
- ~min~/~max~ — builtins by decision (variadic, evaluate-once), untouched.
|
||||
- The libm pairs — declares, one C symbol each; nothing to collapse.
|
||||
So the survey's whole yield is abs, plus the *checker* generalizations above
|
||||
that let user code write generic bit/shift/mod helpers it could not write at
|
||||
all before (int-generic.flan's ~low-bits~, ~even?~, ~toggle~, ~halve~).
|
||||
|
||||
** The join, superseding "widening does not cross a generic binding"
|
||||
The 2026-09-20 milestone-5 entry above took refusal as the walk-backable
|
||||
direction and recorded the join as the coherent alternative. The author
|
||||
walked it back the same day: *just pick the wider type for both.* The old
|
||||
entry stands as written; this one supersedes it.
|
||||
|
||||
The rule as landed: numeric scalars bound to one ~$t~ resolve it to
|
||||
whichever written type every one of them widens into — ~Types.join~, so
|
||||
value-preserving widening only, never an invented third type... except that
|
||||
an upper bound *in the set* found through a later argument is exactly that:
|
||||
~(tri u32 i32 i64)~ has no join at the second argument and a perfectly good
|
||||
one at the third, so a joinless pair is deferred and re-asked against the
|
||||
final binding rather than refused on the spot. That is what makes acceptance
|
||||
order-independent, which is pinned two ways: both orders accept, and both
|
||||
orders of the whole program instantiate exactly one copy, at the wider type
|
||||
(the pin counts ~eq2?-i64~ in the checked program's functions).
|
||||
|
||||
Still refused, each in its own words: a pair with no join anywhere (u64
|
||||
against i64 — no type holds every value of both), and a variable the
|
||||
signature also reaches through a container or function type (~index-of~'s
|
||||
slice binds its element exactly; elements cannot be rewritten wider). The
|
||||
arguments the final binding out-widened catch up through the same ~Cast~
|
||||
node the written conversion builds, so the emitted copy never sees the
|
||||
narrow type. Literals still decide as before — a bare literal at a bound
|
||||
~$t~ takes the binding — and spec-memory.md's Generics section now carries
|
||||
the joined rule.
|
||||
|
||||
** Still refused, known, deferred
|
||||
A *compound constant expression* at a bounded ~$t~ — ~(+ x (+ 1 2))~ where
|
||||
~(+ x 3)~ works — is still refused: the literal arm admits a bare constant
|
||||
at a type variable, and nothing folds the compound to a bare one before the
|
||||
ask. Walk-backable (admitting more programs later invalidates nothing
|
||||
written now), so it waits until a body actually wants it.
|
||||
|
||||
304
lib/check.ml
304
lib/check.ml
@ -169,6 +169,14 @@ type env = {
|
||||
chain. Odin has no cap of its own to copy, so there was nothing to
|
||||
borrow. *)
|
||||
mutable chain : (string * Types.t list * Loc.t) list;
|
||||
(* Set while a struct, data-case or union field's type is being resolved,
|
||||
and only then. It exists for one message: an unknown lowercase name in a
|
||||
type slot is told to introduce a type variable with [$name] in the
|
||||
parameter vector, and a field has no parameter vector — only a defn
|
||||
signature binds, and a field is built at one type for every value. The
|
||||
flag is what lets [resolve_name] say the honest thing in each place
|
||||
instead of a suggestion that cannot be followed. *)
|
||||
mutable in_field : bool;
|
||||
}
|
||||
|
||||
let new_env () = {
|
||||
@ -196,6 +204,7 @@ let new_env () = {
|
||||
subst = [];
|
||||
tvpreds = [];
|
||||
chain = [];
|
||||
in_field = false;
|
||||
}
|
||||
|
||||
(* Where a named type was declared, and what it has, as a note.
|
||||
@ -618,10 +627,18 @@ let unimplemented loc what milestone =
|
||||
|
||||
Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is
|
||||
[where intrinsics.type_is_ordered(T)]) with forty-one predicates against
|
||||
these four. There is no [copyable?] any more and no Odin counterpart
|
||||
these five. There is no [copyable?] any more and no Odin counterpart
|
||||
either: Odin has no move semantics, and since the repeal neither does this
|
||||
language, so [$T] never has to answer the question. *)
|
||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?" ]
|
||||
language, so [$T] never has to answer the question.
|
||||
|
||||
[integer?] is the narrowest of the five and exists because [numeric?] was
|
||||
one type too wide for a family of bodies: an integer body under [numeric?]
|
||||
is instantiated at f32 and f64 too, and (if (< x 0) (- 0 x) x) at -0.0 is
|
||||
the wrong abs while %, the bitwise operators and the shifts have no float
|
||||
meaning at all. A function that can be generalized should not need a
|
||||
variant per numeric type, and [integer?] is what lets the integer-only
|
||||
ones say exactly what they need. *)
|
||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "integer?" ]
|
||||
|
||||
(* ── What a type owns, transitively ────────────────────────────────────
|
||||
The one structural ownership question that survived the repeal, because it
|
||||
@ -693,6 +710,7 @@ let pred_holds p (t : Types.t) =
|
||||
[key_pair]. *)
|
||||
| "hashable?" -> Types.keyable t
|
||||
| "numeric?" -> Types.is_numeric t
|
||||
| "integer?" -> Types.is_integer t
|
||||
| _ -> false
|
||||
|
||||
(* What one declared predicate *also* gives you. These are entailments over
|
||||
@ -705,8 +723,14 @@ let pred_holds p (t : Types.t) =
|
||||
let pred_entails ~declared ~wanted =
|
||||
String.equal declared wanted
|
||||
|| match wanted, declared with
|
||||
| "ordered?", "numeric?" -> true
|
||||
| "equal?", ("numeric?" | "ordered?") -> true
|
||||
| "ordered?", ("numeric?" | "integer?") -> true
|
||||
| "equal?", ("numeric?" | "ordered?" | "integer?") -> true
|
||||
(* Every integer type is a number, so [integer?] gives a body everything
|
||||
[numeric?] does — the arithmetic, the written 0, the untyped integer
|
||||
literal — on top of the operations only it admits. The reverse is
|
||||
never true: [numeric?] admits floats, which is exactly what a body
|
||||
under [integer?] is promising it never meets. *)
|
||||
| "numeric?", "integer?" -> true
|
||||
| _ -> false
|
||||
|
||||
let declares preds v wanted =
|
||||
@ -1027,11 +1051,25 @@ and resolve_name env ~seen loc n =
|
||||
silently became a type parameter and made the signature more
|
||||
permissive than it was written to be. *)
|
||||
| _ when n <> "" && n.[0] = Char.lowercase_ascii n.[0] ->
|
||||
Loc.failk "check/unknown-type" loc
|
||||
"unknown type %s. A lowercase name is a type variable only where a \
|
||||
defn signature introduced it — write $%s in the parameter vector \
|
||||
to introduce one, and %s reads it from there"
|
||||
n n n
|
||||
(* The parameter-vector suggestion is only followable where a
|
||||
parameter vector exists. A field has none and never will — only a
|
||||
defn signature binds a variable, and a field is built at one type
|
||||
for every value — so at a field the message offers the two things
|
||||
that can actually be written there. *)
|
||||
if env.in_field then
|
||||
Loc.failk "check/unknown-type" loc
|
||||
"unknown type %s. A lowercase name is a type variable, and a \
|
||||
field cannot hold one: only a defn signature introduces type \
|
||||
variables, and a field is built at one type for every value — \
|
||||
generic types are not there. Write a concrete type here, or dyn \
|
||||
to hold any value"
|
||||
n
|
||||
else
|
||||
Loc.failk "check/unknown-type" loc
|
||||
"unknown type %s. A lowercase name is a type variable only where a \
|
||||
defn signature introduced it — write $%s in the parameter vector \
|
||||
to introduce one, and %s reads it from there"
|
||||
n n n
|
||||
| _ -> Loc.failk "check/unknown-type" loc "unknown type %s" n
|
||||
|
||||
and array_len env loc = function
|
||||
@ -2813,17 +2851,28 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
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
|
||||
(* Under {:where (integer? $t)} the sentence is simpler and its own:
|
||||
the bound has no float half at all, so the literal has no meaning
|
||||
at *any* type the variable can become, not merely at some. *)
|
||||
if declares ctx.env.tvpreds v "integer?" then
|
||||
Loc.failk literal_at_want loc
|
||||
"the float literal %g cannot stand where $%s is wanted: \
|
||||
{:where (integer? $%s)} admits no float type, so there is no \
|
||||
instantiation at which this literal means anything. Write an \
|
||||
integer literal, or take the value as a parameter"
|
||||
x v v
|
||||
else
|
||||
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
|
||||
@ -5248,7 +5297,7 @@ and not_numeric name what (a : Tast.expr) =
|
||||
else
|
||||
fail where "%s takes %s, found %s" name what (Types.to_string a.Tast.ty)
|
||||
|
||||
and fold_left_prim ctx ~want loc name p ok what args =
|
||||
and fold_left_prim ctx ~want loc name p ~needs ok what args =
|
||||
let x, y, rest =
|
||||
match args with x :: y :: rest -> x, y, rest | _ -> assert false
|
||||
in
|
||||
@ -5259,7 +5308,13 @@ and fold_left_prim ctx ~want loc name p ok what args =
|
||||
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
|
||||
dyn_fold ctx ~want loc name [ a; b ] rest
|
||||
else begin
|
||||
unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
|
||||
(* [~needs] is the operator's own bound: [numeric?] for the arithmetic,
|
||||
[integer?] for the bitwise fold. Asking the tighter question here is what
|
||||
keeps a bitwise body's refusal at the *definition* — under [numeric?] the
|
||||
abstract pass admitted [(bit-and x 1)] and the refusal arrived from
|
||||
inside the generic's source at whichever call site first instantiated at
|
||||
a float, which is the misplaced diagnostic the pass exists to avoid. *)
|
||||
unconstrained ctx.env loc name ~needs a.Tast.ty;
|
||||
(* Past [unconstrained] a variable here is one the [where] clause admitted,
|
||||
so the concrete predicate below has nothing to say about it — it is
|
||||
answered again, per copy, at the instantiation. *)
|
||||
@ -5617,7 +5672,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
| _ -> Tast.Div
|
||||
in
|
||||
fold_arity loc name args;
|
||||
fold_left_prim ctx ~want loc name p Types.is_numeric "numbers" args
|
||||
fold_left_prim ctx ~want loc name p ~needs:"numeric?" Types.is_numeric
|
||||
"numbers" args
|
||||
(* Remainder stays at two: (% a b c) is (% (% a b) c), which is a thing
|
||||
nobody writes on purpose. *)
|
||||
| "%" ->
|
||||
@ -5718,8 +5774,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
| _ -> Tast.BitXor
|
||||
in
|
||||
fold_arity loc name args;
|
||||
fold_left_prim ctx ~want loc name p
|
||||
(function Types.Int _ -> true | _ -> false) "integers" args
|
||||
fold_left_prim ctx ~want loc name p ~needs:"integer?" Types.is_integer
|
||||
"integers" args
|
||||
(* The shifts stay at two, and not only because a shift chain reads badly:
|
||||
each count would be checked against the same width below, so (<< x 30 30)
|
||||
would pass two legal shifts and still shift the value away entirely.
|
||||
@ -5738,6 +5794,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
let a, b = binary ctx ~join:false name loc ~want:(numeric_want want) args in
|
||||
(match a.Tast.ty with
|
||||
| Types.Int _ -> ()
|
||||
(* A type variable under {:where (integer? $t)}: every type the bound
|
||||
admits has a width to shift within, so the abstract pass lets the
|
||||
body through and each instantiation meets the concrete checks below
|
||||
at its own width. Anything weaker — [numeric?] included — is refused
|
||||
here, at the definition, because a shift at f32 means nothing. *)
|
||||
| t when generic_ty t ->
|
||||
unconstrained ctx.env loc name ~needs:"integer?" t
|
||||
| other -> fail loc "%s takes integers, found %s" name
|
||||
(Types.to_string other));
|
||||
(* A shift by the operand's own width or more is poison in LLVM, which at
|
||||
@ -7627,6 +7690,33 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
take its types from. Left to right, which is the order Odin's operands
|
||||
are gathered in and the order [map2_lr] already guarantees. *)
|
||||
let subst = ref [] in
|
||||
(* Does the signature bind [v] anywhere *inside* a type — [[$t]],
|
||||
[(Fn [$t $t] bool)], [(Vec $t)]? A bare [$t] parameter is a scalar the
|
||||
join below may move; a variable reached through a constructor is bound
|
||||
exactly, because a container's elements cannot be rewritten and a
|
||||
function value's type is its own. One scan, answered per variable. *)
|
||||
let rec mentions v (t : Types.t) =
|
||||
match t with
|
||||
| Types.Var u -> String.equal u v
|
||||
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
|
||||
| Types.Option e -> mentions v e
|
||||
| Types.Map (k, w) -> mentions v k || mentions v w
|
||||
| Types.Fn (ps, r) -> List.exists (mentions v) ps || mentions v r
|
||||
| _ -> false
|
||||
in
|
||||
let bound_exactly v =
|
||||
List.exists
|
||||
(fun (p : Types.t) ->
|
||||
match p with Types.Var _ -> false | t -> mentions v t)
|
||||
pats
|
||||
in
|
||||
(* Pairs that met no join while the arguments were walked. They are not
|
||||
refused on the spot because a *later* argument can still settle them:
|
||||
(f u32-x i32-y i64-z) has no join at the second argument and a perfectly
|
||||
good one — i64, which both widen into — at the third. Each entry is
|
||||
re-asked against the final binding below, so acceptance cannot depend on
|
||||
the order the arguments were written in. *)
|
||||
let pending = ref [] in
|
||||
let targs =
|
||||
map2_lr
|
||||
(fun pat a ->
|
||||
@ -7664,44 +7754,55 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
| Error _ -> check ctx ~want:p a)
|
||||
else check ctx ~want:p a
|
||||
in
|
||||
(* **Implicit widening does not cross a generic binding.** A concrete
|
||||
argument at a variable an earlier argument already bound has to be
|
||||
the same type, not merely a type that widens into it.
|
||||
(* **Mixed widths at one variable join at the wider type.** The rule
|
||||
used to refuse the pair both ways — FIX.org, "Generics and
|
||||
implicit widening", recorded the join as the coherent alternative
|
||||
and refusing as the direction that could be walked back. It was
|
||||
walked back on 2026-09-20, by the author: a numeric argument at a
|
||||
variable an earlier argument already bound resolves the variable
|
||||
to whichever of the pair the other widens into, value-preserving
|
||||
widening only, so [(eq2? (i8 3) (i64 3))] and its reverse are one
|
||||
copy at i64. A pair with no join — u64 against i64 — is still
|
||||
refused: there is no type that holds every value of both, and
|
||||
inventing one would be picking a type neither argument was
|
||||
written at.
|
||||
|
||||
This is a decision and not a consequence. Widening landed after
|
||||
generics did, and left behind a rule that depended on argument
|
||||
order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
|
||||
first and the i8 widened into the want; [(pair-eq? i8 i64)] was
|
||||
refused, because [$t] bound to i8 and i64 into i8 can lose. Same
|
||||
two values, same function, two answers. Neither is unsound — a
|
||||
widen cannot change a number — but which instantiation a program
|
||||
gets should not depend on which argument was written first.
|
||||
|
||||
Refusing both is the direction that can be walked back. Allowing
|
||||
the pair to join at the wider type is a coherent rule too, and it
|
||||
is the one to reach for if the ergonomics turn out to want it; it
|
||||
can be added later without invalidating a program that was written
|
||||
under this rule, and the reverse is not true. FIX.org, "Generics
|
||||
and implicit widening". *)
|
||||
(* Only where the pair is one widening had an opinion about. A string
|
||||
passed where $t was bound to i64 is an ordinary mismatch and gets
|
||||
the ordinary refusal; the sentence below is about the conversion
|
||||
that no longer happens, and it would read as a non-sequitur over a
|
||||
pair that never had one available. *)
|
||||
(match bound_scalar with
|
||||
| Some v
|
||||
when (not (Types.equal p a.Tast.ty))
|
||||
&& Types.is_numeric a.Tast.ty ->
|
||||
Loc.failk "check/tyvar-no-widening" a.Tast.loc
|
||||
"%s's $%s was bound to %s by an earlier argument, and this one \
|
||||
is %s. Implicit widening does not cross a generic binding: a \
|
||||
written type is what a type variable takes, so the same \
|
||||
variable is the same type at every argument. Write the \
|
||||
conversion — (%s x) — or pass the arguments at one type"
|
||||
name v (Types.to_string p) (Types.to_string a.Tast.ty)
|
||||
(Types.to_string p)
|
||||
| _ -> ());
|
||||
if not (bind_ty subst p a.Tast.ty) then
|
||||
Only where the variable is bound by bare scalars. A variable the
|
||||
signature also reaches through a container is bound exactly —
|
||||
a slice's elements cannot be rewritten to a wider width — so
|
||||
those keep the refusal, in their own words. And only where the
|
||||
pair is one widening has an opinion about: a string where $t was
|
||||
bound to i64 is an ordinary mismatch and gets the ordinary
|
||||
refusal below. *)
|
||||
let handled =
|
||||
match bound_scalar with
|
||||
| Some v
|
||||
when (not (Types.equal p a.Tast.ty))
|
||||
&& Types.is_numeric a.Tast.ty ->
|
||||
(match Types.join p a.Tast.ty with
|
||||
| Some j when Types.equal j p ->
|
||||
(* This argument widens into the binding; the wrap happens
|
||||
with the others, once the binding is final. *)
|
||||
true
|
||||
| Some j when not (bound_exactly v) ->
|
||||
subst := (v, j) :: List.remove_assoc v !subst;
|
||||
true
|
||||
| Some _ ->
|
||||
Loc.failk "check/tyvar-no-widening" a.Tast.loc
|
||||
"%s's $%s was bound to %s by an earlier argument, and this \
|
||||
one is %s. The signature also binds $%s inside a \
|
||||
container or function type, which binds its element \
|
||||
exactly — the pair cannot join at the wider type there. \
|
||||
Write the conversion — (%s x) — or pass the arguments at \
|
||||
one type"
|
||||
name v (Types.to_string p) (Types.to_string a.Tast.ty) v
|
||||
(Types.to_string p)
|
||||
| None ->
|
||||
pending := (v, p, a.Tast.ty, a.Tast.loc) :: !pending;
|
||||
true)
|
||||
| _ -> false
|
||||
in
|
||||
if (not handled) && not (bind_ty subst p a.Tast.ty) then
|
||||
fail a.Tast.loc "%s expects %s here, found %s" name
|
||||
(Types.to_string p) (Types.to_string a.Tast.ty);
|
||||
a)
|
||||
@ -7719,6 +7820,44 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
generic function is instantiated from its call site, and there is \
|
||||
no syntax for naming the type" name v)
|
||||
vars;
|
||||
(* The pairs that met no join, re-asked now that every argument has spoken.
|
||||
A later, wider argument dissolves one — u32 and i32 both widen into an
|
||||
i64 that arrived third — and one still standing is the real refusal:
|
||||
these two widths meet at no type. *)
|
||||
List.iter
|
||||
(fun (v, t1, t2, ploc) ->
|
||||
let final = List.assoc v !subst in
|
||||
let fits t =
|
||||
Types.equal t final || Types.widens_to ~from:t ~into:final
|
||||
in
|
||||
if not (fits t1 && fits t2) then
|
||||
Loc.failk "check/tyvar-no-join" ploc
|
||||
"this call binds %s's $%s to both %s and %s, and the two meet at \
|
||||
no type: implicit widening only ever widens — every value kept, \
|
||||
no sign lost — and neither of these holds every value of the \
|
||||
other. Write the conversion you mean at one of the arguments, or \
|
||||
pass them at one type"
|
||||
name v (Types.to_string t1) (Types.to_string t2))
|
||||
!pending;
|
||||
(* The binding is final; the arguments it out-widened catch up. Only a bare
|
||||
[$t] parameter can be here — [bound_exactly] kept every container-bound
|
||||
variable at one exact type — and the cast is the same node the written
|
||||
conversion would have built. *)
|
||||
let targs =
|
||||
map2_lr
|
||||
(fun (pat : Types.t) a ->
|
||||
match pat with
|
||||
| Types.Var v ->
|
||||
(match List.assoc_opt v !subst with
|
||||
| Some f
|
||||
when (not (Types.equal f a.Tast.ty))
|
||||
&& Types.is_numeric a.Tast.ty
|
||||
&& Types.widens_to ~from:a.Tast.ty ~into:f ->
|
||||
widen a.Tast.loc f a
|
||||
| _ -> a)
|
||||
| _ -> a)
|
||||
pats targs
|
||||
in
|
||||
(* **A type variable is not instantiated at dyn.** Nothing stopped it before:
|
||||
[dyn] is an ordinary case of [Types.t], so it substituted like any other
|
||||
type and a copy was generated at it. The copy then reached whatever the
|
||||
@ -7757,11 +7896,11 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
"this call would instantiate %s at $%s = %s, and a type variable \
|
||||
is not instantiated at dyn: a copy is made per *written* type, \
|
||||
and dyn is the one type whose own type is not known until it \
|
||||
runs. One value, two models — (defgeneric %s [...]) with a \
|
||||
(defmethod ...) per class dispatches on what the value turns out \
|
||||
to be, which is the question a dyn argument is asking. Write the \
|
||||
type the value has, or reach for the dyn side"
|
||||
name v (Types.to_string t) name)
|
||||
runs. One value, two models — a defgeneric with a defmethod per \
|
||||
class dispatches on what the value turns out to be, which is the \
|
||||
question a dyn argument is asking. Write the type the value has, \
|
||||
or reach for the dyn side"
|
||||
name v (Types.to_string t))
|
||||
!subst;
|
||||
let cparams = List.map (subst_ty !subst) pats in
|
||||
let cret = subst_ty !subst pret in
|
||||
@ -7829,15 +7968,18 @@ and instantiate env loc gname vars subst cparams cret =
|
||||
gname ^ "-"
|
||||
^ String.concat "-" (List.map (fun v -> mangle_ty (List.assoc v subst)) vars)
|
||||
in
|
||||
if Hashtbl.mem env.fns sym then
|
||||
fail loc
|
||||
"%s at these types is called %s, and %s is already defined — rename \
|
||||
one of them" gname sym sym;
|
||||
runaway env loc gname cparams;
|
||||
(* Each instantiation checks the concrete types answer the [where] clause.
|
||||
This is the half of the feature that only exists per copy: the abstract
|
||||
pass took the predicates on trust, and here is where the trust is
|
||||
settled, at the call site that asked, naming it. *)
|
||||
settled, at the call site that asked, naming it.
|
||||
|
||||
Before the name-collision check, on purpose. The prelude keeps a
|
||||
per-width family beside a generic where the generic's bound refuses
|
||||
some widths — [abs] under [integer?] beside the declared [abs-f32] and
|
||||
[abs-f64] — so a float caller of [abs] computes the sym [abs-f64], and
|
||||
"abs-f64 is already defined, rename one of them" is the wrong sentence
|
||||
for what went wrong: the bound refused the type, and that is the
|
||||
message with the fix in it. *)
|
||||
let fn = Hashtbl.find env.generics gname in
|
||||
List.iter
|
||||
(fun (p : Ast.pred) ->
|
||||
@ -7854,6 +7996,11 @@ and instantiate env loc gname vars subst cparams cret =
|
||||
gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
|
||||
p.Ast.pname gname p.Ast.pname p.Ast.pvar)
|
||||
fn.Ast.fwhere;
|
||||
if Hashtbl.mem env.fns sym then
|
||||
fail loc
|
||||
"%s at these types is called %s, and %s is already defined — rename \
|
||||
one of them" gname sym sym;
|
||||
runaway env loc gname cparams;
|
||||
(* The entry goes in *before* the body is checked, which is what makes a
|
||||
recursive generic function terminate: the call to itself at the same
|
||||
types finds this and does not generate a second copy. *)
|
||||
@ -8637,7 +8784,14 @@ let collect env (decls : Ast.decl list) =
|
||||
in
|
||||
while fold_consts () do () done;
|
||||
let field (f : Ast.field) : Tast.field =
|
||||
let fty = resolve env f.Ast.fty in
|
||||
(* The flag is reset through [Fun.protect] because a refusal here does not
|
||||
end the run: [program_all] carries on collecting diagnostics, and a
|
||||
flag left set would misword every later unknown-type message. *)
|
||||
env.in_field <- true;
|
||||
let fty =
|
||||
Fun.protect ~finally:(fun () -> env.in_field <- false)
|
||||
(fun () -> resolve env f.Ast.fty)
|
||||
in
|
||||
no_zeroed_fn f.Ast.fty.Ast.tloc
|
||||
(Printf.sprintf "the field %s" f.Ast.fname) fty;
|
||||
{ Tast.fname = f.Ast.fname; fty }
|
||||
|
||||
@ -985,34 +985,32 @@ let source = {flan|
|
||||
(declare cbrt-f32 [x f32] f32 "cbrtf")
|
||||
(declare cbrt-f64 [x f64] f64 "cbrt")
|
||||
|
||||
;; Integer magnitude, one per width, and the reason it stays that way changed
|
||||
;; when generics landed. The old one — no generics over the numeric types —
|
||||
;; is not true any more: (defn abs [x $t] $t {:where (numeric? $t)} (if (< x
|
||||
;; 0) (- 0 x) x)) checks and runs at every integer width, and the literal 0
|
||||
;; stands there because the clause admits it.
|
||||
;; Integer magnitude, one body for every integer width. The per-width pair —
|
||||
;; abs-i32 and abs-i64 — waited here on a bound that spells "an integer
|
||||
;; type", and integer? is that bound, so they collapsed into this on
|
||||
;; 2026-09-20 (FIX.org).
|
||||
;;
|
||||
;; **What stops it is the float half of its own bound.** numeric? is the only
|
||||
;; predicate that admits a written 0, and it admits f32 and f64 too — so a
|
||||
;; generic abs would be instantiated at them, and the body above is the wrong
|
||||
;; abs for a float: (< -0.0 0) is false, so it hands back a negative zero
|
||||
;; from a function named abs. The float pair below is libm's for exactly that
|
||||
;; reason, a sign-bit clear rather than a negation, and a generic that shadows
|
||||
;; it at f32 would be a quiet wrong answer rather than a tidier prelude.
|
||||
;;
|
||||
;; So the collapse waits on a bound that spells "an integer type" — an
|
||||
;; integer? predicate, which is language surface and not this file's call.
|
||||
;; FIX.org, "Generics and implicit widening", records it as the candidate.
|
||||
;; Two functions is the honest price until then.
|
||||
;; **The bound is integer? and not numeric?, and that is the whole design.**
|
||||
;; numeric? admits f32 and f64, and this body is the wrong abs for a float:
|
||||
;; (< -0.0 0) is false, so it hands back a negative zero from a function
|
||||
;; named abs. There is no float-safe spelling of the body either — (max x
|
||||
;; (- 0 x)) picks whichever zero sits in the wrong slot, since -0.0 and 0.0
|
||||
;; compare equal. The right float abs is a sign-bit clear, which is libm's
|
||||
;; fabs, declared above as abs-f32 and abs-f64; a caller with a float writes
|
||||
;; those, and (abs 1.5) is refused with the bound named rather than shadowing
|
||||
;; them with a quiet wrong answer. One capability, one spelling per side of
|
||||
;; the integer/float line — not one per width, which is what this collapse
|
||||
;; ends.
|
||||
;;
|
||||
;; The most negative value of each width has no positive counterpart, and this
|
||||
;; does not special-case it: the subtraction is the same subtraction written
|
||||
;; anywhere else and meets whatever the build's overflow rule is. Saturating
|
||||
;; to the maximum would be a wrong answer returned quietly, which is the one
|
||||
;; thing this file does not do.
|
||||
(defn abs-i32 [x i32] i32
|
||||
(if (< x 0) (- 0 x) x))
|
||||
|
||||
(defn abs-i64 [x i64] i64
|
||||
;; thing this file does not do. The unsigned instantiations are the identity,
|
||||
;; for the reason pos? gives about its own: a generic is copied per written
|
||||
;; type, and at a u32 the body says what it says.
|
||||
(defn abs [x $t] $t
|
||||
{:where (integer? $t)}
|
||||
(if (< x 0) (- 0 x) x))
|
||||
|
||||
;; pi and tau at both widths, because a defconst has a type and a cast between
|
||||
|
||||
@ -172,6 +172,13 @@ let rec to_string = function
|
||||
|
||||
let is_numeric = function Int _ | Float _ -> true | _ -> false
|
||||
|
||||
(* Every integer kind, signed and unsigned, at every width — and nothing
|
||||
else. This is [integer?]'s question: the bound that admits a body written
|
||||
with %, the bitwise operators or the shifts, and that keeps the same body
|
||||
from ever being instantiated at a float, where those operations either do
|
||||
not exist or mean something different. *)
|
||||
let is_integer = function Int _ -> true | _ -> false
|
||||
|
||||
(* The key types the first Map implementation admits (spec-memory.md, "Maps —
|
||||
first implementation"): integers, enums, strings, fixed arrays, and value
|
||||
structs composed recursively from those. Equality and hashing for them are
|
||||
|
||||
@ -254,13 +254,17 @@ instantiates it:
|
||||
> field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
|
||||
|
||||
What makes that liveable is a `where` clause of compile-time type predicates,
|
||||
written as a map at the head of the body. There are four — `ordered?`,
|
||||
`equal?`, `hashable?`, `numeric?` — they are not type classes because a
|
||||
predicate carries no implementations and merely gates a builtin the compiler
|
||||
already has, and they entail one another in one direction, so one clause
|
||||
usually does. (`copyable?` was the fifth until the second repeal removed the
|
||||
move concept it opted out of.) plan.org's Types section has the full
|
||||
account.
|
||||
written as a map at the head of the body. There are five — `ordered?`,
|
||||
`equal?`, `hashable?`, `numeric?`, `integer?` — they are not type classes
|
||||
because a predicate carries no implementations and merely gates a builtin the
|
||||
compiler already has, and they entail one another in one direction, so one
|
||||
clause usually does: `integer?` admits every integer kind and no float, and
|
||||
entails `numeric?`, which entails `ordered?`, which entails `equal?`.
|
||||
`integer?` is what admits the bitwise operators, the shifts and an
|
||||
integer-only body like `abs`'s — under `numeric?` those bodies would be
|
||||
instantiated at the floats too (FIX.org 2026-09-20). (`copyable?` was once a
|
||||
sixth until the second repeal removed the move concept it opted out of.)
|
||||
plan.org's Types section has the full account.
|
||||
|
||||
```
|
||||
(defn sort [s [$t]] ()
|
||||
@ -314,12 +318,16 @@ at a type variable even under `numeric?`, because `numeric?` covers the
|
||||
integers too and a float literal is never usable where an integer is wanted.
|
||||
The range check belongs to each copy, not to the definition.
|
||||
|
||||
**Implicit widening does not cross a generic binding.** A concrete argument at
|
||||
a variable an earlier argument already bound has to be that type, not merely
|
||||
one that widens into it — otherwise which copy a call gets depends on which
|
||||
argument was written first. Letting the pair meet at the wider type stays
|
||||
available as a later loosening; nothing written under this rule would stop
|
||||
compiling. An untyped literal is unaffected: it has no type of its own to keep.
|
||||
**Mixed widths at one type variable join at the wider type.** The first rule
|
||||
here refused the pair both ways and recorded the join as the loosening that
|
||||
could be added later; the author added it on 2026-09-20 (FIX.org, the
|
||||
integer? entry). Numeric scalars bound to one `$t` resolve it to whichever
|
||||
type every one of them widens into — value-preserving widening only, and in
|
||||
any argument order, so both orders produce the identical copy. A pair with no
|
||||
join (u64 against i64) is still refused, and a variable the signature also
|
||||
reaches through a container or function type is still bound exactly, because
|
||||
a slice's elements cannot be rewritten. An untyped literal is unaffected: it
|
||||
has no type of its own to keep.
|
||||
|
||||
**A type variable is not instantiated at `dyn`.** Two models answer "one body,
|
||||
many types" and they are not rivals: this one copies per written type at
|
||||
|
||||
104
test/programs/int-generic.flan
Normal file
104
test/programs/int-generic.flan
Normal file
@ -0,0 +1,104 @@
|
||||
;;;; integer?, end to end: the bound numeric? was one type too wide for.
|
||||
;;;;
|
||||
;;;; Three families in here, in order. The collapsed abs — one written body
|
||||
;;;; under {:where (integer? $t)} where abs-i32 and abs-i64 used to be, pinned
|
||||
;;;; at six widths, at both signed minimums (the answer is itself, because the
|
||||
;;;; negation wraps — what every two's-complement abs does), and beside the
|
||||
;;;; libm float pair it deliberately does not shadow: (abs-f64 -0.0) is 0
|
||||
;;;; because fabs clears the sign bit, which no integer body spells. Then the
|
||||
;;;; operations only integer? admits in a generic body — bit-and, bit-or,
|
||||
;;;; bit-xor, the shifts, and % — at several widths each. Then the join:
|
||||
;;;; mixed widths at one $t resolve to the wider type in either argument
|
||||
;;;; order (FIX.org 2026-09-20), so both orders print the same number from
|
||||
;;;; the same copy.
|
||||
|
||||
(defvar i32min i32 -2147483648)
|
||||
(defvar i64min i64 -9223372036854775808)
|
||||
|
||||
;; The low n bits, which needs a shift, a bit-and and the literal 1 — every
|
||||
;; one of them admitted by integer? and none by anything weaker.
|
||||
(defn low-bits [x $t n $t] $t
|
||||
{:where (integer? $t)}
|
||||
(bit-and x (- (<< 1 n) 1)))
|
||||
|
||||
;; Truncated %, the semantics everywhere in the language, in a generic body.
|
||||
(defn even? [x $t] bool
|
||||
{:where (integer? $t)}
|
||||
(= (% x 2) 0))
|
||||
|
||||
;; xor and or, and the shift right.
|
||||
(defn toggle [x $t m $t] $t
|
||||
{:where (integer? $t)}
|
||||
(bit-xor x m))
|
||||
|
||||
(defn with-flag [x $t f $t] $t
|
||||
{:where (integer? $t)}
|
||||
(bit-or x f))
|
||||
|
||||
(defn halve [x $t] $t
|
||||
{:where (integer? $t)}
|
||||
(>> x 1))
|
||||
|
||||
;; The untyped literal at a bounded variable: admitted under integer? by the
|
||||
;; same arm that admits it under numeric?, ranged per copy.
|
||||
(defn plus-300 [x $t] $t
|
||||
{:where (integer? $t)}
|
||||
(+ x 300))
|
||||
|
||||
;; The join family. eq2? is the pair the refusal used to be pinned on.
|
||||
(defn eq2? [a $t b $t] bool
|
||||
{:where (equal? $t)}
|
||||
(= a b))
|
||||
|
||||
(defn tri [a $t b $t c $t] $t
|
||||
{:where (numeric? $t)}
|
||||
(+ a (+ b c)))
|
||||
|
||||
(defn main [] ()
|
||||
;; abs, one body, six widths.
|
||||
(println (abs (i8 -7)))
|
||||
(println (abs -7))
|
||||
(println (abs (i64 -7)))
|
||||
(println (abs (u8 7)))
|
||||
(println (abs (u32 7)))
|
||||
(println (abs (u64 7)))
|
||||
;; The signed minimums answer themselves: the negation wraps, and saturating
|
||||
;; quietly would be the wrong answer this file exists to refuse.
|
||||
(println (abs i32min))
|
||||
(println (abs i64min))
|
||||
;; The float abs stays libm's: a sign-bit clear, so -0.0 comes back 0.
|
||||
(println (abs-f64 -0.0))
|
||||
(println (abs-f32 -0.0))
|
||||
(println (abs-f64 -1.5))
|
||||
(println (abs-f32 -2.5))
|
||||
|
||||
;; The integer?-only operations, per width.
|
||||
(println (low-bits 255 3))
|
||||
(println (low-bits (u16 65535) (u16 4)))
|
||||
(println (low-bits (i64 1023) (i64 5)))
|
||||
(println (even? 4))
|
||||
(println (even? (u8 3)))
|
||||
(println (even? (i64 -2)))
|
||||
(println (toggle (u8 255) (u8 15)))
|
||||
(println (with-flag 8 1))
|
||||
(println (halve (u64 10)))
|
||||
(println (halve (i64 -4)))
|
||||
(println (plus-300 1))
|
||||
(println (plus-300 (i64 1)))
|
||||
|
||||
;; The join: both orders, one copy, one answer.
|
||||
(let [a (i8 3)
|
||||
b (i64 3)]
|
||||
(println (eq2? a b))
|
||||
(println (eq2? b a)))
|
||||
(let [x (u32 1)
|
||||
y (i32 2)
|
||||
z (i64 3)]
|
||||
;; u32 and i32 meet at no type of their own; all three meet at the i64,
|
||||
;; wherever it stands in the argument list.
|
||||
(println (tri x y z))
|
||||
(println (tri z y x)))
|
||||
;; A literal beside a wider variable joins too: 4 arrives as an i32 and the
|
||||
;; copy is i64's.
|
||||
(let [w (i64 38)]
|
||||
(println (tri w 3 1))))
|
||||
@ -89,10 +89,11 @@
|
||||
(show64 (round-f64 2.5)) ; 3
|
||||
(println "")
|
||||
|
||||
;; Integer magnitude, one per width.
|
||||
(print (abs-i32 -7)) (print " ") ; 7
|
||||
(print (abs-i64 (i64 -7))) (print " ") ; 7
|
||||
(print (abs-i32 7)) (print " ") ; 7
|
||||
;; Integer magnitude, one generic under integer? — the per-width pair
|
||||
;; collapsed into it (FIX.org 2026-09-20). Two widths, two copies.
|
||||
(print (abs -7)) (print " ") ; 7
|
||||
(print (abs (i64 -7))) (print " ") ; 7
|
||||
(print (abs 7)) (print " ") ; 7
|
||||
;; tau is 2pi at both widths. Pinning the relation rather than the digits is
|
||||
;; what catches a constant written to too few of them.
|
||||
(print (= tau-f32 (* 2.0 pi-f32))) (print " ")
|
||||
|
||||
@ -2645,6 +2645,25 @@ let () =
|
||||
outputs "generics" "programs/generics.flan" generics_out;
|
||||
outputs ~opt:"-O0" "generics, -O0" "programs/generics.flan" generics_out;
|
||||
|
||||
(* integer?, end to end — see the program's own header. The first eight
|
||||
lines are the collapsed abs at six widths and both signed minimums
|
||||
(which answer themselves; the negation wraps). The [0 0] after them is
|
||||
the libm float pair at -0.0, the sign-bit clear no integer body
|
||||
spells. Then the integer?-only operations at several widths, and last
|
||||
the join family: [true true], [6 6] and [42] are mixed widths at one
|
||||
$t answering identically in both argument orders, from one copy at
|
||||
the wider type (FIX.org 2026-09-20). *)
|
||||
let int_generic_out =
|
||||
"7\n7\n7\n7\n7\n7\n-2147483648\n-9223372036854775808\n\
|
||||
0\n0\n1.5\n2.5\n\
|
||||
7\n15\n31\ntrue\nfalse\ntrue\n240\n9\n5\n-2\n301\n301\n\
|
||||
true\ntrue\n6\n6\n42\n"
|
||||
in
|
||||
outputs "integer? and the collapsed abs" "programs/int-generic.flan"
|
||||
int_generic_out;
|
||||
outputs ~opt:"-O0" "integer? and the collapsed abs, -O0"
|
||||
"programs/int-generic.flan" int_generic_out;
|
||||
|
||||
(* Reach's walk, edge by edge. Pruning is what makes the link follow the
|
||||
program, and the cost of getting it wrong is not a wrong answer: a
|
||||
function the walk fails to reach is not emitted, and the build dies in
|
||||
|
||||
@ -1165,11 +1165,17 @@ let () =
|
||||
used to be reported as unimplemented generics; generics are implemented,
|
||||
and a lowercase name is a type variable only where a defn signature
|
||||
introduced one with the sigil — a struct field is not such a place and
|
||||
never will be, since only a signature binds. So the sentence names the
|
||||
sigil rather than a milestone. A defn's parameter vector stopped being a
|
||||
type-only slot, which is why the rule is exercised at a field. *)
|
||||
rejects_check "a real type variable" "(defstruct Holder [x elem])"
|
||||
~needle:"write $elem in the parameter vector";
|
||||
never will be, since only a signature binds. The message used to tell a
|
||||
field to "write $elem in the parameter vector", and a field has no
|
||||
parameter vector — the suggestion could not be followed where it was
|
||||
printed. A field now gets its own sentence, naming the two things that
|
||||
can actually be written there; the parameter-vector suggestion survives
|
||||
where it works, which the return-type pin further down exercises. *)
|
||||
rejects_check "a real type variable at a field" "(defstruct Holder [x elem])"
|
||||
~needle:"a field is built at one type for every value";
|
||||
rejects_check "and the field message offers what a field can hold"
|
||||
"(defstruct Holder [x elem])"
|
||||
~needle:"Write a concrete type here, or dyn to hold any value";
|
||||
rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
|
||||
~needle:"unknown type Widget";
|
||||
|
||||
@ -4771,6 +4777,61 @@ let () =
|
||||
"(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))";
|
||||
accepts "numeric? entails ordered?"
|
||||
"(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))";
|
||||
|
||||
(* ── integer? — the bound numeric? was one type too wide for ─────────
|
||||
It admits every integer kind, signed and unsigned, at every width, and
|
||||
refuses floats and everything else. It exists so a function that can be
|
||||
generalized does not need a variant per numeric type: an integer body
|
||||
under numeric? was instantiated at f32 and f64 too, which is why abs
|
||||
stayed per-width for a milestone. It entails numeric? — every integer
|
||||
is a number — so the arithmetic, the written 0 and the untyped integer
|
||||
literal all come with it; the reverse entailment would let floats into
|
||||
bit-and and does not exist. *)
|
||||
accepts "integer? admits +, via the entailment"
|
||||
"(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))";
|
||||
accepts "integer? admits <, via the entailment"
|
||||
"(defn small? [x $t] bool {:where (integer? $t)} (< x 10))";
|
||||
accepts "integer? admits bit-and"
|
||||
"(defn low? [x $t] bool {:where (integer? $t)} (= (bit-and x 1) 1))";
|
||||
accepts "integer? admits the shifts"
|
||||
"(defn dbl [x $t] $t {:where (integer? $t)} (<< x 1))";
|
||||
rejects_check "numeric? does not admit bit-and"
|
||||
~needle:"nothing here says t is integer?"
|
||||
"(defn low? [x $t] bool {:where (numeric? $t)} (= (bit-and x 1) 1))";
|
||||
rejects_check "nor the shifts"
|
||||
~needle:"nothing here says t is integer?"
|
||||
"(defn dbl [x $t] $t {:where (numeric? $t)} (<< x 1))";
|
||||
(* An integer?-bounded caller satisfies a numeric?-bounded callee: the
|
||||
entailment carries across generic calls exactly as ordered?-over-equal?
|
||||
does. *)
|
||||
accepts "integer? carries a numeric? callee"
|
||||
"(defn z? [x $t] bool {:where (numeric? $t)} (= x 0))\n\
|
||||
(defn odd-z? [x $t] bool {:where (integer? $t)} (z? (bit-and x 1)))";
|
||||
(* The integer literal is admitted at a bounded variable by the same arm
|
||||
under both bounds — the bound promises the literal a meaning at every
|
||||
type the variable can become, and integer?'s types are a subset of
|
||||
numeric?'s. *)
|
||||
accepts "an integer literal stands where an integer?-bounded $t is wanted"
|
||||
"(defn bump [x $t] $t {:where (integer? $t)} (+ x 300))";
|
||||
(* A float at integer?, refused at the call that asked, naming the bound. *)
|
||||
rejects_check "a float does not instantiate an integer?-bounded variable"
|
||||
~needle:"f64 does not answer integer?"
|
||||
"(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
|
||||
(defn main [] () (println (bump 1.5)))";
|
||||
(* And dyn is refused by the bound too — the clause's own refusal, the more
|
||||
specific of the two answers, exactly as at numeric?. *)
|
||||
rejects_check "dyn does not instantiate an integer?-bounded variable"
|
||||
~needle:"dyn does not answer integer?"
|
||||
"(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
|
||||
(defvar d dyn 5)\n\
|
||||
(defn main [] () (println (bump d)))";
|
||||
(* A float literal inside an integer?-bounded body is refused at the
|
||||
definition, in the bound's own words: there is no instantiation at which
|
||||
it means anything. *)
|
||||
rejects_check "a float literal has no meaning under integer?"
|
||||
~needle:"admits no float type"
|
||||
"(defn h [x $t] $t {:where (integer? $t)} (+ x 1.5))";
|
||||
|
||||
accepts "a variable read twice under one predicate"
|
||||
"(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
|
||||
rejects_check "a predicate nobody has heard of"
|
||||
@ -4903,28 +4964,72 @@ let () =
|
||||
(defvar d dyn 5)\n\
|
||||
(defn main [] () (println (twice d)))";
|
||||
|
||||
(* ── Implicit widening does not cross a generic binding ─────────────
|
||||
Widening landed after generics did, and the rule it left behind depended
|
||||
on the order the arguments were written in: the i8-then-i64 call was
|
||||
refused because i64 into i8 can lose, and the i64-then-i8 call was
|
||||
*accepted*, because $t had already bound to i64 and the i8 widened into
|
||||
the want. Same two values, same function, two answers.
|
||||
|
||||
Neither was unsound — a widen cannot change a number — but which copy a
|
||||
program gets should not turn on which argument came first, so both are
|
||||
refused now and both name the binding. Letting the pair join at the wider
|
||||
type is the other coherent rule and it stays available: it can be added
|
||||
without invalidating anything written under this one, which is why this
|
||||
is the direction to be wrong in. FIX.org, "Generics and implicit
|
||||
widening". *)
|
||||
rejects_check "a narrower argument does not widen into a bound type variable"
|
||||
~needle:"was bound to i64 by an earlier argument"
|
||||
(* ── Mixed widths at one type variable join at the wider type ───────
|
||||
The rule used to refuse the pair both ways, with the join recorded as
|
||||
the coherent alternative that could be added without invalidating
|
||||
anything — the walk-backable direction. The author walked it back on
|
||||
2026-09-20: a scalar pair at one $t resolves to whichever of the two
|
||||
the other widens into, value-preserving widening only, and both
|
||||
argument orders produce the identical copy. A pair with no join — u64
|
||||
against i64 — keeps a refusal, because there is no type that holds
|
||||
every value of both. FIX.org, "Generics and implicit widening", and the
|
||||
2026-09-20 entry that supersedes it. *)
|
||||
accepts "a scalar pair at one $t joins at the wider type"
|
||||
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
|
||||
(defn main [] () (println (eq2? (i64 3) (i8 3))))";
|
||||
rejects_check "and the other argument order refuses identically"
|
||||
~needle:"was bound to i8 by an earlier argument"
|
||||
accepts "and the other argument order joins identically"
|
||||
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
|
||||
(defn main [] () (println (eq2? (i8 3) (i64 3))))";
|
||||
(* Order-independence, pinned on the copies and not only on acceptance:
|
||||
both orders in one program make exactly one instantiation, at i64, and
|
||||
none at i8. *)
|
||||
(let syms order_a order_b =
|
||||
match
|
||||
checked
|
||||
("(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
|
||||
(defn main [] () (do (println (eq2? " ^ order_a ^ "))\
|
||||
(println (eq2? " ^ order_b ^ "))))")
|
||||
with
|
||||
| p ->
|
||||
List.filter_map
|
||||
(fun (f : Tast.fn) ->
|
||||
if String.length f.Tast.name >= 4
|
||||
&& String.sub f.Tast.name 0 4 = "eq2?" then Some f.Tast.name
|
||||
else None)
|
||||
p.Tast.fns
|
||||
| exception _ -> [ "did not check" ]
|
||||
in
|
||||
check "both orders share one copy, at the wider type"
|
||||
(syms "(i8 3) (i64 4)" "(i64 5) (i8 6)" = [ "eq2?-i64" ]);
|
||||
check "and the reversed program instantiates the same one copy"
|
||||
(syms "(i64 5) (i8 6)" "(i8 3) (i64 4)" = [ "eq2?-i64" ]));
|
||||
(* The pair that meets at no type is the refusal that stays: neither u64
|
||||
nor i64 holds every value of the other, and inventing a third type
|
||||
would be picking one neither argument was written at. *)
|
||||
rejects_check "u64 and i64 meet at no type"
|
||||
~needle:"the two meet at no type"
|
||||
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
|
||||
(defvar u u64 3)\n(defvar i i64 3)\n\
|
||||
(defn main [] () (println (eq2? u i)))";
|
||||
(* And a later, wider argument settles a pair that had no join of its own:
|
||||
u32 and i32 meet nowhere, but all three meet at the i64 that arrives
|
||||
third — in either order, which is what the deferred re-ask is for. *)
|
||||
accepts "a later argument settles a joinless pair"
|
||||
"(defn tri [a $t b $t c $t] $t {:where (numeric? $t)} (+ a (+ b c)))\n\
|
||||
(defvar x3 u32 1)\n(defvar y3 i32 2)\n(defvar z3 i64 3)\n\
|
||||
(defn main [] () (println (tri x3 y3 z3)))";
|
||||
accepts "and the same trio in the other order"
|
||||
"(defn tri [a $t b $t c $t] $t {:where (numeric? $t)} (+ a (+ b c)))\n\
|
||||
(defvar x3 u32 1)\n(defvar y3 i32 2)\n(defvar z3 i64 3)\n\
|
||||
(defn main [] () (println (tri z3 y3 x3)))";
|
||||
(* A variable the signature also reaches through a container is bound
|
||||
exactly — a slice's elements cannot be rewritten to a wider width — so
|
||||
the join never moves one, in either direction of the mismatch. *)
|
||||
rejects_check "a container-bound variable does not join wider"
|
||||
~needle:"binds its element exactly"
|
||||
"(defn main [] () (let [ns [5 3 9 1]] \
|
||||
(match (index-of (slice ns 0 4) (i64 9)) \
|
||||
(Some i) (println i) _ (println -1))))";
|
||||
(* The written conversion is what the message asks for, and it is accepted:
|
||||
the refusal is about the *implicit* step, not about reaching i64. *)
|
||||
accepts "the written conversion is accepted"
|
||||
|
||||
@ -1051,7 +1051,7 @@ over.</p>
|
||||
<tr><td>text</td><td><code>split-on-byte</code>, <code>split-next</code>, <code>split</code>, <code>lower-ascii</code>, <code>upper-ascii</code>, <code>to-lower</code>, <code>to-upper</code></td></tr>
|
||||
<tr><td>building bytes</td><td><code>append</code>, <code>append-i64</code>, <code>append-f64</code>, <code>concat</code>, <code>join</code>, <code>repeat-bytes</code>, <code>replace-bytes</code>, <code>slices-new</code>, <code>format-f64</code></td></tr>
|
||||
<tr><td>UTF-8</td><td><code>decode-rune</code>, <code>rune-at</code>, <code>rune-count</code>, <code>rune-size</code>, <code>rune-start?</code>, <code>valid-utf8?</code>, <code>encode-rune</code></td></tr>
|
||||
<tr><td>numbers</td><td><code>sign-f32</code>, <code>lerp</code>, <code>clamp</code>, <code>floor-f32</code>, <code>ceil-f32</code>, <code>round-f32</code>, <code>abs-i32</code>, <code>abs-i64</code>, the constants <code>pi-f32</code>, <code>pi-f64</code>, <code>tau-f32</code>, <code>tau-f64</code>, and libm through a <code>declare</code> at both widths: <code>sqrt</code>, <code>abs</code>, <code>floor</code>, <code>ceil</code>, <code>round</code>, <code>fmod</code>, <code>sin</code>, <code>cos</code>, <code>tan</code>, <code>asin</code>, <code>acos</code>, <code>atan</code>, <code>atan2</code>, <code>log</code>, <code>log2</code>, <code>log10</code>, <code>exp</code>, <code>pow</code>, <code>hypot</code>, <code>cbrt</code> — each spelled <code>-f32</code> or <code>-f64</code></td></tr>
|
||||
<tr><td>numbers</td><td><code>sign-f32</code>, <code>lerp</code>, <code>clamp</code>, <code>floor-f32</code>, <code>ceil-f32</code>, <code>round-f32</code>, <code>abs</code> (generic over every integer width), the constants <code>pi-f32</code>, <code>pi-f64</code>, <code>tau-f32</code>, <code>tau-f64</code>, and libm through a <code>declare</code> at both widths: <code>sqrt</code>, <code>abs</code>, <code>floor</code>, <code>ceil</code>, <code>round</code>, <code>fmod</code>, <code>sin</code>, <code>cos</code>, <code>tan</code>, <code>asin</code>, <code>acos</code>, <code>atan</code>, <code>atan2</code>, <code>log</code>, <code>log2</code>, <code>log10</code>, <code>exp</code>, <code>pow</code>, <code>hypot</code>, <code>cbrt</code> — each spelled <code>-f32</code> or <code>-f64</code></td></tr>
|
||||
<tr><td>time</td><td><code>monotonic-ns</code>, <code>monotonic-seconds</code>, <code>unix-ns</code>, <code>unix-seconds</code>, <code>sleep-ns</code>, <code>sleep-seconds</code>, and <code>ns-per-second</code> and its two smaller siblings</td></tr>
|
||||
<tr><td>files</td><td><code>file-exists?</code> and <code>file-size</code>, which answer a value; <code>slurp</code>, <code>barf</code>, <code>delete-file</code>, <code>rename-file</code> and <code>make-directory</code>, which signal <code>FileError</code> under <code>retry</code> and <code>use-value</code></td></tr>
|
||||
<tr><td>the operating system</td><td><code>getenv</code>, which answers an <code>(Option [u8])</code> viewing the process environment</td></tr>
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user