§ 09 · draft · depth 8 · edit the source

The prelude

Every function's signature carries the stratum it costs. Reading this section is how a programmer finds out what a thing will do to their program's depth, so nothing here may be deeper than it must.

The prelude is deliberately small. It should be readable in full in ten minutes.

The listings below are a notation and not a program. A signature and a semicolon is not something section 04 parses — func_decl wants a block — and there is no production for one because nothing a program can write would supply a body for read. They are here the way a header file is here: to be read.

9.1 Capabilities

These are the names descend accepts. An implementation MUST NOT define others.

Each grants its own stratum and no other. The table is a bijection — one capability per stratum, one stratum per capability — which is what lets §2.1 treat a set of capabilities and a set of strata as the same object.

The ! suffix marks the writing half of a pair, and reads as it does in the rest of the language: this one does not take back.

9.2 Depth 0

I64   min(I64 a, I64 b)                @0;
I64   max(I64 a, I64 b)                @0;
I64   abs(I64 x)                       @0;

I64   len(Bytes b)                     @0;
Bytes slice(Bytes b, I64 from, I64 to) @0;
Bytes concat(Bytes a, Bytes b)         @0;
Bool  starts_with(Bytes b, Bytes p)    @0;

Answer<Str> utf8(Bytes b)              @0;   // Refused malformed
Bytes raw(Str s)                       @0;
Str   join(Str[] parts, Str sep)       @0;
Str[] split(Str s, Str sep)            @0;

Cairn cairn_of(Bytes b)                @0;   // the same value `seal` would give
Str   hex(Cairn c)                     @0;

Refusal absent; denied; malformed;           // the six closed codes,
Refusal unreachable; exhausted; conflict;    // bound as prelude constants

Bool    given(Answer<T> a)             @0;   // did the world say yes?
Refusal refusal(Answer<T> a)           @0;   // which no was it? collapses if given
T       must(Answer<T> a)              @0;   // the value. collapses if refused

Answer<T> answered(T v)                @0;   // a yes a program built
Answer<T> refused(Refusal r)           @0;   // a no a program built

given and refusal are how a program handles a no. must is how it declares it will not: this cannot be refused, and if it is, that is a bug and I want the burial to stop. It is the right thing to write when a refusal would mean the program's assumptions were already wrong, and the wrong thing to write anywhere else.

There is no pattern matching in this draft, so an answer is inspected the way C has always inspected one:

Answer<Bytes>@3 a = descend disk { read("main.nc") };

if (given(a)) {
  Bytes@3 src = must(a);
  // ...
} else if (refusal(a) == absent) {
  // ...
}

answered and refused go the other way, so a function a program writes can hand its caller the shape utf8 hands it, and say no without collapsing:

// verdict.nc — a function that says no the way the prelude does. §9.2.

Answer<Bytes> first(Bytes b)
{
  if (len(b) == 0) {
    return refused(absent);
  }
  return answered(slice(b, 0, 1));
}

U0 report()
{
  Answer<Bytes> a = first(b"nether");
  Answer<Bytes> none = first(b"");
  if (given(a)) { concat(must(a), b"\n"); }
  if (refusal(none) == absent) { "nothing there\n"; }
}

demand report();

$ nether lamp 0909a5ab
n
nothing there

answered takes its T from its argument, the way the three inspectors do. refused has no T to take: a refusal is a code and nothing else. It takes the one it is declared into, so it MUST be the whole value of a binding or a return whose declared type is an Answer. Anywhere else it is an error, because anywhere else nothing says what it is a refusal of:

$ nether bury unlanded.nc
error: expected a declared `Answer<T>` for `refused`
 --> unlanded.nc:1:24
  |
1 | Answer<Bytes> x = must(refused(absent));
  |                        ^^^^^^^^^^^^^^^

Both are at depth 0 and neither records a witness. Nothing was asked, so there is nobody whose answer §1.4 would be recording — the same reason utf8's malformed has none.

compile is not in the prelude. Nether C does not know how to compile Nether C until Self-Burial; until then it is an ordinary function a program supplies for itself.

9.3 Stratum 1 — store

Answer<Bytes> fetch_node(Cairn c)      @1;   // Refused absent
Bool          has_node(Cairn c)        @1;

Reading the ledger is at depth 1 rather than 0 because the ledger is a place on a machine, and a program that reads it can fail in a way a pure program cannot. The value it returns is nevertheless fully determined by the cairn, which is why it is only one stratum down.

9.4 Stratum 2 — env

Answer<Str> env(Str name)              @2;   // Refused absent
I64         clock()                    @2;   // the pinned build time
Str         target()                   @2;   // the target triple

env distinguishes two different mistakes. Reading a variable that was declared and is not set is a refusal: the world was asked and said no. Reading a variable that was never declared is not a refusal, it is a bug in the program, and it collapses (§9.9).

Neither returns empty. A build that silently behaves differently because a variable was absent is exactly the class of bug this language exists to make impossible.

The declaration lives outside the program, in the exhumation that answers the hole: §8.3.1 is the invocation.

A trace records every value read from it, as a Witness like any other, and does not record the declared set. It does not need to. A read produces a witness; a refusal is an answer and is witnessed the same way; and a name that was never declared collapses, which produces no trace at all. So everything the declaration did to the program is already named by the trace, and what is left over is a name the program never read — which changed nothing, and which two cairns therefore must not be made to differ by.

9.5 Strata 3 and 4 — disk, disk!

Answer<Bytes> read(Str path)           @3;   // absent, denied
Answer<Str[]> list(Str path)           @3;   // absent, denied
Bool          exists(Str path)         @3;

Answer<U0> write(Str p, Bytes c)       @4;   // denied, exhausted
Answer<U0> remove(Str path)            @4;   // absent, denied

read becomes a hole; the answer is sealed and recorded before it reaches the program. write is the first genuinely irreversible thing the language can do, and the only prelude function whose witness records something the ledger cannot later reproduce on its own.

Where a path is rooted is not said here. It is the invocation's, and §8.3.4 is where an operator says it — which is also where denied comes from for a path that would climb out, as against the absent of a path that is simply not there.

9.6 Strata 5 and 6 — net, net!

Answer<Bytes> get(Str url)             @5;   // unreachable, denied, absent
Answer<Bytes> post(Str url, Bytes b)   @6;   // unreachable, denied, conflict

The response is sealed on arrival, with the request as its witness. Replay serves the recorded response and MUST NOT open a socket.

A URL names a scheme, and an implementation MUST state which schemes it serves. It is not required to serve all of them: https is TLS, and an implementation that wrote its own would be writing its own cryptography. One that will not serve a scheme MUST refuse it with denied rather than unreachable, because those are different sentences — denied is this build saying no, and unreachable is the world not answering. A trace would otherwise record "the host was down" for a build that never dialled.

Where an implementation may reach at all is §8.3.2, and is a fact about the invocation rather than about the language.

9.7 Stratum 7 — entropy

Bytes draw(I64 n)                      @7;

draw is the only source of nondeterminism in the language, and it is nearly the deepest thing in it.

Entropy is stratum 7: the deepest recordable thing. Once drawn bytes affect a trace, the source alone is not enough to re-derive it. Replay needs the recorded answer.

A trace that called draw records the drawn bytes as a witness, so replay is exact. What is lost is re-derivation: burying the same source again produces a different trace. See §6.7.

9.8 Stratum 8 — unrecorded

Answer<Bytes> call_foreign(Str sym, Bytes args) @8;

Marks the trace, permanently and transitively. Everything downstream of the call is at depth 8 and the trace can no longer claim to be replayable.

An implementation MUST make this unpleasant to reach for — at minimum, naming the symbol in nether strata output — because a stratum-8 call is a hole in the record that no later care can fill in.

What may be loaded at all is §8.3.3.

9.8.1 The other side

sym names a function with C linkage and this signature:

int32_t sym(const uint8_t *args, size_t args_len,
            uint8_t *out, size_t out_cap, size_t *out_len);

That is C, not Nether C. It is here the way a header file is here: to be read, and written against.

It is handed the Bytes the program passed, and a buffer to write its answer into. It MUST set *out_len to the length of its answer whether or not the answer fit, and MUST NOT write more than out_cap bytes. It returns:

On 1 the implementation MUST call once more with a buffer of at least *out_len, and MUST NOT call a third time: a callee whose answer grows every time it is asked is a callee that never finishes.

Neither side frees the other's memory. The buffer belongs to the caller for its whole life, and args belongs to the caller too — a callee that keeps either pointer after it returns has kept a pointer to something it does not own, and no wording here can stop it. That is what stratum 8 is, and it is why §1.7 marks the trace rather than trying to make the call safe.

An implementation MUST NOT assume anything else about the callee. In particular it MUST record the witness before the call, so that a callee which does not return leaves a trace saying what was attempted.

9.9 Failure, and the difference between two of them

Nether C has no exceptions and no unwinding. Unwinding has no meaning in a language where evaluation is demand-driven and partially staged, and a stack that can be unwound is a stack that can be observed.

It has two things instead, and the whole of failure handling is knowing which one you are looking at.

A refusal is an answer

When the world is asked a question it is entitled to answer no to — the file is not there, the response never came — that no is the answer. It is a value, of type Answer⟨T⟩, and it is recorded as a witness exactly like a yes.

This is not a concession to practicality. It follows from §1.4: everything the world says gets written down before the program sees it. A missing file is something the world said. Replay serves it back, and a program that handled it replays identically.

The world is where most refusals come from and it is not where the type comes from. utf8 is at depth 0 and refuses malformed: bytes that are not UTF-8 are a fact about bytes the program already had, nothing was asked of anybody, and there is no witness because nothing happened. A program's own parser is in the same position, and §9.2 gives it the same two constructors rather than leaving the prelude able to do something a program cannot. What Answer⟨T⟩ says is that this can be refused and which no it was; where the no came from is what the stratum says, and a depth-0 refusal is one nobody owes a witness for.

A collapse is a bug

An expression collapses when it cannot produce a value and never will: must on a refusal, refusal on a given answer, an out-of-range slice, env on a variable that was never declared.

A collapse is not catchable. There is no rescue, no try, no recovery form, and there will not be one. A burial that hits one caves in: it stops and reports the source span, because every way to collapse is a mistake in the program rather than a fact about the world, and a mistake that can be caught is a mistake that will be ignored.

A collapse is not a starvation, which is what an expression does while it waits on a hole (§6.4). That is ordinary: a starved expression is residualised and finishes later, at somebody else's exhumation. A collapsed one never finishes.

What it costs

Every call site that touches the world gets a check, or an explicit must that says a check is unnecessary. Code that reads six files reads as six answers.

That is the bargain C has always offered — if (fp == NULL) — and Nether C is a C dialect, so it offers the same one rather than a better-looking one that hides where the world can say no. The rejected alternatives are in §90.2.