The duplicity audit: where the two sides meet, and where they already leak
This commit is contained in:
parent
5bd533c64e
commit
477ec2226e
590
docs/SPIKE-DUPLICITY.md
Normal file
590
docs/SPIKE-DUPLICITY.md
Normal file
@ -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 `<vec>` 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
|
||||
|
||||
#<simple-type-error expected-type: number datum: "a">
|
||||
```
|
||||
|
||||
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 `<vec>` 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.
|
||||
Loading…
x
Reference in New Issue
Block a user