diff --git a/lib/check.ml b/lib/check.ml index 1691019..0e4b2f9 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -854,8 +854,19 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t = | "Map", _ -> fail loc "(Map K V) takes exactly two types" | "Result", _ -> unimplemented loc "(Result T E)" 6 | _ -> + (* Not generics, which are here: a *function* is generic over [$t] and + instantiated per call site. This is a parameterised named type — + [(Pair i32 f64)] — and that is a different thing and is not built. + [Types.Named] is a bare string with no parameters, so there is + nowhere to put the arguments, and giving it some is a change to + [Types.t] and therefore to the layout calculator, both backends, + [Render] and the DWARF path. docs/SPIKE-GENERICS.md, question 4, + prices it and leaves it out. *) fail loc - "%s takes no type arguments — generics are milestone 5" name) + "%s takes no type arguments. A generic *function* is written with \ + [$t] in its parameter vector and copied per call site; a generic \ + *type* — (%s ...) — is not there yet" + name name) (* One edit away from a type that exists — a substitution, an insertion, a deletion or a transposition of neighbours. Bounded at one, because two edits @@ -951,12 +962,26 @@ and resolve_name env ~seen loc n = | _ when near_miss env n <> None -> Loc.failk "check/unknown-type" loc "unknown type %s — did you mean %s?" n (Option.get (near_miss env n)) - (* Lowercase is a type variable, Capitalized is concrete — no sigil - (plan.org, Types). A variable parses, but nothing at milestone 2 can - give a value one, so it is rejected here rather than later. *) + (* An unknown lowercase name, and the sentence it gets used to be that + generics were milestone 5 work. They are not: [$t] binds a type + variable and bare [t] uses one, and [resolve_name] has already + consulted [env.tyvars] and [env.subst] before anything reaches here. + So a lowercase name arriving at this arm is one of exactly two + things, and the message names both rather than sending somebody to a + schedule. + + Either it is a typo too far from any type to be guessed at — the + near-miss arm above catches the one-edit ones — or it is a type + variable that was never introduced, which is the sigil's whole + purpose to notice: without the binding site a mistyped type name + 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] -> - unimplemented loc - (Printf.sprintf "generic code over the type variable %s" n) 5 + 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 @@ -5651,7 +5676,17 @@ and named_call ctx ~want loc name args = in let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in (* [min] and [max] are [<] with a pick, so [ordered?] is what they want — - not [numeric?]. A generic that declares [ordered?] gets both. *) + not [numeric?]. A generic that declares [ordered?] gets both. + + They stay builtins now that generics could express them, and the reason + is the two lines above rather than the type system: they are variadic, + and each step puts both of its sides in slots so that every operand is + evaluated exactly once. A prelude [(defn min [a $t b $t] $t ...)] would + be binary and would have to be nested at the call site, which is where + the double evaluation this arm exists to prevent would come back. The + generic half is already theirs — [ordered?] admits them inside any + body that declares it — so collapsing them would cost the arity and + the evaluation rule and buy nothing. *) unconstrained ctx.env loc name ~needs:"ordered?" a.Tast.ty; if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then not_numeric name "numbers" a; @@ -7409,8 +7444,9 @@ and ordinary_call ctx ~want loc name args = the fork the form fell down. *) Loc.failk "check/unknown-function" loc "unknown function %s. A capitalised name is a type, and a type \ - given type arguments — (%s ...) — is generic code, which is \ - milestone 5" + given type arguments — (%s ...) — is a generic type, which is \ + not there yet. A generic *function* is: it is written with \ + [$t] in its parameter vector and copied per call site" name name else Loc.failk "check/unknown-function" loc "unknown function %s" name diff --git a/lib/prelude.ml b/lib/prelude.ml index 16c3062..76c4cb7 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -467,6 +467,44 @@ let source = {flan| (push v (at s i)))) v)) +;; ── The sign questions, over every numeric type at once ─────────────── +;; +;; The family the whole of generics was asked for. Three questions about a +;; number's sign, one body each, answering at i8 through u64 and at both +;; float widths — where without a type variable they would be three functions +;; per width, which is why they were never written at all. +;; +;; What makes them writable is not the type variable on its own: it is that a +;; written 0 may stand where $t stands. That needs the {:where (numeric? $t)} +;; clause and nothing weaker, because the bound is what promises the literal +;; has a meaning at every type the variable can become. An unconstrained +;; variable is refused, and so is [ordered?] — it admits an enum, which holds +;; no number. +;; +;; The comparison is the clause's too: [numeric?] entails [ordered?], so one +;; predicate on the line gives the body both the < it writes and the 0 it +;; writes it against. +;; +;; **The unsigned instantiations are not mistakes.** (neg? (u8 3)) is false at +;; every u8 and the copy is a constant, which a reader may find odd in the +;; emitted code and which is exactly right: a generic is copied per written +;; type, and the body says what it says at each of them. Refusing the copy +;; would mean a bound that spells "signed", and there is no such predicate. +(defn pos? [x $t] bool + {:where (numeric? $t)} + (> x 0)) + +(defn neg? [x $t] bool + {:where (numeric? $t)} + (< x 0)) + +;; Named zero? rather than =0 because it reads as the question it is. The +;; float instantiations answer true for both zeros, since -0.0 = 0.0 is what +;; IEEE says and this does not second-guess it. +(defn zero? [x $t] bool + {:where (numeric? $t)} + (= x 0)) + ;; ── The per-type layer that stays ───────────────────────────────────── ;; ;; sum is the one shape a type variable cannot express, and it is worth being @@ -947,9 +985,24 @@ let source = {flan| (declare cbrt-f32 [x f32] f32 "cbrtf") (declare cbrt-f64 [x f64] f64 "cbrt") -;; Integer magnitude, one per width because there are no generics over the -;; numeric types and min and max are builtins rather than functions, so a -;; single abs is not expressible today. +;; 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. +;; +;; **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 most negative value of each width has no positive counterpart, and this ;; does not special-case it: the subtraction is the same subtraction written diff --git a/test/programs/generics.flan b/test/programs/generics.flan index 12ddee7..78944a8 100644 --- a/test/programs/generics.flan +++ b/test/programs/generics.flan @@ -51,21 +51,25 @@ (min (max x lo) hi)) ;; An integer *literal* where the type variable is wanted, which is what the -;; author's motivating family needs: one pos? over every numeric type rather -;; than one per width. The literal is admitted because {:where (numeric? $t)} -;; is declared, and the bound is what makes it sound rather than optimistic — -;; every type numeric? admits is an integer or a float, and an untyped integer -;; constant is usable at all of them, so there is no instantiation at which -;; this 0 has no meaning. Without the clause it is refused at the definition; -;; see the rejects in test_flan.ml. +;; sign family needs: one pos? over every numeric type rather than one per +;; width. The literal is admitted because {:where (numeric? $t)} is declared, +;; and the bound is what makes it sound rather than optimistic — every type +;; numeric? admits is an integer or a float, and an untyped integer constant +;; is usable at all of them, so there is no instantiation at which this 0 has +;; no meaning. Without the clause it is refused at the definition; see the +;; rejects in test_flan.ml. ;; ;; The literal is never emitted from here. The abstract pass builds a ;; placeholder and throws it away with the rest of the body; each copy ;; re-checks (> x 0) with $t substituted, and *that* is where the literal is ;; built at the concrete width and range-checked. -(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0)) -(defn neg? [x $t] bool {:where (numeric? $t)} (< x 0)) -(defn zero-p? [x $t] bool {:where (numeric? $t)} (= x 0)) +;; +;; The -t? suffix is because the prelude now carries pos?/neg?/zero? itself. +;; These are the same three bodies written in an ordinary program, which is +;; what says the machinery belongs to the language and not to the prelude. +(defn pos-t? [x $t] bool {:where (numeric? $t)} (> x 0)) +(defn neg-t? [x $t] bool {:where (numeric? $t)} (< x 0)) +(defn zero-t? [x $t] bool {:where (numeric? $t)} (= x 0)) ;; The same literal in arithmetic rather than comparison, and answering $t ;; rather than bool, so the placeholder has to survive being the operand of a @@ -161,18 +165,25 @@ ;; The literal-at-a-type-variable family, at six numeric types from three ;; written bodies. i32, i64, u8, u16, f32 and f64 all reach the same 0 and ;; the same 1. - (println (pos? 3)) - (println (neg? (i8 -3))) - (println (zero-p? (u8 0))) - (println (zero-p? 0.0)) - (println (pos? (u16 1))) - (println (neg? (f32 -0.5))) + (println (pos-t? 3)) + (println (neg-t? (i8 -3))) + (println (zero-t? (u8 0))) + (println (zero-t? 0.0)) + (println (pos-t? (u16 1))) + (println (neg-t? (f32 -0.5))) (println (next-after 3)) (println (next-after (i64 10))) (println (next-after 2.5)) (println (next-after (u8 254))) (println (plus-300 1)) + ;; And the prelude's own three, which are these bodies under their real + ;; names. The -0.0 is the one worth asserting: IEEE says -0.0 = 0.0 and + ;; zero? does not second-guess it. + (println (pos? (i64 3))) + (println (zero? -0.0)) + (println (neg? (u8 3))) + (show 3) (show 4.5) (show "text") diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index f84c9e9..1a2dbc0 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2592,10 +2592,14 @@ let () = and f64. [255] is next-after at u8 and is the one that would say whether the placeholder width the abstract pass builds had leaked into a copy; [301] is plus-300 at i32, whose range check belongs to the copy - and not to the definition. *) + and not to the definition. The [true true false] after them is the + prelude's own pos?/zero?/neg? — the same three bodies under their real + names — and the middle one is zero? at -0.0, which IEEE says is zero + and which this does not second-guess. *) let generics_out = "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\ true\ntrue\ntrue\ntrue\ntrue\ntrue\n4\n11\n3.5\n255\n301\n\ + true\ntrue\nfalse\n\ 3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n\ 0\n-1\n2.5\n0\ntrue\nfalse\ntrue\n2\n0\n\ 3\n3\n0\n21\n7\n3\n4.5\n" diff --git a/test/test_flan.ml b/test/test_flan.ml index 57b64be..9965aca 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1161,12 +1161,15 @@ let () = | Some { Tast.params = [ Types.Dyn; Types.Dyn ]; _ } -> () | _ -> check "an unannotated pair is two dyn parameters" false) | exception _ -> check "an unannotated pair is two dyn parameters" false); - (* A bare lowercase name is still an unimplemented type variable everywhere a - type is the only thing a slot can hold. A defn's parameter vector stopped - being such a place — a slot there may be a parameter instead — so the rule - is exercised where it still decides, at a field. *) + (* A bare lowercase name where a type is the only thing a slot can hold. It + 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:"milestone 5"; + ~needle:"write $elem in the parameter vector"; rejects_check "an unknown concrete type" "(defn f [x Widget] ())" ~needle:"unknown type Widget"; @@ -2073,9 +2076,16 @@ let () = (* [(Pair i32)] in a defvar falls down the value fork now that the third element takes either reading, and the generics answer the type fork gave it has to be reachable from here too. *) - rejects_check "a capitalised call with arguments is generics" + (* A capitalised head with arguments is a *type* given type arguments, and + that is the half of generics that is not built — Types.Named is a bare + string with no room for parameters. The sentence says which half, since + generic functions are here and pointing at them is the useful part. *) + rejects_check "a capitalised call with arguments is a generic type" "(defvar x (Pair i32)) (defn f [] i32 0)" - ~needle:"is generic code, which is milestone 5"; + ~needle:"is a generic type, which is not there yet"; + accepts "and the generic function it points at is" + "(defn pair-fst [a $t b $u] $t (do b a))\n\ + (defn main [] () (println (pair-fst 1 true)))"; rejects_check "defined twice" "(defn f [] ()) (defn f [] ())" ~needle:"defined twice"; accepts "main with no parameters and no return" "(defn main [] ())"; @@ -2895,8 +2905,8 @@ let () = defn's body that just answers one says nothing about them. *) rejects_check "an fn with nothing to say what it takes" "(defn f [] () (fn [x] x))" ~needle:"nothing here says what this fn"; - rejects_check "type variables are milestone 5" "(defn f [] a 0)" - ~needle:"milestone 5"; + rejects_check "a lowercase return type no signature introduced" + "(defn f [] a 0)" ~needle:"write $a in the parameter vector"; (* The other half: a name in value position now *works*, and the arity is checked against the function it names. *) rejects_check "a function value at the wrong arity" @@ -4806,9 +4816,15 @@ let () = has no meaning. That is the whole rule, and the four pins below are its two halves and its one asymmetry. *) accepts "an integer literal stands where a numeric? type variable is wanted" - "(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))"; + "(defn above-zero? [x $t] bool {:where (numeric? $t)} (> x 0))"; accepts "and in arithmetic, answering the variable" "(defn next [x $t] $t {:where (numeric? $t)} (+ x 1))"; + (* And the prelude's own three, which are that body under its real name at + every numeric type from one definition. *) + accepts "the prelude's sign family answers at six numeric types" + "(defn main [] () (println (pos? 3) ) (println (neg? (i8 -1))) \ + (println (zero? (u8 0))) (println (zero? 0.0)) \ + (println (pos? (u64 1))) (println (neg? (f32 -0.5))))"; (* [numeric?] is what admits it and nothing weaker does. [ordered?] admits an enum, which holds no number, so a literal under it has an instantiation at which it means nothing — and the refusal below is what