diff --git a/lib/check.ml b/lib/check.ml index f0b3730..99c1675 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -406,20 +406,14 @@ let unimplemented loc what milestone = Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is [where intrinsics.type_is_ordered(T)]) with forty-one predicates against - these five. The fifth, [copyable?], has no Odin counterpart at all: Odin - has no move semantics, so [$T] never has to answer the question. The prior - art there is Rust's [T: Copy], with the difference that [copyable?] is a - question the compiler answers rather than a trait a user implements. *) -let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ] + these four. There is no [copyable?] any more and no Odin counterpart + either: Odin has no move semantics, and since the repeal neither does this + language, so [$T] never has to answer the question. *) +let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?" ] (* ── What a type owns, transitively ──────────────────────────────────── - spec-memory.md: "Ownership is structural, not declared." [Types.is_move_only] - answers the same question one level deep and deliberately stops there — a - [Named] is not move-only, because making it so is the transitive ownership - model that recursive teardown would need, and there is no recursive teardown. - This walk is the *other* use of the same fact, and the two must not be - collapsed: nothing here feeds the move checker, and a type this says yes - about is still copied and still tracked exactly as it was yesterday. + The one structural ownership question that survived the repeal, because it + is not about copying at all. What it decides, and the only thing it decides, is whether a container of this element type has to be built against a region allocator — see @@ -438,12 +432,11 @@ let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable contain itself by value anyway — [check_finite] refuses that — only through a container, which is an arm that answers for itself. - [env.unions], the untagged ones, are deliberately not consulted: a move-only - member in one is refused outright, and that refusal is not waiting on - teardown the way these were — nothing anywhere records which member is - live, so there is no fact a release could read. A region removes the - teardown question and leaves that one exactly where it was, so an untagged - union owns nothing and there is nothing here to walk. *) + [env.unions], the untagged ones, are deliberately not consulted: nothing + anywhere records which member of one is live, so there is no fact this + walk could read — an untagged union is treated as owning nothing, and what + its members point at is the program's, through whatever tag it keeps + beside the union. *) let owning_fields env n = match Hashtbl.find_opt env.structs n with | Some s -> [ s.Tast.fields ] @@ -488,23 +481,20 @@ let pred_holds p (t : Types.t) = [key_pair]. *) | "hashable?" -> Types.keyable t | "numeric?" -> Types.is_numeric t - | "copyable?" -> not (Types.is_move_only t) | _ -> false (* What one declared predicate *also* gives you. These are entailments over the type system as it stands, not conveniences: every type [is_comparable] - admits is a number or an enum, so it is equatable and it is not move-only. - The table is only sound while that is true — an ordered move-only type, or - an ordered type with no [=], would make it wrong — so it lives in one place - and says so. The gain is real ergonomics: [{:where (ordered? $t)}] is - enough for a [sort!] that also compares and reads its elements twice, - rather than three predicates on one line. *) + admits is a number or an enum, so it is equatable. The table is only sound + while that is true — an ordered type with no [=] would make it wrong — so + it lives in one place and says so. The gain is real ergonomics: + [{:where (ordered? $t)}] is enough for a [sort!] that also compares, + rather than two predicates on one line. *) let pred_entails ~declared ~wanted = String.equal declared wanted || match wanted, declared with | "ordered?", "numeric?" -> true | "equal?", ("numeric?" | "ordered?") -> true - | "copyable?", ("numeric?" | "ordered?" | "equal?" | "hashable?") -> true | _ -> false let declares preds v wanted = @@ -518,27 +508,6 @@ let declares preds v wanted = properties are the Vec's. *) let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None -(* ── Move-only, with a type variable defaulting to move ──────────────── - [Types.is_move_only (Var _)] is [false] and cannot be anything else: the - same variable is [i32] at one instantiation and [(Vec i32)] at the next, so - the property is not decidable abstractly. The author's decision is to - default to **move**, because move is the *stricter* rule: assuming it can - only refuse a program that would have been fine, never admit one that - double-frees. [copyable?] is the opt-out, exactly as Rust's [T: Copy] is. - - In the body this means a generic may not use a parameter twice without - declaring [copyable?]. Since the repeal this gates the structural rules - only — what a struct or union may own — not any use of a binding. - - A [Var] only ever survives the abstract pass. Inside an instantiation - [env.subst] has made everything concrete, so this is [Types.is_move_only] - there and the strictness costs nothing at a call site. *) -let rec move_only preds (t : Types.t) = - match t with - | Types.Var v -> not (declares preds v "copyable?") - | Types.Option e | Types.Array (_, e) -> move_only preds e - | t -> Types.is_move_only t - (* ── (Map K V), spec-memory.md ────────────────────────────────────────── Both halves are checked where the type is written, not where an operation is, so that a map nothing ever uses is still refused if it cannot work. @@ -567,8 +536,8 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) = (* The key, as far as the type alone can say. A struct passes here and is decided at the operation, by [key_pair], which walks its fields — the struct table is not necessarily complete while a type is being resolved, - and every map that exists reaches an operation anyway, because a global of - move-only type is refused and a local needs (map-new). *) + and every map that exists reaches an operation anyway, because a global + map starts zeroed and a local needs (map-new). *) (* A type variable is a map key exactly when the [where] clause says it is hashable. Nothing else about it is knowable here, and falling through to [Types.keyable] would answer no for a variable that is about to be @@ -1944,16 +1913,17 @@ and var ctx loc ~want name = | None -> captured ctx loc name; Loc.failk "check/unknown-name" loc "unknown name %s" name) -(* What remains of spec-memory.md's ownership section after the repeal of - 2026-09-18 is entirely in the types: move-only decides what may be copied, - the struct/union rules below decide what may own what, and the - allocator's capability decides what a free means at run time. Which frees - run, and in what order, is the program's own business — the same contract - Odin ships with — and the dev build's generation words are the net under - it. The flow analysis that used to live here (a per-function dead set, a - borrow flag over container reads, a loop-iteration diff) tracked use-after- - move and double-free statically; it was repealed rather than repaired when - its holes proved structural. See spec-memory.md, "The repeal". *) +(* What remains of spec-memory.md's ownership section after the repeals of + 2026-09-18 is the allocator's side alone: the region rule decides where a + container of owning elements may be built, and the allocator's capability + decides what a free means at run time. Everything copies — a container as + its header, the copies aliasing one buffer — and which frees run, and in + what order, is the program's own business, the same contract Odin ships + with; the dev build's epoch words are the net under it. The flow analysis + that used to live here (a per-function dead set, a borrow flag, a + loop-iteration diff) went in the first repeal; the move-only concept + itself — copy refusals, [copyable?], the struct/union owning rules — went + in the second. See spec-memory.md, "The repeal". *) (* [defer_ok] is granted again before *every* form, not once before the block: [check] withdraws it as it starts, so granting it once would let the first @@ -3913,9 +3883,8 @@ and named_call ctx ~want loc name args = (* A field is never freed on its own: it would leave its owner partly dead with no way to say so. *) fail loc - "free takes a move-only value — a Vec, a Map, or a struct that owns \ - one — found %s. A resource type with a drop hook is step 5 and does \ - not exist yet" + "free takes an owning container — a Vec or a Map — found %s. A \ + resource type with a drop hook is step 5 and does not exist yet" (Types.to_string other)) (* (clone v) uses the current allocator, (clone v a) names one. A deep, independent copy: spec-memory.md's "copying is always explicit". *) @@ -4076,7 +4045,8 @@ and named_call ctx ~want loc name args = | _ -> assert false) (* (get m k) -> (Option V). Absence is None, not an untyped nil, and the - first implementation admits copyable values only, so this is a copy. + answer is a copy of the value's bytes — for an owning value, a copy of + its header, aliasing what the map's slot points at. There is no allocation here and therefore no guard: a lookup that finds nothing is an answer, not a failure. *) | "get" -> @@ -4582,11 +4552,10 @@ and named_call ctx ~want loc name args = and a reader who sees it has already been told where the promise comes from. - **It owns nothing.** The result is a [Types.Slice], which is not - move-only, carries no allocator, and is the same non-owning view - (as-slice v) answers — so [free] refuses it by the rule it already had - ("free takes a move-only value"), and nothing in the move analysis needed - to learn about this form. *) + **It owns nothing.** The result is a [Types.Slice], which carries no + allocator and is the same non-owning view (as-slice v) answers — so + [free] refuses it by the rule it already had ("free takes an owning + container"). *) | "slice-from-ptr" -> arity loc name 2 args; (match args with @@ -4929,8 +4898,8 @@ and named_call ctx ~want loc name args = | Some b -> (match b.bty with Types.Fn _ -> true | _ -> false) | None -> false) -> (* The binding the guard already found, read directly. Going back through - [check] would repeat the lookup and walk the move and capture paths for - a type that is neither move-only nor capturable. *) + [check] would repeat the lookup and walk the capture path for a type + that is not capturable. *) (match lookup ctx name with | Some b -> call_value ctx ~want loc (mk loc b.bty (Tast.Local b.slot)) args | None -> assert false) @@ -5035,7 +5004,7 @@ and generic_call ctx ~want loc name vars pats pret args = code the caller did not write, which is the thing the pass exists to avoid. So the caller has to declare at least what the callee asks for, and [pred_entails] means [ordered?] covers a callee wanting - [copyable?] without anyone writing both. *) + [equal?] without anyone writing both. *) (match Hashtbl.find_opt ctx.env.generics name with | None -> () | Some gfn -> @@ -5346,45 +5315,16 @@ let collect env (decls : Ast.decl list) = aborts the whole compilation, so an entry left behind by a declaration that is about to be refused is never read. *) Hashtbl.replace env.structs n { Tast.sname = n; fields }; - (* spec-memory.md: "Ownership is structural, not declared" — a struct - containing a Vec is itself move-only, and freeing one recurses into - its owning fields while (free (.items b)) is refused because it - would leave the owner partly dead. None of that transitive - machinery exists, and it is what [drop] would have brought. So the - field is still refused at the declaration, where the message can - say so, rather than accepted into a struct that copies its header - on assignment and gives two owners one buffer. + (* A struct field may own storage. Since the repeal a struct + holding a [(Vec i32)] is an ordinary value: assignment copies the + header bytes, the copies alias one buffer, and freeing through + two copies is the program's bug — Odin's contract, kept whole. - With one exception, and it is exact: a field whose container holds - *owning* elements. That container cannot exist outside a region — - the guard at its construction is what makes sure of it (see - [vec-new]) — so the struct's field is region-allocated too, - transitively and by the same guard, and the whole graph is released - by one [free-all]. There is nothing for a teardown to recurse into - because there is no teardown, and the two-owners-one-buffer problem - is not one when the owner is the region and neither copy is it. - - The plain case stays refused precisely because nothing enforces - anything there: a [(Vec i32)] field is happily built against the - heap, nothing would object, and then (free (.items b)) through two - copies of the struct is a double free with no guard between it and - the program. *) - List.iter - (fun (f : Tast.field) -> - if Types.is_move_only f.Tast.fty - && not (region_only env f.Tast.fty) then - fail loc - "%s's field %s is %s, which is move-only, and a struct that \ - owns one is move-only too — transitively, with recursive \ - teardown and with a field that cannot be freed on its own. \ - That rule does not exist; hold the %s in a local and pass \ - it. A container whose *elements* own storage is the one \ - kind admitted here, because it can only have been built \ - against a region allocator and a single (free-all) takes \ - the whole graph" - n f.Tast.fname (Types.to_string f.Tast.fty) - (Types.to_string f.Tast.fty)) - fields + The region rule is separate and survives on its own ground: a + field whose container holds *owning* elements can only have been + built against a region allocator — the guard at its construction + is what makes sure of it (see [vec-new]) — so that graph is + released by one [free-all] and no teardown recurses anywhere. *) | Ast.Defdata (n, vs) -> (* A data type with no cases has no value, so nothing could ever be given one, and a parameter of that type would be a function nothing can @@ -5419,115 +5359,23 @@ let collect env (decls : Ast.decl list) = because a data type that could hold a container where a struct could not would be a hole in the same rule. *) Hashtbl.replace env.datas n { Tast.dname = n; cases }; - (* The same refusal a struct field gets, for the same reason, in the - same words, and with the same one exception: a data type case's - fields are a struct, the data type copies bytewise on assignment, - and there is no recursive teardown to make that safe — except where - the field's container holds owning elements, which can only have - been built against a region and is therefore released whole. - - This is the arm the recursive dynamic value needs, and it is worth - naming what it buys: a [Value] with a [(Vec Value)] case and a - [(Map string Value)] case is now declarable, parsed into an arena, - walked, and released by one [free-all] with no per-element teardown - anywhere. What it costs is that a [Value] is copied bytewise like - any other data value, so two copies share the inner blocks. In a - region that is aliasing and not a double free, because neither copy - owns anything — the region does. *) - List.iter - (fun (vloc, (c : Tast.variant)) -> - List.iter - (fun (f : Tast.field) -> - if Types.is_move_only f.Tast.fty - && not (region_only env f.Tast.fty) then - fail vloc - "%s.%s's field %s is %s, which is move-only, and a \ - data type case that owns one makes the data type \ - move-only too — transitively, with recursive teardown. \ - That rule does not exist; hold the %s in a local and \ - pass it. A \ - container whose *elements* own storage is the one kind \ - admitted here, because it can only have been built \ - against a region allocator and a single (free-all) \ - takes the whole graph" - n c.Tast.vname f.Tast.fname (Types.to_string f.Tast.fty) - (Types.to_string f.Tast.fty)) - c.Tast.vfields) - cases_with_loc; + (* A case's fields are a struct and may own storage, on the struct's + terms since the repeal: copies alias, and the free is the + program's to write. The region rule still applies on its own + ground — a [(Vec Value)] case field can only have been built + against a region, so the recursive dynamic value parses into an + arena and one [free-all] releases the graph, no teardown + anywhere. *) List.iter (fun (c : Tast.variant) -> Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c); Hashtbl.replace env.cases c.Tast.vname (n, c)) cases - (* ── The untagged union ────────────────────────────────────────── - C's semantics, deliberately and in full: the members overlay one - storage, the size is the largest of them, the alignment the - strictest, and nothing anywhere records which member was written - last. - - {2 What Flan says about reading a member that was not written} - - It reads the bytes that are there, through that member's type. Not - undefined behaviour, and not a refusal either — a *definition*, and - this is the one place in the checker that chooses bytes over safety - on purpose, so it is worth saying why. - - Refusing it was the alternative, and it would have made the feature - nothing: type punning *is* reading the member that was not written, - and both uses this type exists for are that read. Binding a C header - means holding the union the library holds and reading whichever - member the library's own tag says is live — a tag Flan cannot see, - because it is a field of the enclosing struct and the rule that - relates them is prose in a manual. Overlaying an f32 on a u32 to look - at its bits is the other use and is the same read. A checker that - refused it would be refusing the type. - - So the promise is the one C's implementations actually make and - C's standard does not: the layout is the target's, the bytes are the - bytes, and a read is a reinterpretation of them. What is *not* - promised is anything about bytes never written — a member larger - than the one last stored reads its own size, and the tail is - indeterminate exactly as a struct's padding is. That is the honest - line, and it is narrower than it sounds: the ZII rule means a union - starts all-bytes-zero unless [uninit] says otherwise, so the tail is - zero rather than garbage in every program that did not ask for - garbage. - - {2 uninit} - - Allowed, unlike on a data type. The refusal there is not about - garbage — [uninit] is garbage everywhere and says so — it is that a - data type's tag *steers*, and a tag no case names falls past every - comparison in a [match] into a block LLVM is entitled to treat as - unreachable. An untagged union steers nothing. Reading a member of - one is already a reinterpretation of whatever bytes are there, so - [uninit] makes those bytes arbitrary and changes nothing else, which - is exactly what it means on an [i64]. - - {2 Why bool is not a member} - - An [i1] loaded out of a byte that is neither 0 nor 1 is not a - [false], it is a value the optimiser is entitled to assume cannot - exist, and a union is the one type that can hand it one — write the - [u8] member 2, read the [bool] member. Nothing about that is visible - at the read, so it cannot be refused there. The alternative was to - load a union's bool as an [i8] and compare it against zero in both - backends, which is a correct answer and a real cost paid by every - bool in the language to make one type safe. Refused at the - declaration instead, where the message can name the replacement: - [u8], compared explicitly. The check below is recursive, because a - bool inside a struct member is the same byte. - - {2 Why no member may be move-only} - - Because nothing knows which member is live, so nothing can tear one - down. That is not a limitation of today's compiler, which is what - the struct and data type refusals above say about themselves; it is - a property of the type, and it does not go away when recursive - teardown lands. A [drop] of a union would have to free whichever - member is live and there is no such fact — freeing the wrong one is - a free of a pointer that was an f64 a moment ago. *) - | Ast.Defunion (n, ms) -> + (* Nothing records which member of a union is live, so nothing — the + program included — can free the right one through the union itself. + Since the repeal that is a fact about the value and not a refusal: + a member may own storage, and freeing it is done through whatever + tag the program keeps beside the union, as C does. *) | Ast.Defunion (n, ms) -> if ms = [] then fail loc "%s declares no members, so it has no size and nothing could be \ @@ -5536,20 +5384,6 @@ let collect env (decls : Ast.decl list) = if List.length (List.sort_uniq compare names) <> List.length names then fail loc "%s declares the same member twice" n; let fields = List.map field ms in - List.iter - (fun (f : Tast.field) -> - if Types.is_move_only f.Tast.fty then - fail loc - "%s's member %s is %s, which is move-only, and a union may \ - not own one: the members overlay one storage and nothing \ - records which was written, so nothing can free the right \ - one. Unlike a struct's, this is not waiting on recursive \ - teardown — there is no fact for teardown to read. Hold the \ - %s beside the union, or in a struct with a tag you check \ - yourself" - n f.Tast.fname (Types.to_string f.Tast.fty) - (Types.to_string f.Tast.fty)) - fields; Hashtbl.replace env.unions n { Tast.sname = n; fields } | Ast.Defn fn -> (* A signature that introduces a type variable is a *pattern*, not a @@ -5823,9 +5657,7 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn = whichever call site happened to instantiate it at a type that worked. The holes in it are real and are the report's business: [println] is - plan.org's one compiler-provided exception and this pass rejects it, and - move-only-ness is not decidable abstractly at all — [Types.is_move_only - (Var _)] is false, but the same variable at [(Vec i32)] is move-only. *) + plan.org's one compiler-provided exception and this pass rejects it. *) and check_generic env (fn : Ast.fn) = let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in let saved_lifted = env.lifted and saved_vars = env.tyvars @@ -5850,14 +5682,12 @@ and check_generic env (fn : Ast.fn) = checking a function. *) let () = check_fn_ref := check_fn -(* A global of move-only type is legal. Before the repeal what made it legal - was a flow rule — reading one was always a borrow, so nothing could take - or free it. That rule is gone with the rest of the flow analysis: a global - Vec may now be handed to a function, bound, or freed, and keeping its - process-long lifetime honest is the program's business, on the same terms - as every other free. +(* A container's only compile-time constant is the zeroed one: a Vec's or a + Map's real value exists at run time, behind an allocator. That is a fact + about initialisers and it survived both repeals untouched — nothing here + is about copying or moving. - What this pass still decides is how such a global may be *started*, and the + What this pass decides is how such a global may be *started*, and the answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null block, zero length, zero capacity — so the ZII value is the value a program would have written anyway, and filling it is an ordinary (set g (slurp @@ -5880,15 +5710,21 @@ let () = check_fn_ref := check_fn A global *Allocator* is not any of this — an allocator is a copyable opaque handle — which is what makes the handler-owns-the-arena shape in exhausted.flan expressible. *) -let move_only_global_init loc n (ty : Types.t) (init : Ast.init) = - if Types.is_move_only ty then +let rec zero_only (t : Types.t) = + match t with + | Types.Vec _ | Types.Map _ -> true + | Types.Option e | Types.Array (_, e) -> zero_only e + | _ -> false + +let container_global_init loc n (ty : Types.t) (init : Ast.init) = + if zero_only ty then match init with | Ast.Zeroed -> () | _ -> fail loc - "the global %s is %s, which is move-only, and a move-only global \ - starts zeroed: a global's initialiser is a compile-time constant and \ - %s is not one. Write (defvar %s %s) with no initialiser — a zeroed \ + "the global %s is %s, and such a global starts zeroed: a global's \ + initialiser is a compile-time constant, %s is not one, and a \ + container's only constant value is the empty one. Write (defvar %s %s) with no initialiser — a zeroed \ %s is an empty one, and that is a value, not a placeholder — then \ load it with (set %s ...) in the function that loads it, which runs \ once and whose result outlives every call to main" @@ -5896,19 +5732,21 @@ let move_only_global_init loc n (ty : Types.t) (init : Ast.init) = (match init with Ast.Uninit -> "uninit" | _ -> "this initialiser") n (Types.to_string ty) (Types.to_string ty) n -(* A move-only global has to be a [defvar]. A [defconst] is not an assignable - place — [check_place] refuses one by name — so a constant Vec could only - ever hold the zeroed value it was declared with, and nothing could ever put - the file's bytes in it. Refused here, where the fix is one keyword, rather - than at the (set ...) that discovers it three forms later. *) -let no_move_only_defconst loc n (ty : Types.t) = - if Types.is_move_only ty then +(* A container global has to be a [defvar]. A [defconst] is not an assignable + place — [check_place] refuses one by name — and a container's only constant + is the zeroed one, so a constant Vec could only ever hold the empty value + it was declared with: nothing could ever put the file's bytes in it. + Refused here, where the fix is one keyword, rather than at the (set ...) + that discovers it three forms later. *) +let no_container_defconst loc n (ty : Types.t) = + if zero_only ty then fail loc - "the global %s is %s, which is move-only, and a move-only global is a \ - defvar and not a defconst: a constant is not an assignable place, so \ - nothing could ever load this one — it would stay the empty %s it was \ - declared as. Write (defvar %s %s) and fill it in a function" - n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty) + "the global %s is %s, and a %s global is a defvar and not a defconst: \ + a constant is not an assignable place, so nothing could ever load \ + this one — it would stay the empty %s it was declared as. Write \ + (defvar %s %s) and fill it in a function" + n (Types.to_string ty) (Types.to_string ty) (Types.to_string ty) + n (Types.to_string ty) (* A union member written into a global would have to be encoded into the blob at link time, which is the byte-level encoder a data type case does not have @@ -5939,7 +5777,7 @@ let check_global env (d : Ast.decl) : Tast.global option = | Ast.Defvar (n, _, init) -> let ty, _ = Hashtbl.find env.globals n in no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty; - move_only_global_init d.Ast.dloc n ty init; + container_global_init d.Ast.dloc n ty init; let ginit = match init with | Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc } @@ -5972,7 +5810,7 @@ let check_global env (d : Ast.decl) : Tast.global option = | Ast.Defconst (n, _, v) -> let ty, _ = Hashtbl.find env.globals n in no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty; - no_move_only_defconst d.Ast.dloc n ty; + no_container_defconst d.Ast.dloc n ty; (* [collect] already folded the integer constants, because an array length has to be known before any type resolves. Use that value here rather than the expression it came from: a global's initialiser has to be a diff --git a/lib/prelude.ml b/lib/prelude.ml index 78482b7..4eb5d96 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -228,29 +228,16 @@ let source = {flan| ;; variable supports only what it is declared to support — an unconstrained ;; one is refused at the *definition*, not at some later call site — and ;; [ordered?] is the predicate that admits [<], [<=], [>], [>=], [min] and -;; [max]. It admits [=] and [copyable?] too: every type the language orders is -;; a number or an enum, so it is equatable and it is not move-only. +;; [max]. It admits [=] too: every type the language orders is a number or an +;; enum, so it is equatable. ;; -;; [{:where (copyable? $t)}] is the opt-out from the other default. A type -;; variable is **move-only** until it says otherwise, because move is the -;; stricter rule and assuming it can only refuse a valid program rather than -;; admit a broken one: [reduce]'s accumulator is read into [f] and then -;; assigned again, which is correct at [i32] and a double move at [(Vec i32)], -;; and the checker cannot tell which until it substitutes. -;; -;; **Two of these ten are forced and the rest are convention, and the -;; difference is worth knowing.** [filter] and [reduce] do not check without -;; [copyable?]: the first returns a [(Vec $t)], and a Vec of an owning element -;; is refused, and the second holds its accumulator in a local and reads it -;; twice. [swap!], [reverse!], [map!] and [sort-by!] check *without* it, -;; because the move analysis tracks locals and parameters and does not track a -;; read out of a slice — so [(let [t (at s i)] ... (set (at s j) t))] is not -;; seen as a move even when the element owns storage. They declare it anyway, -;; and should: at [[(Vec i32)]] those bodies would duplicate a header. It is -;; the one place move-by-default is not conservative, and until element-level -;; moves are tracked, a [copyable?] on a body that moves elements between -;; slots is a convention the reader has to keep rather than a fact the checker -;; enforces. +;; There is no [copyable?] any more. Since the repeal every value copies — +;; a container copies as its header, the copies alias one buffer, and what +;; the copies then do is the program's business, as it is in Odin. A body +;; that reads an element into a local and writes it into another slot is +;; duplicating a header when the element owns storage, and nothing here +;; says otherwise any more: that sentence moved from a predicate into this +;; comment, which is where Odin keeps it too. ;; ;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32] ;; widen their element into [i64] and [f64]; "the wider type $t accumulates @@ -263,13 +250,11 @@ let source = {flan| ;; keeping attached to something. (defn swap! [s [$t] i i32 j i32] () - {:where (copyable? $t)} (let [t (at s i)] (set (at s i) (at s j)) (set (at s j) t))) (defn reverse! [s [$t]] () - {:where (copyable? $t)} (let [i 0 j (- (len s) 1)] (while (< i j) @@ -317,7 +302,6 @@ let source = {flan| ;; predicates existed, and it stays because passing a comparison is a real ;; thing to want and not only a workaround. (defn sort-by! [s [$t] before? (Fn [$t $t] bool)] () - {:where (copyable? $t)} (let [i 1] (while (< i (len s)) (let [j i] @@ -369,7 +353,6 @@ let source = {flan| ;; here: it is two type variables and a second signature, and nothing has ;; wanted it. (defn map! [s [$t] f (Fn [$t] $t)] () - {:where (copyable? $t)} (dotimes [i (len s)] (set (at s i) (f (at s i))))) @@ -377,7 +360,6 @@ let source = {flan| ;; in. The accumulator comes first in the step, which is the order that reads ;; as (f acc x) and the order Odin's slice.reduce uses. (defn reduce [s [$t] init $t f (Fn [$t $t] $t)] $t - {:where (copyable? $t)} (let [acc init] (dotimes [i (len s)] (set acc (f acc (at s i)))) @@ -391,7 +373,6 @@ let source = {flan| ;; runtime needed no change at all, because SizeOf and AlignOf are computed at ;; the instantiation site, where the element type is concrete. (defn filter [s [$t] keep? (Fn [$t] bool)] (Vec $t) - {:where (copyable? $t)} (let [v (vec-new t)] (dotimes [i (len s)] (when (keep? (at s i)) diff --git a/lib/types.ml b/lib/types.ml index 62bc6f2..6c93489 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -124,17 +124,6 @@ let rec to_string = function let is_numeric = function Int _ | Float _ -> true | _ -> false -(* Move-only: binding, passing or returning one transfers ownership and the - source binding is dead afterwards (spec-memory.md, "The four container - types"). That rule is what makes a double free unrepresentable, which is why - [free] needs no analysis of its own. A struct that owns one is move-only - too; that arrives with [drop], which is the step after this one. *) -let rec is_move_only = function - | Vec _ | Map _ -> true - | Option t -> is_move_only t - | Array (_, t) -> is_move_only t - | _ -> false - (* The key types the first Map implementation admits (spec-memory.md, "Maps — first implementation"): integers, enums, strings, fixed arrays, and value structs composed recursively from those. Equality and hashing for them are diff --git a/spike/generics/prelude-shapes.flan b/spike/generics/prelude-shapes.flan index a53425e..b17b777 100644 --- a/spike/generics/prelude-shapes.flan +++ b/spike/generics/prelude-shapes.flan @@ -3,7 +3,6 @@ ;; prelude; it is the same bodies, over $t, checked and run. (defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t) - {:where (copyable? $t)} (let [v (vec-new t)] (dotimes [i (len s)] (when (keep? (at s i)) @@ -15,7 +14,6 @@ (set (at s i) (f (at s i))))) (defn fold [s [$t] init $t f (Fn [$t $t] $t)] t - {:where (copyable? $t)} (let [acc init] (dotimes [i (len s)] (set acc (f acc (at s i)))) diff --git a/test/programs/generic-runaway.flan b/test/programs/generic-runaway.flan index a124b36..16bbe9f 100644 --- a/test/programs/generic-runaway.flan +++ b/test/programs/generic-runaway.flan @@ -5,6 +5,6 @@ ;;;; Session.eval runs the same code the thing that hung was C-c C-c with the ;;;; dev daemon wedged behind it. The refusal names the chain of ;;;; instantiations rather than a depth it gave up at. -(defn grow [x $t] () {:where (copyable? $t)} (grow [x x])) +(defn grow [x $t] () (grow [x x])) (defn main [] () (grow 1)) diff --git a/test/programs/generics.flan b/test/programs/generics.flan index 14b1466..c16c704 100644 --- a/test/programs/generics.flan +++ b/test/programs/generics.flan @@ -21,13 +21,11 @@ ;; The variable is bound *inside* a type constructor, which is a structural ;; walk rather than a name match. (defn first-or [s [$t] d $t] $t - {:where (copyable? $t)} (if (= (len s) 0) d (at s 0))) ;; A generic calling a generic at its own variable: the copy of [swap!] is ;; generated when [rotate!] is instantiated and not before. (defn rotate! [s [$t]] () - {:where (copyable? $t)} (dotimes [i (- (len s) 1)] (swap! s i (+ i 1)))) @@ -37,7 +35,7 @@ (+ x x)) ;; equal? admits = and !=; ordered? admits < <= > >= min max, and entails -;; equal? and copyable?. +;; equal?. (defn count-of [s [$t] x $t] i32 {:where (equal? $t)} (let [n 0] @@ -52,14 +50,12 @@ ;; Two variables, and the second is determined by its own argument. (defn fst [a $t b $u] $t - {:where [(copyable? $t) (copyable? $u)]} (do b a)) ;; println over a type variable is the one form the abstract pass defers to ;; the instantiation, because its legality is only decidable after ;; substituting. The structural printer is selected per copy. (defn show [x $t] () - {:where (copyable? $t)} (println x)) ;; A cast to a type variable. [(t x)] is not a name [is_cast] knows — [t] is @@ -73,7 +69,6 @@ ;; The builtins that take a *type name* as an argument, over a variable. Each ;; reaches the one list of what names a type; (map-new t i32) is the other. (defn one-of [x $t] (Vec $t) - {:where (copyable? $t)} (let [v (vec-new t)] (push v x) v)) @@ -81,7 +76,6 @@ ;; (zeroed) takes its type from the position it is written in, so a variable ;; in that position is answered by the instantiation like any other type. (defn zero-of [x $t] $t - {:where (copyable? $t)} (do x (zeroed))) ;; The map operations over a key that is a type variable. The hash and the diff --git a/test/programs/reload-generic.flan b/test/programs/reload-generic.flan index 3e7db4a..c3131fb 100644 --- a/test/programs/reload-generic.flan +++ b/test/programs/reload-generic.flan @@ -11,13 +11,11 @@ (defvar counter i64) (defn put! [xs [$t] i i32 v $t] () - {:where (copyable? $t)} (set (at xs i) v)) ;;; Calls [put!] at its own variable, so the copy of [put!] is generated when ;;; [hold!] is instantiated and not before. (defn hold! [xs [$t] v $t] () - {:where (copyable? $t)} (put! xs 0 v)) (defn pick [xs [$t]] $t diff --git a/test/programs/vec-in-struct.flan b/test/programs/vec-in-struct.flan index e0a5a08..72b72b2 100644 --- a/test/programs/vec-in-struct.flan +++ b/test/programs/vec-in-struct.flan @@ -1,9 +1,7 @@ -;;;; spec-memory.md: "Ownership is structural, not declared" — a struct -;;;; containing a Vec is itself move-only, transitively, with recursive -;;;; teardown, and with a field that cannot be freed on its own. None of that -;;;; machinery exists: it is the same recursive teardown `drop` brings, and it -;;;; lands with it. Accepting the field meanwhile would give a struct that -;;;; copies its header on assignment two owners of one buffer. +;;;; A struct may own a Vec since the second repeal: the field is header +;;;; bytes, assignment copies them, and the two copies alias one buffer. +;;;; Which copy's free runs is the program's business — Odin's contract. +;;;; This used to be a negative fixture; now it pins the admission. (defstruct Builder [buf (Vec u8)]) (defn main [] i32 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 3fa5aa5..8d7fe44 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1992,13 +1992,10 @@ let () = the Vec of a Vec is a run-time question about the allocator instead, so its program runs rather than being refused (programs/arena-region.flan). - This one stays, and the narrowing is exactly why: a [(Vec u8)] field - holds elements that own nothing, so nothing forces it into a region, - and two copies of the struct would be two headers over one heap buffer. - A container whose *elements* own storage is the case that is admitted, - because that one can only have been built against a region. *) - refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan" - "a struct that owns one is move-only too"; + Since the second repeal the plain field is admitted: two copies of + the struct are two headers over one buffer, and that is the program's + to manage — Odin's contract. The program compiles and runs. *) + outputs "a struct field that owns a Vec" "programs/vec-in-struct.flan" ""; (* And it does not cross to C: the shim would flatten a header that owns storage. Refused by the shim generator, where the message can say what to pass instead. *) @@ -2789,9 +2786,6 @@ ERR@7 unexpected token: not the kind the caller was reading refuses_src "a data type with no cases" "(defdata U [])\n(defn f [u U] () 0)" "declares no cases"; - refuses_src "a data type case that owns a Vec" - "(defdata U [(A [v (Vec i32)])])\n(defn f [u U] () 0)" - "which is move-only"; (* At the operation, not at the type: a struct key is decided by walking its fields and the struct table is not necessarily complete while a type is resolving, so both are answered where the hash and equality diff --git a/test/test_flan.ml b/test/test_flan.ml index 969e00e..4c6c92d 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -896,12 +896,12 @@ let () = rejects_check "slice-from-ptr with a negative literal length" "(defn f [p (Ptr i32)] i32 (len (slice-from-ptr p -1)))" ~needle:"is negative"; - (* The storage stays C's. A slice is not move-only and carries no allocator, - so free refuses one by the rule it already had — this pins that the new - form did not become a thing anybody could hand to free. *) + (* The storage stays C's. A slice carries no allocator, so free refuses one + by the rule it already had — this pins that the new form did not become + a thing anybody could hand to free. *) rejects_check "free of a slice made from a pointer" "(defn f [p (Ptr i32)] () (free (slice-from-ptr p 3)))" - ~needle:"free takes a move-only value"; + ~needle:"free takes an owning container"; (* ── Structs, fields and auto-deref ────────────────────────────── *) let cursor = "(defstruct Cursor [src [u8] pos i32]) " in @@ -1040,17 +1040,14 @@ let () = "(defdata Value [Nil (List [items (Vec Value)])])"; accepts "a data type case holding a Map of itself" "(defdata Value [Nil (Table [entries (Map string Value)])])"; - (* And the narrowing is exact, which is what these two are for. A container - whose elements own *nothing* is not forced into a region by anything, so - it would sit in a copyable aggregate on the heap with two headers and one - buffer between them — the double free the original refusal existed to - prevent. It stays refused, in a struct and in a union alike. *) - rejects_check "a data type case holding a plain Vec" - "(defdata Value [Nil (Bytes [bs (Vec u8)])])" - ~needle:"makes the data type move-only"; - rejects_check "a struct field holding a plain Vec" - "(defstruct B [buf (Vec u8)])" - ~needle:"a struct that owns one is move-only too"; + (* Since the second repeal the plain case is admitted too: a struct or a + case holding a heap-backed Vec copies as bytes, the copies alias one + buffer, and a free through two copies is the program's bug — Odin's + contract exactly. These pin the admission. *) + accepts "a data type case holding a plain Vec" + "(defdata Value [Nil (Bytes [bs (Vec u8)])])"; + accepts "a struct field holding a plain Vec" + "(defstruct B [buf (Vec u8)])"; (* free does not recurse and does not quietly release the outer block: it names free-all, which is the operation that actually releases the graph. *) rejects_check "free on a container of owning elements" @@ -1622,12 +1619,11 @@ let () = rejects_check "a union that contains itself by value" "(defunion U [a i32 b U])\n(defn f [u U] i32 0)" ~needle:"contains itself by value"; - (* Not waiting on drop, unlike the struct and data type refusals: nothing - records which member is live, so there is no fact recursive teardown - could read. *) - rejects_check "a union member that is move-only" - "(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)" - ~needle:"nothing records which was written"; + (* Nothing records which member is live, and since the second repeal that + is the program's fact to keep rather than a refusal: a union member may + own storage, C's way. *) + accepts "a union member that owns storage" + "(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)"; (* And the one the optimiser would otherwise be handed: a byte that is neither 0 nor 1 read as an i1. Refused at any depth, which is why the second row goes through a struct. *) @@ -2604,7 +2600,7 @@ let () = accepts "a map return type, written the one way there is" "(defn f [] (Map string i32) (map-new string i32))"; accepts "a map return type followed by a constraint map" - "(defn f [x $t] (Map string i32) {:where (copyable? $t)} \ + "(defn f [x $t] (Map string i32) {:where (equal? $t)} \ (do x (map-new string i32)))"; rejects_check "braces in type position say where the spelling went" ~needle:"written (Map K V)" @@ -2621,13 +2617,13 @@ let () = ~needle:"nothing here says t is ordered?" "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))"; (* The entailments, which are the reason a signature is one predicate long - rather than three. Every type the language orders is a number or an enum, - so it is equatable and it is not move-only. *) + rather than two. Every type the language orders is a number or an enum, + so it is equatable. *) accepts "ordered? entails equal?" "(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))"; accepts "numeric? entails ordered?" "(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))"; - accepts "ordered? entails copyable?" + accepts "a variable read twice under one predicate" "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))"; rejects_check "a predicate nobody has heard of" ~needle:"is not a type predicate" @@ -2636,12 +2632,13 @@ let () = ~needle:"is not a type variable of f" "(defn f [a i32] i32 {:where (ordered? $t)} a)"; - (* Move-only by default still decides the structural rules for a $t — what - may own one — but since the repeal a double use of a binding is not - checked, so both of these are accepted with and without the clause. *) - accepts "a type variable is usable twice without copyable?" + (* Everything copies since the second repeal, so a double use of a binding + needs no clause at all — and [copyable?] itself is gone, refused the way + any unknown predicate is, which is this pin's job to remember. *) + accepts "a type variable is usable twice with no clause" "(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))"; - accepts "and copyable? is still a clause a signature may state" + rejects_check "copyable? is no longer a predicate" + ~needle:"is not a type predicate" "(defn twice [a $t b (Fn [$t $t] $t)] $t {:where (copyable? $t)} (b a a))"; (* The allow-list, and it has two members. println over a type variable is @@ -2649,16 +2646,16 @@ let () = after substituting — which is the one thing the abstract pass otherwise refuses to do. *) accepts "println over a type variable is deferred" - "(defn show [x $t] () {:where (copyable? $t)} (println x))"; + "(defn show [x $t] () {:where (equal? $t)} (println x))"; accepts "and so is print" - "(defn show [x $t] () {:where (copyable? $t)} (print x))"; + "(defn show [x $t] () {:where (equal? $t)} (print x))"; (* A predicate a body relies on has to be carried by every signature between it and the call site, or the refusal moves into code the caller did not write. *) rejects_check "a predicate is not carried through a generic call" ~needle:"has to be carried by every signature" - "(defn outer [s [$t]] () {:where (copyable? $t)} (sort! s))"; + "(defn outer [s [$t]] () {:where (equal? $t)} (sort! s))"; accepts "and is accepted when it is" "(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))"; @@ -2670,7 +2667,7 @@ let () = itself is refused where it is written, at the definition. *) rejects_check "a map keyed by a type variable that is not hashable?" ~needle:"is not a map key" - "(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))"; + "(defn f [m (Map $t i32)] i32 {:where (numeric? $t)} (len m))"; accepts "and hashable? is what says it is" "(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))"; accepts "and under it the operations are deferred, not refused" diff --git a/test/test_session.ml b/test/test_session.ml index cc7e2c5..0962cbb 100644 --- a/test/test_session.ml +++ b/test/test_session.ml @@ -791,7 +791,7 @@ let () = installed nothing and did not say anything had gone wrong. Both copies have to be named, and the copy of [put!] that [hold!] pulls in has to be there too, which is transitivity. *) - (match Session.eval (gen ()) "(defn hold! [xs [$t] v $t] () {:where (copyable? $t)} (put! xs 0 v) (put! xs 0 v))" with + (match Session.eval (gen ()) "(defn hold! [xs [$t] v $t] () (put! xs 0 v) (put! xs 0 v))" with | c -> if not c.Session.installs then fail "redefining a generic installed nothing"; @@ -814,7 +814,7 @@ let () = instantiation that generated them was transitive, and finding them again is one table lookup rather than a walk, because a whole-program check has already regenerated all of them. *) - (match Session.eval (gen ()) "(defn put! [xs [$t] i i32 v $t] () {:where (copyable? $t)} (set (at xs i) v))" with + (match Session.eval (gen ()) "(defn put! [xs [$t] i i32 v $t] () (set (at xs i) v))" with | c -> List.iter (fun want -> @@ -884,7 +884,7 @@ let () = caller. *) (match Session.eval (gen ()) - "(defn put! [xs [$t] i i64 v $t] () {:where (copyable? $t)} \ + "(defn put! [xs [$t] i i64 v $t] () \ (set (at xs (i32 i)) v))" with | _ -> fail "a generic's changed parameter type was accepted" @@ -902,7 +902,7 @@ let () = long before the session is asked anything. *) (match Session.eval (gen ()) - "(defn pick [xs [$t]] $t {:where [(ordered? $t) (copyable? $t)]} (at xs 0))" + "(defn pick [xs [$t]] $t {:where (ordered? $t)} (at xs 0))" with | c -> if not (List.mem "pick-i32" c.Session.fns) then diff --git a/web/index.html b/web/index.html index 8860532..1af28df 100644 --- a/web/index.html +++ b/web/index.html @@ -886,11 +886,10 @@ type as an argument — (vec-new t), (map-new t i32), (min (max x lo) hi)) (defn first-or [s [$t] d $t] $t ; the variable inside a slice type - {:where (copyable? $t)} + {:where (equal? $t)} (if (= (len s) 0) d (at s 0))) (defn one-of [x $t] (Vec $t) ; bare t is the type-name argument - {:where (copyable? $t)} (let [v (vec-new t)] (push v x) v)) @@ -927,8 +926,8 @@ $t)} at the head of the body, or take the operation as a parameter — a

What makes that liveable is a where clause, written as a Clojure-style map at the head of the body — {:where (ordered? $t)}, or a vector when -there is more than one: {:where [(copyable? $t) (copyable? $u)]}. There -are five predicates, and each gates builtins the compiler already has:

+there is more than one: {:where [(ordered? $t) (hashable? $u)]}. There +are four predicates, and each gates builtins the compiler already has:

@@ -937,30 +936,19 @@ are five predicates, and each gates builtins the compiler already has:

-
ordered?< <= > >= min max
equal?= and !=
hashable?the variable as a Map key — (map-new t V), get, put, has-key?
copyable?reading the value more than once; Pool and Vec element positions

They entail each other in one direction, so one clause usually does: -numeric? gives ordered?, ordered? gives -equal?, and any of the four gives copyable?. A -sort! that compares its elements and reads them twice declares +numeric? gives ordered?, and ordered? gives +equal?. A sort! that compares its elements declares ordered? and nothing else.

-

A type variable is move-only by default, and -copyable? is the opt-out. Types.is_move_only of a variable is -not decidable abstractly — the same variable is i32 at one instantiation -and (Vec i32) at the next — so the checker assumes the stricter rule, -which can only refuse a program that would have been fine and never admit one that -double-frees. It is Rust's T: Copy, with the difference that the compiler -answers the question rather than a user implementing a trait. So -(defn twice [x $t] $t (+ x x)) does not merely want -numeric?; reading x a second time is a use after move:

- -
x was moved at twice.flan:1:26 and cannot be used again — t is move-only, so
-binding, passing or returning one transfers ownership and the source binding is
-dead afterwards (spec-memory.md). That rule is what makes a double free
-unrepresentable; (clone x) if you wanted a second one
+

Every value copies. There used to be a fifth predicate, +copyable?, gating a second read of a move-only variable; the move +concept was repealed on 2026-09-18 — a container copies as its header, the +copies alias one buffer, and which free runs is the program's business, as it +is in Odin — so the predicate went with it.

Each instantiation then checks the concrete type against what the signature declared, and refuses the call site when it does not answer: