From f71cc40bb57b69d4540611ad3dc4336d04484163 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 21:42:50 +0700 Subject: [PATCH] integer? bounds the integer-only bodies, and abs is one generic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- FIX.org | 108 ++++++++++++ lib/check.ml | 304 +++++++++++++++++++++++++-------- lib/prelude.ml | 42 +++-- lib/types.ml | 7 + spec-memory.md | 34 ++-- test/programs/int-generic.flan | 104 +++++++++++ test/programs/math3.flan | 9 +- test/test_acceptance.ml | 19 +++ test/test_flan.ml | 151 +++++++++++++--- web/index.html | 2 +- 10 files changed, 642 insertions(+), 138 deletions(-) create mode 100644 test/programs/int-generic.flan diff --git a/FIX.org b/FIX.org index de939ef..9deab2c 100644 --- a/FIX.org +++ b/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. diff --git a/lib/check.ml b/lib/check.ml index bebe66f..eba422b 100644 --- a/lib/check.ml +++ b/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 } diff --git a/lib/prelude.ml b/lib/prelude.ml index 76c4cb7..ce2eb22 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -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 diff --git a/lib/types.ml b/lib/types.ml index 110bcaf..919ea6b 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -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 diff --git a/spec-memory.md b/spec-memory.md index 3430b07..86520ef 100644 --- a/spec-memory.md +++ b/spec-memory.md @@ -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 diff --git a/test/programs/int-generic.flan b/test/programs/int-generic.flan new file mode 100644 index 0000000..63e1ed0 --- /dev/null +++ b/test/programs/int-generic.flan @@ -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)))) diff --git a/test/programs/math3.flan b/test/programs/math3.flan index fca8255..3e81f29 100644 --- a/test/programs/math3.flan +++ b/test/programs/math3.flan @@ -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 " ") diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index bea8d35..fbab847 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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 diff --git a/test/test_flan.ml b/test/test_flan.ml index 7b21077..fd138cc 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -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" diff --git a/web/index.html b/web/index.html index 1458723..16f5cd2 100644 --- a/web/index.html +++ b/web/index.html @@ -1051,7 +1051,7 @@ over.

textsplit-on-byte, split-next, split, lower-ascii, upper-ascii, to-lower, to-upper building bytesappend, append-i64, append-f64, concat, join, repeat-bytes, replace-bytes, slices-new, format-f64 UTF-8decode-rune, rune-at, rune-count, rune-size, rune-start?, valid-utf8?, encode-rune -numberssign-f32, lerp, clamp, floor-f32, ceil-f32, round-f32, abs-i32, abs-i64, the constants pi-f32, pi-f64, tau-f32, tau-f64, and libm through a declare at both widths: sqrt, abs, floor, ceil, round, fmod, sin, cos, tan, asin, acos, atan, atan2, log, log2, log10, exp, pow, hypot, cbrt — each spelled -f32 or -f64 +numberssign-f32, lerp, clamp, floor-f32, ceil-f32, round-f32, abs (generic over every integer width), the constants pi-f32, pi-f64, tau-f32, tau-f64, and libm through a declare at both widths: sqrt, abs, floor, ceil, round, fmod, sin, cos, tan, asin, acos, atan, atan2, log, log2, log10, exp, pow, hypot, cbrt — each spelled -f32 or -f64 timemonotonic-ns, monotonic-seconds, unix-ns, unix-seconds, sleep-ns, sleep-seconds, and ns-per-second and its two smaller siblings filesfile-exists? and file-size, which answer a value; slurp, barf, delete-file, rename-file and make-directory, which signal FileError under retry and use-value the operating systemgetenv, which answers an (Option [u8]) viewing the process environment