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

where predicates admit operators, and a type variable is move-only until it says otherwise

Browse Source 
The spike proved the shape; this makes it the feature. A generic body is
still checked abstractly once, but now it may be told what to assume:
{:where (ordered? $t)} at the head of the body, Clojure's {:pre [...]}
spelling, with five predicates - ordered?, equal?, hashable?, numeric?
and copyable?.

The syntax catch settled structurally: {K V} is still a legal return
type, and a constraint map is told from one by its leading keyword. A
keyword is not a type anywhere in the language, so the slot after the
return type is unambiguous and {K V} did not have to go.

A type variable is move-only by default, with copyable? the opt-out.
Move is the stricter rule, so assuming it can only refuse a valid
program, never admit a bad one. That is Rust's T: Copy and not Odin's
anything - Odin has no move semantics at all.

The runaway refusal no longer names a depth. It names the chain: a
generic already on the instantiation stack, asked for again at a type
built around the one it had before, is growing and will not stop.
This commit is contained in:
Joseph Ferano 2026-09-13 14:33:45 +07:00
parent 70e19753dd
commit 7f86f32699
5 changed files with 415 additions and 55 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
lib/ast.ml
View File

@ -126,10 +126,21 @@ and pattern =
(* ── Declarations ──────────────────────────────────────────────────── *)
(* One [where] predicate: [(ordered? $t)] is [{ pname = "ordered?"; pvar = "t" }].
A predicate is a *compile-time question about a type*, not a type class: it
carries no implementation and selects no instance, it only tells the
abstract pass which builtin operators the variable may be used with, and
makes each instantiation check the concrete type answers yes. *)
type pred = { pname : string; pvar : string; ploc : Loc.t }
type fn = {
name : string;
params : field list;
ret : texpr option; (* None means (); only declare omits it *)
(* The [{:where ...}] map at the head of the body, already unpacked. Empty
for every function that has none, which is every function that is not
generic and most that are. *)
fwhere : pred list;
fbody : expr list;
nloc : Loc.t;
}

374
lib/check.ml
View File

@ -102,14 +102,24 @@ type env = {
[resolve_name] consults it before anything else, so the body resolves
[t] to [i32] and every node under it is concrete. *)
mutable subst : (string * Types.t) list;
(* How many instantiations deep the checker is. A generic that calls itself
at a *larger* type — [(defn grow [x $t] () (grow [x x]))] — asks for a
copy at [[2 t]], which asks for one at [[2 [2 t]]], forever. Without this
the checker does not fail, it hangs, and since [Session.eval] runs the
same code that is the editor hanging with the daemon wedged behind it.
Odin has no cap of its own to copy; the number is arbitrary and the
refusal that names the chain is still to design. *)
mutable depth : int;
(* The [where] predicates in scope: what the abstract pass may assume about
the variables, and what each instantiation checks its concrete types
answer yes to. Empty everywhere a generic signature or body is not being
resolved, which is what keeps every refusal below the default. *)
mutable tvpreds : Ast.pred list;
(* The chain of instantiations currently being generated, innermost last:
the generic's name and the concrete parameter types each copy was asked
for. It is the refusal for a generic that instantiates itself without
end — [(defn grow [x $t] () (grow [x x]))] asks for a copy at [[2 t]],
which asks for one at [[2 [2 t]]], forever — and without it the checker
does not fail, it *hangs*, which through [Session.eval] is [C-c C-c]
hanging with the dev daemon wedged behind it.
The test is structural rather than a depth count. A depth count names a
number the programmer did not write and cannot act on; this names the
chain. Odin has no cap of its own to copy, so there was nothing to
borrow. *)
mutable chain : (string * Types.t list * Loc.t) list;
}
let new_env () = {
@ -130,7 +140,8 @@ let new_env () = {
instances = [];
tyvars = [];
subst = [];
depth = 0;
tvpreds = [];
chain = [];
}
(* Where a named type was declared, and what it has, as a note.
@ -388,6 +399,87 @@ let unimplemented loc what milestone =
fail loc "%s is not implemented yet — milestone %d (see plan.org)"
what milestone
(* ── where predicates ──────────────────────────────────────────────────
A predicate is a compile-time question about a type, and that is the whole
of it. It carries no implementation, selects no instance, and is not
extensible: it gates a builtin the compiler already has. So there are no
dictionaries, no coherence rules and no run-time cost — and the ceiling is
that nobody can supply a [<] of their own, which does not bind because
every operation the prelude and the containers need is a primitive.
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?" ]
(* Does a concrete type answer yes? Checked at every instantiation, against
the type the call site asked for. *)
let pred_holds p (t : Types.t) =
match p with
| "ordered?" -> Types.is_comparable t
| "equal?" -> Types.is_equatable t
(* [Types.keyable] says yes to a struct and leaves its fields to [key_pair],
which walks them at the operation. That split is the existing one and is
kept: a generic declared [hashable?] and instantiated at a struct whose
fields are not keyable is refused where every other program is, by
[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. *)
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 =
List.exists
(fun (p : Ast.pred) ->
String.equal p.Ast.pvar v && pred_entails ~declared:p.Ast.pname ~wanted)
preds
(* Which variable, if any, a type bottoms out at. Only a bare variable can
carry a predicate: [(Vec t)] is a Vec whatever [t] is, and its own
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?]: [(defn twice [x $t] $t (+ x x))] is refused, which
is right — correct at [i32], a double read of a moved value at [(Vec i32)],
and the checker cannot tell which until it substitutes.
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.
@ -395,12 +487,12 @@ let unimplemented loc what milestone =
and repeats these refusals rather than assuming: the two are reached by
different paths and a silent disagreement between them would be worse than
saying the same thing twice. *)
let map_type loc (k : Types.t) (v : Types.t) =
let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
(* The value. The restriction is the one [(Vec (Vec T))] already carries,
for the identical reason: the runtime copies and releases entries
bytewise, so an owning value would have its header duplicated by clone
and its buffer dropped on the floor by free. *)
if Types.is_move_only v then
if move_only preds v then
fail loc
"(Map %s %s) holds a move-only value, and the type-erased runtime \
copies entries bytewise — so clone would duplicate headers instead of \
@ -423,7 +515,13 @@ let map_type loc (k : Types.t) (v : Types.t) =
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). *)
if not (Types.keyable k) then
(* 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
instantiated at [string]. *)
if not (match k with
| Types.Var v -> declares preds v "hashable?"
| k -> Types.keyable k) then
fail loc
"%s is not a map key. The first implementation takes integers, enums, \
bools, strings, fixed arrays of those, and value structs composed of \
@ -471,7 +569,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
braces two meanings is what the colon-to-dot change was for. A map is
built with (map-new) and filled with (put). *)
| Ast.Tmap (k, v) ->
map_type loc (resolve env ~seen k) (resolve env ~seen v)
map_type ~preds:env.tvpreds loc (resolve env ~seen k)
(resolve env ~seen v)
(* (Fn [T ...] R): a function value, which is one code address and no
environment beside it. There is no capture — [check_fn] refuses a
reference to an enclosing local by name — so this is a pointer with a
@ -497,7 +596,7 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
buffers on the floor. Recursive teardown is what step 5's [drop]
brings, and this is refused until it does rather than shipping the
shallow answer under the deep name. *)
if Types.is_move_only e then
if move_only env.tvpreds e then
fail loc
"(Vec %s) holds a move-only element, and the type-erased runtime \
copies and releases elements bytewise — so clone would duplicate \
@ -507,7 +606,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
Types.Vec e
| "Vec", _ -> fail loc "(Vec T) takes exactly one type"
| "Map", [ k; v ] ->
map_type loc (resolve env ~seen k) (resolve env ~seen v)
map_type ~preds:env.tvpreds loc (resolve env ~seen k)
(resolve env ~seen v)
| "Map", _ -> fail loc "(Map K V) takes exactly two types"
| "Result", _ -> unimplemented loc "(Result T E)" 6
| "Pool", [ a ] ->
@ -516,7 +616,7 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
runtime is type-erased and copies and releases slots bytewise, so a
release would drop what an owning element owns. Recursive teardown
arrives with drop. *)
if Types.is_move_only e then
if move_only env.tvpreds e then
fail loc
"(Pool %s) holds a move-only element, and the type-erased runtime \
copies and releases slots bytewise — so releasing a slot would \
@ -735,17 +835,27 @@ let rec generic_ty (t : Types.t) =
operator says the same thing: with no constraints a type variable supports
only what *every* type supports, so [=], [<], [+] and [hash] over one are
rejected rather than silently instantiated at whatever type the first call
site happened to use. The way out is the one plan.org names — pass the
operation in as a function value, which is what [sort-i32-by!] already
does with [(Fn [i32 i32] bool)]. *)
let unconstrained loc op (t : Types.t) =
site happened to use.
With [where] there are now two ways out and the message names both: declare
the predicate, or take the operation as a function value the way
[sort-by!] does. Declaring it is the one that keeps the call site short,
which is the whole reason predicates exist — under the no-constraint rule
[(sort! xs)] had to become [(sort-by! xs (fn [a b] (< a b)))] at every call
site in the corpus. *)
let unconstrained env loc op ~needs (t : Types.t) =
if generic_ty t then
Loc.failk "check/unconstrained-type-variable" loc
"%s over the type variable %s is refused: an unconstrained type \
variable supports only what every type supports, and %s is not that \
(plan.org, Types). Take the operation as a parameter — a (Fn [%s %s] \
...) — and call it here"
op (Types.to_string t) op (Types.to_string t) (Types.to_string t)
match tyvar_of t with
| Some v when declares env.tvpreds v needs -> ()
| _ ->
Loc.failk "check/unconstrained-type-variable" loc
"%s over the type variable %s is refused: a type variable supports \
only what it is declared to support, and nothing here says %s is \
%s. Write {:where (%s $%s)} at the head of the body, or take the \
operation as a parameter — a (Fn [%s %s] ...) — and call it here"
op (Types.to_string t) (Types.to_string t) needs needs
(Types.to_string t) (Types.to_string t) (Types.to_string t)
(* How a concrete type is spelled inside an instantiation's name. The prelude
already writes this by hand — [filter-i32], [sum-f32], [append-i64] — so a
@ -768,6 +878,82 @@ let rec mangle_ty (t : Types.t) =
(String.concat "-" (List.map mangle_ty ps)) (mangle_ty r)
| t -> Types.to_string t
(* ── The runaway instantiation, refused by name rather than by depth ────
[(defn grow [x $t] () (grow [x x]))] asks for a copy at [[t]], which asks
for one at [[[t]]], forever. Before this the checker did not fail, it
*hung*, and [Session.eval] runs the same code — so what hung was [C-c C-c],
with the dev daemon wedged behind it and nothing to show the editor. That
is the project's stated priority stopped by three lines of ordinary-looking
Flan, which is why this is a refusal and not a cap.
The spike stopped it with a depth counter refusing past 32. A number is the
wrong thing to say: 32 is not in the program, the programmer cannot act on
it, and a legitimate deep instantiation and a runaway one look identical in
the message. **The structural test is exact.** A generic that is already on
the chain and is being asked for again at a type that *contains* the type
it was asked for before is growing, and growing without a smaller case is
not going to stop. A generic that recurses at the *same* types never
reaches here — the cache entry goes in before the body is checked — and one
that recurses at a *smaller* or unrelated type is fine and stays fine.
The message prints the chain, which is what the programmer can act on: each
link is a call site and a type, and the place the type started growing is
visible in the list.
Odin has no cap of its own to copy, so there was nothing to borrow and this
is the whole design. The depth backstop below stays as a backstop only: it
catches a growth this test does not recognise, and it is never the thing
the message is about. *)
let rec occurs_in ~needle (t : Types.t) =
Types.equal needle t
||
match t with
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
| Types.Pool e | Types.Handle e | Types.Option e -> occurs_in ~needle e
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
| Types.Fn (ps, r) ->
List.exists (occurs_in ~needle) ps || occurs_in ~needle r
| _ -> false
(* [b] is [a] with something built around it: same shape, strictly bigger. *)
let grows ~from_:a ~to_:b =
List.length a = List.length b
&& List.for_all2 (fun x y -> occurs_in ~needle:x y) a b
&& not (List.for_all2 Types.equal a b)
let runaway env loc gname cparams =
let chain_text () =
String.concat "\n "
(List.map
(fun (g, ps, l) ->
Printf.sprintf "%s at (%s), asked for at %s" g
(String.concat " " (List.map Types.to_string ps))
(Loc.to_string l))
(env.chain @ [ (gname, cparams, loc) ]))
in
let earlier =
List.find_opt
(fun (g, ps, _) -> String.equal g gname && grows ~from_:ps ~to_:cparams)
env.chain
in
(match earlier with
| Some _ ->
Loc.failk "check/runaway-instantiation" loc
"%s instantiates itself without end. Each copy asks for another at a \
type built around the one before, so there is no last copy to \
generate:\n %s\nA generic function may call itself, but not at a \
type built out of its own type variable — the argument has to get \
smaller, or stay the same"
gname (chain_text ())
| None -> ());
(* The backstop. Nothing known reaches it; it exists so that a growth the
test above does not recognise is still a refusal with the chain in it
rather than a hang. *)
if List.length env.chain >= 64 then
Loc.failk "check/runaway-instantiation" loc
"%s has been instantiated 64 deep and is still going:\n %s"
gname (chain_text ())
(* [check_fn] is defined after the expression checker and an instantiation is
made from inside it, so the knot is tied here and closed at the bottom of
the file. One forward reference rather than moving a 90-line function. *)
@ -1035,6 +1221,19 @@ let direct = function
two maps with the same key type share one pair. *)
let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
match k with
(* A hash and an equality for a type variable would have to be *chosen*,
and nothing here can choose: the pair is emitted as concrete symbols and
the concrete type does not exist until the instantiation. Refused rather
than assumed — falling through to [bytewise_key] would hash whatever
bytes the variable turned out to have, which is the wrong answer for a
[string] and for any struct with padding. Inside an instantiation this
arm is unreachable: [env.subst] has already made [k] concrete. *)
| Types.Var v ->
Loc.failk "check/generic-map-key" loc
"a map keyed by the type variable %s cannot have its hash and equality \
emitted here — they are chosen from the concrete type, which does not \
exist until this generic is instantiated. The key pair is emitted per \
copy, so this operation belongs in a body the checker has substituted" v
| Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
| t when bytewise_key t ->
Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
@ -1510,7 +1709,8 @@ and var ctx loc ~want name =
| _ ->
match lookup ctx name with
| Some b ->
if Types.is_move_only b.bty then moved ~ty:b.bty ctx loc name b.slot;
if move_only ctx.env.tvpreds b.bty then
moved ~ty:b.bty ctx loc name b.slot;
expect loc ~want (mk loc b.bty (Tast.Local b.slot))
| None ->
match Hashtbl.find_opt ctx.env.globals name with
@ -2716,8 +2916,11 @@ and fold_left_prim ctx ~want loc name p ok what args =
match args with x :: y :: rest -> x, y, rest | _ -> assert false
in
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
unconstrained loc name a.Tast.ty;
if not (ok a.Tast.ty) then
unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
(* Past [unconstrained] a variable here is one the [where] clause admitted,
so the concrete predicate below has nothing to say about it — it is
answered again, per copy, at the instantiation. *)
if not (ok a.Tast.ty || generic_ty a.Tast.ty) then
fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
let ty = a.Tast.ty in
let acc =
@ -2977,7 +3180,7 @@ and pool_new_elem ctx ~want loc args =
in
match named with
| Some (t, rest) ->
if Types.is_move_only t then
if move_only ctx.env.tvpreds t then
fail loc
"(Pool %s) holds a move-only element, and the type-erased runtime \
copies and releases slots bytewise. Recursive teardown arrives with \
@ -3044,8 +3247,8 @@ and named_call ctx ~want loc name args =
| "%" ->
arity loc name 2 args;
let a, b = binary ctx name loc ~want:(numeric_want want) args in
unconstrained loc name a.Tast.ty;
if not (Types.is_numeric a.Tast.ty) then
unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
prim Tast.Rem a.Tast.ty [ a; b ]
| "=" | "!=" | "<" | "<=" | ">" | ">=" ->
@ -3064,8 +3267,10 @@ and named_call ctx ~want loc name args =
| "=" | "!=" -> Types.is_equatable a.Tast.ty
| _ -> Types.is_comparable a.Tast.ty
in
unconstrained loc name a.Tast.ty;
if not ok then
unconstrained ctx.env loc name
~needs:(match name with "=" | "!=" -> "equal?" | _ -> "ordered?")
a.Tast.ty;
if not (ok || generic_ty a.Tast.ty) then
fail loc
"%s compares machine numbers; %s has no built-in comparison \
(plan.org, Types)" name (Types.to_string a.Tast.ty);
@ -3123,7 +3328,10 @@ and named_call ctx ~want loc name args =
match args with x :: y :: rest -> x, y, rest | _ -> assert false
in
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
if not (Types.is_numeric a.Tast.ty) then
(* [min] and [max] are [<] with a pick, so [ordered?] is what they want —
not [numeric?]. A generic that declares [ordered?] gets both. *)
unconstrained ctx.env loc name ~needs:"ordered?" a.Tast.ty;
if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
let ty = a.Tast.ty in
let cmp = if String.equal name "min" then Tast.Lt else Tast.Gt in
@ -3796,7 +4004,7 @@ and named_call ctx ~want loc name args =
| "map-new" ->
let k, v, args = map_new_types ctx ~want loc args in
let a = allocator_arg ctx loc args in
let mty = map_type loc k v in
let mty = map_type ~preds:ctx.env.tvpreds loc k v in
let m = fresh_slot ctx mty in
let attempt =
rt loc (Types.Int Types.I8) "flan_map_init"
@ -4318,6 +4526,30 @@ and named_call ctx ~want loc name args =
printing of one would be its last. *)
let target = List.hd args in
let a = borrowed ctx target (fun () -> check ctx target) in
(* ── The allow-list, and it has exactly two members: [print] and
[println]. ──────────────────────────────────────────────────────
plan.org names [println] as the one compiler-provided exception — it
"selects a structural printer at each concrete instantiation" — and
that cannot be reconciled with an abstract pass as written: a pass that
decides an operator's legality *without* substituting cannot make an
exception for the one operator whose legality is only decidable after
substituting. So the exception is made explicit: these two forms are
*deferred* to instantiation, and every other operator is answered where
it is written.
Every member of this list is a place where a refusal moves from the
definition to a call site, which is the thing the abstract pass exists
to prevent. That is the whole cost of the exception and the reason the
list stays two long and is written down here. There is no [where]
predicate for printability on purpose: every type prints, so the
predicate would always hold and would only be noise on a signature.
The node produced here is a unit no-op, thrown away with the rest of
the abstract pass. The real printer is selected when the copy is
checked with [t] concrete. *)
if generic_ty a.Tast.ty then
mk loc Types.Unit Tast.Unit
else
let bslice = Types.Slice (Types.Int Types.U8) in
let write x = mk loc Types.Unit (Tast.Prim (Tast.WriteStdout, [ x ])) in
let conv pr x = mk loc bslice (Tast.Prim (pr, [ x ])) in
@ -4560,29 +4792,43 @@ and instantiate env loc gname vars subst cparams cret =
fail loc
"%s at these types is called %s, and %s is already defined — rename \
one of them" gname sym sym;
runaway env loc gname cparams;
(* Each instantiation checks the concrete types answer the [where] clause.
This is the half of the feature that only exists per copy: the abstract
pass took the predicates on trust, and here is where the trust is
settled, at the call site that asked, naming it. *)
let fn = Hashtbl.find env.generics gname in
List.iter
(fun (p : Ast.pred) ->
match List.assoc_opt p.Ast.pvar subst with
| None -> ()
| Some t ->
if not (pred_holds p.Ast.pname t) then
Loc.failk "check/predicate-unsatisfied" loc
"%s here would instantiate %s at $%s = %s, and %s is not %s — \
the body of %s is written against {:where (%s $%s)}"
gname gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
p.Ast.pname gname p.Ast.pname p.Ast.pvar)
fn.Ast.fwhere;
(* The entry goes in *before* the body is checked, which is what makes a
recursive generic function terminate: the call to itself at the same
types finds this and does not generate a second copy. *)
if env.depth >= 32 then
fail loc
"%s instantiates itself without end — the copy at (%s) asks for \
another at a larger type, 32 deep and still growing. A generic \
function may call itself, but not at a type built out of its own \
type variable" gname
(String.concat " " (List.map Types.to_string cparams));
cache := (cparams, cret, sym) :: !cache;
Hashtbl.replace env.fns sym (cparams, cret);
let fn = Hashtbl.find env.generics gname in
let saved_subst = env.subst and saved_vars = env.tyvars in
let saved_subst = env.subst and saved_vars = env.tyvars
and saved_preds = env.tvpreds and saved_chain = env.chain in
(* Inside the copy there are no variables left: [resolve_name] answers
[t] with the concrete type, so every node the body produces is as
concrete as one written out by hand. *)
concrete as one written out by hand. The [where] clause goes out of
scope with them — there is nothing abstract left for it to permit, and
every operator is answered by the concrete type it now has. *)
env.subst <- List.map (fun v -> (v, List.assoc v subst)) vars;
env.tyvars <- [];
env.depth <- env.depth + 1;
env.tvpreds <- [];
env.chain <- env.chain @ [ (gname, cparams, loc) ];
let restore () =
env.subst <- saved_subst; env.tyvars <- saved_vars;
env.depth <- env.depth - 1
env.tvpreds <- saved_preds; env.chain <- saved_chain
in
let tfn =
match !check_fn_ref env { fn with Ast.name = sym } with
@ -4871,7 +5117,28 @@ let collect env (decls : Ast.decl list) =
[fns], because nothing can be called at [t]. Every call site turns
it into an ordinary entry. *)
let vars = signature_tyvars fn in
(* The [where] clause is checked against the signature here, once,
rather than at every use of it: a predicate nobody has heard of,
or one about a variable the signature never bound, is a mistake
about this definition and is refused at this definition. *)
List.iter
(fun (p : Ast.pred) ->
if not (List.mem p.Ast.pname predicate_names) then
Loc.failk "check/unknown-predicate" p.Ast.ploc
"%s is not a type predicate. The ones there are: %s"
p.Ast.pname (String.concat ", " predicate_names);
if not (List.mem p.Ast.pvar vars) then
Loc.failk "check/unbound-predicate-variable" p.Ast.ploc
"$%s is not a type variable of %s — a where clause \
constrains the variables the signature binds%s"
p.Ast.pvar fn.Ast.name
(if vars = [] then ", and this signature binds none"
else
", which here are "
^ String.concat ", " (List.map (fun v -> "$" ^ v) vars)))
fn.Ast.fwhere;
env.tyvars <- vars;
env.tvpreds <- fn.Ast.fwhere;
let params =
List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
in
@ -4879,6 +5146,7 @@ let collect env (decls : Ast.decl list) =
match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
in
env.tyvars <- [];
env.tvpreds <- [];
if vars = [] then Hashtbl.replace env.fns fn.Ast.name (params, ret)
else begin
Hashtbl.replace env.generics fn.Ast.name fn;
@ -5050,13 +5318,19 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
(Var _)] is false, but the same variable at [(Vec i32)] is move-only. *)
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 in
let saved_lifted = env.lifted and saved_vars = env.tyvars
and saved_preds = env.tvpreds in
env.tyvars <- vars;
(* What the abstract pass may assume. Every operator the body reaches asks
[env.tvpreds] whether the variable was declared to support it, and every
instantiation asks the concrete type the same question again. *)
env.tvpreds <- fn.Ast.fwhere;
Hashtbl.replace env.fns fn.Ast.name (params, ret);
let finish () =
Hashtbl.remove env.fns fn.Ast.name;
env.lifted <- saved_lifted;
env.tyvars <- saved_vars
env.tyvars <- saved_vars;
env.tvpreds <- saved_preds
in
(match check_fn env fn with
| _ -> finish ()

2
lib/cimport.ml
View File

@ -788,7 +788,7 @@ let of_dump ~env ~taken ~bound_syms ~config (d : dump) : imported =
decls :=
{ Ast.d =
Ast.DeclareC
({ Ast.name = flan; params; ret; fbody = []; nloc = f.cloc },
({ Ast.name = flan; params; ret; fwhere = []; fbody = []; nloc = f.cloc },
f.csym);
dloc = f.cloc }
:: !decls)

81
lib/parse.ml
View File

@ -93,6 +93,76 @@ let rec fields (f : Form.t) (items : Form.t list) : Ast.field list =
Loc.fail odd.loc "field %s has no type — these come in name/type pairs"
(Form.to_string odd)
(* ── The constraint map at the head of a defn body ──────────────────────
[(defn sort! [s [$t]] () {:where (ordered? $t)} body ...)]. Clojure's
[{:pre [...] :post [...]}] is the precedent and the reason it is a map
rather than a bare keyword: it leaves room for further keys without new
syntax.
**The disambiguation, since it is the one syntax question the feature had
to settle.** [{K V}] is a legal *return type* spelling for [(Map K V)], so
[(defn f [xs [$t]] {string i32} {:where ...} body)] puts two braces in a
row meaning different things. They are told apart structurally, by the
first form inside: a constraint map leads with a *keyword*, and a map type
leads with a type — [{string i32}], [{K V}] — and a keyword is not a type
anywhere in the language. So [Map ({v = Kw _} :: _)] in the slot after the
return type is a constraint map and nothing else can be. The return-type
slot itself is never ambiguous: [Parse] takes it unconditionally, before
this is consulted. [{K V}] stays exactly as it was — whether it survives is
a separate open question, and this feature does not force it.
A bare [{}] in *expression* position is already refused ([expr] below), so
there is also nothing for a constraint map to be confused with once past
the return type. *)
let constraints (body : Form.t list) : Ast.pred list * Form.t list =
match body with
| ({ Form.v = Form.Map (({ Form.v = Form.Kw _; _ } :: _ as kvs)); _ } as m)
:: rest ->
let pred (p : Form.t) =
match p.Form.v with
(* [$t] at a predicate, not bare [t]: the clause talks about the
variable the signature *bound*, and writing it the way the signature
wrote it is the one spelling that cannot be read as a concrete type
that happens to share the name. *)
| Form.List [ { Form.v = Form.Sym name; _ };
{ Form.v = Form.Sym v; loc = vloc } ]
when String.length v > 1 && v.[0] = '$' ->
ignore vloc;
{ Ast.pname = name; pvar = String.sub v 1 (String.length v - 1);
ploc = p.Form.loc }
| _ ->
Loc.fail p.Form.loc
"a where predicate is (name? $t), one predicate about one type \
variable — found %s" (Form.to_string p)
in
let rec keys = function
| [] -> []
| { Form.v = Form.Kw "where"; _ } :: v :: rest ->
(match v.Form.v with
(* A vector, because two predicates on one variable is the ordinary
case — [{:where [(ordered? $t) (copyable? $t)]}] is what a
comparing generic that also reads its parameter twice needs. One
predicate on its own is accepted unwrapped, which is the same
sugar [:pre] does not have and is worth the line it costs. *)
| Form.Vec ps -> List.map pred ps
| _ -> [ pred v ])
@ keys rest
| { Form.v = Form.Kw k; loc } :: _ :: rest ->
Loc.fail loc
"%s is not a key a defn's constraint map takes; :where is the only \
one" (":" ^ k)
|> fun () -> keys rest
| odd :: _ ->
Loc.fail odd.Form.loc
"a constraint map is keyword/value pairs — found %s"
(Form.to_string odd)
in
if List.length kvs mod 2 <> 0 then
Loc.fail m.Form.loc "a constraint map is keyword/value pairs, and this \
one has an odd number of forms";
(keys kvs, rest)
| _ -> ([], body)
(* ── Expressions ───────────────────────────────────────────────────── *)
let rec expr (f : Form.t) : Ast.expr =
@ -782,8 +852,9 @@ let rec decl (f : Form.t) : Ast.decl =
"%s. This is the return type, which every defn states -- a \
function that returns nothing writes ()" msg
in
let fwhere, body = constraints body in
mk (Ast.Defn { Ast.name = sym n; params = fields f ps;
ret = Some rty; fbody = body_of body;
ret = Some rty; fwhere; fbody = body_of body;
nloc = n.loc })
| _ ->
fail f
@ -814,10 +885,11 @@ let rec decl (f : Form.t) : Ast.decl =
(match List.rev rest with
| [ n; { v = Form.Vec ps; _ } ] ->
mk (mkd { Ast.name = sym n; params = fields f ps;
ret = None; fbody = []; nloc = n.loc } csym)
ret = None; fwhere = []; fbody = []; nloc = n.loc } csym)
| [ n; { v = Form.Vec ps; _ }; r ] ->
mk (mkd { Ast.name = sym n; params = fields f ps;
ret = Some (texpr r); fbody = []; nloc = n.loc } csym)
ret = Some (texpr r); fwhere = []; fbody = [];
nloc = n.loc } csym)
| _ -> fail f "%s" usage)
| _ -> fail f "%s" usage)
@ -873,7 +945,8 @@ let rec decl (f : Form.t) : Ast.decl =
params = [ { Ast.fname = sym p;
fty = { Ast.t = Ast.Tslice form_t; tloc = p.loc };
floc = p.loc } ];
ret = Some form_t; fbody = body_of body; nloc = n.loc })
ret = Some form_t; fwhere = []; fbody = body_of body;
nloc = n.loc })
| _ :: { v = Form.Vec ps; _ } :: body when body <> [] ->
List.iter (fun (p : Form.t) -> ignore (sym p)) ps;
fail f

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

@ -3,6 +3,7 @@
;; 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))
@ -14,6 +15,7 @@
(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))))