diff --git a/README.md b/README.md index 474adb6..686ff7b 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ Concretely, that rules out a few things that would otherwise be tempting: pages the compiler generates rather than a list maintained here. - No examples written here. The playground's are the compiler's corpus at the pinned tag, and the summary under each one is the comment at the top of the - file. Which twelve of them the picker offers is a choice made here, and it is + file. Which thirteen of them the picker offers is a choice made here, and it is the only one: choosing what to show is not writing it, and every file is still served. The landing page's program is the exception, and it is short and its refusal was still produced by running it. @@ -92,13 +92,13 @@ Everything in it comes from somewhere else: each summary is the comment at the top of the file, and the rest is what the pinned artifact answered when asked. What it was asked matters, because "can this be run" has two halves here. -Twenty-one of the twenty-eight have no `main` at all. Six of the remaining +Twenty-two of the twenty-nine have no `main` at all. Six of the remaining seven have one and want the filesystem, which a page does not have, so `needs` records the capabilities they asked for. That leaves exactly one example this -page can start, and Run is off for the other twenty-seven with the reason +page can start, and Run is off for the other twenty-eight with the reason beside it, rather than letting somebody press it and be refused. -The picker shows twelve of the twenty-eight, and that list is in +The picker shows thirteen of the twenty-nine, and that list is in `tools/artifact.mjs` because both tools need it. The corpus is not a menu: about half of it is one language feature at a time, written so the compiler's own tests have something to read, and a visitor scrolling past `sink`, `names` @@ -113,7 +113,7 @@ corpus no longer has, so a promoted or deleted example shortens the menu loudly. `greeting.deed` is left out because it imports two other modules and this page -hands the compiler one file. That is the only one: the other twenty-eight were +hands the compiler one file. That is the only one: the other twenty-nine were checked through the pinned artifact and every one of them is clean. ## Layout @@ -144,7 +144,7 @@ the release the pin names, and the example index still says what the compiler says. That last part is not a shape check. It loads the pinned artifact, asks it its -version, and asks it about all twenty-eight examples, because a committed wasm +version, and asks it about all twenty-nine examples, because a committed wasm is a file nothing here ever built: a truncated copy, or a different build wearing the right name, spells its filename correctly and passes everything else. It runs on every pull request too. diff --git a/assets/deed-v0.2.3-wasm32-unknown-unknown.wasm b/assets/deed-v0.2.3-wasm32-unknown-unknown.wasm deleted file mode 100644 index 96e7a08..0000000 Binary files a/assets/deed-v0.2.3-wasm32-unknown-unknown.wasm and /dev/null differ diff --git a/assets/deed-v0.2.4-wasm32-unknown-unknown.wasm b/assets/deed-v0.2.4-wasm32-unknown-unknown.wasm new file mode 100644 index 0000000..aa68d06 Binary files /dev/null and b/assets/deed-v0.2.4-wasm32-unknown-unknown.wasm differ diff --git a/assets/errors.js b/assets/errors.js index b23de7f..2c5ffd1 100644 --- a/assets/errors.js +++ b/assets/errors.js @@ -5,8 +5,8 @@ // artifact carries all of them, so this page cannot document a code the // compiler does not have, or miss one it does. -const TAG = "v0.2.3"; -const VERSION = "0.2.3"; +const TAG = "v0.2.4"; +const VERSION = "0.2.4"; const WASM_URL = `../assets/deed-${TAG}-wasm32-unknown-unknown.wasm`; const STATUS = document.getElementById("status"); diff --git a/assets/play.js b/assets/play.js index 2b4d577..075bebd 100644 --- a/assets/play.js +++ b/assets/play.js @@ -13,8 +13,8 @@ // release, because a release asset cannot be fetched from a browser at all: // both the download URL and the API one redirect to a host that sends no // `Access-Control-Allow-Origin`. See decisions/2026-07-31-no-build-step.md. -const TAG = "v0.2.3"; -const VERSION = "0.2.3"; +const TAG = "v0.2.4"; +const VERSION = "0.2.4"; const WASM_URL = `../assets/deed-${TAG}-wasm32-unknown-unknown.wasm`; const SOURCE = document.getElementById("source"); diff --git a/examples/index.json b/examples/index.json index 59ca38a..c7104d5 100644 --- a/examples/index.json +++ b/examples/index.json @@ -1,5 +1,5 @@ { - "tag": "v0.2.3", + "tag": "v0.2.4", "examples": [ { "file": "calculator.deed", @@ -146,7 +146,7 @@ }, { "file": "proven.deed", - "shown": 11, + "shown": 12, "summary": "The Proven tier, which is the part of this language that is supposed to be interesting.", "runs": false, "needs": [], @@ -192,6 +192,14 @@ "needs": [], "tests": 7 }, + { + "file": "tasks.deed", + "shown": 11, + "summary": "Tasks, out of the library.", + "runs": false, + "needs": [], + "tests": 2 + }, { "file": "tic_tac_toe.deed", "shown": 1, diff --git a/examples/proven.deed b/examples/proven.deed index 35db3dc..7157ac0 100644 --- a/examples/proven.deed +++ b/examples/proven.deed @@ -118,6 +118,29 @@ fn unbounded_span(low: Int, high: Int) -> Positive high - low } +// Proven from a bound the program can name. `Int` is a signed 64-bit integer +// and until `Int.max` existed there was no way to say so: the clause had to +// carry the nineteen digits, or the function had to be written without a +// bound and take the runtime check. +// +// The bound is what makes this Proven rather than Guarded. `n + 100` on an +// unbounded `n` has no answer at the top of the range, and overflow stops the +// program rather than wrapping, so the checker is right to want it said. +fn headroom(n: Int) -> Positive + where + n >= 0, + n <= Int.max - 100, +{ + n + 100 +} + +// The other end, which is the one with no literal. Negation is an operator +// rather than part of a literal, so the digits of the smallest `Int` are one +// past the largest and there is nothing a literal alone could say. +fn is_the_floor(n: Int) -> Bool { + n == Int.min +} + // Proven across a call. `always_one` promises what it returns, the promise is // read here, and the proof one function did is worth something to the next. // Without this every abstraction boundary would restart the reasoning from @@ -354,6 +377,11 @@ test "the guarded ones are checked when they run" { assert one_more(1) == 2 assert unbounded_span(2, 5) == 3 assert squared(7) == 49 + assert headroom(5) == 105 + assert is_the_floor(Int.min) + assert !is_the_floor(0) + assert to_string(Int.min) == "-9223372036854775808" + assert Int.max == 9223372036854775807 } // The half that was missing. Every one of these is a `Guarded` obligation diff --git a/examples/scheduler.deed b/examples/scheduler.deed index ab82aa6..71ae092 100644 --- a/examples/scheduler.deed +++ b/examples/scheduler.deed @@ -32,22 +32,27 @@ // // It is also not a library, and the reason is worth being exact about, because // "concurrency is a library here" is the claim this file is usually read as -// making. What it shows is that a scheduler can be *written* in Deed. It cannot -// be *shipped*, and a program that wants one has to copy this file and edit it. +// making. What it shows is that a scheduler can be *written* in Deed. When this +// file was written it could not be *shipped*, and a program that wanted one had +// to copy this file and edit it. // // The wall is one line above: `Schedule.fork` takes a // `Fn() uses Schedule.fork, Schedule.yield, Log.note -> ()`, and that row names // `Log.note` because these particular tasks log. A library cannot know what its // tasks will perform, so the queue element type would have to be -// `Fn() uses r -> ()` for a row variable `r` belonging to the effect. Effects do -// not take row parameters: `effect Schedule` does not parse, and -// `DEED5008` separately confines a row variable to a function-typed parameter's -// row and the declaration's own `uses`, which a handler's `state` is neither. +// `Fn() uses r -> ()` for a row variable `r` belonging to the effect. // -// So the queue's element type has to name a concrete row, the row has to name -// every effect a task might perform, and both are things only the program -// knows. That is why `std/task` does not exist next to `std/list`, and it is a -// row-polymorphism gap rather than anything about concurrency. +// That is what `effect Task` is, and `std/task` is the scheduler +// written that way. An effect declares row variables, they are in scope in its +// operation signatures and in the state of any handler that implements it, and +// each `Task.fork` fills the variable in from the value it was passed, so a +// program that forks a task which logs is charged with logging. +// `examples/tasks.deed` is this program written against the library. +// +// This file is kept as it was, because the difference between the two is the +// whole of what a row variable on an effect buys, and it is easier to see side +// by side than described. What is written below still works and still says +// `Log.note` in a type that has nothing to do with logging. module examples/scheduler diff --git a/examples/tasks.deed b/examples/tasks.deed new file mode 100644 index 0000000..59a041f --- /dev/null +++ b/examples/tasks.deed @@ -0,0 +1,112 @@ +// Tasks, out of the library. +// +// The scheduler is `std/task`. Nothing in this file implements one: it forks +// three tasks that log, runs them, and reads the log back. What is worth +// noticing is that `std/task` says nothing about logging. `Task.fork` takes a +// `Fn() uses r -> ()`, `r` is filled in from the value passed at each fork, +// and that is why `main` below has to declare `Log.note` even though it never +// calls it directly. The tasks perform it, `main` chose them, and the row +// says so. +// +// `examples/scheduler.deed` is the same scheduler written out by hand, from +// before an effect could take a row variable. Its queue names `Log.note` in +// its own type, which is why it could not be a library and this can. + +module examples/tasks + +use std/task.{Task, RoundRobin, run, run_up_to} + +effect Log { + fn note(message: String) -> () + fn messages() -> List +} + +handler Recorder implements Log { + state log: List + + fn note(message) -> () { + log = push(log, message) + } + + fn messages() -> List { + log + } +} + +fn greet() -> () + uses + Log.note, +{ + Log.note("hello") +} + +fn count() -> () + uses + Log.note, +{ + Log.note("one") + Log.note("two") +} + +// A task that forks the rest of itself. This is how a task leaves room for +// another one to run: there are no resumptions, so a task that wants to yield +// splits, and the second half goes behind whatever else is waiting. +fn later() -> () + uses + Log.note, + Task.fork, +{ + Log.note("first half") + Task.fork(rest) +} + +fn rest() -> () + uses + Log.note, +{ + Log.note("second half") +} + +// Everything the three tasks perform, and nothing about scheduling beyond +// installing the handler. +fn transcript() -> List + uses + Log.note, + Log.messages, + Diverge, +{ + with RoundRobin { queue: [] } { + Task.fork(greet) + Task.fork(later) + Task.fork(count) + run() + Log.messages() + } +} + +// The bounded runner, for when the number of tasks is the point. +fn first_two() -> Int + uses + Log.note, +{ + with RoundRobin { queue: [] } { + Task.fork(greet) + Task.fork(count) + Task.fork(greet) + run_up_to(2) + } +} + +test "tasks run in the order they were forked" { + let log = with Recorder { log: [] } { + transcript() + } + assert log == ["hello", "first half", "one", "two", "second half"] +} + +test "a bounded run stops at the limit" { + let ran = with Recorder { log: [] } { + first_two() + } + assert ran == 2 +} diff --git a/install/index.html b/install/index.html index 93d27a8..fff50d5 100644 --- a/install/index.html +++ b/install/index.html @@ -62,7 +62,7 @@

Install