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

Three messages about milestone 5, from a milestone that arrived

Browse Source 
The refusals generics obsoleted, swept. Every message that sent
somebody to a schedule now says what is actually true of the thing in
front of them.

An unknown lowercase type name used to be reported as unimplemented
generic code over a type variable. Generics are implemented, and
resolve_name consults env.tyvars and env.subst long before anything
reaches that arm -- so a lowercase name arriving there is a typo too
far from any type to guess at, or a type variable nobody introduced.
The sentence names the sigil that would introduce it.

A capitalised name given type arguments is the other half, and it is
still genuinely unbuilt: Types.Named is a bare string with no room for
parameters, and giving it some is a change to Types.t and therefore to
the layout calculator, both backends, Render and DWARF. Both sites
that reported it -- the type resolver and the value-position fork --
now say a generic *type* is not there yet and point at the generic
function that is.

Plus the prelude's side of it. pos?, neg? and zero? are three
questions about a number's sign, one body each, answering at every
numeric type -- the family the whole feature was asked for, and the
one thing the landed generics could not write until a literal was
allowed to stand at a bounded type variable.

Two collapses examined and declined, with the real reason written
where the old one was. abs stays per width because numeric? is the
only bound that admits a written 0 and it admits floats too, and the
integer body is the wrong abs for a float: it hands back a negative
zero. It waits on an integer? predicate, which is language surface.
min and max stay builtins because they are variadic and slot each
operand so it is evaluated once; a binary prelude generic would put
the double evaluation back at the call site. Their generic half was
never missing -- ordered? already admits them in any body that
declares it.
This commit is contained in:
Joseph Ferano 2026-09-20 20:46:35 +07:00
parent c372a98238
commit d5fed12d48
5 changed files with 159 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
lib/check.ml
View File

@ -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

59
lib/prelude.ml
View File

@ -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

43
test/programs/generics.flan
View File

@ -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")

6
test/test_acceptance.ml
View File

@ -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"

36
test/test_flan.ml
View File

@ -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