From 56040ec6bdc09276360d43227f28f60d54e90dac Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 21:04:37 +0700 Subject: [PATCH] The account of generics catches up with the three rules it gained The spike banner names plan.org's Types section and spec-memory.md's Generics section as the current account. Neither said anything about a literal at a type variable, about widening meeting a generic binding, or about dyn, and all three are now observable from a program -- so the account had a hole rather than an error. Filled, in spec-memory.md, in the terms a programmer meets them in. And one stale claim found and deliberately left: plan.org still lists five predicates and describes copyable? and move-only-by-default at length. spec-memory.md already records that copyable? went with the second repeal and check.ml has four. That sentence belongs to the ownership-repeal lane, so it is flagged in FIX.org rather than rewritten here. --- FIX.org | 14 ++++++++++++++ spec-memory.md | 27 +++++++++++++++++++++++++++ 2 files changed, 41 insertions(+) diff --git a/FIX.org b/FIX.org index aafb23f..6b8c2f1 100644 --- a/FIX.org +++ b/FIX.org @@ -3490,3 +3490,17 @@ Dev-loop reload needed nothing: test_session already pins ~C-c C-c~ on a generic installing its copies, the callee side, the absence of a stale cache across two evaluations, and a redefinition that needs a copy the process was never built with. + +** One stale claim flagged, not touched +plan.org's Types section still lists *five* predicates and describes +~copyable?~ and "a type variable is move-only by default" at length. +spec-memory.md's Generics section already records that ~copyable?~ went with +the second repeal, and ~predicate_names~ in check.ml has four. plan.org is the +one that is behind. Left alone deliberately: it is the ownership-repeal lane's +sentence to retire, not this one's, and it is flagged here so that lane picks +it up. + +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. diff --git a/spec-memory.md b/spec-memory.md index 5345170..3430b07 100644 --- a/spec-memory.md +++ b/spec-memory.md @@ -301,6 +301,33 @@ Type arguments are **inferred at call sites** from the argument types; there is no explicit instantiation syntax in the first implementation. A type variable that appears only in the return type is therefore an error. +Three further rules about what a call site may pass, all decided 2026-09-20 and +written up in FIX.org, "Milestone 5, and the sweep behind it": + +**A written number may stand where a type variable stands, under `numeric?`.** +`(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))` is the family the +feature was asked for, and the bound is what makes the `0` 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. Nothing weaker admits it — +`ordered?` admits an enum, which holds no number. A *float* literal is refused +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. + +**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 +compile time, `defgeneric`/`defmethod` dispatch at run time on a value that +carries its own. A dyn argument asks the second question of the first +machinery, and the refusal says so. Whether dyn should ever flow through a +generic is open. + ## Function values Three cases, split by whether the value escapes the frame that made it.