diff --git a/docs/SPIKE-DUPLICITY.md b/docs/SPIKE-DUPLICITY.md new file mode 100644 index 0000000..e0b208b --- /dev/null +++ b/docs/SPIKE-DUPLICITY.md @@ -0,0 +1,590 @@ +# The duplicity audit: where the two sides meet, and where one side repeats itself + +> **Nothing was built.** This is a reading of `lib/check.ml`, `lib/types.ml`, `lib/emit.ml`, +> `runtime/flan_dyn.c`, `lib/prelude.ml`, `vendor/edn/read.flan`, `plan.org` and `spec-memory.md`, with +> twenty-odd probe programs run through `_build/default/bin/main.exe check|emit|run` where a probe settles +> something a reading cannot. Every claim below is either cited to a line or reproduced from a probe whose +> output is quoted. Read against `dev-loop` at `5bd25b6`. A sibling lane is implementing dyn on the x86 +> backend; nothing here turns on it. + +The doctrine being audited: **every capability has two sides, and the rule is never to repeat yourself on +the same one.** The dyn side is tagged, GC-heap, heterogeneous, unannotated, and wrong at run time. The +native side is untagged, allocator-managed, annotated, and wrong at compile time. A dyn vec and a `(Vec T)` +are two implementations of one idea and that is correct; two implementations on the *same* side is the +smell. SBCL is the named model for the error half: derive what is derivable at compile time, be dynamic +where it is not. + +The audit found **one memory-safety hole**, **three silent acceptances that should be refusals**, **two +capabilities the typed side lacks and the runtime already implements**, and **two same-side duplications +ready to retire**. Ranked questions are in §B; the duplications are in §C. + +--- + +## 0. The first correction: the doctrine's "no annotations" is not what shipped + +The doctrine says the dyn side takes no annotations. The implementation takes no *parameter* annotations. +The return slot is mandatory and always was — `HANDOFF-dyn-m1.md:9-19` records the decision and its reason, +which is structural rather than a TODO: an optional return slot has no syntactic resolution, because +`(defn f [] (Rune {.code 65}) (bar))` is both a type application and a struct literal in the same position, +and that misparse is what removed the old optional slot. + +The probe confirms it. `(defn f [x] (println x))`: + +``` +e4.flan:1:13: println takes no type arguments — generics are milestone 5 +``` + +`(println x)` was read as the return *type*. Every dyn function in this document is spelled +`(defn f [x] dyn ...)`, with `dyn` written out. + +**Verdict: doctrine-vs-implementation mismatch, benign but load-bearing.** It means the author's sketching +case — `(defn settle [row col] ...)` — is still not writable, which is `SPIKE-INFERENCE.md`'s answer +arrived at from the other direction (`docs/SPIKE-INFERENCE.md:17-20`: that spelling "provably cannot be +given the meaning they want"). It also flattens item 3 below: neither `[x $t]` nor `[x]` frees anybody from +writing a return type, so the choice between them is never about annotation volume. + +--- + +## 1. Absence — Option on one side, nil on the other + +**There is no nil.** Not "two absence systems"; one, plus a documented value with no producer. + +``` +$ flan check a1.flan # (defn f [] dyn nil) +a1.flan:1:16: unknown name nil +``` + +`flan_dyn_nil` is defined in the runtime (`runtime/flan_dyn.c:696`), in the stub +(`runtime/flan_dyn_stub.c:80`), declared in the ABI (`runtime/flan_dyn.h:35`), declared to LLVM +(`lib/emit.ml:3001`), and exercised eleven times in `test/dyn_ops.c`. **No path in `lib/check.ml` +constructs one.** The dyn side's absence value is reachable from C and from nothing a Flan program can +write. + +The sharpest thing in the audit is what stands in its place. `box` refuses `Unit` with this +(`lib/check.ml:1436-1439`): + +> `()` does not box into dyn — a value of the zero-sized type carries nothing a dyn could hold. The absent +> dyn value is **nil, which is what an `if` with no else branch answers here**. + +The message describes behaviour the compiler does not implement. `(defn f [x] dyn (if x 1))` does not +answer nil; it is refused, by that very message: + +``` +a2.flan:1:17: () does not box into dyn — ... The absent dyn value is nil, which is what an if + with no else branch answers here +``` + +The sentence is a design note that reads as a description. A user following it writes the form it names and +gets the refusal that names it. + +`(Option dyn)` checks clean (probe `a3`) and is coherent: `Option` is a two-case data type decided +structurally in the checker (`lib/check.ml:3025-3033`) and never desugared, so its payload type is +unconstrained; `owning` walks `Option e` into `e` (`lib/check.ml:451`) and `Dyn` owns nothing, so no region +rule fires. + +**Verdict: undecided-needs-author, but simpler than the brief assumes.** There is one reachable absence +system today, not two. The conflict is prospective, and the decision is not "reconcile two systems" but +"what may produce a nil, and what does one do at a typed boundary". The three coherent answers: + +1. **`nil` is never produced.** Delete the sentence at `check.ml:1436-1439`, keep the `Unit` refusal, and + let `(Option dyn)` be the dyn side's absence too. Cheapest, and loses the Clojure feel. +2. **`nil` is produced and unboxes to a trap.** Symmetrical with every other `need_*`: `flan_dyn_need_i64` + of a nil traps exactly as it traps on a text. +3. **`nil` is produced and unboxes to `None` at an `(Option T)` want.** The only answer that makes the two + absence systems one, and the only one that puts an implicit conversion at the boundary + `check.ml:1367-1380` exists to keep sharp — "nowhere else does the compiler decide a dyn is an i64 on its + own", and this would be the compiler deciding a dyn is a `None`. + +Related, and not in the brief's ten: **truthiness**. `(defn f [x] dyn (if x 1 2))` checks and runs, and the +condition goes through `flan_dyn_need_bool` (`lib/check.ml:1455-1459`), so a dyn `if` is strict-bool — a nil +or an int in the condition traps. `plan.org:908-910` declares the CL-vs-Clojure truthiness question "moot +under static typing". **It is not moot on the dyn side**, and the strict-bool answer is currently the one +that fell out rather than the one that was chosen. + +--- + +## 2. Equality and ordering — not two meanings, one side missing a case + +Typed `=` is numbers and enums and nothing else. `lib/types.ml:166-168`: + +```ocaml +let is_comparable = function Enum _ -> true | t -> is_numeric t +let is_equatable = is_comparable +``` + +`is_equatable` is a bare alias for `is_comparable`. The dyn `=` is structural over everything and is the one +dyn operation that never traps (`SPIKE-DYNAMIC.md:285-287`), and dyn `<` orders text bytewise by `memcmp` +(`SPIKE-DYNAMIC.md:273-275`). + +One probe, both operators, one line apart: + +``` +$ flan check b3.flan +(defn f [x] dyn x) +(defn main [] i32 (do (println (= (f "hi") (f "hi"))) ; accepted + (println (= "hi" "hi")) ; refused + 0)) +b3.flan:2:64: = compares machine numbers; string has no built-in comparison (plan.org, Types) +``` + +And the generic side inverts the same way (`d1`): + +``` +d1.flan:2:32: this call instantiates biggest at $t = string, and string does not answer ordered? +``` + +while `(defn biggest-d [a b] dyn (if (> a b) a b))` at `"a"` and `"b"` checks clean (`c2`). + +The reflex reading is "same operator, two meanings — trap". It is the wrong reading, because it treats the +dyn answer as the anomaly. The dyn answer is *right*, it is cheap, and **the code that implements it already +exists on the typed side too**: `flan_hash_str` and the map's string equality +(`runtime/flan_rt.c:1939`, and `Types.keyable` says `String -> true` at `lib/types.ml:156`). So the typed +side already has a string equality good enough to key a `(Map string V)` — and refuses to let a program call +`=` on two strings. + +That is **same-side duplication in the making, on the typed side**: `keyable` and `is_equatable` are two +answers to "does this type have an equality", they disagree about `string`, and one of them is a `Map` +implementation detail rather than a language rule. + +The four-predicate ceiling is where it shows. `predicate_names` is exactly `[ "ordered?"; "equal?"; +"hashable?"; "numeric?" ]` (`lib/check.ml:412`), and `pred_entails` (`lib/check.ml:490-497`) admits its +table is "only sound while" ordered ⊆ equatable holds — which is only true *because* the set is so small. +`lib/prelude.ml:247-248` says the quiet part: `sort-bytes` exists as a hand-written `sort-by` because "a +`[[u8]]` is not `[ordered?]` **and cannot be**". + +**Verdict: same-side gap on the typed side, not a boundary conflict.** The author's question is not "which +meaning wins" — it is whether typed `=` and `ordered?` grow the `string` case the runtime already implements +with `memcmp`. Growing them retires `sort-bytes`, unifies `keyable` with `is_equatable`, and makes the two +sides agree on strings at no representational cost. + +--- + +## 3. Generics and dyn — two ways to take "any type", and they are not the same way + +Both `[x $t]` and `[x]` take a value whose type is not written. The difference is *where the operations on +it are checked*, and it is total: + +- A generic is checked **at the definition**. An operator over a type variable with no predicate asserting + it is refused there, at the `defn`, before any call exists (`lib/check.ml:976-990`, and + `SPIKE-INFERENCE.md:26-29` quotes the refusal: "`+` over the type variable `t` is refused"). The call site + then re-checks the predicate against the concrete type (`d1` above, and `pred_holds` at + `lib/check.ml:471-483`). +- A dyn parameter is checked **nowhere**. `(defn f [x] dyn (+ x "a"))` checks clean; it traps at run time + (probe `a6`): `dyn +: int and text, and it takes two numbers — (+ 1 "a")`. + +So they overlap on exactly one function — `id` — and diverge on every function with an operator in it. The +generic is monomorphised and costs nothing; the dyn is tagged, heap-allocating and rooted +(`emit.ml:705`: a rooted alloca escapes through `flan_dyn_root_push`, so mem2reg cannot promote it, at every +optimisation level). + +The user's rule falls out and needs no new machinery to state: **write `[x $t]` when the operation is the +same for every type and the caller knows which; write `[x]` when the operation *depends* on the type and +nobody knows it until the value arrives.** `sort` is the first; a config reader is the second. + +**Verdict: clean.** Genuine duplicity, correctly placed. With the caveat that the four-predicate ceiling of +§2 is what makes the generic side look weaker than it is: a generic can only express the four questions the +compiler has builtins for, so every capability outside that set reads as "use dyn" when the honest answer is +"the predicate does not exist yet". + +--- + +## 4. Conditions — the refusal is right, and its absence everywhere else is the hole + +`signal` refuses a dyn condition and a condition with a dyn *field*, each by name +(`lib/check.ml:1976-2005`). Probe `f1`: + +``` +f1.flan:2:31: dyn does not cross into a written type yet — the field payload of the condition Oops + is one, and a payload has to stay rooted across a handler transfer, which is milestone 2 +``` + +The reason given is exact and correct: a payload crosses a handler boundary as a pointer to a frame that is +still alive, and a dyn in it has to stay rooted across a transfer the root stack knows nothing about. + +**But an ordinary `defstruct` with a dyn field is accepted, and nothing roots it.** Probes `e2`, `e5`, `e7`, +`f3` all check clean: + +```lisp +(defstruct S [x dyn]) +(defvar boxes (Vec S)) +(defn stash [] () (push boxes (S {.x (vec-new dyn)}))) +``` + +`flan emit f3.flan` shows what happens: + +```llvm + %dr0 = alloca i64 + call void @flan_dyn_root_push(ptr %dr0) + %t1 = call i64 @flan_dyn_vec_new() +``` + +One root — the *temporary*, for the duration of `stash`'s frame. It is popped at the `ret`. After that the +dyn vec's only reference is `S.x`, inside a `(Vec S)` whose storage belongs to an allocator the collector +never traces. The next allocation collects a live object. + +Nothing in the tree refuses this. `box` has no arm for it — a `Named` type is refused only when it is being +*boxed into* dyn (`lib/check.ml:1450-1452`), not when it *contains* one. `dyn_roots` +(`lib/emit.ml:710`) counts nodes, not fields. `dyn_sites`, the `--no-gc` pass, walks globals' types, +parameters, the return type and `flan_dyn*` call nodes (`lib/check.ml:7104-7136`) — **not struct fields**, so +`(defstruct S [x dyn])` passes `--no-gc` (probe `e6`, clean). That last one is vacuous today, since filling +the field needs a `flan_dyn*` call which the pass does catch; it will stop being vacuous the moment a typed +container boxes into dyn. + +`SPIKE-DYNAMIC.md:402-406` names the machinery that is missing: "a handle to a typed `(Vec Enemy)` would +need the collector to know which fields of `Enemy` are dyn, and a per-type descriptor emitted by the +compiler is how that arrives." The descriptor is M2. The *field* is M1 and is already writable. + +**Verdict: conflict, and the most urgent one in this document.** Not a design conflict — an implementation +hole the design already knows how to close, protected in exactly one place and open everywhere else. Whether +the dyn side needs its own signal story is the *second* question and the easy one: typed payloads serve both +sides fine, because the answer to "I want a dyn in my condition" is the same as the answer to "I want a dyn +in my struct", and both wait on the same descriptor. + +--- + +## 5. Collections — the dyn side is one third built, and `edn/Value` is the other two thirds + +What the dyn runtime has: a vec, mutable, GC-owned (`runtime/flan_dyn.c`, `OBJ_VEC`). What it does not have: +a **map**, a **set**, and **keywords**. There are three object kinds — `OBJ_TEXT | OBJ_VEC | OBJ_INT` +(`SPIKE-DYNAMIC.md:108`) — and four spare box tags (`SPIKE-DYNAMIC.md:57`). + +Keywords are not absent by oversight; they are *typed-side only, at compile time*. `plan.org:920-923`: +"`:space` resolves at compile time against the parameter's enum type... **No runtime cost.**" That is a +different thing from EDN's `Key`, which is a value that exists at run time and can be a map key nobody +declared. + +Meanwhile `vendor/edn/read.flan:71-80` is a complete tagged dynamic value, hand-written in typed Flan: + +```lisp +(defdata Value + [(Nil []) (Bool [b bool]) (Int [n i64]) (Float [x f64]) (Text [s string]) + (Key [s string]) (List [items (Vec Value)]) (Set [items (Vec Value)]) + (Table [entries (Map string Value)])]) +``` + +with its own structural equality, `value=?` (`read.flan:99`), its own list equality (`:116`), its own set +equality (`:128`), its own table equality (`:145`). Every one of those is an operation `flan_dyn_eq` +implements (`SPIKE-DYNAMIC.md:283-300`). + +Counted by *capability* rather than by implementation language, this is unambiguous: `Value` and the dyn +runtime both answer "a heterogeneous value that carries its type at run time". **One capability, two +implementations, same side.** The author's lean is right. + +The price is worth stating precisely, because it is the whole of the decision: + +| `Value` has | dyn has | what closing the gap costs | +|---|---|---| +| `Nil` | `flan_dyn_nil`, unreachable from source (§1) | a producer and a boundary rule | +| `Bool`/`Int`/`Float`/`Text` | all four | nothing | +| `List` | vec | nothing | +| `Key` | — | a fifth object kind or a spare tag; interning if `=` is to stay O(1) | +| `Table` | — | a fourth object kind, a structural hash over tags, ordering for iteration | +| `Set` | — | **hardest**: `keyable` refuses `Value`-shaped keys (`read.flan:57-62`), so a dyn set cannot just be a dyn map either; `Value.Set` is an O(n) vec for exactly that reason and says so (`read.flan:64-69`) | + +The M2 shape that falls out: **`OBJ_MAP` on tag 3 as a fourth kind, keywords as a fifth, and a dyn set as a +dyn map to a unit** — which works on the dyn side precisely because `flan_dyn_eq` has no `keyable` +restriction to run into. The thing `Value` cannot do, dyn can, and that is the argument for the retirement +rather than against it. + +Note the counterpart landed on the *other* side while this audit was being written: **the type-provider lane +has merged to `dev-loop`** — `(edn/defedn Tileset "assets/tileset.edn")` derives a struct from the file at +expansion time (`lib/parse.ml:1321`, `lib/check.ml:4702`, `lib/macro.ml:302`, `docs/BUILT.md:5810-5830`), +`defjson` is the same over a different grammar and shares "the design and not the code" +(`docs/BUILT.md:5944-5960`), and `macro-slurp` is the prelude half (`lib/prelude.ml:1822-1830`). +`docs/PORTING.md:633-637` marks `read-edn` built under that name. So the data-file capability now has both +its sides in the tree at once: `defedn` is the perf side (a struct, at compile time), and a dyn map with no +struct given is the dynamic side. **`Value` is neither.** It is the dynamic side, written before the dynamic +side existed. + +**Verdict: same-side duplication, retire — sequenced behind a dyn map and dyn keywords.** Retiring it before +those land would delete the only thing in the tree that can read a config file whose keys are unknown. + +--- + +## 6. Strings — a one-way door + +Typed `string` is a builtin ptr+len, non-owning, the same shape as a slice (`lib/types.ml:22`, and the +`Allocator` comment at `:35` calls it "a builtin ptr+len"). It appears in no arm of `owning` +(`lib/check.ml:449-459`), which is the operational statement that it borrows: a `(Vec string)` is not +region-only, because the strings in it own nothing to release. + +Dyn text is the opposite: immutable, length-prefixed, **copied on construction**, owned by the collector +(`SPIKE-DYNAMIC.md:118-121`). + +Typed → dyn works and copies, via `flan_dyn_from_bytes` (`lib/check.ml:1430`). The copy is not a wart, it is +forced, and `vendor/edn/read.flan:41-47` already wrote the argument for the same case: a view handed back +out of the function that owns the buffer is "garbage with nothing to say so" once the caller reads the next +file into it. A dyn value can outlive any frame, so a dyn text must own its bytes. Correct. + +Dyn → typed is **refused outright**. Probe `b5`: + +``` +b5.flan:2:20: string does not cross into a written type yet +``` + +`unbox` has arms for `i64`, `f64` and `bool` and a catch-all refusal for everything else +(`lib/check.ml:1450-1474`). So a program can put a string into dyn and can never get it back as a `string`. +It can get the *bytes* — `flan_dyn_at` answers a byte as an int (`SPIKE-DYNAMIC.md:304-305`) — one at a +time. + +The refusal is understandable and the reason is not a representation problem: a `string` is ptr+len and the +text object's bytes are right there inline after the header. It is a **lifetime** problem, and the same one +§4 has. A `string` borrowed out of a GC object is valid until the next collection, and nothing in the +language says so. + +**Verdict: conflict.** Dyn text is a one-way door today, which makes every string-shaped dyn program a +dead end at the moment it wants a typed function. Three exits: a copying `(string-of d alloc)` into a named +allocator (safe, explicit, the arena idiom already in the language); a borrowing one that is valid until the +next collection (fast, and needs a rule the language has no vocabulary for); or leave it refused and make +the dyn side's own string operations complete enough that nobody wants out. The first is the one that fits +`spec-memory.md`. + +--- + +## 7. Allocators vs the GC — the refusal is written for the spelling nobody uses + +`(vec-new dyn alloc)` is refused by name, with a good sentence (`lib/check.ml:4094-4100`): + +> `(vec-new dyn)` takes no allocator — the dyn container's storage is the dyn runtime's, which is what lets +> the collector find the values inside it. + +But **`(with-allocator arena (vec-new dyn))` is accepted in silence.** Probes `b4` and `c5` both check +clean. The ambient allocator is not consulted, not refused, not mentioned. + +That is the wrong way round, because of what `spec-memory.md` decided. The allocator is in the *calling +convention* — `vendor/edn/read.flan:11-18` states the consequence plainly: "`read` takes no allocator and +names none. It does not need to: spec-memory.md puts the allocator in the calling convention, so every +`(vec-new)` and `(map-new)` below takes the *context*". The explicit allocator argument is the rare +spelling; `with-allocator` is the idiom the whole language is written in. The compiler refuses the spelling +a user almost never writes and says nothing about the one they always do. + +`check.ml:627` and `:1289` both record that `with-allocator` "rebinds a dynamic variable, so the tier a +`(vec-new)` will meet is not a property of where the type is written" — so the checker cannot in general +know statically which allocator is ambient. It does not have to: the question here is not *which* allocator, +it is whether an enclosing `with-allocator` is a lie when the form under it ignores it. + +**Verdict: conflict — silent acceptance where a refusal or a note is owed.** The user's model of +`with-allocator` is "everything allocated in here comes from this"; a dyn construction is the one exception, +and the exception is invisible. The author's call: refuse a dyn construction lexically inside a +`with-allocator`, warn, or write the exception down and accept it. Refusing is probably too strong — +`(with-allocator frame (edn/read bytes))` will want to hold a dyn somewhere — which makes this a +documentation-plus-note decision rather than a checker one. + +--- + +## 8. `defstruct` vs `defclass` — the class is dyn with named slots, minus one thing + +`plan.org:132-190` designs `defclass` and it predates dyn entirely. Read its ingredient list against what +the dyn runtime now has: + +| `defclass` needs (plan.org) | dyn already is | +|---|---| +| "runtime class/shape metadata" (`:157`) | the tag, and `flan_dyn_tag_name` | +| identity, so a class instance is not a value that copies (`:135`) | a `flan_obj *`; `test_dyn`'s `sharing` mode asserts identity, not just equality (`SPIKE-DYNAMIC.md:561`) | +| "a managed allocation strategy" (`:157`) | the mark-sweep heap | +| "A small tracing GC confined to class instances remains an option" (`:161`) | built, and confined to exactly dyn values | +| live schema change, "existing instances at their old layout until an explicit migration" (`:173-176`) | a heterogeneous object has no layout to be stale | + +Five of five. Building `defclass` as a third memory model — a third answer to identity, a third allocation +strategy, a third metadata scheme — would be **same-side duplication on the managed side**, and by the +doctrine it is the thing not to do. + +What the dyn side genuinely lacks, and what a `defclass` therefore *adds* rather than duplicates: + +1. **Named slots.** There is no record kind; a dyn vec is positional. This is the same missing `OBJ_MAP` of + §5 — a class instance is a map from slot name to value with a declared slot set, which is a map with a + shape check. +2. **Dispatch.** `(defmethod update ((e Enemy) dt) ...)` — "exact-class, single-argument dispatch" first + (`plan.org:168-170`). The tag is already the dispatch key; a class id in the object header is the + extension. +3. **A declared slot set at all**, which is what makes the compile-time half possible: a `defclass` can + report an unknown slot where a dyn map cannot. + +The one thing that does **not** collapse into dyn, and should stay where it is: `plan.org:157-160`'s "but +*not necessarily* a tracing GC — a world or session arena, pool allocation behind generational `(Handle T)` +values". That is the **typed** side's answer to identity and longevity, and it is a real second side of the +same capability, not a duplicate. A pooled `(Handle Enemy)` over a `defstruct` is the perf side; a `defclass` +is the managed side. Both should exist. + +**Verdict: undecided-needs-author, with the doctrine's answer close to forced.** `defclass` is dyn plus +named slots plus dispatch, sharing one heap and one collector — not a third thing. The corollary, and the +part worth deciding early: `plan.org:192-194` says "Do not add classes until ordinary `struct`, `Handle`, +and reload semantics are working." Under this reading the gating item changed. Classes are now gated on the +**dyn side's map/record kind**, which is M2 and in flight, rather than on `Handle`. + +--- + +## 9. Print, hash, sort — one family already duplicated, two not yet + +**Printing is duplicated three ways on one side, and it is not the dyn/typed split.** +`runtime/flan_dyn.c:308-313` says so itself: + +> A text inside a structure, quoted and escaped. The same table as `flan_rt.c`'s `flan_escape_bytes` and +> `flan_dev.c`'s `flan_dev_emit_str`... + +Three escape tables: `runtime/flan_rt.c:383` (`flan_escape_bytes`, with `:366-372` noting it is already "the +same escape table as `flan_dev_emit_str`"), `runtime/flan_dev.c:237` and again at `:551`, and +`runtime/flan_dyn.c:314` (`emit_escaped`). `SPIKE-DYNAMIC.md:329-332` calls its own "the third copy" and +leaves the instruction "If that table changes, change all three." + +Two of those three are on the same side. `flan_rt.c`'s is `println`'s; `flan_dev.c`'s is the inspector's, so +the REPL can parse the printed form back. That pair predates dyn and is same-side duplication that dyn has +now made three-way. The *dyn* copy is the one with a defence, and `SPIKE-DYNAMIC.md:334-338` gives it: a +typed `Vec` prints as `` because the typed printer will not walk storage it does not own, while a dyn +vec's storage belongs to the collector and the printer is inside the runtime that owns it. That is correct +duplicity. Three tables is not. + +**Hashing is typed-only.** `flan_hash_fn`, `flan_hash_flat`, `flan_hash_str`, `flan_hash_combine` +(`runtime/flan_rt.c:1807, 1911, 1939, 1954`), reached through `Types.keyable` and the checker's `key_pair` +walk. The dyn side has none, because it has no map. **Verdict: clean today, and the first thing M2 gets +wrong if it is careless** — a dyn map needs a structural hash over tags, and that hash must *call* +`flan_hash_mem`/`flan_hash_str` rather than re-derive them, or the family duplicates on the dyn side the way +printing duplicated on the typed one. + +**Sorting is typed-only** — `sort` (`lib/prelude.ml:277`), `sort-by` (`:304`), `sort-bytes` (`:1399`). +Nothing is built on the dyn `lt`/`le`/`gt`/`ge`. `sort-bytes` is already a half-duplicate of `sort` that +exists only because `[[u8]]` cannot answer `ordered?` (`lib/prelude.ml:247-248`) — so it is the §2 gap, +appearing in the prelude as an extra function. + +--- + +## 10. The SBCL lesson, concretely + +SBCL's mechanism is a **type lattice plus an IR1 fixpoint**. `ir1-optimize-cast` +(`src/compiler/ir1opt.lisp:3765`) intersects the value's *derived* type with the *asserted* one; where the +intersection is empty the conflict is unconditional, and the node is rewritten to +`%compile-time-type-error` (`ir1opt.lisp:3837`), whose warner is `%compile-time-type-error-warn` +(`ir1util.lisp:4351`). That is a full `WARNING` at compile time, and the form is **still emitted**, so the +program that was warned about also signals at run time. What cannot be *proved* wrong is not dropped either: +`convert-type-check` (`src/compiler/checkgen.lisp:518`), driven by `generate-type-checks` (`:684`), lowers +the unprovable assertion to a run-time check. + +Measured, not paraphrased — `sbcl --noinform --non-interactive` on `(defun f () (+ 1 "a"))` then calling it: + +``` +; caught warning: +; Constant "a" conflicts with its asserted type number. +; See also: +; The SBCL Manual, Node "Handling of Types" +; +; compilation unit finished +; caught 1 WARNING condition + +# +``` + +Both halves in one run: a compile-time `WARNING` naming the constant and the asserted type, **and** a +function that still exists and still signals. The warning changed the diagnostics and nothing else. + +Two things carry over and one does not. + +**Does not carry over: the derivation.** Flan has `Types.equal` and `fits` (`lib/types.ml:173`), and `fits` +is `equal` with one exception for `Never`. No lattice, no unions, no intersection, no fixpoint. "Derive the +type of every expression and intersect it with what is wanted" is not a change to `check.ml`; it is a +different `check.ml`. Anyone reading "be like SBCL" as "add type derivation" is reading a year of work into +a sentence. + +**Carries over, and is nearly free: refuse at the site where the pre-box type is still in hand.** This is +the part worth doing. `box` (`lib/check.ml:1418`) and `dyn_fold` (`lib/check.ml:3414`) both receive the +*typed* expression before it is boxed — `dyn_fold`'s own comment says "the typed side of a mixed pair is +boxed on the way in". So at `(+ dyn-x "a")` the second operand's type is `Types.String`, sitting in a +variable, at the moment the compiler decides to emit `flan_dyn_add`. Today that compiles (probe `a6`) and +traps: + +``` +dyn +: int and text, and it takes two numbers — (+ 1 "a") +``` + +The trap message is written from information the *checker* had. One match in `dyn_fold` — if an operand's +pre-box type is known and no arm of the dyn operator accepts that tag, refuse — is SBCL's empty-intersection +case exactly, with no inference, no lattice and no new pass. It catches every literal and every typed +binding flowing into a dyn operator, which is most of what a beginner writes wrong, and it catches nothing +that is genuinely dynamic, which is the whole point. + +**Carries over, and is the part to resist skipping: warn, and still emit.** SBCL's discipline is that a +compile-time type warning never changes what the program does. If Flan takes the refusal route instead, it +should be a refusal only where the conflict is unconditional — a known non-numeric tag into an arithmetic +operator — and never a refusal on a heuristic, because the dyn side's contract is that it runs. + +One piece of evidence about how thin the typed side's own derivation is, since it bears on how much of SBCL +is even reachable from here. Fully typed `(+ 1 "a")` refuses like this (probe `a5`): + +``` +a5.flan:1:35: expected string, found the integer literal 1 +``` + +It refused because the literal `1` adopted the type of the *second* operand and failed — not because `+` +rejects text. The typed side has no statement anywhere that `+` takes numbers; it has literal adoption and +`Types.equal`. That is worth knowing before promising SBCL-shaped diagnostics. + +--- + +## A. The two sides, as the language stands + +| capability | native side | dyn side | verdict | +|---|---|---|---| +| parameter types | written | omitted | clean | +| **return type** | written | **written** (`HANDOFF-dyn-m1.md:9-19`) | doctrine mismatch (§0) | +| integers | `i8`…`i64`, `u8`…`u64` | `i64` only, 48-bit inline + box | clean | +| floats | `f32`, `f64` | `f64` only | clean | +| absence | `(Option T)`, `Some`/`None` | `nil` — **unreachable from source** (§1) | undecided | +| truthiness | n/a | strict bool via `need_bool` | undecided (§1) | +| equality | numbers + enums (`types.ml:168`); `string` refused | structural, never traps, text bytewise | typed side missing a case (§2) | +| ordering | `ordered?` = numbers + enums | numbers + text `memcmp` | same (§2) | +| map keys | `keyable`: ints, enums, bool, **string**, arrays, structs | — no map — | typed side self-inconsistent (§2, §5) | +| "any type" | `$t` + `{:where}`, checked at the `defn` | dyn, checked nowhere | clean (§3) | +| conditions | struct payloads | refused, by name (`check.ml:1976-2005`) | clean; the hole is elsewhere (§4) | +| struct with a dyn field | **accepted, unrooted** (§4) | — | **conflict** | +| vec | `(Vec T)`, allocator-owned, moves | `(vec-new dyn)`, GC-owned | clean | +| map | `(Map K V)`, open-addressed | **absent** | gap (§5) | +| set | absent (`Value.Set` is an O(n) vec) | absent | gap (§5) | +| keywords | compile-time enum resolution (`plan.org:920`) | absent | gap (§5) | +| strings | ptr+len view, borrows, owns nothing | GC text, immutable, copies in | one-way door (§6) | +| storage | `with-allocator`, in the calling convention | GC; ambient allocator **silently ignored** (§7) | conflict | +| identity / long-lived objects | `defstruct` + pooled `(Handle T)` — planned | `flan_obj *` | clean; `defclass` is the dyn side (§8) | +| dynamic data value | `defedn`/`defjson` → a struct, at compile time — **landed** | dyn value; **plus `edn/Value`** | same-side duplication (§5) | +| printing | `flan_rt.c` + `flan_dev.c` — **two on one side** | `flan_dyn.c` | typed side duplicated (§9) | +| hashing | `flan_hash_*` | absent | clean, at risk in M2 (§9) | +| sorting | `sort`, `sort-by`, **`sort-bytes`** | absent | typed side half-duplicated (§9) | +| compile-time type errors | `Types.equal` + literal adoption | none at all | the SBCL question (§10) | +| C interop | `declare`/`declare-c` | refused, by name (`check.ml:6082`) | clean | + +--- + +## B. The genuine conflicts, ranked, each as one question + +1. **A `defstruct` may hold a `dyn` field, and nothing roots it once the frame that built it returns — should the field be refused until the per-type descriptor exists, the way a condition's field already is?** (§4; `check.ml:1976-2005` refuses one case, `box`'s `Named` arm at `:1450` permits the rest; `emit f3.flan` shows the single root popped at `ret`.) +2. **What produces a `nil`, and what does a `nil` do at a typed boundary — trap, or become `None`?** (§1; `check.ml:1436-1439` describes a producer that does not exist.) +3. **Does `with-allocator` around a dyn construction refuse, warn, or stay silent?** (§7; the explicit spelling is refused at `check.ml:4096`, the idiomatic one is accepted at probes `b4`/`c5`.) +4. **Should typed `=` and `ordered?` grow the `string` case, given `keyable` already says `string` has an equality and `flan_hash_str` already implements it?** (§2; `types.ml:156` vs `types.ml:168`.) +5. **Can a dyn text become a typed `string` — by copy into a named allocator, by borrow until the next collection, or not at all?** (§6; `check.ml:1450-1474` has no arm.) +6. **Is `defclass` the dyn side with named slots and dispatch, sharing one heap — or a third memory model?** (§8; if the former, classes are gated on the dyn map, not on `Handle` as `plan.org:192` says.) +7. **Is a dyn `if` strict-bool because that was chosen, or because `need_bool` was the arm that existed?** (§1; `plan.org:908-910` calls the question moot and it is not.) +8. **Does `dyn_fold` refuse an operand whose pre-box type no arm of the operator accepts — SBCL's empty-intersection case, with no inference added?** (§10; the type is in hand at `check.ml:3414`.) +9. **What is M2's object-kind budget: `OBJ_MAP`, a keyword kind, both — and does a dyn set become a dyn map to unit?** (§5; four spare tags, `SPIKE-DYNAMIC.md:57`.) +10. **Does the doctrine's "no annotations" concede the mandatory return slot permanently, or is `SPIKE-INFERENCE.md`'s return-type inference the way back?** (§0.) + +--- + +## C. Same-side duplications to retire + +1. **`vendor/edn/read.flan`'s `Value`** — a tagged dynamic value hand-written on the typed side, with its + own structural `value=?` (`:99`), `items=?` (`:116`), `sets=?` (`:128`), `tables=?` (`:145`). One + capability, two implementations. **Retire — sequenced behind a dyn map and dyn keywords (§5), not + before.** `defedn`/`defjson` landing on the perf side is what makes the pair complete once dyn's half + is; `Value` is the leftover middle. +2. **The three escape tables and their number formatters** — `flan_rt.c:383`, `flan_dev.c:237` and `:551`, + `flan_dyn.c:314`, with three files each instructing the reader to change the others. The dyn copy has a + defence (§9). **The `flan_rt.c`/`flan_dev.c` pair does not, predates dyn, and should collapse to one + exported entry point the other two call.** +3. **`Types.keyable` vs `Types.is_equatable`** (`types.ml:156` vs `:168`) — two answers to "does this type + have an equality", disagreeing about `string`, one of them a `Map` implementation detail wearing a + language rule's name. **Unify** (this is question B4 by another route). +4. **`sort-bytes`** (`prelude.ml:1399`) — a hand-written `sort-by` that exists only because `[[u8]]` cannot + answer `ordered?`. **Falls out** the moment B4 is answered; not worth touching on its own. + +Not duplication, and listed so nobody retires it by mistake: a typed `Vec` printing as `` while a dyn +vec prints its elements (`SPIKE-DYNAMIC.md:334-338`); the dyn operators promoting `(+ 1 2.5)` while the +typed language has no implicit widening (`SPIKE-DYNAMIC.md:258-262`); and `flan_dyn.c` being its own +translation unit with a strictly one-way dependency on `flan_rt.c` (`SPIKE-DYNAMIC.md:427-434`), which is +what makes `--no-gc` a file-selection change rather than a dead-code-elimination wish.