JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

The move-only concept follows the flow analysis out: everything copies, and the frees are yours

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-18 12:16:05 +07:00
parent c46fd56447
commit 4a563d0e67
12 changed files with 158 additions and 383 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

350
lib/check.ml
View File

@ -406,20 +406,14 @@ let unimplemented loc what milestone =
Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is 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 [where intrinsics.type_is_ordered(T)]) with forty-one predicates against
these five. The fifth, [copyable?], has no Odin counterpart at all: Odin these four. There is no [copyable?] any more and no Odin counterpart
has no move semantics, so [$T] never has to answer the question. The prior either: Odin has no move semantics, and since the repeal neither does this
art there is Rust's [T: Copy], with the difference that [copyable?] is a language, so [$T] never has to answer the question. *)
question the compiler answers rather than a trait a user implements. *) let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?" ]
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ]
(* ── What a type owns, transitively ──────────────────────────────────── (* ── What a type owns, transitively ────────────────────────────────────
spec-memory.md: "Ownership is structural, not declared." [Types.is_move_only] The one structural ownership question that survived the repeal, because it
answers the same question one level deep and deliberately stops there — a is not about copying at all.
[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.
What it decides, and the only thing it decides, is whether a container of 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 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 contain itself by value anyway — [check_finite] refuses that — only through
a container, which is an arm that answers for itself. a container, which is an arm that answers for itself.
[env.unions], the untagged ones, are deliberately not consulted: a move-only [env.unions], the untagged ones, are deliberately not consulted: nothing
member in one is refused outright, and that refusal is not waiting on anywhere records which member of one is live, so there is no fact this
teardown the way these were — nothing anywhere records which member is walk could read — an untagged union is treated as owning nothing, and what
live, so there is no fact a release could read. A region removes the its members point at is the program's, through whatever tag it keeps
teardown question and leaves that one exactly where it was, so an untagged beside the union. *)
union owns nothing and there is nothing here to walk. *)
let owning_fields env n = let owning_fields env n =
match Hashtbl.find_opt env.structs n with match Hashtbl.find_opt env.structs n with
| Some s -> [ s.Tast.fields ] | Some s -> [ s.Tast.fields ]
@ -488,23 +481,20 @@ let pred_holds p (t : Types.t) =
[key_pair]. *) [key_pair]. *)
| "hashable?" -> Types.keyable t | "hashable?" -> Types.keyable t
| "numeric?" -> Types.is_numeric t | "numeric?" -> Types.is_numeric t
| "copyable?" -> not (Types.is_move_only t)
| _ -> false | _ -> false
(* What one declared predicate *also* gives you. These are entailments over (* What one declared predicate *also* gives you. These are entailments over
the type system as it stands, not conveniences: every type [is_comparable] 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. admits is a number or an enum, so it is equatable. The table is only sound
The table is only sound while that is true — an ordered move-only type, or while that is true — an ordered type with no [=] would make it wrong — so
an ordered type with no [=], would make it wrong — so it lives in one place it lives in one place and says so. The gain is real ergonomics:
and says so. The gain is real ergonomics: [{:where (ordered? $t)}] is [{:where (ordered? $t)}] is enough for a [sort!] that also compares,
enough for a [sort!] that also compares and reads its elements twice, rather than two predicates on one line. *)
rather than three predicates on one line. *)
let pred_entails ~declared ~wanted = let pred_entails ~declared ~wanted =
String.equal declared wanted String.equal declared wanted
|| match wanted, declared with || match wanted, declared with
| "ordered?", "numeric?" -> true | "ordered?", "numeric?" -> true
| "equal?", ("numeric?" | "ordered?") -> true | "equal?", ("numeric?" | "ordered?") -> true
| "copyable?", ("numeric?" | "ordered?" | "equal?" | "hashable?") -> true
| _ -> false | _ -> false
let declares preds v wanted = let declares preds v wanted =
@ -518,27 +508,6 @@ let declares preds v wanted =
properties are the Vec's. *) properties are the Vec's. *)
let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None 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 ────────────────────────────────────────── (* ── (Map K V), spec-memory.md ──────────────────────────────────────────
Both halves are checked where the type is written, not where an operation 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. 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 (* 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 decided at the operation, by [key_pair], which walks its fields — the
struct table is not necessarily complete while a type is being resolved, 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 and every map that exists reaches an operation anyway, because a global
move-only type is refused and a local needs (map-new). *) map starts zeroed and a local needs (map-new). *)
(* A type variable is a map key exactly when the [where] clause says it is (* 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 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 [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; | None -> captured ctx loc name;
Loc.failk "check/unknown-name" loc "unknown name %s" name) Loc.failk "check/unknown-name" loc "unknown name %s" name)
(* What remains of spec-memory.md's ownership section after the repeal of (* What remains of spec-memory.md's ownership section after the repeals of
2026-09-18 is entirely in the types: move-only decides what may be copied, 2026-09-18 is the allocator's side alone: the region rule decides where a
the struct/union rules below decide what may own what, and the container of owning elements may be built, and the allocator's capability
allocator's capability decides what a free means at run time. Which frees decides what a free means at run time. Everything copies — a container as
run, and in what order, is the program's own business — the same contract its header, the copies aliasing one buffer — and which frees run, and in
Odin ships with — and the dev build's generation words are the net under what order, is the program's own business, the same contract Odin ships
it. The flow analysis that used to live here (a per-function dead set, a with; the dev build's epoch words are the net under it. The flow analysis
borrow flag over container reads, a loop-iteration diff) tracked use-after- that used to live here (a per-function dead set, a borrow flag, a
move and double-free statically; it was repealed rather than repaired when loop-iteration diff) went in the first repeal; the move-only concept
its holes proved structural. See spec-memory.md, "The repeal". *) 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: (* [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 [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 (* A field is never freed on its own: it would leave its owner partly
dead with no way to say so. *) dead with no way to say so. *)
fail loc fail loc
"free takes a move-only value — a Vec, a Map, or a struct that owns \ "free takes an owning container — a Vec or a Map — found %s. A \
one — found %s. A resource type with a drop hook is step 5 and does \ resource type with a drop hook is step 5 and does not exist yet"
not exist yet"
(Types.to_string other)) (Types.to_string other))
(* (clone v) uses the current allocator, (clone v a) names one. A deep, (* (clone v) uses the current allocator, (clone v a) names one. A deep,
independent copy: spec-memory.md's "copying is always explicit". *) independent copy: spec-memory.md's "copying is always explicit". *)
@ -4076,7 +4045,8 @@ and named_call ctx ~want loc name args =
| _ -> assert false) | _ -> assert false)
(* (get m k) -> (Option V). Absence is None, not an untyped nil, and the (* (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 There is no allocation here and therefore no guard: a lookup that finds
nothing is an answer, not a failure. *) nothing is an answer, not a failure. *)
| "get" -> | "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 and a reader who sees it has already been told where the promise comes
from. from.
**It owns nothing.** The result is a [Types.Slice], which is not **It owns nothing.** The result is a [Types.Slice], which carries no
move-only, carries no allocator, and is the same non-owning view allocator and is the same non-owning view (as-slice v) answers — so
(as-slice v) answers — so [free] refuses it by the rule it already had [free] refuses it by the rule it already had ("free takes an owning
("free takes a move-only value"), and nothing in the move analysis needed container"). *)
to learn about this form. *)
| "slice-from-ptr" -> | "slice-from-ptr" ->
arity loc name 2 args; arity loc name 2 args;
(match args with (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) | Some b -> (match b.bty with Types.Fn _ -> true | _ -> false)
| None -> false) -> | None -> false) ->
(* The binding the guard already found, read directly. Going back through (* The binding the guard already found, read directly. Going back through
[check] would repeat the lookup and walk the move and capture paths for [check] would repeat the lookup and walk the capture path for a type
a type that is neither move-only nor capturable. *) that is not capturable. *)
(match lookup ctx name with (match lookup ctx name with
| Some b -> call_value ctx ~want loc (mk loc b.bty (Tast.Local b.slot)) args | Some b -> call_value ctx ~want loc (mk loc b.bty (Tast.Local b.slot)) args
| None -> assert false) | 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 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, avoid. So the caller has to declare at least what the callee asks for,
and [pred_entails] means [ordered?] covers a callee wanting 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 (match Hashtbl.find_opt ctx.env.generics name with
| None -> () | None -> ()
| Some gfn -> | Some gfn ->
@ -5346,45 +5315,16 @@ let collect env (decls : Ast.decl list) =
aborts the whole compilation, so an entry left behind by a aborts the whole compilation, so an entry left behind by a
declaration that is about to be refused is never read. *) declaration that is about to be refused is never read. *)
Hashtbl.replace env.structs n { Tast.sname = n; fields }; Hashtbl.replace env.structs n { Tast.sname = n; fields };
(* spec-memory.md: "Ownership is structural, not declared" — a struct (* A struct field may own storage. Since the repeal a struct
containing a Vec is itself move-only, and freeing one recurses into holding a [(Vec i32)] is an ordinary value: assignment copies the
its owning fields while (free (.items b)) is refused because it header bytes, the copies alias one buffer, and freeing through
would leave the owner partly dead. None of that transitive two copies is the program's bug — Odin's contract, kept whole.
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.
With one exception, and it is exact: a field whose container holds The region rule is separate and survives on its own ground: a
*owning* elements. That container cannot exist outside a region — field whose container holds *owning* elements can only have been
the guard at its construction is what makes sure of it (see built against a region allocator — the guard at its construction
[vec-new]) — so the struct's field is region-allocated too, is what makes sure of it (see [vec-new]) — so that graph is
transitively and by the same guard, and the whole graph is released released by one [free-all] and no teardown recurses anywhere. *)
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
| Ast.Defdata (n, vs) -> | Ast.Defdata (n, vs) ->
(* A data type with no cases has no value, so nothing could ever be given (* 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 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 because a data type that could hold a container where a struct
could not would be a hole in the same rule. *) could not would be a hole in the same rule. *)
Hashtbl.replace env.datas n { Tast.dname = n; cases }; Hashtbl.replace env.datas n { Tast.dname = n; cases };
(* The same refusal a struct field gets, for the same reason, in the (* A case's fields are a struct and may own storage, on the struct's
same words, and with the same one exception: a data type case's terms since the repeal: copies alias, and the free is the
fields are a struct, the data type copies bytewise on assignment, program's to write. The region rule still applies on its own
and there is no recursive teardown to make that safe — except where ground — a [(Vec Value)] case field can only have been built
the field's container holds owning elements, which can only have against a region, so the recursive dynamic value parses into an
been built against a region and is therefore released whole. arena and one [free-all] releases the graph, no teardown
anywhere. *)
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;
List.iter List.iter
(fun (c : Tast.variant) -> (fun (c : Tast.variant) ->
Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c); Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c);
Hashtbl.replace env.cases c.Tast.vname (n, c)) Hashtbl.replace env.cases c.Tast.vname (n, c))
cases cases
(* ── The untagged union ────────────────────────────────────────── (* Nothing records which member of a union is live, so nothing — the
C's semantics, deliberately and in full: the members overlay one program included — can free the right one through the union itself.
storage, the size is the largest of them, the alignment the Since the repeal that is a fact about the value and not a refusal:
strictest, and nothing anywhere records which member was written a member may own storage, and freeing it is done through whatever
last. tag the program keeps beside the union, as C does. *) | Ast.Defunion (n, ms) ->
{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) ->
if ms = [] then if ms = [] then
fail loc fail loc
"%s declares no members, so it has no size and nothing could be \ "%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 if List.length (List.sort_uniq compare names) <> List.length names then
fail loc "%s declares the same member twice" n; fail loc "%s declares the same member twice" n;
let fields = List.map field ms in 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 } Hashtbl.replace env.unions n { Tast.sname = n; fields }
| Ast.Defn fn -> | Ast.Defn fn ->
(* A signature that introduces a type variable is a *pattern*, not a (* 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. 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 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 plan.org's one compiler-provided exception and this pass rejects it. *)
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. *)
and check_generic env (fn : Ast.fn) = and check_generic env (fn : Ast.fn) =
let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in
let saved_lifted = env.lifted and saved_vars = env.tyvars let saved_lifted = env.lifted and saved_vars = env.tyvars
@ -5850,14 +5682,12 @@ and check_generic env (fn : Ast.fn) =
checking a function. *) checking a function. *)
let () = check_fn_ref := check_fn let () = check_fn_ref := check_fn
(* A global of move-only type is legal. Before the repeal what made it legal (* A container's only compile-time constant is the zeroed one: a Vec's or a
was a flow rule — reading one was always a borrow, so nothing could take Map's real value exists at run time, behind an allocator. That is a fact
or free it. That rule is gone with the rest of the flow analysis: a global about initialisers and it survived both repeals untouched — nothing here
Vec may now be handed to a function, bound, or freed, and keeping its is about copying or moving.
process-long lifetime honest is the program's business, on the same terms
as every other free.
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 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 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 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 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 handle — which is what makes the handler-owns-the-arena shape in
exhausted.flan expressible. *) exhausted.flan expressible. *)
let move_only_global_init loc n (ty : Types.t) (init : Ast.init) = let rec zero_only (t : Types.t) =
if Types.is_move_only ty then 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 match init with
| Ast.Zeroed -> () | Ast.Zeroed -> ()
| _ -> | _ ->
fail loc fail loc
"the global %s is %s, which is move-only, and a move-only global \ "the global %s is %s, and such a global starts zeroed: a global's \
starts zeroed: a global's initialiser is a compile-time constant and \ initialiser is a compile-time constant, %s is not one, and a \
%s is not one. Write (defvar %s %s) with no initialiser — a zeroed \ 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 \ %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 \ load it with (set %s ...) in the function that loads it, which runs \
once and whose result outlives every call to main" 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") (match init with Ast.Uninit -> "uninit" | _ -> "this initialiser")
n (Types.to_string ty) (Types.to_string ty) n 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 (* A container 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 place — [check_place] refuses one by name — and a container's only constant
ever hold the zeroed value it was declared with, and nothing could ever put is the zeroed one, so a constant Vec could only ever hold the empty value
the file's bytes in it. Refused here, where the fix is one keyword, rather it was declared with: nothing could ever put the file's bytes in it.
than at the (set ...) that discovers it three forms later. *) Refused here, where the fix is one keyword, rather than at the (set ...)
let no_move_only_defconst loc n (ty : Types.t) = that discovers it three forms later. *)
if Types.is_move_only ty then let no_container_defconst loc n (ty : Types.t) =
if zero_only ty then
fail loc fail loc
"the global %s is %s, which is move-only, and a move-only global is a \ "the global %s is %s, and a %s global is a defvar and not a defconst: \
defvar and not a defconst: a constant is not an assignable place, so \ a constant is not an assignable place, so nothing could ever load \
nothing could ever load this one — it would stay the empty %s it was \ this one — it would stay the empty %s it was declared as. Write \
declared as. Write (defvar %s %s) and fill it in a function" (defvar %s %s) and fill it in a function"
n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty) 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 (* 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 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) -> | Ast.Defvar (n, _, init) ->
let ty, _ = Hashtbl.find env.globals n in let ty, _ = Hashtbl.find env.globals n in
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty; 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 = let ginit =
match init with match init with
| Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc } | 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) -> | Ast.Defconst (n, _, v) ->
let ty, _ = Hashtbl.find env.globals n in let ty, _ = Hashtbl.find env.globals n in
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty; 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 (* [collect] already folded the integer constants, because an array length
has to be known before any type resolves. Use that value here rather 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 than the expression it came from: a global's initialiser has to be a

37
lib/prelude.ml
View File

@ -228,29 +228,16 @@ let source = {flan|
;; variable supports only what it is declared to support — an unconstrained ;; variable supports only what it is declared to support — an unconstrained
;; one is refused at the *definition*, not at some later call site — and ;; one is refused at the *definition*, not at some later call site — and
;; [ordered?] is the predicate that admits [<], [<=], [>], [>=], [min] and ;; [ordered?] is the predicate that admits [<], [<=], [>], [>=], [min] and
;; [max]. It admits [=] and [copyable?] too: every type the language orders is ;; [max]. It admits [=] too: every type the language orders is a number or an
;; a number or an enum, so it is equatable and it is not move-only. ;; enum, so it is equatable.
;; ;;
;; [{:where (copyable? $t)}] is the opt-out from the other default. A type ;; There is no [copyable?] any more. Since the repeal every value copies —
;; variable is **move-only** until it says otherwise, because move is the ;; a container copies as its header, the copies alias one buffer, and what
;; stricter rule and assuming it can only refuse a valid program rather than ;; the copies then do is the program's business, as it is in Odin. A body
;; admit a broken one: [reduce]'s accumulator is read into [f] and then ;; that reads an element into a local and writes it into another slot is
;; assigned again, which is correct at [i32] and a double move at [(Vec i32)], ;; duplicating a header when the element owns storage, and nothing here
;; and the checker cannot tell which until it substitutes. ;; says otherwise any more: that sentence moved from a predicate into this
;; ;; comment, which is where Odin keeps it too.
;; **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.
;; ;;
;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32] ;; **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 ;; widen their element into [i64] and [f64]; "the wider type $t accumulates
@ -263,13 +250,11 @@ let source = {flan|
;; keeping attached to something. ;; keeping attached to something.
(defn swap! [s [$t] i i32 j i32] () (defn swap! [s [$t] i i32 j i32] ()
{:where (copyable? $t)}
(let [t (at s i)] (let [t (at s i)]
(set (at s i) (at s j)) (set (at s i) (at s j))
(set (at s j) t))) (set (at s j) t)))
(defn reverse! [s [$t]] () (defn reverse! [s [$t]] ()
{:where (copyable? $t)}
(let [i 0 (let [i 0
j (- (len s) 1)] j (- (len s) 1)]
(while (< i j) (while (< i j)
@ -317,7 +302,6 @@ let source = {flan|
;; predicates existed, and it stays because passing a comparison is a real ;; predicates existed, and it stays because passing a comparison is a real
;; thing to want and not only a workaround. ;; thing to want and not only a workaround.
(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] () (defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
{:where (copyable? $t)}
(let [i 1] (let [i 1]
(while (< i (len s)) (while (< i (len s))
(let [j i] (let [j i]
@ -369,7 +353,6 @@ let source = {flan|
;; here: it is two type variables and a second signature, and nothing has ;; here: it is two type variables and a second signature, and nothing has
;; wanted it. ;; wanted it.
(defn map! [s [$t] f (Fn [$t] $t)] () (defn map! [s [$t] f (Fn [$t] $t)] ()
{:where (copyable? $t)}
(dotimes [i (len s)] (dotimes [i (len s)]
(set (at s i) (f (at s i))))) (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 ;; 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. ;; as (f acc x) and the order Odin's slice.reduce uses.
(defn reduce [s [$t] init $t f (Fn [$t $t] $t)] $t (defn reduce [s [$t] init $t f (Fn [$t $t] $t)] $t
{:where (copyable? $t)}
(let [acc init] (let [acc init]
(dotimes [i (len s)] (dotimes [i (len s)]
(set acc (f acc (at s i)))) (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 ;; runtime needed no change at all, because SizeOf and AlignOf are computed at
;; the instantiation site, where the element type is concrete. ;; the instantiation site, where the element type is concrete.
(defn filter [s [$t] keep? (Fn [$t] bool)] (Vec $t) (defn filter [s [$t] keep? (Fn [$t] bool)] (Vec $t)
{:where (copyable? $t)}
(let [v (vec-new t)] (let [v (vec-new t)]
(dotimes [i (len s)] (dotimes [i (len s)]
(when (keep? (at s i)) (when (keep? (at s i))

11
lib/types.ml
View File

@ -124,17 +124,6 @@ let rec to_string = function
let is_numeric = function Int _ | Float _ -> true | _ -> false 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 — (* The key types the first Map implementation admits (spec-memory.md, "Maps —
first implementation"): integers, enums, strings, fixed arrays, and value first implementation"): integers, enums, strings, fixed arrays, and value
structs composed recursively from those. Equality and hashing for them are structs composed recursively from those. Equality and hashing for them are

2
spike/generics/prelude-shapes.flan
View File

@ -3,7 +3,6 @@
;; prelude; it is the same bodies, over $t, checked and run. ;; prelude; it is the same bodies, over $t, checked and run.
(defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t) (defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t)
{:where (copyable? $t)}
(let [v (vec-new t)] (let [v (vec-new t)]
(dotimes [i (len s)] (dotimes [i (len s)]
(when (keep? (at s i)) (when (keep? (at s i))
@ -15,7 +14,6 @@
(set (at s i) (f (at s i))))) (set (at s i) (f (at s i)))))
(defn fold [s [$t] init $t f (Fn [$t $t] $t)] t (defn fold [s [$t] init $t f (Fn [$t $t] $t)] t
{:where (copyable? $t)}
(let [acc init] (let [acc init]
(dotimes [i (len s)] (dotimes [i (len s)]
(set acc (f acc (at s i)))) (set acc (f acc (at s i))))

2
test/programs/generic-runaway.flan
View File

@ -5,6 +5,6 @@
;;;; Session.eval runs the same code the thing that hung was C-c C-c with the ;;;; 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 ;;;; dev daemon wedged behind it. The refusal names the chain of
;;;; instantiations rather than a depth it gave up at. ;;;; 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)) (defn main [] () (grow 1))

8
test/programs/generics.flan
View File

@ -21,13 +21,11 @@
;; The variable is bound *inside* a type constructor, which is a structural ;; The variable is bound *inside* a type constructor, which is a structural
;; walk rather than a name match. ;; walk rather than a name match.
(defn first-or [s [$t] d $t] $t (defn first-or [s [$t] d $t] $t
{:where (copyable? $t)}
(if (= (len s) 0) d (at s 0))) (if (= (len s) 0) d (at s 0)))
;; A generic calling a generic at its own variable: the copy of [swap!] is ;; A generic calling a generic at its own variable: the copy of [swap!] is
;; generated when [rotate!] is instantiated and not before. ;; generated when [rotate!] is instantiated and not before.
(defn rotate! [s [$t]] () (defn rotate! [s [$t]] ()
{:where (copyable? $t)}
(dotimes [i (- (len s) 1)] (dotimes [i (- (len s) 1)]
(swap! s i (+ i 1)))) (swap! s i (+ i 1))))
@ -37,7 +35,7 @@
(+ x x)) (+ x x))
;; equal? admits = and !=; ordered? admits < <= > >= min max, and entails ;; equal? admits = and !=; ordered? admits < <= > >= min max, and entails
;; equal? and copyable?. ;; equal?.
(defn count-of [s [$t] x $t] i32 (defn count-of [s [$t] x $t] i32
{:where (equal? $t)} {:where (equal? $t)}
(let [n 0] (let [n 0]
@ -52,14 +50,12 @@
;; Two variables, and the second is determined by its own argument. ;; Two variables, and the second is determined by its own argument.
(defn fst [a $t b $u] $t (defn fst [a $t b $u] $t
{:where [(copyable? $t) (copyable? $u)]}
(do b a)) (do b a))
;; println over a type variable is the one form the abstract pass defers to ;; println over a type variable is the one form the abstract pass defers to
;; the instantiation, because its legality is only decidable after ;; the instantiation, because its legality is only decidable after
;; substituting. The structural printer is selected per copy. ;; substituting. The structural printer is selected per copy.
(defn show [x $t] () (defn show [x $t] ()
{:where (copyable? $t)}
(println x)) (println x))
;; A cast to a type variable. [(t x)] is not a name [is_cast] knows — [t] is ;; 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 ;; 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. ;; reaches the one list of what names a type; (map-new t i32) is the other.
(defn one-of [x $t] (Vec $t) (defn one-of [x $t] (Vec $t)
{:where (copyable? $t)}
(let [v (vec-new t)] (let [v (vec-new t)]
(push v x) (push v x)
v)) v))
@ -81,7 +76,6 @@
;; (zeroed) takes its type from the position it is written in, so a variable ;; (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. ;; in that position is answered by the instantiation like any other type.
(defn zero-of [x $t] $t (defn zero-of [x $t] $t
{:where (copyable? $t)}
(do x (zeroed))) (do x (zeroed)))
;; The map operations over a key that is a type variable. The hash and the ;; The map operations over a key that is a type variable. The hash and the

2
test/programs/reload-generic.flan
View File

@ -11,13 +11,11 @@
(defvar counter i64) (defvar counter i64)
(defn put! [xs [$t] i i32 v $t] () (defn put! [xs [$t] i i32 v $t] ()
{:where (copyable? $t)}
(set (at xs i) v)) (set (at xs i) v))
;;; Calls [put!] at its own variable, so the copy of [put!] is generated when ;;; Calls [put!] at its own variable, so the copy of [put!] is generated when
;;; [hold!] is instantiated and not before. ;;; [hold!] is instantiated and not before.
(defn hold! [xs [$t] v $t] () (defn hold! [xs [$t] v $t] ()
{:where (copyable? $t)}
(put! xs 0 v)) (put! xs 0 v))
(defn pick [xs [$t]] $t (defn pick [xs [$t]] $t

10
test/programs/vec-in-struct.flan
View File

@ -1,9 +1,7 @@
;;;; spec-memory.md: "Ownership is structural, not declared" — a struct ;;;; A struct may own a Vec since the second repeal: the field is header
;;;; containing a Vec is itself move-only, transitively, with recursive ;;;; bytes, assignment copies them, and the two copies alias one buffer.
;;;; teardown, and with a field that cannot be freed on its own. None of that ;;;; Which copy's free runs is the program's business — Odin's contract.
;;;; machinery exists: it is the same recursive teardown `drop` brings, and it ;;;; This used to be a negative fixture; now it pins the admission.
;;;; lands with it. Accepting the field meanwhile would give a struct that
;;;; copies its header on assignment two owners of one buffer.
(defstruct Builder [buf (Vec u8)]) (defstruct Builder [buf (Vec u8)])
(defn main [] i32 0) (defn main [] i32 0)

14
test/test_acceptance.ml
View File

@ -1992,13 +1992,10 @@ let () =
the Vec of a Vec is a run-time question about the allocator instead, so 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). its program runs rather than being refused (programs/arena-region.flan).
This one stays, and the narrowing is exactly why: a [(Vec u8)] field Since the second repeal the plain field is admitted: two copies of
holds elements that own nothing, so nothing forces it into a region, the struct are two headers over one buffer, and that is the program's
and two copies of the struct would be two headers over one heap buffer. to manage — Odin's contract. The program compiles and runs. *)
A container whose *elements* own storage is the case that is admitted, outputs "a struct field that owns a Vec" "programs/vec-in-struct.flan" "";
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";
(* And it does not cross to C: the shim would flatten a header that owns (* 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 storage. Refused by the shim generator, where the message can say what
to pass instead. *) 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" refuses_src "a data type with no cases"
"(defdata U [])\n(defn f [u U] () 0)" "(defdata U [])\n(defn f [u U] () 0)"
"declares no cases"; "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 (* 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 its fields and the struct table is not necessarily complete while a
type is resolving, so both are answered where the hash and equality type is resolving, so both are answered where the hash and equality

65
test/test_flan.ml
View File

@ -896,12 +896,12 @@ let () =
rejects_check "slice-from-ptr with a negative literal length" rejects_check "slice-from-ptr with a negative literal length"
"(defn f [p (Ptr i32)] i32 (len (slice-from-ptr p -1)))" "(defn f [p (Ptr i32)] i32 (len (slice-from-ptr p -1)))"
~needle:"is negative"; ~needle:"is negative";
(* The storage stays C's. A slice is not move-only and carries no allocator, (* The storage stays C's. A slice carries no allocator, so free refuses one
so free refuses one by the rule it already had — this pins that the new by the rule it already had — this pins that the new form did not become
form did not become a thing anybody could hand to free. *) a thing anybody could hand to free. *)
rejects_check "free of a slice made from a pointer" rejects_check "free of a slice made from a pointer"
"(defn f [p (Ptr i32)] () (free (slice-from-ptr p 3)))" "(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 ────────────────────────────── *) (* ── Structs, fields and auto-deref ────────────────────────────── *)
let cursor = "(defstruct Cursor [src [u8] pos i32]) " in let cursor = "(defstruct Cursor [src [u8] pos i32]) " in
@ -1040,17 +1040,14 @@ let () =
"(defdata Value [Nil (List [items (Vec Value)])])"; "(defdata Value [Nil (List [items (Vec Value)])])";
accepts "a data type case holding a Map of itself" accepts "a data type case holding a Map of itself"
"(defdata Value [Nil (Table [entries (Map string Value)])])"; "(defdata Value [Nil (Table [entries (Map string Value)])])";
(* And the narrowing is exact, which is what these two are for. A container (* Since the second repeal the plain case is admitted too: a struct or a
whose elements own *nothing* is not forced into a region by anything, so case holding a heap-backed Vec copies as bytes, the copies alias one
it would sit in a copyable aggregate on the heap with two headers and one buffer, and a free through two copies is the program's bug — Odin's
buffer between them — the double free the original refusal existed to contract exactly. These pin the admission. *)
prevent. It stays refused, in a struct and in a union alike. *) accepts "a data type case holding a plain Vec"
rejects_check "a data type case holding a plain Vec" "(defdata Value [Nil (Bytes [bs (Vec u8)])])";
"(defdata Value [Nil (Bytes [bs (Vec u8)])])" accepts "a struct field holding a plain Vec"
~needle:"makes the data type move-only"; "(defstruct B [buf (Vec u8)])";
rejects_check "a struct field holding a plain Vec"
"(defstruct B [buf (Vec u8)])"
~needle:"a struct that owns one is move-only too";
(* free does not recurse and does not quietly release the outer block: it (* 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. *) names free-all, which is the operation that actually releases the graph. *)
rejects_check "free on a container of owning elements" rejects_check "free on a container of owning elements"
@ -1622,12 +1619,11 @@ let () =
rejects_check "a union that contains itself by value" rejects_check "a union that contains itself by value"
"(defunion U [a i32 b U])\n(defn f [u U] i32 0)" "(defunion U [a i32 b U])\n(defn f [u U] i32 0)"
~needle:"contains itself by value"; ~needle:"contains itself by value";
(* Not waiting on drop, unlike the struct and data type refusals: nothing (* Nothing records which member is live, and since the second repeal that
records which member is live, so there is no fact recursive teardown is the program's fact to keep rather than a refusal: a union member may
could read. *) own storage, C's way. *)
rejects_check "a union member that is move-only" accepts "a union member that owns storage"
"(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)" "(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)";
~needle:"nothing records which was written";
(* And the one the optimiser would otherwise be handed: a byte that is (* 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 neither 0 nor 1 read as an i1. Refused at any depth, which is why the
second row goes through a struct. *) second row goes through a struct. *)
@ -2604,7 +2600,7 @@ let () =
accepts "a map return type, written the one way there is" accepts "a map return type, written the one way there is"
"(defn f [] (Map string i32) (map-new string i32))"; "(defn f [] (Map string i32) (map-new string i32))";
accepts "a map return type followed by a constraint map" 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)))"; (do x (map-new string i32)))";
rejects_check "braces in type position say where the spelling went" rejects_check "braces in type position say where the spelling went"
~needle:"written (Map K V)" ~needle:"written (Map K V)"
@ -2621,13 +2617,13 @@ let () =
~needle:"nothing here says t is ordered?" ~needle:"nothing here says t is ordered?"
"(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))"; "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))";
(* The entailments, which are the reason a signature is one predicate long (* 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, rather than two. Every type the language orders is a number or an enum,
so it is equatable and it is not move-only. *) so it is equatable. *)
accepts "ordered? entails equal?" accepts "ordered? entails equal?"
"(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))"; "(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))";
accepts "numeric? entails ordered?" accepts "numeric? entails ordered?"
"(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))"; "(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))"; "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
rejects_check "a predicate nobody has heard of" rejects_check "a predicate nobody has heard of"
~needle:"is not a type predicate" ~needle:"is not a type predicate"
@ -2636,12 +2632,13 @@ let () =
~needle:"is not a type variable of f" ~needle:"is not a type variable of f"
"(defn f [a i32] i32 {:where (ordered? $t)} a)"; "(defn f [a i32] i32 {:where (ordered? $t)} a)";
(* Move-only by default still decides the structural rules for a $t — what (* Everything copies since the second repeal, so a double use of a binding
may own one — but since the repeal a double use of a binding is not needs no clause at all — and [copyable?] itself is gone, refused the way
checked, so both of these are accepted with and without the clause. *) any unknown predicate is, which is this pin's job to remember. *)
accepts "a type variable is usable twice without copyable?" accepts "a type variable is usable twice with no clause"
"(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))"; "(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))"; "(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 (* 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 after substituting — which is the one thing the abstract pass otherwise
refuses to do. *) refuses to do. *)
accepts "println over a type variable is deferred" 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" 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 (* 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 it and the call site, or the refusal moves into code the caller did not
write. *) write. *)
rejects_check "a predicate is not carried through a generic call" rejects_check "a predicate is not carried through a generic call"
~needle:"has to be carried by every signature" ~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" accepts "and is accepted when it is"
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))"; "(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
@ -2670,7 +2667,7 @@ let () =
itself is refused where it is written, at the definition. *) itself is refused where it is written, at the definition. *)
rejects_check "a map keyed by a type variable that is not hashable?" rejects_check "a map keyed by a type variable that is not hashable?"
~needle:"is not a map key" ~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" accepts "and hashable? is what says it is"
"(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))"; "(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
accepts "and under it the operations are deferred, not refused" accepts "and under it the operations are deferred, not refused"

8
test/test_session.ml
View File

@ -791,7 +791,7 @@ let () =
installed nothing and did not say anything had gone wrong. Both copies 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 have to be named, and the copy of [put!] that [hold!] pulls in has to be
there too, which is transitivity. *) 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 -> | c ->
if not c.Session.installs then if not c.Session.installs then
fail "redefining a generic installed nothing"; fail "redefining a generic installed nothing";
@ -814,7 +814,7 @@ let () =
instantiation that generated them was transitive, and finding them again instantiation that generated them was transitive, and finding them again
is one table lookup rather than a walk, because a whole-program check has is one table lookup rather than a walk, because a whole-program check has
already regenerated all of them. *) 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 -> | c ->
List.iter List.iter
(fun want -> (fun want ->
@ -884,7 +884,7 @@ let () =
caller. *) caller. *)
(match (match
Session.eval (gen ()) 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))" (set (at xs (i32 i)) v))"
with with
| _ -> fail "a generic's changed parameter type was accepted" | _ -> fail "a generic's changed parameter type was accepted"
@ -902,7 +902,7 @@ let () =
long before the session is asked anything. *) long before the session is asked anything. *)
(match (match
Session.eval (gen ()) 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 with
| c -> | c ->
if not (List.mem "pick-i32" c.Session.fns) then if not (List.mem "pick-i32" c.Session.fns) then

32
web/index.html
View File

@ -886,11 +886,10 @@ type as an argument — <code>(vec-new t)</code>, <code>(map-new t i32)</code>,
(min (max x lo) hi)) (min (max x lo) hi))
(defn first-or [s [$t] d $t] $t ; the variable inside a slice type (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))) (if (= (len s) 0) d (at s 0)))
(defn one-of [x $t] (Vec $t) ; bare t is the type-name argument (defn one-of [x $t] (Vec $t) ; bare t is the type-name argument
{:where (copyable? $t)}
(let [v (vec-new t)] (let [v (vec-new t)]
(push v x) (push v x)
v)) v))
@ -927,8 +926,8 @@ $t)} at the head of the body, or take the operation as a parameter — a
<p>What makes that liveable is a <code>where</code> clause, written as a Clojure-style <p>What makes that liveable is a <code>where</code> clause, written as a Clojure-style
map at the head of the body — <code>{:where (ordered? $t)}</code>, or a vector when map at the head of the body — <code>{:where (ordered? $t)}</code>, or a vector when
there is more than one: <code>{:where [(copyable? $t) (copyable? $u)]}</code>. There there is more than one: <code>{:where [(ordered? $t) (hashable? $u)]}</code>. There
are five predicates, and each gates builtins the compiler already has:</p> are four predicates, and each gates builtins the compiler already has:</p>
<div class="scroll"> <div class="scroll">
<table> <table>
@ -937,30 +936,19 @@ are five predicates, and each gates builtins the compiler already has:</p>
<tr><td><code>ordered?</code></td><td><code>&lt;</code> <code>&lt;=</code> <code>&gt;</code> <code>&gt;=</code> <code>min</code> <code>max</code></td></tr> <tr><td><code>ordered?</code></td><td><code>&lt;</code> <code>&lt;=</code> <code>&gt;</code> <code>&gt;=</code> <code>min</code> <code>max</code></td></tr>
<tr><td><code>equal?</code></td><td><code>=</code> and <code>!=</code></td></tr> <tr><td><code>equal?</code></td><td><code>=</code> and <code>!=</code></td></tr>
<tr><td><code>hashable?</code></td><td>the variable as a <code>Map</code> key — <code>(map-new t V)</code>, <code>get</code>, <code>put</code>, <code>has-key?</code></td></tr> <tr><td><code>hashable?</code></td><td>the variable as a <code>Map</code> key — <code>(map-new t V)</code>, <code>get</code>, <code>put</code>, <code>has-key?</code></td></tr>
<tr><td><code>copyable?</code></td><td>reading the value more than once; <code>Pool</code> and <code>Vec</code> element positions</td></tr>
</table> </table>
</div> </div>
<p>They entail each other in one direction, so one clause usually does: <p>They entail each other in one direction, so one clause usually does:
<code>numeric?</code> gives <code>ordered?</code>, <code>ordered?</code> gives <code>numeric?</code> gives <code>ordered?</code>, and <code>ordered?</code> gives
<code>equal?</code>, and any of the four gives <code>copyable?</code>. A <code>equal?</code>. A <code>sort!</code> that compares its elements declares
<code>sort!</code> that compares its elements and reads them twice declares
<code>ordered?</code> and nothing else.</p> <code>ordered?</code> and nothing else.</p>
<p><strong>A type variable is move-only by default</strong>, and <p><strong>Every value copies.</strong> There used to be a fifth predicate,
<code>copyable?</code> is the opt-out. <code>Types.is_move_only</code> of a variable is <code>copyable?</code>, gating a second read of a move-only variable; the move
not decidable abstractly — the same variable is <code>i32</code> at one instantiation concept was repealed on 2026-09-18 — a container copies as its header, the
and <code>(Vec i32)</code> at the next — so the checker assumes the stricter rule, copies alias one buffer, and which free runs is the program's business, as it
which can only refuse a program that would have been fine and never admit one that is in Odin — so the predicate went with it.</p>
double-frees. It is Rust's <code>T: Copy</code>, with the difference that the compiler
answers the question rather than a user implementing a trait. So
<code>(defn twice [x $t] $t (+ x x))</code> does not merely want
<code>numeric?</code>; reading <code>x</code> a second time is a use after move:</p>
<pre><code class="sh">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</code></pre>
<p>Each instantiation then checks the concrete type against what the signature declared, <p>Each instantiation then checks the concrete type against what the signature declared,
and refuses the <em>call site</em> when it does not answer:</p> and refuses the <em>call site</em> when it does not answer:</p>