enum? admits exactly the enums, entails ordered? and equal?, and licenses a generic conversion from an enum to a number beside numeric?
This commit is contained in:
parent
58d1e35225
commit
b8c81d94ee
8
TODO.org
8
TODO.org
@ -680,14 +680,6 @@ A machine-type target needs =numeric?=; an enum target needs =integer?=;
|
||||
by what it claims, not by the set it happens to denote this week — which is why
|
||||
=ordered?= is refused even though every type it admits today converts.
|
||||
|
||||
** NEXT There is now no generic enum to integer conversion
|
||||
Decided 2026-09-25: build =enum?= as described.
|
||||
Recorded as a loss. The one spelling that worked did so by not asking about the
|
||||
operand at all, so removing it was still right. =enum?= is the eventual answer —
|
||||
it would entail =ordered?= and =equal?= and not =numeric?=, so the cast rule
|
||||
becomes a disjunction and the refusal has to name whichever the reader meant. Each
|
||||
part of that is a decision and the author has not been asked.
|
||||
|
||||
** DONE The Ptr and union arms of the fill boundary are relaxable
|
||||
CLOSED: [2026-09-25]
|
||||
A =Ptr= may be byte-filled, and an untagged union is filled over its whole
|
||||
|
||||
53
lib/check.ml
53
lib/check.ml
@ -873,18 +873,24 @@ let no_such_rand name =
|
||||
|
||||
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. There is no [copyable?] any more and no Odin counterpart
|
||||
these six. There is no [copyable?] any more and no Odin counterpart
|
||||
either: Odin has no move semantics, and since the repeal neither does this
|
||||
language, so [$T] never has to answer the question.
|
||||
|
||||
[integer?] is the narrowest of the five and exists because [numeric?] was
|
||||
[integer?] is the narrowest numeric bound and exists because [numeric?] was
|
||||
one type too wide for a family of bodies: an integer body under [numeric?]
|
||||
is instantiated at f32 and f64 too, and (if (< x 0) (- 0 x) x) at -0.0 is
|
||||
the wrong abs while %, the bitwise operators and the shifts have no float
|
||||
meaning at all. A function that can be generalized should not need a
|
||||
variant per numeric type, and [integer?] is what lets the integer-only
|
||||
ones say exactly what they need. *)
|
||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "integer?" ]
|
||||
ones say exactly what they need.
|
||||
|
||||
[enum?] admits exactly the enums. It entails [ordered?] and [equal?] and
|
||||
not [numeric?]: an enum compares, and it converts to a number, but it is
|
||||
not one — no arithmetic, no literal. It is what licenses the generic
|
||||
enum-to-number conversion, beside [numeric?]. *)
|
||||
let predicate_names =
|
||||
[ "ordered?"; "equal?"; "hashable?"; "numeric?"; "integer?"; "enum?" ]
|
||||
|
||||
(* ── What a type owns, transitively ────────────────────────────────────
|
||||
The one structural ownership question that survived the repeal, because it
|
||||
@ -1023,6 +1029,7 @@ let pred_holds p (t : Types.t) =
|
||||
| "hashable?" -> Types.keyable t
|
||||
| "numeric?" -> Types.is_numeric t
|
||||
| "integer?" -> Types.is_integer t
|
||||
| "enum?" -> (match t with Types.Enum _ -> true | _ -> false)
|
||||
| _ -> false
|
||||
|
||||
(* What one declared predicate *also* gives you. These are entailments over
|
||||
@ -1035,8 +1042,8 @@ let pred_holds p (t : Types.t) =
|
||||
let pred_entails ~declared ~wanted =
|
||||
String.equal declared wanted
|
||||
|| match wanted, declared with
|
||||
| "ordered?", ("numeric?" | "integer?") -> true
|
||||
| "equal?", ("numeric?" | "ordered?" | "integer?") -> true
|
||||
| "ordered?", ("numeric?" | "integer?" | "enum?") -> true
|
||||
| "equal?", ("numeric?" | "ordered?" | "integer?" | "enum?") -> true
|
||||
(* Every integer type is a number, so [integer?] gives a body everything
|
||||
[numeric?] does — the arithmetic, the written 0, the untyped integer
|
||||
literal — on top of the operations only it admits. The reverse is
|
||||
@ -7709,9 +7716,16 @@ and not_numeric name what (a : Tast.expr) =
|
||||
so that the family says it one way: a body with no clause is given the
|
||||
whole clause, and a body that already has one is told which predicate to
|
||||
add rather than a clause that would drop the ones it has. *)
|
||||
and cast_operand ctx loc name ~needs ~what ~is v =
|
||||
if declares ctx.env.tvpreds v needs then ()
|
||||
and cast_operand ctx loc name ~needs ?also ~what ~is v =
|
||||
if declares ctx.env.tvpreds v needs
|
||||
|| (match also with
|
||||
| Some (p, _) -> declares ctx.env.tvpreds v p
|
||||
| None -> false)
|
||||
then ()
|
||||
else
|
||||
(* A conversion two bounds license is refused naming both, since which one
|
||||
the reader meant is theirs to say. *)
|
||||
let is = match also with Some (_, is') -> is ^ " or " ^ is' | None -> is in
|
||||
let declared =
|
||||
List.filter_map
|
||||
(fun (p : Ast.pred) ->
|
||||
@ -7727,10 +7741,19 @@ and cast_operand ctx loc name ~needs ~what ~is v =
|
||||
(String.concat " and " ps) is
|
||||
in
|
||||
let fix =
|
||||
let alt clause =
|
||||
match also with
|
||||
| Some (p, is') ->
|
||||
Printf.sprintf ", or %s for %s"
|
||||
(Printf.sprintf clause p v) is'
|
||||
| None -> ""
|
||||
in
|
||||
if ctx.env.tvpreds = [] then
|
||||
Printf.sprintf "write {:where (%s $%s)} at the head of the body"
|
||||
needs v
|
||||
else Printf.sprintf "add (%s $%s) to the where clause" needs v
|
||||
Printf.sprintf "write {:where (%s $%s)} at the head of the body%s"
|
||||
needs v (alt "{:where (%s $%s)}")
|
||||
else
|
||||
Printf.sprintf "add (%s $%s) to the where clause%s" needs v
|
||||
(alt "(%s $%s)")
|
||||
in
|
||||
Loc.failk "check/unconstrained-type-variable" loc
|
||||
"%s converts %s. %s — %s" name what known fix
|
||||
@ -10587,8 +10610,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
[ordered?] admits a type that does not, and that day is why the
|
||||
question is asked of the predicate and not of the set it denotes. *)
|
||||
| Types.Var v ->
|
||||
cast_operand ctx loc name ~needs:"numeric?" ~what:"a number"
|
||||
~is:"a number" v
|
||||
cast_operand ctx loc name ~needs:"numeric?" ~also:("enum?", "an enum")
|
||||
~what:"a number or an enum" ~is:"a number" v
|
||||
| t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
|
||||
prim (Tast.Cast target) target [ a ]
|
||||
| _ when is_cast name && List.length args = 1 ->
|
||||
@ -10619,8 +10642,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
||||
machine type, so what is in question is only the operand, and the
|
||||
[where] clause is what answers it. *)
|
||||
| Types.Var v ->
|
||||
cast_operand ctx loc name ~needs:"numeric?" ~what:"a number"
|
||||
~is:"a number" v
|
||||
cast_operand ctx loc name ~needs:"numeric?" ~also:("enum?", "an enum")
|
||||
~what:"a number or an enum" ~is:"a number" v
|
||||
| t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
|
||||
(match a.Tast.ty with
|
||||
| Types.Dyn -> cast_dyn ctx loc target a
|
||||
|
||||
11
plan.org
11
plan.org
@ -248,11 +248,12 @@ and on a managed ~class~ instance. An ordinary ~struct~ never carries one.
|
||||
already refused so nothing else it could be. ~sort~ declares ~ordered?~ of its
|
||||
variable, the abstract pass then allows ~<~ in the body, and each instantiation
|
||||
checks the concrete type satisfies the predicate and refuses the call site if it
|
||||
does not. There are *five* predicates — ~ordered?~, ~equal?~, ~hashable?~,
|
||||
~numeric?~, ~integer?~ — against Odin's forty-one, and they entail one another
|
||||
in one direction, so one clause usually does: ~integer?~ gives ~numeric?~,
|
||||
~numeric?~ gives ~ordered?~, and ~ordered?~ gives ~equal?~. ~integer?~ exists
|
||||
because ~numeric?~ admits floats.
|
||||
does not. There are *six* predicates — ~ordered?~, ~equal?~, ~hashable?~,
|
||||
~numeric?~, ~integer?~, ~enum?~ — against Odin's forty-one, and they entail one
|
||||
another in one direction, so one clause usually does: ~integer?~ gives
|
||||
~numeric?~, ~numeric?~ gives ~ordered?~, and ~ordered?~ gives ~equal?~.
|
||||
~integer?~ exists because ~numeric?~ admits floats. ~enum?~ gives ~ordered?~
|
||||
and a conversion to a number, and not arithmetic.
|
||||
~hashable?~ is what lets a variable *key a map*: without it the type
|
||||
~(Map $t i32)~ is refused where it is written, and with it the refusal moves to
|
||||
the call site that names an unhashable key.
|
||||
|
||||
@ -268,12 +268,14 @@ instantiates it:
|
||||
> field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
|
||||
|
||||
What makes that liveable is a `where` clause of compile-time type predicates,
|
||||
written as a map at the head of the body. There are five — `ordered?`,
|
||||
`equal?`, `hashable?`, `numeric?`, `integer?` — they are not type classes
|
||||
written as a map at the head of the body. There are six — `ordered?`,
|
||||
`equal?`, `hashable?`, `numeric?`, `integer?`, `enum?` — they are not type classes
|
||||
because a predicate carries no implementations and merely gates a builtin the
|
||||
compiler already has, and they entail one another in one direction, so one
|
||||
clause usually does: `integer?` admits every integer kind and no float, and
|
||||
entails `numeric?`, which entails `ordered?`, which entails `equal?`.
|
||||
`enum?` admits exactly the enums and entails `ordered?` and `equal?`, not
|
||||
`numeric?`.
|
||||
`integer?` is what admits the bitwise operators, the shifts and an
|
||||
integer-only body like `abs`'s — under `numeric?` those bodies would be
|
||||
instantiated at the floats too (TODO.org, "abs is one generic, and a bound joins
|
||||
@ -354,14 +356,14 @@ where the type is written, so neither is refused at the variable. A conversion
|
||||
was never a claim that the value survives. The conversion *to* an enum needs
|
||||
`integer?` exactly, because an enum is an `i32` and a float has no enum
|
||||
reading, and `numeric?` would admit an `f32` copy the concrete rule refuses.
|
||||
The conversion *from* an enum to a number needs `enum?` or `numeric?`, and
|
||||
its refusal names both.
|
||||
`ordered?`, `equal?` and `hashable?` admit no conversion at all: they say what
|
||||
can be compared or keyed, not what is a number — and that is a claim about
|
||||
what the predicate says, not about the set it denotes today, which currently
|
||||
does admit only numbers and enums. The refusal names the predicate to write
|
||||
(TODO.org, "A conversion is legal at a bounded variable when it is legal at every
|
||||
type the bound admits"). One consequence is recorded as open: no predicate now
|
||||
licenses a generic enum → integer conversion (TODO.org, "There is now no generic
|
||||
enum to integer conversion").
|
||||
type the bound admits").
|
||||
|
||||
**A type variable is not instantiated at `dyn`.** Two models answer "one body,
|
||||
many types" and they are not rivals: this one copies per written type at
|
||||
|
||||
28
test/programs/enum-generic.flan
Normal file
28
test/programs/enum-generic.flan
Normal file
@ -0,0 +1,28 @@
|
||||
;;;; A generic conversion from an enum, licensed by {:where (enum? $t)}. enum?
|
||||
;;;; admits exactly the enums and entails ordered? and equal?, so a body under
|
||||
;;;; it may convert, compare and test for equality, at any enum.
|
||||
|
||||
(defenum Color [red green blue])
|
||||
(defenum Size [small 10 large 20])
|
||||
|
||||
(defn code [x $t] i32
|
||||
{:where (enum? $t)}
|
||||
(i32 x))
|
||||
|
||||
(defn later? [a $t b $t] bool
|
||||
{:where (enum? $t)}
|
||||
(> a b))
|
||||
|
||||
(defn same? [a $t b $t] bool
|
||||
{:where (enum? $t)}
|
||||
(and (= a b) (<= a b)))
|
||||
|
||||
(defn main [] i32
|
||||
(let [c (Color 2)
|
||||
s (Size 20)]
|
||||
(println (code c)) ; 2
|
||||
(println (code s)) ; 20
|
||||
(println (later? c (Color 0))) ; true
|
||||
(println (same? (Color 1) (Color 1))) ; true
|
||||
(println (f64 (code s)))) ; 20
|
||||
0)
|
||||
@ -4171,6 +4171,11 @@ level "1"
|
||||
lo\nmid\nhi\nother\n"
|
||||
in
|
||||
outputs "enum conversion" "programs/enum-convert.flan" enum_conv_out;
|
||||
(* The generic enum-to-number conversion enum? licenses. *)
|
||||
outputs "a generic enum conversion" "programs/enum-generic.flan"
|
||||
"2\n20\ntrue\ntrue\n20\n";
|
||||
outputs ~x86:true "a generic enum conversion, --x86"
|
||||
"programs/enum-generic.flan" "2\n20\ntrue\ntrue\n20\n";
|
||||
outputs ~opt:"-O0" "enum conversion, -O0" "programs/enum-convert.flan"
|
||||
enum_conv_out;
|
||||
|
||||
|
||||
@ -6171,7 +6171,8 @@ let () =
|
||||
and the message says which predicate to write. *)
|
||||
rejects_check "ordered? does not admit a conversion"
|
||||
~needle:"The where clause says t is ordered?, and that does not make it \
|
||||
a number — add (numeric? $t) to the where clause"
|
||||
a number or an enum — add (numeric? $t) to the where clause, or \
|
||||
(enum? $t) for an enum"
|
||||
"(defn to32 [x $t] i32 {:where (ordered? $t)} (i32 x))";
|
||||
rejects_check "nor does equal?"
|
||||
~needle:"add (numeric? $t) to the where clause"
|
||||
@ -6182,9 +6183,28 @@ let () =
|
||||
(* With no clause at all the message hands over the whole clause rather
|
||||
than a predicate to add to one that is not there. *)
|
||||
rejects_check "an unbounded variable does not convert"
|
||||
~needle:"i32 converts a number. Nothing here says t is a number — write \
|
||||
{:where (numeric? $t)} at the head of the body"
|
||||
~needle:"i32 converts a number or an enum. Nothing here says t is a \
|
||||
number or an enum — write {:where (numeric? $t)} at the head of \
|
||||
the body, or {:where (enum? $t)} for an enum"
|
||||
"(defn to32 [x $t] i32 (i32 x))";
|
||||
(* enum? is the other bound a conversion to a number takes: it admits the
|
||||
enums, which convert as an i32, and entails ordered? and equal? but not
|
||||
numeric?. The running side is programs/enum-generic.flan. *)
|
||||
accepts "enum? admits the conversion from an enum"
|
||||
"(defn code [x $t] i32 {:where (enum? $t)} (i32 x))";
|
||||
accepts "and compares, being ordered? and equal?"
|
||||
"(defn later? [a $t b $t] bool {:where (enum? $t)} (and (> a b) (= a b)))";
|
||||
rejects_check "but is not a number"
|
||||
~needle:"$t"
|
||||
"(defn sum [a $t b $t] $t {:where (enum? $t)} (+ a b))";
|
||||
rejects_check "and admits no integer at the call"
|
||||
~needle:"i32 is not enum?"
|
||||
"(defn code [x $t] i32 {:where (enum? $t)} (i32 x))\n\
|
||||
(defn f [] i32 (code (i32 3)))";
|
||||
rejects_check "nor the conversion to an enum, which needs an integer"
|
||||
~needle:"add (integer? $t) to the where clause"
|
||||
"(defenum K [lo -1 hi 1])\n\
|
||||
(defn as-k [n $t] K {:where (enum? $t)} (K n))";
|
||||
(* The operand of a cast to a *variable* target is asked the same question
|
||||
the target was: the target's bound says nothing about a second variable
|
||||
standing in the argument. *)
|
||||
|
||||
@ -1275,13 +1275,14 @@ $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
|
||||
map at the head of the body — <code>{:where (ordered? $t)}</code>, or a vector when
|
||||
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 six predicates, and each gates builtins the compiler already has:</p>
|
||||
|
||||
<div class="scroll">
|
||||
<table>
|
||||
<tr><th>Predicate</th><th>What it admits</th></tr>
|
||||
<tr><td><code>integer?</code></td><td><code>bit-and</code> <code>bit-or</code> <code>bit-xor</code> <code><<</code> <code>>></code> — every integer type, no float</td></tr>
|
||||
<tr><td><code>numeric?</code></td><td><code>+</code> <code>-</code> <code>*</code> <code>/</code> <code>%</code>, and a cast <code>(t x)</code></td></tr>
|
||||
<tr><td><code>enum?</code></td><td>a cast to a number, <code>(i32 x)</code> — every enum type</td></tr>
|
||||
<tr><td><code>ordered?</code></td><td><code><</code> <code><=</code> <code>></code> <code>>=</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>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>
|
||||
@ -1290,7 +1291,8 @@ are five predicates, and each gates builtins the compiler already has:</p>
|
||||
|
||||
<p>They entail each other in one direction, so one clause usually does:
|
||||
<code>integer?</code> gives <code>numeric?</code>, <code>numeric?</code> gives
|
||||
<code>ordered?</code>, and <code>ordered?</code> gives <code>equal?</code>. A
|
||||
<code>ordered?</code>, and <code>ordered?</code> gives <code>equal?</code>;
|
||||
<code>enum?</code> gives <code>ordered?</code> too. A
|
||||
<code>sort</code> that compares its elements declares <code>ordered?</code> and
|
||||
nothing else, and the prelude's <code>abs</code> declares <code>integer?</code>
|
||||
alone — the bound is what keeps its integer body away from the floats, whose
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user