A generic sort takes its comparison as a value, and an operator over a variable is refused
This commit is contained in:
parent
cb56fc14b1
commit
50798aac89
57
lib/check.ml
57
lib/check.ml
@ -722,6 +722,22 @@ let rec generic_ty (t : Types.t) =
|
||||
| Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
|
||||
| _ -> false
|
||||
|
||||
(* The refusal plan.org's Types section asks for, in one place so that every
|
||||
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) =
|
||||
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)
|
||||
|
||||
(* 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
|
||||
generated name reads like the handwritten one it replaces, which is what a
|
||||
@ -2691,6 +2707,7 @@ 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
|
||||
fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
|
||||
let ty = a.Tast.ty in
|
||||
@ -3011,6 +3028,7 @@ 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
|
||||
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
|
||||
prim Tast.Rem a.Tast.ty [ a; b ]
|
||||
@ -3030,6 +3048,7 @@ 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
|
||||
fail loc
|
||||
"%s compares machine numbers; %s has no built-in comparison \
|
||||
@ -4455,19 +4474,26 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
mentions a variable — there is nothing to expect until the argument has
|
||||
said what it is. So an untyped literal falls to its own default and
|
||||
[(id 3)] instantiates at i32, which is the one place inference at a
|
||||
generic call site is weaker than at a monomorphic one. *)
|
||||
generic call site is weaker than at a monomorphic one.
|
||||
|
||||
A variable already bound by an earlier argument is substituted back into
|
||||
the parameters still to come, so [(sort-by! (slice ns 0 4) (fn [a b] (< a
|
||||
b)))] works: by the time the [fn] is reached, [(Fn [$t $t] bool)] has
|
||||
become [(Fn [i32 i32] bool)] and the literal has the position it needs to
|
||||
take its types from. Left to right, which is the order Odin's operands
|
||||
are gathered in and the order [map2_lr] already guarantees. *)
|
||||
let subst = ref [] in
|
||||
let targs =
|
||||
map2_lr
|
||||
(fun p a -> if generic_ty p then check ctx a else check ctx ~want:p a)
|
||||
(fun p a ->
|
||||
let p = subst_ty !subst p in
|
||||
let a = if generic_ty p then check ctx a else check ctx ~want:p a in
|
||||
if not (bind_ty subst p a.Tast.ty) then
|
||||
fail a.Tast.loc "%s expects %s here, found %s" name
|
||||
(Types.to_string p) (Types.to_string a.Tast.ty);
|
||||
a)
|
||||
pats args
|
||||
in
|
||||
let subst = ref [] in
|
||||
List.iter2
|
||||
(fun p (a : Tast.expr) ->
|
||||
if not (bind_ty subst p a.Tast.ty) then
|
||||
fail a.Tast.loc "%s expects %s here, found %s" name
|
||||
(Types.to_string p) (Types.to_string a.Tast.ty))
|
||||
pats targs;
|
||||
(* Every variable has to be determined by an argument. A return-only
|
||||
variable has nothing to bind it — there is no explicit instantiation
|
||||
syntax by design (plan.org) — so it is refused here, where the signature
|
||||
@ -4482,8 +4508,17 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
vars;
|
||||
let cparams = List.map (subst_ty !subst) pats in
|
||||
let cret = subst_ty !subst pret in
|
||||
let sym = instantiate ctx.env loc name vars !subst cparams cret in
|
||||
expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
|
||||
if List.exists generic_ty cparams || generic_ty cret then
|
||||
(* One generic function calling another at its *own* variable, seen from
|
||||
the abstract pass over the caller's body — [sort-by!] calling [swap!]
|
||||
at [t]. There is no copy to make yet: [t] is not a type. The node is
|
||||
built so the call still type-checks and is thrown away with the rest of
|
||||
the abstract pass; the real copy is generated when the caller is
|
||||
instantiated and the same call site resolves [t] to a concrete type. *)
|
||||
expect loc ~want (mk loc cret (Tast.Call (name, targs)))
|
||||
else
|
||||
let sym = instantiate ctx.env loc name vars !subst cparams cret in
|
||||
expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
|
||||
|
||||
(* Cache or generate, Odin's loop. The key is the whole concrete signature
|
||||
compared pairwise with [Types.equal] — [are_types_identical] — so calling
|
||||
|
||||
4
spike/generics/reject.flan
Normal file
4
spike/generics/reject.flan
Normal file
@ -0,0 +1,4 @@
|
||||
(defn add2 [a $t b $t] t (+ a b))
|
||||
|
||||
(defn main [] ()
|
||||
(println (add2 1 2)))
|
||||
25
spike/generics/sort.flan
Normal file
25
spike/generics/sort.flan
Normal file
@ -0,0 +1,25 @@
|
||||
;; The shape prelude.ml's sort-i32-by! / sort-f32-by! pair would collapse into:
|
||||
;; one generic body, the comparison passed in as a function value because an
|
||||
;; unconstrained type variable has no < of its own.
|
||||
|
||||
(defn swap! [xs [$t] i i32 j i32] ()
|
||||
(let [tmp (at xs i)]
|
||||
(set (at xs i) (at xs j))
|
||||
(set (at xs j) tmp)))
|
||||
|
||||
(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
|
||||
(let [i 1]
|
||||
(while (< i (len s))
|
||||
(let [j i]
|
||||
(while (and (> j 0) (before? (at s j) (at s (- j 1))))
|
||||
(swap! s (- j 1) j)
|
||||
(set j (- j 1))))
|
||||
(set i (+ i 1)))))
|
||||
|
||||
(defn main [] ()
|
||||
(let [ns [5 3 9 1]
|
||||
fs [2.5 0.5 1.5]]
|
||||
(sort-by! (slice ns 0 4) (fn [a b] (< a b)))
|
||||
(sort-by! (slice fs 0 3) (fn [a b] (> a b)))
|
||||
(dotimes [i 4] (println (at ns i)))
|
||||
(dotimes [i 3] (println (at fs i)))))
|
||||
19
spike/generics/swap.flan
Normal file
19
spike/generics/swap.flan
Normal file
@ -0,0 +1,19 @@
|
||||
;; One generic function over one type variable, called at two concrete types
|
||||
;; in one program. The sigil binds ($t), a bare use reads it (t).
|
||||
|
||||
(defn swap! [xs [$t] i i32 j i32] ()
|
||||
(let [tmp (at xs i)]
|
||||
(set (at xs i) (at xs j))
|
||||
(set (at xs j) tmp)))
|
||||
|
||||
(defn main [] ()
|
||||
(let [ns [10 20 30]
|
||||
fs [1.5 2.5 3.5]]
|
||||
(swap! (slice ns 0 3) 0 2)
|
||||
(swap! (slice fs 0 3) 0 1)
|
||||
(swap! (slice ns 0 3) 1 2)
|
||||
(println (at ns 0))
|
||||
(println (at ns 1))
|
||||
(println (at ns 2))
|
||||
(println (at fs 0))
|
||||
(println (at fs 1))))
|
||||
Loading…
x
Reference in New Issue
Block a user