From 7f86f32699c9f24efd2bfe33ca65335bb49cf174 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 14:33:45 +0700 Subject: [PATCH] where predicates admit operators, and a type variable is move-only until it says otherwise 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. --- lib/ast.ml | 11 + lib/check.ml | 374 +++++++++++++++++++++++++---- lib/cimport.ml | 2 +- lib/parse.ml | 81 ++++++- spike/generics/prelude-shapes.flan | 2 + 5 files changed, 415 insertions(+), 55 deletions(-) diff --git a/lib/ast.ml b/lib/ast.ml index e90b2d3..4359b7f 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -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; } diff --git a/lib/check.ml b/lib/check.ml index 00a4c1a..305b1d8 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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 () diff --git a/lib/cimport.ml b/lib/cimport.ml index faee6fd..a3fede3 100644 --- a/lib/cimport.ml +++ b/lib/cimport.ml @@ -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) diff --git a/lib/parse.ml b/lib/parse.ml index 6530821..44020fb 100644 --- a/lib/parse.ml +++ b/lib/parse.ml @@ -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 diff --git a/spike/generics/prelude-shapes.flan b/spike/generics/prelude-shapes.flan index b17b777..a53425e 100644 --- a/spike/generics/prelude-shapes.flan +++ b/spike/generics/prelude-shapes.flan @@ -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))))