The two specs catch up with generics and with the conditions the runtime signals
spec-memory.md's generics section still said there were no constraints and wrote its type variable as a bare lowercase name, which is the spelling the $t sigil replaced -- the largest example in it would not have compiled. The where clause and the five predicates are plan.org's account and this now agrees with it rather than contradicting it. The empty-map example named no types and used defvar, neither of which is how map-new is called. spec-conditions.md named BoundsError once and nothing else. The four conditions the runtime signals, and the split between the two that establish a retry and the two that deliberately establish nothing, belong in \xc2\xa75 because that is the section whose account of restarts the split could have falsified. It does not: the rule is that the restart a bad index wants is the one the program already had.
This commit is contained in:
parent
00163bcf34
commit
daee402026
@ -139,6 +139,31 @@ non-idempotent mutation bites. §3's rule that every clause body and the body
|
||||
share a type places the restart syntactically; nothing places it *semantically*,
|
||||
and that choice is the author's.
|
||||
|
||||
**Which of the runtime's own conditions establish a restart, and why only some
|
||||
do.** Four are signalled from below the program with `error`: `StorageExhausted`
|
||||
when an allocator cannot satisfy a request, `FileError` when a file operation
|
||||
fails, `BoundsError` for an index or a slice outside its container, and
|
||||
`ArithError` for an arithmetic operation that has no answer — a divide or
|
||||
remainder by zero, `INT64_MIN / -1`, and a float-to-integer cast whose value does
|
||||
not fit, each of which was a raw `SIGFPE` or an undefined result before it was a
|
||||
condition. The first two establish a `retry` restart at the failing site, because
|
||||
their attempt is repeatable: a handler frees something or supplies another path
|
||||
and the same operation then succeeds. The last two establish **nothing**, and
|
||||
that is a decision rather than an omission. Nothing a handler can do makes index
|
||||
51 valid for a length-50 array or makes a division by zero have a quotient, so
|
||||
there is no attempt to resume into. A site restart would also have to be
|
||||
allocated by the `restart-case` that offers it, on its own stack (§3), which
|
||||
means an `alloca` and a push/pop pair emitted at every indexing and every
|
||||
division in every checked build — and what it would buy is a *different* answer,
|
||||
silently.
|
||||
|
||||
So the rule this section describes is unchanged by them: the restarts that matter
|
||||
for a bad index or a bad division are the ones the program already established —
|
||||
a frame loop's `continue` — and those are on the restart stack and reachable from
|
||||
a handler or from the break loop without anything being pushed at the failing
|
||||
site. Allocation and file failure are the named exceptions, and spec-memory.md's
|
||||
"Allocation failure" says why they have to be.
|
||||
|
||||
## 6. Crossing compiler-generated frames
|
||||
|
||||
Transfer is lowered **explicitly** — result propagation plus branch targets — not
|
||||
|
||||
@ -38,12 +38,16 @@ enums, strings, fixed arrays, and value structs composed recursively from those
|
||||
types. Tuples and triples join that set when they are introduced. `Ptr`, slices,
|
||||
`Vec`, and `Map` are not map keys yet.
|
||||
|
||||
Equality and hashing for those keys are compiler-provided structural operations,
|
||||
not type classes and not operations available to an unconstrained type variable.
|
||||
An empty map takes its type from its context:
|
||||
Equality and hashing for those keys are compiler-provided structural operations
|
||||
and not type classes. They are not available to an unconstrained type variable
|
||||
either; a variable that means to key a map declares `hashable?` in the signature
|
||||
that binds it, and the refusal then lands at the call site that names an
|
||||
unhashable key. An empty map names its key and value types, because a global
|
||||
cannot hold one and there is therefore no declaration for it to take a type from:
|
||||
|
||||
```
|
||||
(defvar enemies (Map string Enemy) (map-new))
|
||||
(let [enemies (map-new string Enemy)]
|
||||
...)
|
||||
```
|
||||
|
||||
`(get m k)` returns `(Option V)`: absence is `None`, not an untyped `nil`.
|
||||
@ -128,26 +132,48 @@ visible in the type:
|
||||
|
||||
## Generics
|
||||
|
||||
Parametric polymorphism is monomorphisation, with **no type classes and no
|
||||
constraints**. The consequence is a hard rule:
|
||||
Parametric polymorphism is monomorphisation, with **no type classes**. A type
|
||||
variable is written `$t` wherever a *type* goes — a parameter, the return type,
|
||||
or nested as `[$t]` or `(Vec $t)` — and bare `t` where a type's *name* is an
|
||||
argument in expression position, as in `(vec-new t)` and the cast `(t x)`. A
|
||||
generic body is checked **abstractly**, with nothing substituted, so the rule
|
||||
below bites at the definition rather than at whichever call site first
|
||||
instantiates it:
|
||||
|
||||
> A type variable `a` supports only what every type supports: move, `clone`,
|
||||
> A type variable `$t` supports only what every type supports: move, `clone`,
|
||||
> field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
|
||||
|
||||
Anything else is passed in explicitly as a function value:
|
||||
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?`, `copyable?` — 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. A variable is move-only by default and `copyable?` is the opt-out, because
|
||||
whether a variable moves is not decidable abstractly. plan.org's Types section
|
||||
has the full account.
|
||||
|
||||
```
|
||||
(defn largest [xs [a] gt (Fn [a a] bool)] (Option a) ...)
|
||||
(defn sort! [s [$t]] ()
|
||||
{:where (ordered? $t)}
|
||||
...)
|
||||
```
|
||||
|
||||
Ordered/arithmetic operators over `a` are therefore rejected, not silently
|
||||
instantiated. The alternatives — compile-time interfaces, or intrinsics
|
||||
restricted to primitives — are deliberately deferred until the base checker is
|
||||
stable (build sequence milestone 4).
|
||||
Without such a clause the operator is rejected where it is written, not silently
|
||||
instantiated, and the operation is passed in explicitly as a function value
|
||||
instead:
|
||||
|
||||
```
|
||||
(defn largest [xs [$t] gt (Fn [$t $t] bool)] (Option $t) ...)
|
||||
```
|
||||
|
||||
The alternatives to predicates — compile-time interfaces, or intrinsics
|
||||
restricted to primitives — remain deliberately deferred until the base checker is
|
||||
stable (build sequence milestone 4). The ceiling is that nobody can supply a
|
||||
user-defined `<`.
|
||||
|
||||
`println` is the deliberate exception. It is a compiler-provided,
|
||||
type-directed intrinsic: monomorphisation selects or emits a structural printer
|
||||
for each concrete instantiation, so `(println x)` is legal for `x : a` without
|
||||
for each concrete instantiation, so `(println x)` is legal for `x : $t` without
|
||||
introducing a `Printable` type class. Structs, fixed arrays, options and,
|
||||
eventually, Vecs and Maps print structurally. `Ptr` and `Handle` print their
|
||||
address or identity rather than recursively dereferencing, and collection
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user