335 lines
25 KiB
Markdown
335 lines
25 KiB
Markdown
# The generics spike, answered: it runs, and the bill lands on the dev loop rather than on the checker
|
||
|
||
Milestone 5's parametric polymorphism, run early and deliberately out of order, as a spike rather than as a
|
||
decision. **Feasible, and smaller than expected.** A generic function written in Flan goes through the ordinary
|
||
frontend, is instantiated at each concrete type its call sites ask for, is emitted as real functions and runs,
|
||
answering correctly at every one of them. The whole of it is `lib/check.ml`; `lib/types.ml`, `lib/tast.ml`,
|
||
`lib/emit.ml` and every backend are untouched, and `dune test --root .` is green (203 checks, 0 failures) either
|
||
side of it.
|
||
|
||
The demonstrations are `spike/generics/*.flan` and are run with the ordinary driver —
|
||
`dune exec --root . bin/main.exe -- run spike/generics/sort.flan`. The measurement is `spike/generics/measure.ml`,
|
||
driven by `bash spike/generics/run.sh` with ocamlfind against the `flan.cmxa` dune already builds, exactly as
|
||
`spike/backend` is and for the same reason: nothing under `spike/` is wired into the build.
|
||
|
||
**The headline is not that it works.** It is that the two costs everyone expects to be the problem — checking and
|
||
instantiating — are under the noise floor, and the cost that is real is one nobody named: `C-c C-c` on a generic
|
||
function today **silently installs nothing**, and making it install something multiplies the part of the dev loop
|
||
that was already the slowest. Measured below.
|
||
|
||
## The sigil, since it changed under the spike
|
||
|
||
plan.org says lowercase is a type variable and there is no sigil. That was revised while this was being built, and
|
||
this is built against the revision: **`$t` at the binding site, bare `t` at every use**, which is Odin's spelling
|
||
(`$T` in the signature, `T` in the body).
|
||
|
||
```lisp
|
||
(defn swap! [xs [$t] i i32 j i32] () ...) ; $t binds
|
||
(defn fold [s [$t] init $t f (Fn [$t $t] $t)] t ...) ; later $t are the same variable; t reads it
|
||
```
|
||
|
||
Both spellings are accepted at a use — `resolve_name` strips the sigil before it looks anything up — because that
|
||
is one `String.sub` and refusing the sigil at a use would be a second rule to explain. The binding rule is the one
|
||
that is enforced: **only a `defn` signature introduces a variable**, and `$t` anywhere else (a struct field, a
|
||
global, a `let` annotation) is a refusal that says so.
|
||
|
||
The decision costs one function and one `match` arm, both in `check.ml`. The reader already treats `$` as an
|
||
ordinary symbol character, so `$t` arrives as `Ast.Tname "$t"` with no change to `reader.ml`, `parse.ml` or
|
||
`ast.ml`, and changing the sigil to anything else is changing one character in `resolve_name` and one in
|
||
`signature_tyvars`. Nothing else in the compiler knows the character means anything.
|
||
|
||
The revision's reasoning holds up in the code. `signature_tyvars` scans for the sigil and puts the bare names in
|
||
`env.tyvars`; `resolve_name` consults that list and nothing else. So an unknown lowercase type name is still the
|
||
unknown-type error it always was, and the old rule's failure mode — a mistyped type name silently becoming a type
|
||
parameter, making the function *more* permissive than it was written to be — cannot happen. The near-miss guard at
|
||
`check.ml:553` stays where it is and keeps `f65` a typo.
|
||
|
||
## Question 1 — does it work end to end
|
||
|
||
Yes, at four shapes, all of them run and checked against their output.
|
||
|
||
**One variable, one function, two types** (`spike/generics/id.flan`):
|
||
|
||
```lisp
|
||
(defn id [x $t] t x)
|
||
(defn main [] ()
|
||
(println (id 3)) (println (id 4.5)) (println (id 7)) (println (id true)))
|
||
```
|
||
|
||
prints `3 / 4.5 / 7 / true`, and emits exactly three bodies — `flan.id-i32`, `flan.id-f64`, `flan.id-bool`. Four
|
||
calls, three copies: `(id 3)` and `(id 7)` share one, which is the instantiation cache doing its job.
|
||
|
||
**Through a slice, mutating in place** (`spike/generics/swap.flan`): `(defn swap! [xs [$t] i i32 j i32] () ...)`
|
||
called at `[i32]` and `[f64]`, correct both times. The variable is bound *inside* a type constructor here, which
|
||
is the `is_polymorphic_type_assignable` walk rather than a name match.
|
||
|
||
**The one that matters — a generic calling a generic, with the operator passed in** (`spike/generics/sort.flan`):
|
||
|
||
```lisp
|
||
(defn swap! [xs [$t] i i32 j i32] () ...)
|
||
|
||
(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
|
||
(let [i 1]
|
||
(while (< i (len s))
|
||
(let [j i]
|
||
(while (and (> j 0) (before? (at s j) (at s (- j 1))))
|
||
(swap! s (- j 1) j)
|
||
(set j (- j 1))))
|
||
(set i (+ i 1)))))
|
||
|
||
(defn main [] ()
|
||
(let [ns [5 3 9 1] fs [2.5 0.5 1.5]]
|
||
(sort-by! (slice ns 0 4) (fn [a b] (< a b)))
|
||
(sort-by! (slice fs 0 3) (fn [a b] (> a b)))
|
||
...))
|
||
```
|
||
|
||
prints `1 3 5 9` then `2.5 1.5 0.5`, and emits four bodies: `sort-by!-i32`, `sort-by!-f64`, `swap!-i32`,
|
||
`swap!-f64`. This is prelude.ml's `sort-i32-by!`/`sort-f32-by!` pair, collapsed, running. Note what had to work
|
||
for it: `sort-by!` calls `swap!` at its *own* variable `t`, so the copy of `swap!` is generated when `sort-by!`
|
||
is instantiated and not before — instantiation is transitive.
|
||
|
||
It also forced the one piece of real inference in the spike. Arguments are checked left to right and **each
|
||
binding is substituted back into the parameters still to come**, so by the time `(fn [a b] (< a b))` is reached,
|
||
`(Fn [$t $t] bool)` has already become `(Fn [i32 i32] bool)` and the literal has the position it needs to take
|
||
its types from. Without that the `fn` literal has no types and the call does not check. This is the same
|
||
left-to-right operand order Odin gathers its operands in.
|
||
|
||
**Two variables** (`spike/generics/two-vars.flan`) was out of scope and fell out for free: `(defn fst [a $t b $u]
|
||
t a)` at three combinations works, because the substitution is a list and was never written as a single binding.
|
||
|
||
**The refusal.** `(defn add2 [a $t b $t] t (+ a b))` is rejected *at the definition*, before any call site:
|
||
|
||
```
|
||
spike/generics/reject.flan:1:26: + over the type variable t is refused: an unconstrained type variable supports
|
||
only what every type supports, and + is not that (plan.org, Types). Take the operation as a parameter — a
|
||
(Fn [t t] ...) — and call it here
|
||
1 | (defn add2 [a $t b $t] t (+ a b))
|
||
| ^^^^^^^
|
||
```
|
||
|
||
`=` and `<` get the same refusal from the same place. This is what `sort-by!` above is the positive case of: the
|
||
comparison it cannot have is the comparison it is given.
|
||
|
||
## Question 2 — where instantiation belongs in this pipeline
|
||
|
||
**In the checker, at the call site, which is where Odin puts it.** `check_expr.cpp`'s
|
||
`find_or_generate_polymorphic_procedure` runs from call checking: it builds the concrete proc type from the
|
||
operands, scans the base entity's `gen_procs` for an `are_types_identical` match, and generates a new `Entity`
|
||
only on a miss. `check.ml`'s `generic_call` and `instantiate` are that loop, with `Types.equal` pairwise standing
|
||
in for `are_types_identical`.
|
||
|
||
It belongs there and nowhere else for a reason specific to this pipeline: the call site is the only place the
|
||
concrete types exist, and it is the same argument `check.ml` already makes for `SizeOf`/`AlignOf` ("the checker
|
||
builds these at the site where the concrete element type is known"). A pass after checking would have to re-derive
|
||
every argument type it had just thrown away; a pass before it has nothing to work with.
|
||
|
||
**What that means for `Tast`: a generic `defn` does not reach the typed IR at all.** Only its instantiations do.
|
||
Concretely:
|
||
|
||
- `collect` puts a generic signature in a new `gsigs` table and **not** in `env.fns`. Nothing can be called at
|
||
`t`, so nothing may find it by the ordinary path.
|
||
- `build_program`'s pass-two fold skips generic `defn`s. They produce no `Tast.fn`.
|
||
- Each instantiation is an ordinary `Tast.fn` appended to the program next to the handler clauses `env.lifted`
|
||
already collects, with `fparent = None` — unlike a lifted clause it is reached *by name* from arbitrary call
|
||
sites, so it needs a cell, and it gets one automatically: `flan.cell.sort-by!-i32` is in the `--dev` output with
|
||
no change to `emit.ml`.
|
||
- `Tast` is unchanged. `Types.Var` already existed, and after instantiation no node carries one.
|
||
|
||
The naming convention is the prelude's own: `id-i32`, `sort-by!-f64`, `keep-i32`, and for constructed types
|
||
`slice-i32`, `vec-f32`, `opt-i64`, `arr8-u8`. A generated name reads like the handwritten one it replaces, which
|
||
is what a backtrace, a `Reach` edge and a dev-build cell all end up showing. `Types.to_string` cannot serve —
|
||
`[i32]` and `(Vec i32)` are not symbols — so there is a second spelling function, `mangle_ty`, and it is a
|
||
namespace hazard: see the "no plan" bucket.
|
||
|
||
## Question 3 — the cost to the dev loop, measured
|
||
|
||
This is the question the spike exists for, and the answer has two halves: the half that is free, and the half
|
||
that is not implemented and will not be free.
|
||
|
||
`spike/generics/run.sh` sweeps one generic pair (`gswap` + `gsort`, the insertion sort above) called at N distinct
|
||
element types, N = 1..8, against the handwritten N-copies program it would replace. Best of three per cell, on an
|
||
otherwise idle machine:
|
||
|
||
```
|
||
n check-gen check-mono emit-1 emit-N build-1 build-N fns
|
||
1 1.8 1.8 0.1 0.1 19.0 21.3 2
|
||
2 1.8 1.8 0.1 0.3 19.6 24.7 4
|
||
3 1.9 1.6 0.1 0.4 19.2 28.1 6
|
||
4 1.9 1.9 0.1 0.4 18.5 31.9 8
|
||
5 2.1 2.1 0.1 0.6 19.3 35.9 10
|
||
6 1.8 1.9 0.1 0.7 18.8 39.1 12
|
||
7 2.0 1.8 0.1 0.8 18.6 41.9 14
|
||
8 1.8 2.0 0.1 0.8 19.0 45.1 16
|
||
```
|
||
|
||
`check-*` is `Check.program_with_env` over the whole accumulated program, which is what `Session.eval` does on
|
||
**every** evaluation. `emit-*` is `Emit.redefinition`. `build-*` is `Build.shared` — llc + `ld -shared` — with the
|
||
same options `dev.ml` passes (`dev = true`, `-O2`). Under load every column scales by about 3×; the ratios hold.
|
||
|
||
Read off it:
|
||
|
||
1. **Checking a generic program costs what checking the handwritten one costs.** 1.8 ms either way, flat in N.
|
||
Instantiation — matching, substituting, cache scan, and checking each copy's body — does not show above the
|
||
noise, because whole-program checking is dominated by the 1665-line prelude. The instantiation cache is rebuilt
|
||
from scratch on every `C-c C-c`, since `Check.program_with_env` makes a fresh `env`, and that is affordable:
|
||
there is no persistent cache to invalidate and therefore no staleness to get wrong.
|
||
2. **Emitting is free.** 0.1 ms for one body, 0.8 ms for sixteen.
|
||
3. **`llc` + `ld` is the whole bill, and it is per body.** 19 ms for one, 45 ms for sixteen — about **+1.7 ms per
|
||
extra body**, roughly linear. A redefinition module with one function is ~19 ms; the same redefinition of a
|
||
generic used at 8 element types is ~45 ms.
|
||
|
||
**What the 19 ms is and is not.** It is `Build.shared` alone: `llc` plus `ld -shared`. The ~35 ms the brief
|
||
quotes for `C-c C-c` is the whole round trip, and `dev.ml:446` pays several things around this call that are not
|
||
in it — `Session.eval`'s read/parse/Load/check (the 1.8 ms column), writing the `.ll` and the `.o`, `deliver` and
|
||
the `dlopen` at a frame boundary, and the wire exchange with the editor. So the two numbers are not in conflict;
|
||
they are measuring different brackets, and the ~16 ms between them is the part this spike does not change.
|
||
|
||
**The marginal number is the one that transfers, and it is invariant to which baseline it is added to: +1.7 ms
|
||
per extra body.** In the terms the brief asks for: a generic used at two element types adds about 3.5 ms to a
|
||
~35 ms loop (one generic that calls another, so four bodies rather than two — 10%); at three types, ~7 ms; at
|
||
eight types, ~26 ms, which is a loop of ~61 ms rather than ~35. It stays well under the "redefine a whole file"
|
||
cost and is proportional to what changed rather than to the size of the program.
|
||
|
||
**And the half that is not implemented.** The last line of the sweep is the finding:
|
||
|
||
```
|
||
Session.eval on the generic gswap itself: 2.5 ms, installs=false, fns=[], names=[gswap]
|
||
```
|
||
|
||
`session.ml:eval` computes `fns` as the names in the incoming form that appear in `program.Tast.fns`. A generic
|
||
`defn` is not in `Tast.fns` — by design, per question 2 — so `fns` is empty, `installs` is false, and the editor
|
||
is told nothing was installed. **Today, `C-c C-c` on a generic function is a no-op that does not lie about it but
|
||
does not do anything either.** The fix is not in this lane (`session.ml` is held elsewhere) and is small in
|
||
principle: expand a redefined generic name to its instantiations, transitively through generics that call it, and
|
||
pass *those* to `Emit.redefinition`. The cells already exist. The cost of doing so is the table above.
|
||
|
||
Two things that cost nothing and are worth having in writing: the compatibility check (`Session.compatible`) sees
|
||
instantiations as ordinary functions and compares their signatures as it always did; and a generic whose
|
||
*signature* changes produces differently-named instantiations, so the old ones stay in the process with nothing
|
||
calling them — dead, not stale.
|
||
|
||
## Question 4 — what the whole feature would have to lower
|
||
|
||
Against what a generic function has to survive, in DISCUSS.md item 15's buckets:
|
||
|
||
| | |
|
||
|---|---|
|
||
| **Done in the spike** | one or more type variables in a signature; binding through `[t]`, `(Ptr t)`, `(Option t)`, `(Fn [t] t)` and nesting; return types mentioning a variable; left-to-right binding with substitution into later parameters so an `fn` literal gets its types; the Odin-keyed instantiation cache; generic calling generic, transitively; `(vec-new t)`; the abstract refusal pass for `+`, `-`, `*`, `/`, `%`, `=`, `!=`, `<`, `<=`, `>`, `>=`, the bitwise operators and the shifts; instantiations as ordinary `Tast.fn`s with dev cells and `Reach` edges for free; a depth cap so runaway instantiation refuses instead of hanging |
|
||
| **Mechanical** | the remaining builtins that take a *type name* as an argument — `pool-new`, `map-new`, `zeroed`, `uninit`, the casts — each of which reaches `type_named`/`resolve_name` by its own path, exactly as `vec-new` did (one line there fixed `vec-new`; the others are one line each); `hash` and the map key-pair path, which must refuse a `Var` rather than assume; the `fns` expansion in `session.ml` described above |
|
||
| **Bulky, not hard** | error messages that say *where* an instantiation came from — Odin's "in instantiation of" note. Today a refusal inside an instantiated body points at the generic's source with no indication which call site asked for that type, and with three or four instantiations that is the difference between a readable refusal and a puzzle. It is a context stack in `ctx` and a `Loc.note` per frame, and it touches every `fail` under an instantiation |
|
||
| **Fiddly** | move-only and ownership. `Types.is_move_only (Var _)` is false, but the same variable at `(Vec i32)` is move-only — so the abstract pass **cannot decide ownership at all**, and the dead-set analysis is only sound per instantiation. Today that means a generic body that moves its parameter type-checks abstractly and is caught, if at all, at one instantiation and not another. The rule has to be stated: either ownership is checked only per copy (and the abstract pass skips it, so a generic may be accepted and its instantiation refused), or type variables carry a move-only constraint, which is a constraint system and plan.org says not yet. One smaller thing in the same bucket, found and left alone: the abstract pass over a generic body that calls *another* generic at a concrete type generates that copy and keeps it, so plain `flan emit` can carry a body no call site asked for. It is a valid instantiation and `Reach.link` drops it, so `flan build` and `flan run` are unaffected — but the abstract pass is meant to leave nothing behind and this is the one thing it does |
|
||
| **No plan** | (1) **Unbounded instantiation.** `(defn grow [x $t] () (grow [x x]))` asks for a copy at `[2 t]`, which asks for one at `[2 [2 t]]`, forever. Before the cap it did not fail, it *hung* — and since `Session.eval` runs this same code, the thing that hangs is `C-c C-c`, with the dev daemon wedged behind it and no error to show. That is the project's stated priority hanging on three lines of ordinary-looking Flan, so the spike stops it: a depth counter in `env`, refusing past 32 and naming the type it had reached (`spike/generics/runaway.flan`). **The number is arbitrary and the designed refusal — one that names the chain of instantiations rather than the depth it gave up at — is still open.** **Odin has no cap of its own**, so there is no implementation to copy. (2) **Generic structs and containers.** `Types.Named` is a bare string with no parameters, so `(defstruct Pair [a $t b $t])` cannot be spelled at all — a parameterised named type is a change to `Types.t` and therefore to every backend, `Render`, DWARF and the layout calculator. (3) **`println` over a type variable.** plan.org's one compiler-provided exception; the abstract pass rejects it (`no printer for t`), see question 6. (4) **Generics across packages.** `Load` flattens imports into one namespace before checking, so it happens to work here, but a package boundary that is ever a real compilation-unit boundary would need the generic's *body* to cross it — the thing separate compilation cannot do and the reason C++ puts templates in headers |
|
||
|
||
The "no plan" row's first entry is the one to take seriously: it is not a missing feature, it is a hang, and it is
|
||
reachable from three lines of ordinary-looking Flan.
|
||
|
||
## Question 5 — what collapsing prelude.ml's 34 functions would actually require
|
||
|
||
Bucketed by what the body needs from the element type, which is readable straight off the sources. `spike/generics/prelude-shapes.flan` is the experiment: the same bodies over `$t`, checked, instantiated and run at `i32`
|
||
and `f32`, printing the right answers and emitting `keep-i32`, `fold-i32`, `fold-f32`, `apply!-i32`, `apply!-f32`,
|
||
`flip!-i32`, `flip!-f32`.
|
||
|
||
**Collapse as they are written — nothing but the signature changes.** `swap-i32!`/`swap-f32!`/`swap-bytes!`,
|
||
`reverse-i32!`/`reverse-f32!`, `map-i32!`/`map-f32!`, `reduce-i32`/`reduce-f32`, `filter-i32`/`filter-f32`,
|
||
`sort-i32-by!`/`sort-f32-by!`. They only move elements, or they already take the operation as a function value.
|
||
`filter` is the strongest case and the one that surprised: it allocates — `(vec-new t)`, `push`, returns
|
||
`(Vec t)` — and the type-erased container runtime made that work with no changes at all, because `SizeOf`/`AlignOf`
|
||
are computed at the instantiation site where the type is concrete. **That is the direct confirmation that
|
||
spec-memory.md's type-erased `Vec`/`Map` and monomorphised functions compose**, which is the thing to check before
|
||
building either.
|
||
|
||
**Do not collapse without a signature change.** `sort-i32!`/`sort-f32!`/`sort-bytes!` need `<`;
|
||
`index-of-i32`/`index-of-byte` need `=`; `min-i32`/`min-f32`/`max-i32`/`max-f32` need `<`. Under plan.org's
|
||
rejection rule every one of them must take the comparison as a `(Fn [t t] bool)` — which means `(sort! xs)`
|
||
becomes `(sort-by! xs (fn [a b] (< a b)))` at every call site in the corpus. The functions collapse; the *calls*
|
||
get longer. That is the visible cost of "no constraints", and it is a language-ergonomics decision rather than a
|
||
compiler one.
|
||
|
||
**Do not collapse at all, as written.** `sum-i32` returns `i64` and `sum-f32` returns `f64`: each widens its
|
||
element with an explicit cast, because there is no implicit widening anywhere in the language. "The wider type
|
||
that `t` accumulates into" is not expressible over an unconstrained variable — it is a type-level function, which
|
||
is a constraint system or an associated type, and plan.org rules both out for now. A generic `sum` would have to
|
||
be `(defn sum [s [$t] init $u add (Fn [$u $t] $u)] u ...)`, at which point it is `reduce` and should just be
|
||
`reduce`. Likewise `append-i64!`/`append-f64!`: their bodies are `I64ToBytes` and `F64ToBytes`, two different
|
||
primitives, and picking between them per instantiation is exactly the compile-time overloading plan.org says
|
||
multimethods are for.
|
||
|
||
Counted by name, the 27 of the family I could account for split **13 / 9 / 5**:
|
||
|
||
- 13 collapse cleanly into 6 generics — `swap-i32!` `swap-f32!` `swap-bytes!`, `reverse-i32!` `reverse-f32!`,
|
||
`map-i32!` `map-f32!`, `reduce-i32` `reduce-f32`, `filter-i32` `filter-f32`, `sort-i32-by!` `sort-f32-by!`.
|
||
- 9 collapse into 4 but change their signatures and every call site — `sort-i32!` `sort-f32!` `sort-bytes!`,
|
||
`index-of-i32` `index-of-byte`, `min-i32` `min-f32` `max-i32` `max-f32`.
|
||
- 5 do not collapse — `sum-i32` `sum-f32`, `append!` `append-i64!` `append-f64!` — because they are not one
|
||
function written twice; they are functions that happen to rhyme.
|
||
|
||
So the net is on the order of **27 → 15**, not 27 → 6, and the prelude keeps a per-type layer for the numeric
|
||
ones.
|
||
|
||
## Question 6 — what contradicts plan.org
|
||
|
||
**1. plan.org bundles two decisions that are independent, and the spike had to implement both separately.** It
|
||
says parametric polymorphism is "Odin's model", and it says an unconstrained variable's `=`, `<`, `+` and `hash`
|
||
are "rejected, not silently instantiated". **Odin does not do the second.** Odin checks a polymorphic body only
|
||
per instantiation, so `a + b` over a `$T` compiles there and fails only when — and if — someone instantiates it at
|
||
a type without `+`. Getting plan.org's rule instead requires a second pass that type-checks the body with nothing
|
||
substituted, which is `check_generic` in this spike: one extra whole-body check per generic `defn`, discarded.
|
||
It is cheap and it is worth it, but it is *not* Odin's model and the plan should stop saying it is.
|
||
|
||
**2. The abstract pass rejects `println` over a type variable**, and plan.org names `println` as "the one
|
||
compiler-provided exception: it selects a structural printer at each concrete instantiation". Those two statements
|
||
cannot both hold as written: a pass that decides an operator's legality without substituting cannot make an
|
||
exception for the one operator whose legality is only decidable after substituting. `(defn show [x $t] () (println
|
||
x))` gets `no printer for t` today. The resolution is small but it is a decision, not an oversight: the abstract
|
||
pass needs an explicit allow-list of forms it defers to instantiation, `println` being the first member. Every
|
||
member of that list is a place where a refusal moves from the definition to a call site, which is exactly what
|
||
plan.org's rule was trying to avoid — so the list should stay short and be written down.
|
||
|
||
**3. The sigil.** Already superseded by the author's revision, and the spike is built to the revision. Recorded
|
||
here because plan.org still says "no sigil" and the correction belongs in the record rather than being patched
|
||
over: without a binding site there is no way to tell introduction from use, and `check.ml:563` already had the
|
||
contradiction in miniature — an unknown *length* name in `[n t]` is an error while an unknown *type* name in the
|
||
same brackets became a type parameter.
|
||
|
||
**4. Ownership is not decidable without the type.** Not contradicted by plan.org, because plan.org does not
|
||
mention it; stated here because it is the interaction that will bite. `Types.is_move_only` is a property of the
|
||
concrete type, and spec-memory.md's whole dead-set analysis is downstream of it. Every other analysis in the
|
||
checker survives abstraction; that one does not.
|
||
|
||
## `$n` in length position, as asked
|
||
|
||
Not built, and it does not fall out for free. `(defn rotate [xs [$n i32]] ...)` would let a function be generic
|
||
over array length the way Odin's `$N: int` does. The cost, specifically:
|
||
|
||
- `Ast.len` is `Lint of int64 | Lname of string`, so `$n` parses today as `Lname "$n"` and needs no reader or
|
||
parser change — the same free ride the type sigil got.
|
||
- But `Types.Array` is `int64 * t`. A length that is a *variable* means either a third case or a `len` type
|
||
inside `Types.t`, and `Types.t` is consumed by `emit.ml`'s layout calculator, `x86.ml`, `render.ml`, the DWARF
|
||
path and the map key-pair emitter. That is the same "change `Types.t` and every backend" price generic structs
|
||
pay, for a smaller prize.
|
||
- `bind_ty` gains a length-binding case (`Array (n, p)` against `Array (m, a)` binds `n := m`), `mangle_ty` gains
|
||
a number, and `array_len` has to answer "a variable" rather than failing — which means the checker's
|
||
compile-time constant folding has to know a length can be symbolic until instantiation.
|
||
|
||
Everything after the second bullet is the expensive part, and it is expensive for the same reason generic structs
|
||
are. If both are wanted, they are one project and should be sequenced together; if only one is, this is the one
|
||
to drop.
|
||
|
||
## Reproducing
|
||
|
||
`dune test --root .` is green either side of this work. One caveat for anyone reproducing under load:
|
||
`test_dev`'s `the daemon never listened` check is timing-sensitive and fails identically at `97cb77d` with
|
||
`lib/check.ml` restored from that commit — it is not this lane's. On an idle machine it passes.
|
||
|
||
```
|
||
dune exec --root . bin/main.exe -- run spike/generics/id.flan
|
||
dune exec --root . bin/main.exe -- run spike/generics/swap.flan
|
||
dune exec --root . bin/main.exe -- run spike/generics/sort.flan
|
||
dune exec --root . bin/main.exe -- run spike/generics/two-vars.flan
|
||
dune exec --root . bin/main.exe -- run spike/generics/prelude-shapes.flan
|
||
dune exec --root . bin/main.exe -- check spike/generics/reject.flan # the refusal
|
||
dune exec --root . bin/main.exe -- check spike/generics/runaway.flan # the depth cap
|
||
bash spike/generics/run.sh # the sweep
|
||
```
|