JDL — Cast-System, Effect-Row-Architektur, Funktions-Refinements und Deklarative Runtime¶

Status: Entwurf v0.3 — ersetzt v0.2 (Status Normativ) vollständig Autor: Elias

Ersetzt in Teilen: - 02-typsystem.md § 3 – Typ-Konversion - 04-qualifier-effekte-konversionen-wire.md § 4 – Effektsystem - 04-qualifier-effekte-konversionen-wire.md § 5 – Konversionssystem - 20-spec-v3-effect-system-archiv.md – Effect-System-Architektur (Archiv) - 28-syntax-exploration-archiv.md – Konversions- und Effekt-Abschnitte

Bei Widerspruch gilt dieses Dokument.

Statushinweis: Diese Fassung ist ausdrücklich nicht normativ. Sie enthält Notationsvorschläge, die noch nicht gegen die Grammatik-Spec abgeglichen sind. Alle derartigen Stellen sind mit // spekulativ markiert. Sie ist gedacht als Arbeitsgrundlage für den Übergang von der Effect-Wert-Architektur zur Effect-Row-Architektur.

0. Änderungsprotokoll gegenüber v0.2¶

0.1 Was ersatzlos entfällt¶

Entfallen	Grund
`Effect[R, E, D]` als Typ	Alle drei Parameter sind aufgelöst: `D` und `E` in die Effect Row, `R` ist der gewöhnliche Rückgabetyp. Der Typkonstruktor hat keine Aufgabe mehr.
`=?` als Propagationsoperator	Der Fehlerkanal steckt nicht mehr im Rückgabetyp, also gibt es nichts zu propagieren.
`CastTo`-Ketten im Fehlerpfad	Folgt aus dem Wegfall von `=?`.
„Zwei Funktionsstile" (§2.2 v0.2)	Es gibt nur noch einen Stil. Der Unterschied zwischen imperativ und Effect-Stil war ein Unterschied in der Kodierung, nicht in der Semantik.
Effect-AST zur Laufzeit (§2.6 v0.2)	Handler werden zur Übersetzungszeit aufgelöst (Evidence Passing). Es gibt keinen interpretierten Effekt-Baum mehr.
`Effect.ok(...)` und die Effect-Kompositions-API	Ersetzt durch direkten Stil plus Kombinatoren über suspendierte Berechnungen.

0.2 Was neu hinzukommt¶

Effect Row als Bestandteil des Funktionstyps: ->{...}
Services als Forderungsmechanismus (bestehendes service), Handler als Erfüllungsmechanismus (bestehendes provide)
Throw[E] — der Fehlerkanal als Row-Element
Alloc[A] — Allokation als Effekt
Instanz-Tags (Db[Primary], Alloc[ReqArena]) statt benannter Slots
Pure und Deterministic als zwei getrennte Labels
Evidence Passing als Lowering-Strategie
Folgen für den Bootstrap Seed (Core-Service-IDs)

0.3 Was unverändert bleibt¶

Das Cast-System (§1) und die deklarative Runtime (§9) sind in ihrer Substanz unberührt. Beim Cast-System ändert sich nur der Try-Modus, bei der deklarativen Runtime nur die Rolle des CallGraph.

Präambel¶

Dieses Dokument konsolidiert Designentscheidungen, die konzeptuell zusammengehören:

Konversionen sind ein gewöhnliches Protocol mit Operator-Bindung — CastTo[T] via ->.
Effekte stehen im Funktionspfeil, nicht im Rückgabetyp. Eine Funktionssignatur nennt vollständig, was die Funktion von ihrer Umgebung verlangt.
Querschnittsbelange wie Caching, Retry und Transaktionalität gehören ins Meta-Record der Funktion, nicht in ihre Logik.
Deklarative Konstrukte sind zur Laufzeit composable Dictionaries.

Die zweite Entscheidung ist neu und die folgenreichste. Ihre Kernaussage lautet: Ein Effekt ist keine Beschreibung, die man herumreicht, sondern eine Bedingung darüber, wo eine Funktion laufen darf. Die Signatur trägt diese Bedingung; die Umgebung erfüllt sie.

1. Das Cast-System¶

1.1 Motivation¶

Die vierte Form von provide – provide Target from Source – löste ein konzeptuelles Problem nicht sauber: Konversion ist keine Implementierung eines Protokolls für einen Typ, sondern eine gerichtete Beziehung zwischen zwei Typen.

Konversion ist ein gewöhnliches Protocol namens CastTo[T], gebunden an den Operator ->. Damit verschwindet die vierte provide-Form vollständig. provide hat genau drei Formen:

provide Equatable for User        – Protocol-Implementierung
provide User                      – Methoden am Typ
provide UserDb[PostgresHandler]   – Service-Handler-Bindung

1.2 Der Operator `->` als Flow-Metapher¶

-> ist in JDL als Flow-Symbol etabliert: in Funktionssignaturen beschreibt er den Datenfluss von Eingabe zu Ausgabe, im CallGraph die Sequenz von Knoten. Als Cast-Operator setzt er diese Metapher fort – ein Wert fließt von einem Typ in einen anderen.

1.3 Grammatik-Abgrenzung: Cast-Pfeil und Funktionspfeil¶

Mit der Effect Row trägt -> zwei Rollen. Sie werden durch eine einzige Regel getrennt:

Regel C-1. Ein Funktionstyp hat immer eine geklammerte Parameterliste. Der ungeklammerte Pfeil ist ausnahmslos dem Cast-Ausdruck vorbehalten.

val summary = user -> UserSummary        // Cast: linke Seite ist ein Wert
type F = (User) -> UserSummary           // Funktionstyp: geklammerte Parameterliste
type G = (User) ->{Db} UserSummary       // Funktionstyp mit Effect Row

Damit muss der Parser nie raten. Diese Regel löst zugleich den Widerspruch zwischen Sprachüberblick und Blueprint-Spec auf, in dem beide Formen ungeklammert auftraten.

1.4 Drei Modi¶

Der Modus eines Casts liegt auf der Implementierung, nicht auf dem Aufruf.

// Lossless – verlustfrei, darf implizit angewendet werden
provide CastTo[UserResponse] for User {
    def castTo(self) -> UserResponse = UserResponse {
        id:    self.id
        name:  self.name
        email: self.email
        role:  self.role
    }
}

// Narrow – verlustbehaftet, immer explizit erzwungen
provide CastTo[UserSummary]: Narrow for User {
    def castTo(self) -> UserSummary = UserSummary {
        name: self.name
    }
}

// Try – fallibel; wirft statt Result zurückzugeben
provide CastTo[UserId]: Try[ConvError] for User {
    def castTo(self) ->{Throw[ConvError]} UserId =
        if self.id.value.isEmpty() then
            Throw.throw(ConvError.InvalidId { reason: "Id ist leer" })
        else
            self.id
}

Änderung gegenüber v0.2: Der Try-Modus gibt kein Result mehr zurück, sondern trägt Throw[E] in der Row. Das hält den Fehlerkanal an genau einer Stelle (§4). Wer ein Result will, ruft den Cast unter catching auf.

1.5 Anwendung¶

val user: User = ...

val response: UserResponse = user         // Lossless – implizit
val response  = user -> UserResponse      // Lossless – explizit
val summary   = user -> UserSummary       // Narrow – explizit erzwungen
val id        = user -> UserId            // Try – wirft; Row der Funktion trägt Throw[ConvError]

// Wenn der Fehler als Wert gebraucht wird:
val idResult  = catching { user -> UserId }   // : Result[UserId, ConvError]   // spekulativ

Bemerkenswert: Der Aufruf sieht bei allen drei Modi gleich aus. Der Unterschied steht in der Row der aufrufenden Funktion — bei Try erscheint dort Throw[ConvError], sonst nicht.

1.6 Primitive Widening¶

Primitive Widening – etwa i32 zu i64 – ist eingebaut und braucht keinen provide-Block. Verengungen brauchen immer einen expliziten Cast.

2. Die Effect Row¶

2.1 Grundprinzip: Effekte stehen im Pfeil¶

Eine Funktionssignatur nennt zwischen Parameterliste und Rückgabetyp die Menge der Effekte, die der Rumpf verwenden darf:

def loadUser(id: UserId) ->{Db, Throw[NotFound]} User

Gelesen: „loadUser nimmt eine UserId, liefert einen User, und ist nur in einem Kontext aufrufbar, der Db und Throw[NotFound] behandelt."

Die Row ist keine versteckte Parameterliste. Es wird nichts hineingereicht, was die Funktion dann in der Hand hielte. Sie ist eine Bedingung an den Aufrufkontext. Das passende Bild ist eine Schuld, die abgetragen wird: Jeder installierte Handler streicht ein Element, bis in main die leere Menge übrig bleibt.

2.2 Die drei Notationsregeln¶

Regel R-1. Ein Funktionstyp hat immer eine geklammerte Parameterliste (siehe §1.3).

Regel R-2. Die Effektmenge steht zwischen schließender Klammer und Rückgabetyp: (P) ->{E} R.

Regel R-3. Eine fehlende Effektmenge bedeutet die leere Menge, nicht eine unbestimmte. def f(a: i32) -> i32 ist exakt def f(a: i32) ->{} i32.

Regel R-3 ist rückwärtskompatibel: Jede bisher geschriebene Signatur bleibt gültig und bedeutet dasselbe wie zuvor, sofern sie effektfrei war. Historisch ist das keine Erfindung — schon Lucassen und Gifford schrieben die allgemeine Form als σ -ε-> τ. Der schlichte Pfeil war immer heimlich der Pfeil mit leerer Menge; er wird nur sichtbar, sobald ε variiert.

2.3 Algebra¶

Die Row ist eine ungeordnete Menge. Zwei Regeln bestimmen ihr Verhalten:

Vereinigung bei Komposition. Ruft ein Rumpf mehrere Funktionen auf, ist seine Row mindestens die Vereinigung der Rows der Aufgerufenen.

f: (A) ->{Db} B
g: (B) ->{Api} C
--------------------------------
g ∘ f : (A) ->{Db, Api} C

Abschwächung (Subeffecting). Eine Funktion mit kleinerer Row ist überall dort einsetzbar, wo eine größere erwartet wird.

f: (A) ->{} B     ist zuweisbar an     (A) ->{Db} B

Die Umkehrung gilt nicht.

Row-Variablen erlauben Polymorphie über die Effektmenge:

def map[T, U, g](xs: [T], f: (T) ->{g} U) ->{g} [U]

map führt keine eigenen Effekte ein; es reicht durch, was der Aufrufer mitbringt. Wird map mit einer reinen Funktion aufgerufen, ist g leer und map selbst rein.

2.4 Die leere Menge bedeutet leer¶

JDL folgt hier der Unison-Lesart, nicht der Frank-Lesart.

Unison: ->{} verbietet ausdrücklich jede Ability. Polymorphie braucht eine explizite Variable ->{g}.
Frank: die leere Klammer steht für die ambiente Ability — sie ist implizit polymorph. Franks Konvention lautet, dass A in Wahrheit für [ε|·]A steht.

Frank erkauft sich damit, dass Funktionen höherer Ordnung ohne Effektvariable auskommen. Der Preis ist, dass sich Reinheit nicht mehr durch Weglassen ausdrücken lässt — ein nackter Pfeil bedeutete dann „nimmt, was da ist", nicht „garantiert effektfrei".

Für eine Sprache, deren Constitution auf beweisbaren Grenzen aufbaut, ist die Unison-Lesart die richtige. Der Preis ist real und wird in §2.7 sowie §11 benannt: Jede Funktion höherer Ordnung in der Stdlib trägt eine explizite Row-Variable. Das ist kein Schönheitsfehler, sondern genau das, was ->{} überhaupt erst zu einer Aussage macht.

2.5 Ein Stil statt zwei¶

Version 0.2 kannte zwei Funktionsstile: imperativ (Abhängigkeiten als Parameter, Result im Rückgabetyp) und Effect-Stil (Effect[R, E, D] als Rückgabetyp). Beide verschwinden zugunsten eines einzigen Stils.

// v0.2, imperativ
def fetchUser(db: UserDb, id: UserId) -> Result[User, UserDbError]

// v0.2, Effect-Stil
def fetchUser(id: UserId) -> Effect[User, UserDbError, UserDb]

// v0.3
def fetchUser(id: UserId) ->{UserDb, Throw[UserDbError]} User

Die Rechnung, die dahintersteht:

Effect[R, E, D]   ──D in den Pfeil──▶   Effect[R, E]
                  ──E in den Pfeil──▶   Effect[R]
                                     ═  R

Effect trug genau drei Aufgaben: R tragen, E tragen, D tragen. Zwei sind in die Row gewandert, die dritte ist schlicht der Rückgabetyp. Der Typkonstruktor hat keine Aufgabe mehr und entfällt.

Damit entfällt auch das Problem aus v0.2, dass E zweimal existierte — einmal als Result[R, E] im imperativen Stil, einmal als Parameter von Effect[R, E, D]. Es gibt jetzt einen Fehlerkanal, Throw[E], und genau einen Umwandlungspunkt (catching), der vom Aufrufer gewählt wird, nicht vom Autor der Funktion.

2.6 Suspendierte Berechnungen ersetzen Effect-Werte¶

Ein Effect-Wert konnte eines, was ein Aufruf nicht kann: nicht laufen. val e: Effect[R,E,D] = ... führte nichts aus, es beschrieb. Genau darauf bauten withRetry, Cache und die übrigen Kombinatoren auf.

Der Ersatz ist die suspendierte Berechnung — ein Thunk, dessen Effekte im Typ stehen:

// v0.2
def withRetry[R, E, D](e: Effect[R, E, D], n: u32) -> Effect[R, E, D]

// v0.3
def withRetry[T, g](body: () ->{g} T, n: u32) ->{g} T

Das ist dieselbe Sache in anderer Notation. Frank macht diesen Zusammenhang explizit sichtbar: dort sind die geschweiften Klammern der suspendierte Berechnungstyp.

Der Default hat sich dabei umgedreht, und das ist eine bewusste Entscheidung. In v0.2 war alles eine Beschreibung, und Ausführen war der explizite Schritt. In v0.3 läuft alles sofort, und Aufschieben ist der explizite Schritt. Damit tauscht sich auch die typische Fehlerklasse: aus „vergessen auszuführen, es passiert stillschweigend nichts" wird „vergessen zu suspendieren, es läuft zu früh". Der zweite Fehler ist der bessere, weil etwas passiert statt nichts — aber er ist neu und muss dokumentiert sein.

Notationsvorschlag (spekulativ). Um () => an jeder Aufrufstelle zu vermeiden, bietet sich eine Trailing-Block-Form an:

withRetry(3) { loadUser(id) }        // spekulativ

Die geschweiften Klammern sind die Suspension. Das ist bewusst kein typgesteuertes implizites Einwickeln (wie Scalas By-Name-Parameter => T): Wer den Block sieht, weiß, dass er nicht sofort läuft, und wird nicht davon überrascht, dass er dreimal läuft. Die Sichtbarkeit des Aufschubs bleibt erhalten; nur das Rauschen verschwindet.

Dieselbe Form löst zugleich die Handler-Verschachtelung (§3.5).

2.7 Inferenz¶

Ohne Inferenz müsste jede Funktion jeden Effekt aufzählen, den sie transitiv durchreicht. Bei drei Ebenen Aufrufkette wird das eine Zeile Signatur pro Zeile Rumpf. Frank hat bewusst keine Effektinferenz; Zig kommt mit fein granularen Fehlermengen nur deshalb durch, weil es sie herleitet.

Regel R-4. Effektinferenz ist modul-intern. An Modulgrenzen — also für alles, was exportiert wird — ist die Row zu deklarieren.

Damit bleibt der Proof Trace an den Grenzen deklarativ, wo er zählt, und die Aufzählungslast fällt innen weg. Für die Stdlib heißt das: dort wird durchgehend deklariert, was in §2.4 als Preis benannt wurde und dort auch hingehört.

3. Services als Effektträger¶

3.1 Deklaration — kein neues Schlüsselwort¶

Was die Effektsystem-Literatur Ability nennt, heißt in JDL bereits service. Die Trennung zu protocol ist in 04-qualifier §3.1 begründet: protocol beschreibt das Verhalten eines Typs, service eine Capability in Effektkontexten.

service Fs {
    def readText(p: Path) -> str
    def writeText(p: Path, s: str) -> ()
}

service Db[i] {
    def query(sql: str) -> [Row]
    def exec(sql: str)  -> u64
}

Gegenüber der bisherigen Form ändern sich genau zwei Dinge:

Optionaler Instanz-Parameter [i] (siehe §3.4).
Kein Result mehr in den Operationssignaturen. Bisher stand dort def query(sql: str) -> Result[Rows, DbError]. Der Fehler wandert in die Row des Handlers (§4).

Die Signaturen innerhalb einer Service-Deklaration tragen selbst keine Row. Eine Operation ist eine Anfrage an die Umgebung; welche Effekte bei ihrer Beantwortung anfallen, steht in der Signatur des Handlers.

Zu bereinigender Widerspruch. 10-runtime-handles X.2.1 deklariert dieselben Capabilities als protocol Db { ... }, während 04-qualifier §3.4 als Invariante festhält, dass Protocols nicht im Effekttyp erscheinen und Services nicht wie Protocol-Constraints behandelt werden. Es gilt service. X.2.1 ist entsprechend zu korrigieren.

3.2 Aufruf und Auflösung¶

Ein Service wird über seinen Namen aufgerufen, nicht über einen Wert:

def loadUser(id: UserId) ->{Db[Replica]} Option[User] =
    Db.query(f"SELECT * FROM users WHERE id = {id}")
    |> first
    |> map(rowToUser)

Regel A-1. Enthält die Row genau ein Element des gesuchten Service, ist der Aufruf unqualifiziert zulässig. Die Auflösung ist dann eindeutig.

Der Tag lebt nur in der Signatur — dort, wo er Dokumentation und Prüfung ist. Gewöhnlicher Code zahlt für die Instanz-Parametrisierung nichts.

3.3 Ein Service ist eine Forderung, kein Wert¶

Die Row ist nicht ein Satz benannter Slots, die von der Umgebung befüllt werden. Sie ist eine Bedingung an den Aufrufkontext. Das passende Bild ist eine Schuld, die abgetragen wird: Jede Handler-Installation streicht ein Element, bis in main die leere Menge übrig bleibt.

Regel A-5. Nutzercode kann einen Service-Handler nicht als Wert erlangen. Die Operation Runtime.getHandler[Cap]() -> Cap aus 10-runtime-handles X.2.2 entfällt.

Begründung: getHandler ist der einzige Weg, auf dem ein Handler aus dem Effektkontext in gewöhnlichen Code entweicht. X.2.5 braucht es nur, um den vorherigen Handler vor einer Überschreibung zu sichern — das erledigt der Scope-Mechanismus selbst. Ohne A-5 wäre die Abgrenzung zu Capability[T] (unten) nicht haltbar.

Abgrenzung zu Capabilities. Ein Service ist eine Forderung: steht im Pfeil, wird vom umgebenden Handler aufgelöst, Nutzercode hält ihn nie in der Hand. Eine Capability[T] mit rights und attenuate ist ein Wert: unfälschbar, explizit weitergereicht, abschwächbar, an ein konkretes Objekt gebunden. Beide greifen ineinander — der Service sagt „hier braucht es Dateizugriff", die Capability, die der Handler benutzt, sagt „auf genau diese Datei, nur lesend". Sie dürfen aber nicht begrifflich zusammengezogen werden.

3.4 Instanzen über Tags, nicht über Namen¶

Ein Record-artiges ->{db: Db, req: Alloc[ReqArena]} wurde erwogen und verworfen. Ein Record-Label ist nützlich, weil es eine Verwendungsstelle hat (r.field). Ein Row-Label hätte keine: Im Rumpf steht Db.query(...), und das benennt den Service, nicht den Slot. Hinzu käme ein Kompositionsproblem — ob ->{db: Db} mit ->{database: Db} unifiziert, hat keine gute Antwort.

Das echte Bedürfnis dahinter — zwei Instanzen desselben Service — ist anerkannt; {Db, Db} ist als Menge bedeutungslos. In der Literatur heißt die Lösung named effect handlers. JDL löst es über Typ-Tags, die es mit tag Primary ohnehin schon gibt (08-grammar-sketch §4):

tag Primary
tag Replica

->{Db[Primary], Db[Replica]}

Db[Primary] und Db[Replica] sind verschiedene Elemente der Menge, nicht ein Service mit Argument. Ein Handler für die eine erfüllt die andere nicht.

Der Tag ist einem Namen in drei Punkten überlegen: Er ist ein Typ und nimmt an Unifikation teil; er ist polymorphierbar (->{Alloc[a]}); und er ist global eindeutig statt pro Signatur neu erfunden.

Ein Tag ist eine Rolle, keine Instanz. Derselbe Tag kann in verschiedenen Läufen von verschiedenen Handlern bedient werden — Produktion und Test —, ohne dass die aufrufende Funktion eine Zeile ändert. Genau darauf beruht der TestSimulator.

3.5 Mehrdeutigkeit ist ein Fehler¶

Regel A-2. Enthält die Row mehrere Elemente desselben Service, ist ein unqualifizierter Aufruf ein Fehler. Es gilt keine „innerster Handler gewinnt"-Regel.

def refreshUser(id: UserId) ->{Db[Replica], Db[Primary]} Option[User] {
    val rows = Db[Replica].query(f"SELECT * FROM users WHERE id = {id}")
    match rows |> first {
        | Some(row) => {
            Db[Primary].exec(f"UPDATE seen SET at = now() WHERE id = {id}")
            Some(rowToUser(row))
        }
        | None => None
    }
}

Unqualifiziert wäre das:

Fehler [EFF-AMB-001]: Mehrdeutiger Service-Aufruf `Db.query`
  Zwei Instanzen im Effektsatz sichtbar: Db[Replica], Db[Primary]
  Qualifiziere den Aufruf, z. B. `Db[Replica].query(...)`

Kokas Row-Polymorphismus beruht auf scoped labels, erlaubt also doppelte Labels und löst sie über „innerster Handler gewinnt" auf. Das ist bequem, aber genau die Art impliziter Regel, gegen die JDL sonst argumentiert.

Regel A-3. Enthält die Row eine Row-Variable, ist Qualifikation verpflichtend, auch wenn nur eine Instanz sichtbar ist.

def audit[g](id: UserId) ->{g, Db[Primary]} () =
    Db[Primary].exec(f"INSERT INTO audit VALUES ({id})")   // Tag verpflichtend

Begründung: Es ist statisch nicht bekannt, ob g ein weiteres Db[_] enthält. Die konservative Regel garantiert, dass sich die Bedeutung eines Rumpfes nie dadurch ändert, dass ein Aufrufer einen Service hinzufügt.

3.6 Handler-Definition — `provide`, unverändert¶

Ein Handler ist ein gewöhnlicher Wert, der die Operationen des Service implementiert. Das ist die dritte provide-Form aus 04-qualifier §3.4, ohne jede Änderung:

provide Db[PostgresHandler] {
    def query(sql: str) ->{Net} [Row] = Net.request(url, sql) |> parseRows
    def exec(sql: str)  ->{Net} u64   = Net.request(url, sql) |> affected
}

Der Instanz-Tag steht hier bewusst nicht. Ein Handler ist polymorph in der Instanz — derselbe PostgresHandler bedient Primary wie Replica; welche Rolle er erfüllt, entscheidet die Installation (§3.7). Damit bleibt die Klammer in provide Db[...] eindeutig der Handler-Typ, wie bisher, und es entsteht kein Grammatikkonflikt mit der Tag-Notation.

Kein resume, kein Operations-Matching. Das ist die Folge von A-4: Bei einem tail-resumptiven Handler ist resume(x) in Endposition dasselbe wie „gib x zurück". Ein Handler ist damit eine gewöhnliche Methodenimplementierung.

3.7 Handler-Installation — drei bestehende Formen¶

Alle drei existieren bereits und brauchen nur den Instanz-Tag im Typparameter.

Global (10-runtime-handles X.2.3):

rt.registerHandler[Db[Primary]](PostgresHandler { pool: ConnectionPool.new(cfg.primaryUrl) })

Bereichsbegrenzt (X.2.5) — eine gewöhnliche Stdlib-Funktion mit Block, kein Schlüsselwort:

Runtime.withHandler[Db[Primary]](postgres(cfg.primaryUrl)) {
    buildReport()
}

Deklarativ (X.2.4) — im Blueprint:

CallGraph app(req: HttpRequest) ->{Throw[AppError]} HttpResponse {
    env: {
        Db[Primary]:     PostgresHandler { pool }
        Db[Replica]:     PostgresHandler { replicaPool }
        Alloc[ReqArena]: ArenaHandler { size: 64.kib }
    }

    handleRequest(req)
}

Regel A-6. withHandler ist die Quellform, Evidence Passing das Lowering (§7.2). Die Laufzeit-Zuordnung „Capability-Typ → Handler-Wert" aus X.2.2 entfällt als Auflösungsmechanismus für statisch bekannte Rows.

Begründung: Die Row macht an jeder Aufrufstelle bekannt, welche Handler im Umlauf sind. Eine Laufzeitsuche würde diese Information wegwerfen und neu beschaffen.

Abgrenzung zu with. with expr as name { body } ist der Ressourcen-Scope: verlangt eine Scopeable[R]-Instanz, senkt zu call @acquire + Body + call @release (auch auf Fehlerpfaden), im IR die Extended-Op WithScope. with bindet einen Wert und lässt die Row des Körpers unverändert; eine Handler-Installation bindet keinen Wert und entfernt ein Element aus der Row. Zwei verschiedene Operationen auf Typebene — daher withHandler als eigene Funktion, nicht als with-Variante. Siehe §11 zu O-2.

3.8 Handler-Klassen und die Resumption-Beschränkung¶

Klasse	Bedingung	Beispiele	Kosten
Tail-resumptiv	`resume` genau einmal, in Endposition	`Alloc`, `Db`, `Fs`, `Api`	Indirekter Call
Abortiv	`resume` nie	`Throw[E]`	Stack-Unwinding
Allgemein	`resume` später, mehrfach oder gespeichert	Generatoren, Backtracking, async	Continuation-Capture

Regel A-4. Phase 1 unterstützt ausschließlich tail-resumptive und abortive Handler. Allgemeine Resumption wird vom Checker mit eigener Diagnostik abgelehnt.

Tail-Resumption lässt sich zu einem gewöhnlichen Funktionsaufruf senken, ohne die Fortsetzung einzufangen. Abortive Handler brauchen Unwinding, das für release auf Fehlerpfaden ohnehin existiert (IR: WithScope). Allgemeine Resumption verlangt, dass ein Stück des Aufrufstapels kopiert und wiederhergestellt werden kann; das berührt Frame-Layout, Call/Return und den Scheduler.

A-4 zahlt sich zweimal aus: billig zur Laufzeit und ohne neue Syntax — ohne die Beschränkung bräuchte es eine handle-Form mit explizitem resume. Die Beschränkung ist additiv aufhebbar.

4. Fehler als Service: `Throw[E]`¶

4.1 Motivation und Form¶

Zigs Fehlermengen und die Effect Row haben dieselbe Algebra: beides sind Mengen, beide vereinigen sich bei Komposition, beide erlauben Teilmengen-Coercion. error{A} passt in error{A,B} wie ->{} in ->{Db} passt. Der Fehlerkanal ist also kein Fremdkörper in der Row, sondern ein Spezialfall dessen, was sie ohnehin tut.

Regel E-1. Jeder Fehlertyp ist ein eigenes Row-Element Throw[E], keine Menge innerhalb eines Service-Parameters.

def loadConfig(p: Path) ->{Fs, Throw[NotFound], Throw[Malformed]} Config

Damit ist die Row-Vereinigung die Fehlermengen-Vereinigung; es gibt keinen zweiten Mengenmechanismus.

service Throw[e] {
    def throw(err: e) -> Never
}

Zwei Vorteile gegenüber Zigs Modell:

Nutzlasten. Zigs Fehler sind flache Tags ohne Daten — man kann dort nicht „Datei nicht gefunden: /etc/foo.conf" sagen, ohne Out-Parameter oder Seitenkanal. Hier ist der Fehlertyp Tag und Nutzlast, weil eine Service-Operation Argumente hat.
Glücklicher Pfad. Zig zahlt an jeder try-Stelle einen Branch. Ein abortiver Handler kostet nichts, solange nicht geworfen wird; der Preis fällt erst beim Unwinding an.

Was aufgegeben wird — bewusst. Zigs try macht an jeder Stelle im Rumpf sichtbar, wo die Funktion aussteigen kann. Mit Throw als Service verschwindet das: Der Aufruf einer Funktion, die intern wirft, ist syntaktisch unauffällig. Bei Db.query(...) ist das kein Problem, weil der Service-Name im Aufruf steht; bei geworfenen Fehlern steht er nicht da. JDL tauscht damit Aufrufstellen-Sichtbarkeit gegen Signatur-Sichtbarkeit.

Never ist der Bottom-Typ, damit throw in beliebiger Position typprüft.

4.2 `catching` materialisiert `Result`¶

Result[T, E] verschwindet nicht — es hört auf, ein Rückgabetyp-Mechanismus zu sein, und wird zu dem, was ein abortiver Handler produziert:

// spekulativ
def catching[T, E, g](body: () ->{g, Throw[E]} T) ->{g} Result[T, E]

Regel E-2. Ob ein Fehler Kontrollfluss oder Wert ist, entscheidet die Aufrufstelle, nicht der Autor der Funktion.

Das ist der Kern der Vereinfachung gegenüber v0.2, wo E in zwei Kodierungen existierte und Umwandlungsregeln zwischen ihnen nötig gewesen wären.

4.3 Verhältnis zu Trap und Abbruch¶

JDL kennt vier Fehlschlagsarten. Ihre Abgrenzung war in v0.2 nicht formuliert und wird hiermit festgehalten:

Art	Fangbar	Ort
`Option`-Abwesenheit	n/a — kein Fehlschlag	Wert
`Throw[E]`	ja, über Handler	Sprachebene
Trap	nein	Engine; invalidiert laut Constitution den lokalen Scope
Abbruch	nein	Prozessende (Verifier-Korruption o. Ä.)

Regel E-3. Ein Trap ist auf Sprachebene nicht fangbar und lässt sich nicht in ein Result verwandeln. Trap-Behandlung ist Sache der Engine, nicht des Nutzercodes.

Ohne diese Regel wäre der Unterschied zwischen Fehler und Trap fließend.

4.4 Offen: Fehleridentität¶

Zigs Fehlermenge ist global — error.NotFound aus zwei Bibliotheken ist derselbe Fehler. Das ist bequem für Interop und riskant für Kollisionen. Bei nominaler Identität wären es zwei verschiedene Typen.

Für JDL ist nominale Identität der Default, aber die Entscheidung ist nicht getroffen. Zu bedenken: Fehler, die über Netzgrenzen wandern, brauchen ohnehin eine stabile Kennung — vermutlich denselben Fingerprint-Mechanismus, den die Plugin-Spec für Interfaces vorsieht. Siehe §11.

5. Allokation als Service: `Alloc[A]`¶

5.1 Warum Allokation ein Effekt ist¶

Eine Allokation verändert globalen Zustand und kann fehlschlagen. Sie ist damit nach der Definition aus §6.1 ein Seiteneffekt und gehört in die Row. Das folgt Zigs Philosophie, Allokatoren explizit zu machen — mit einem Unterschied, der zugunsten von JDL ausfällt.

Was die Service-Form Zigs Parameter-Ansatz voraushat: austauschbare Fehlerpolitik ohne Codeänderung. In Zig ist alloc fallibel, Punkt — jede Allokationsstelle trägt ein try. Für JDL wäre das ergonomisch untragbar, weil dann jedes Struct-Literal fehlschlagen kann. Als Service lässt sich stattdessen der Default-Handler trappend auslegen und im JadeOS-Kernel oder auf eingebetteten Zielen ein Handler installieren, der Result liefert — derselbe Code, anderer Handler.

Regel M-1. Der Default-Handler für Alloc[A] trappt bei Erschöpfung. Fallibilität ist eine Handler-Entscheidung, keine Eigenschaft der Operation.

Begründung: Andernfalls wanderte Result in jede Konstruktion zurück — und damit =? durch die Hintertür, das mit v0.3 gerade entfallen ist.

5.2 Typgeankerte Auflösung statt Namensauflösung¶

Alloc unterscheidet sich grundlegend von Db, Fs und Api:

	nutzeraufgerufen	compiler-aufgerufen
Beispiel	`Db`, `Fs`, `Api`	`Alloc`
Auslöser	`Db.query(sql)` im Quelltext	`Point { x: 1, y: 2 }`
Qualifikation möglich?	ja — der Aufruf existiert	nein — es gibt keine Aufrufstelle
Auflösung	Eindeutigkeit in der Row (§3.2), sonst explizit	über den Typ

Bei zwei Arenen in der Row — ->{Alloc[ReqArena], Alloc[FrameArena]} — könnte ein Struct-Literal nicht sagen, welche es meint. Bei nutzeraufgerufenen Services entsteht diese Frage nie.

Regel M-2. Die Zielarena einer Allokation ergibt sich aus der memory-Policy des allozierten Typs, nicht aus dem Handler-Stack.

tag ReqArena

type Report: struct {
    lines: [str]
    total: i64
} <{ memory: arena[ReqArena] }>

def buildReport() ->{Db[Replica], Alloc[ReqArena]} Report {
    val rows = Db.query("SELECT * FROM events")
    Report { lines: rows |> map(fmtRow), total: rows |> length }
}

Das Alloc[ReqArena] in der Signatur steht dort nicht, weil der Rumpf es erwähnt — es wird aus Reports memory: arena[ReqArena] hergeleitet und gegen die Deklaration geprüft. Kein Raten, keine Innermost-wins-Dynamik, und die Row bleibt eine Prüfung statt einer Wahl.

Als Nebenwirkung fällt eine Invariante heraus, die sonst separat erzwungen werden müsste: Ein Wert mit InArena(A) kann gar nicht anders als aus Alloc[A] stammen.

Lackmustest für zukünftige Services: Wer sie nicht aufrufen kann, ohne dass der Compiler es für ihn tut, braucht einen typseitigen Anker statt einer Namensauflösung.

5.3 Arenapolymorphie¶

Der Fall, für den sich die Tag-Parametrisierung überhaupt erst auszahlt:

def build[a](...) ->{Alloc[a]} Buf[a]

Eine Funktion, die in irgendeiner Arena baut, entschieden vom Aufrufer. Mit einem flachen Alloc-Service und Laufzeitauswahl wäre das nicht ausdrückbar.

5.4 Escape-Regeln¶

Ein Arena-Scope muss verhindern, dass Werte ihn überleben — nach dem Reset zeigte sonst alles ins Leere.

Regel M-3. Für Arena-Werte gilt dieselbe positionale Escape-Regel wie für Borrows: nicht in Rückgabeposition, nicht in Structfeldern, rein positional, keine Lifetime-Variablen.

Das ist ausdrücklich dieselbe Maschinerie, keine zweite. Bemerkenswert am Rande: Kokas scope-sichere named handlers brauchen Rang-2-Polymorphismus, weil dort kein anderer Mechanismus gegen Entkommen existiert. JDLs Ownership-Modell hat einen; falls dynamische Service-Instanzen später gebraucht werden (§11), könnte das die teuerste Zutat des Ansatzes ersparen.

5.5 Offen: temporäre Werte¶

In rows |> map(fmtRow) entsteht ein Zwischenergebnis, das zu keinem deklarierten Typ mit memory-Policy gehört. Aus welcher Arena kommt es? Regel M-2 beantwortet den Fall Report, nicht den Fall Temporäre.

Denkbare Antworten: dieselbe Arena wie das umschließende Ziel; eine Default-Policy für unannotierte Werte; oder — am schärfsten — Temporäre sind registerresident und allozieren gar nicht, was bei [str] allerdings nicht mehr trägt.

Das ist die nächste zu treffende Entscheidung, und sie betrifft praktisch jede Zeile Stdlib-Code. Siehe §11.

6. Reinheitslabels¶

6.1 Labels sind abgeleitet, nicht setzbar¶

04-axiomatik §2.1 legt fest: Alles, was dem Compiler Rechte gibt — Optimierung, Reordering, Parallelisierung, Retry, Caching —, muss sealed/derived sein. Setzbar sind nur einschränkende Policies und Absichten.

Regel P-0. Pure und Deterministic sind abgeleitete Labels. Sie entstehen ausschließlich in der TruthProfile-Closure (04-axiomatik §5.2) und können nicht per Refinement gesetzt werden.

Eine setzbare Absicht im Stil von WantsRetry ist zulässig; sie ersetzt niemals den Beweis.

6.2 Wo die Row im TruthProfile liegt¶

04-axiomatik §5.1 sieht für parametrisierte Wahrheiten ausdrücklich „Bit + Payload" vor und nennt „Effect-Set/Deps" als Payload-Beispiel. Die Effect Row braucht also keinen neuen Mechanismus:

exec_bits    Pure, Deterministic, Fallible, Concurrent, ...   (abgeleitet)
payload      row: Set[ServiceRef]                             (Effect Row)

Die Closure-Regeln lesen den Payload und setzen daraus Bits.

6.3 Die beiden Labels¶

Regel P-1. Pure gilt, wenn (a) die Row leer ist, (b) kein Parameter RefMut[T] oder Out[T] ist, und (c) die Entscheidungen aus §6.5 erfüllt sind.

Regel P-2. Deterministic gilt, wenn die Row höchstens Alloc[_] enthält und (b) aus P-1 erfüllt ist.

Als Closure-Regeln im Stil von 04-axiomatik §2.2:

row(T) = ∅        ∧ no_refmut(T) ∧ no_out(T)  ⇒  Pure
row(T) ⊆ {Alloc}  ∧ no_refmut(T) ∧ no_out(T)  ⇒  Deterministic
Pure                                           ⇒  Deterministic
Throw[_] ∈ row(T)                              ⇒  Fallible
Fallible ∧ Pure                                ⇒  Retryable          (bereits normiert)

Die letzte Regel steht schon in 04-axiomatik §2.2 und muss nicht neu erfunden werden — sie bekommt durch die Row nur eine präzise Prämisse: Fallible ist jetzt entscheidbar als „Throw[_] ist Element der Row".

Warum zwei Labels. Query-Caching ist korrekt, wenn eine Query deterministisch ist — nicht, wenn sie allokationsfrei ist. Ein Query-Handler, der eine Liste aufbaut, bleibt cachebar. Mit Alloc als Effekt wäre er nicht mehr Pure, und das Label, das die Soundness des Caches begründet, wäre das falsche.

Pure ist damit das starke Label — das, was JadeOS für allokationsfreie Pfade und Interrupt-Handler braucht. Deterministic ist das alltägliche.

Ehrliche Folge: Nach Einführung von Alloc ist fast die gesamte Stdlib ->{Alloc[_]}. In ->{} bleiben Arithmetik, Vergleiche, Feldzugriffe und Pattern-Matching auf registerresidenten Werten. Das ist keine Verwässerung, sondern die Wahrheit, die vorher unsichtbar war — aber Pure wird selten, und die alltäglichen Garantien müssen deshalb an Deterministic hängen.

6.4 Was das für den Proof Trace ändert¶

Der Proof-Trace hält laut 04-axiomatik §5.1 für jedes abgeleitete Label „Regel + Prämissen + Herkunft" fest. Vor der Row hätte die Prämisse für Pure aus dem Rumpf inferiert werden müssen: jeden Aufruf transitiv verfolgen, mit Fixpunkt bei Rekursion.

Jetzt ist die Prämisse eine Signaturaussage, und die Prüfung ist lokal — ein Teilmengentest pro Aufrufstelle gegen die Deklarationen der Callees. Der Beweiseintrag wird damit eine Ebene tief statt transitiv:

Label:     Pure
Regel:     row(T) = ∅ ∧ no_refmut(T) ∧ no_out(T) ⇒ Pure
Prämissen: row(loadUser) = ∅            [deklariert, users/service.jdl:14]
           callees ⊆ ∅                  [3 Aufrufstellen, je Teilmengentest]
           keine RefMut/Out-Parameter

Für die CompilerDB folgt daraus: Eine Rumpfänderung invalidiert die Reinheit der Aufrufer nicht mehr — nur eine Signaturänderung tut das. Die Purity-Query hängt an Deklarationen statt an Bodies und cacht eng.

6.5 Was die Row nicht sieht¶

Drei Lücken müssen entschieden werden, sonst gelten sie im Trace stillschweigend als bewiesen:

Divergenz. Eine ->{}-Funktion darf ewig schleifen. Impliziert Pure Terminierung, liefert die Row das nicht.
Traps. Mit overflow: Trap kann eine ->{}-Funktion trappen. Die meisten Effektsysteme zählen das nicht als Effekt; die Axiomatik darf anders entscheiden.
Mutation durch Parameter. def bump(c: RefMut[Counter]) ->{} () behauptet {} und ist trotzdem ein für den Aufrufer beobachtbarer Seiteneffekt.

Für die dritte Lücke wurden zwei Wege erwogen:

A — Mutation wird selbst zum Service (wie Kokas Heap-Effekte). Dann bedeutet ->{} wirklich rein. Preis: jede lokale Pufferbearbeitung erscheint in Signaturen.
B — Pure ist eine Konjunktion über zwei orthogonale Achsen. Die Effektachse sitzt im Pfeil, die Besitzachse in den bestehenden Wrappern Ref/RefMut/Move/Out (04-axiomatik §7.1).

Gewählt ist B (so kodiert in P-1). Das entspricht der Dreiteilung der fundamentalen Wahrheiten aus 04-axiomatik §1.4: Speicher-, Besitz- und Ausführungswahrheiten bleiben orthogonal. Die Row ist eine Ausführungswahrheit; RefMut ist eine Besitzwahrheit. Sie zu vermischen hieße, genau die Trennung aufzugeben, vor der §1.4 warnt.

6.6 Was Parameter dürfen¶

Die Beschränkung liegt nicht auf den Parametertypen, sondern darauf, was der Rumpf tut.

def apply(f: (i32) ->{Db} i32, x: i32) ->{} i32 = f(x)          // Fehler
def hold(f: (i32) ->{Db} i32) ->{} ((i32) ->{Db} i32) = f       // zulässig

hold ist ehrlich rein. Praktisch relevant: Ein Scheduler, der effektbehaftete Tasks sortiert oder auswählt, ohne sie auszuführen, ist legitim ->{}.

Regel P-3. Ein effektbehafteter Funktionswert darf angenommen, gespeichert und zurückgegeben werden. Nur sein Aufruf verlangt die entsprechenden Elemente in der Row.

7. Lowering und Laufzeitdarstellung¶

7.1 Die Row wird gelöscht¶

Regel L-1. Die Effect Row ist ein reines Übersetzungszeit-Artefakt. Sie erscheint nicht im Bytecode, nicht im Registerfile und in keiner Laufzeitstruktur der VM.

Es gibt keine EffectRow-Struktur im Zig-Code und kein Feld dafür im Instruktionsformat. Was Laufzeitdarstellung braucht, sind nicht die Rows, sondern die Handler.

7.2 Evidence Passing¶

Zwei Ansätze standen zur Wahl:

Dynamische Suche — ein Handler-Stack in der Runtime, bei jeder Operation aufwärts durchsucht. Verlangt neue Opcodes (PushHandler, PopHandler, Perform) und kostet bei jedem Aufruf eine Suche.
Evidence Passing — der Handler wird zur Übersetzungszeit aufgelöst und als versteckter Parameter durchgereicht. Ein Service-Aufruf wird zu einem gewöhnlichen indirekten Call durch einen Registerwert.

Regel L-2. JDL verwendet Evidence Passing.

Begründung: Die Effektmenge steht bereits in der Signatur, also weiß der Compiler an jeder Aufrufstelle exakt, welche Handler im Umlauf sind. Die Information für die statische Auflösung ist vorhanden; eine Laufzeitsuche würde sie wegwerfen und neu beschaffen.

7.3 Keine neuen Core-Instruktionen¶

Regel L-3. Services erfordern keine Erweiterung des Instruktions-Core.

Handler-Installation → Closure + Call
Service-Aufruf → indirekter Call durch ein Feld des Evidence-Records
Abortiver Handler → das bestehende Unwinding (dasselbe, das release auf Fehlerpfaden trägt)

Zulässig ist Extended-Zucker, der vor dem Lowering eliminiert wird. Dass diese Regel hält, ist eine direkte Folge von A-4 (§3.6): Ohne allgemeine Resumption wird keine Continuation-Capture gebraucht.

7.4 Wo der Code liegt¶

Artefakt	Ort	Begründung
Evidence-Record-Layout, Unwinding	Zig, dauerhaft	Stack-Manipulation; gehört zur Ausführungsschleife
Row-Unifikation, Teilmengenprüfung, Handler-Auflösung, Aufbau der Evidence-Vektoren	JDL, Stdlib-Ebene	Compiler-Pässe, also Teil der ~90 %
Effect Row in Modul-Metadaten	Persistent, versioniert	Ein Aufrufer in einem anderen Modul muss die Row prüfen können, ohne den Rumpf zu sehen

Die JDL-Seite muss auf Stdlib-Ebene liegen: Eine Row als Datenstruktur braucht Structs und Collections, und beides verbietet der Bootstrap-Checker.

7.5 Folgen für den Bootstrap Seed¶

Alloc wird während Constructed → Seeded gebraucht, weil der Aufbau der Deskriptortabellen alloziert. Zu diesem Zeitpunkt existiert keine JDL-Handler-Maschinerie.

Zwei Dinge müssen daher vorher da sein:

Ein Wurzel-Handler, gesetzt vom BootstrapInitializer — nicht in JDL geschrieben.
Eine stabile ID. Jede Signatur, die später ->{Alloc[ReqArena]} trägt, verweist auf etwas; beim Laden eines Stdlib-Moduls muss dieser Verweis auflösbar sein.

Der zweite Punkt ist der weniger offensichtliche und folgt genau aus §5.2: Bei Db schreibt der Nutzer den Namen, Db kann also eine gewöhnliche Stdlib-Deklaration sein. Bei Alloc erzeugt der Compiler den Verweis. Damit steht Alloc in derselben Kategorie wie Option und Result — im Seed, weil die Sprache selbst darauf verweist.

Regel S-1. Der Bootstrap Seed erhält eine neue Kategorie: Core-Service-IDs.

11-bootstrap-seeding-praegung/ §11 zählt zulässige Seed-Inhalte auf — Abilities sind nicht dabei, weil es sie beim Entstehen des Abschnitts nicht gab. Das ist eine echte Schema-Änderung: schemaVersion muss hoch, alte Seeds sind mit der neuen VM inkompatibel, der Seed muss neu erzeugt werden. Genau dafür bleibt die schlanke Zig-Referenzimplementierung bestehen.

Vorschlag für §15 der Seed-Spec: Jedes Sprachfeature, bei dem der Compiler ohne Zutun des Nutzers auf ein benanntes Ding verweist, braucht einen Seed-Eintrag — und damit eine Schemaversion.

Querschnittsbelange gehören ins Meta-Record – nicht in die Logik. Die Funktion beschreibt was sie tut, das Refinement wie sie sich verhält.

Gegenüber v0.2 ändert sich hier weniger als erwartet: Refinements waren nie an Effect[R, E, D] gebunden, sondern an das Meta-Record. Was sich ändert, ist ihre Implementierung — sie wickeln den Rumpf jetzt in eine suspendierte Berechnung (§2.6) statt einen Effect-Wert zu transformieren — und ihr Verhältnis zur Row (§8.5).

8.1 Cache¶

type CachePolicy: enum = | Always | Ok | Err

type CacheConfig: struct {
    ttl:  Duration
    only: CachePolicy = CachePolicy.Always
}

typefn Cache(config: CacheConfig) = <{ cache: config }>

def getCachedUser(id: UserId) ->{UserDb, Throw[UserError]} User =
    UserDb.getUserById(id)
:> Cache(CacheConfig { ttl: 24.hours, only: Ok })

Cache-Key wird automatisch generiert: Funktionssignatur als Namespace, Hash der Parameter als Schlüssel. Parameter müssen Hashable implementieren – der Compiler prüft das statisch.

Die Policy only: Ok bezieht sich jetzt auf Throw[E]: Nur Läufe, die nicht geworfen haben, werden abgelegt.

8.2 Retry¶

type BackoffStrategy: enum = | Constant | Linear | Exponential

type RetryConfig: struct {
    max:     u32
    backoff: BackoffStrategy = BackoffStrategy.Exponential
    delay:   Duration        = 100.ms
}

typefn Retry(config: RetryConfig) = <{ retry: config }>

8.3 Timeout¶

type TimeoutConfig: struct {
    after: Duration
}

typefn Timeout(config: TimeoutConfig) = <{ timeout: config }>

8.4 Transactional¶

Transactional macht eine Funktion zur atomaren Einheit.

def persistUserAndAudit(user: User) ->{UserDb, AuditLog, Throw[AppError]} User {
    val saved = UserDb.insert(user)
    AuditLog.write(saved.id)
    saved
}
:> Transactional

Gegenüber v0.2 fällt hier das =? weg: Wirft UserDb.insert, wird AuditLog.write nie erreicht.

Neu in v0.3, weil es vorher nicht ausdrückbar war:

Regel F-1. Ein Refinement, das den Rumpf mehrfach ausführen kann (Retry), verlangt, dass die Row keinen Service enthält, deren Wiederholung unzulässig ist. Die Diagnostik nennt das verletzende Element.

Regel F-2. Cache über einer Funktion mit nichtleerer Row ist zulässig, aber eine bewusste Entscheidung: Der Cache liefert dann einen Wert, ohne die Effekte erneut auszulösen. Der Effektsatz der Funktion erscheint in der Diagnostik.

Regel F-2 ist bewusst erlaubend formuliert — das Cachen eines ->{Db}-Lesezugriffs ist ein legitimes Muster, aber es tauscht Aktualität gegen Geschwindigkeit, und diese Wahl sollte sichtbar sein. Die scharfe Variante wäre, Cache auf Deterministic (§6.1) einzuschränken; das ist eine offene Entscheidung, siehe §11.

8.6 Komposition¶

def robustGetUser(id: UserId) ->{UserDb, Throw[UserError]} User =
    UserDb.getUserById(id)
:> Cache(CacheConfig { ttl: 1.hour, only: Ok })
:> Retry(RetryConfig { max: 3 })
:> Timeout(TimeoutConfig { after: 5.seconds })

Reihenfolge der Ausführung: Timeout → Retry → Cache → Funktion. Der Compiler legt die Reihenfolge fest – nicht der Entwickler.

8.7 Implizite Transaktionalität¶

Sequenzieller Code ist bereits implizit transaktional, weil ein Wurf abbricht:

def handleRequest(req: HttpRequest) ->{AuthService, UserDb, Throw[AppError]} User {
    val token = authenticate(req)
    val input = validate(token)
    val data  = transform(input)
    UserDb.persist(data)
}

UserDb.persist wird nie erreicht, wenn ein vorheriger Schritt wirft. Transactional ist nur nötig, wenn mehrere persistierende Operationen zusammen atomar sein müssen.

9. Deklarative Runtime¶

9.1 Was sich ändert¶

Die Substanz dieses Abschnitts ist unberührt. Eine Rolle verschiebt sich jedoch: Der CallGraph war in v0.2 die Effect-Engine — „der einzige Ort, wo Effect-Beschreibungen zu Ausführungen werden". Das gilt nicht mehr, weil es keine Beschreibungen gibt, die interpretiert werden müssten.

Regel D-1. Der CallGraph ist kein Interpreter mehr, sondern ein deklarativer Ort der Handler-Installation. Die Grenze zwischen „läuft nicht" und „läuft" ist der Handler, nicht der Graph.

CallGraph app(req: HttpRequest) ->{Throw[AppError]} HttpResponse {
    requires: [UserDb, LogService]
    env: {
        UserDb:     PostgresUserDb { pool }
        LogService: ConsoleLogger {}
    }

    handleRequest(req)
}

Der requires-Block ist damit eine Redundanz zur Row von handleRequest — er kann entweder entfallen oder als geprüfte Zusicherung erhalten bleiben. Siehe §11.

9.2 Alles ist ein Dictionary¶

Jedes deklarative Konstrukt in JDL – CallGraph, Aktor, Workflow, UI-Komponente – ist zur Laufzeit ein composable Dictionary. Das ist die Laufzeit-Entsprechung der Compile-Zeit-Meta-Records:

Compile-Zeit:  <{ key: value }>   – Meta-Record, statisch
Laufzeit:      { key: value }     – Dictionary, dynamisch

Serialisierbarkeit ist damit eine strukturelle Eigenschaft, keine Feature-Anforderung. Komposabilität folgt direkt: neue deklarative Konstrukte brauchen kein neues VM-Konzept, nur bekannte Keys. Reflexion wird trivial. Reproduzierbarkeit ist garantiert.

9.3 Distributed Execution¶

Hot Deployment, Distributed Workflows und Remote Actors folgen aus der Serialisierbarkeit. Vorgesehen für Phase 2; Phase 1 lässt die Tür offen.

Neu zu klären: Ein serialisierter Graph trägt Verweise auf Services. Beim Deserialisieren auf einem anderen Node müssen diese Verweise auflösbar sein — das verlangt stabile Service-Kennungen über Prozessgrenzen hinweg, vermutlich denselben Fingerprint-Mechanismus wie für Fehleridentität (§4.4). Siehe §11.

9.4 Services, FFI und Handler¶

Services werden über Handler gebunden, nicht über native Symbole, Intrinsics oder RuntimeBus-Endpunkte. Eine FFI-Bindung kann einen Service implementieren, ist aber selbst kein Row-Element für normalen User-Code.

def loadUsers() ->{Db, Throw[DbError]} [User] =
    Db.query("select * from users")

Nicht zulässig als öffentliche API:

def loadUsers() ->{LibSQLite.sqlite3_exec, Throw[FfiError]} [User]

Die Schichtung lautet:

NativeFunction / extern
    -> FfiBindingEngine
    -> FfiCallDescriptor
    -> Handler / Service-Provide
    -> Service in der Row

Low-Level-Code in jade::ffi darf bewusst NativeFfi-Services exponieren. Normale Bibliotheken müssen eine idiomatische Service-Schicht anbieten, damit das Effektsystem nicht mit ABI-Details kontaminiert wird. C hat schon genug Möglichkeiten, einem Projekt die Möbel anzuzünden.

9.5 Schichtung¶

┌─────────────────────────────────────────────────────┐
│  Zig / Host                                         │
│  Ring-0-Substrate, Trust Anchor, Evidence-Layout,   │
│  Unwinding, Scheduler, JME                          │
│  kein Teil der JDL-Semantikschicht                  │
└──────────────────────┬──────────────────────────────┘
                       │ startet
┌──────────────────────▼──────────────────────────────┐
│  JDL – Deklarativer Stil                            │
│  CallGraph, Aktoren, Workflows, UI-Beschreibungen   │
│  installiert Handler, komponiert Graphen            │
│  "wie hängt alles zusammen"                         │
└──────────────────────┬──────────────────────────────┘
                       │ ruft
┌──────────────────────▼──────────────────────────────┐
│  JDL – Direkter Stil                                │
│  Funktionen mit Effect Row, Handler, Stdlib         │
│  "was passiert, und was es dafür braucht"           │
└─────────────────────────────────────────────────────┘

Gegenüber v0.2 fällt die mittlere Schicht („funktionaler Stil, Effect[R,E,D] als pure Beschreibung") weg. Kommunikation ist weiterhin strikt nach unten.

10. Normative Invarianten¶

Cast-System

provide ... from existiert nicht. Konversion läuft ausschließlich über CastTo[T].
.castTo() ohne expliziten Typparameter ist bei Mehrdeutigkeit ein Compile-Fehler.
Cast-Modi liegen auf der Implementierung, nicht auf dem Aufruf.
Konversionen sind nie transitiv.
Der Try-Modus trägt Throw[E] in der Row und gibt kein Result zurück.
Ein Funktionstyp hat immer eine geklammerte Parameterliste; der ungeklammerte Pfeil gehört ausschließlich dem Cast-Ausdruck (R-1/C-1).

Effect Row

Die Effektmenge steht zwischen Parameterliste und Rückgabetyp (R-2).
Eine fehlende Effektmenge bedeutet die leere Menge, nicht eine unbestimmte (R-3).
Die Row ist eine ungeordnete Menge; Komposition vereinigt, Abschwächung ist erlaubt, die Umkehrung nicht.
Effektinferenz ist modul-intern; an Modulgrenzen wird deklariert (R-4).
Effect[R, E, D] existiert nicht. Es gibt keinen Effect-Typkonstruktor und keine Effect-Kompositions-API.
=? existiert nicht.
Aufgeschobene Ausführung wird durch suspendierte Berechnungen () ->{g} T ausgedrückt, nicht durch einen Wrapper-Typ mit typgesteuertem impliziten Einwickeln.

Services (Abilities)

Was die Literatur Ability nennt, ist in JDL ein service. Es gibt kein eigenes Schlüsselwort dafür. protocol beschreibt Typverhalten, service eine Capability in Effektkontexten; die beiden sind nicht austauschbar.
Ein Service ist eine Forderung an den Kontext, kein Wert. Nutzercode kann einen Handler nicht als Wert erlangen; Runtime.getHandler entfällt (A-5).
Instanzen werden über Typ-Tags unterschieden, nicht über Slot-Namen. Der Tag steht in der Row und bei der Installation, nicht in der Handler-Definition.
Bei genau einem Element des gesuchten Service ist der Aufruf unqualifiziert zulässig (A-1); bei mehreren ist er ein Fehler (A-2); bei vorhandener Row-Variable ist Qualifikation verpflichtend (A-3). Es gibt keine „innerster Handler gewinnt"-Regel.
Handler werden mit provide Service[Handler] { ... } definiert — der dritten provide-Form, unverändert. Kein resume, kein Operations-Matching (Folge von A-4).
Handler werden über registerHandler (global), Runtime.withHandler (bereichsbegrenzt) oder env: (deklarativ) installiert. Alle drei sind bestehende Formen; keine neue Syntax.
Phase 1 unterstützt nur tail-resumptive und abortive Handler (A-4).
with expr as name { body } ist der Scopeable-Ressourcen-Scope und nicht die Handler-Installation. with lässt die Row unverändert; eine Installation entfernt ein Element.
withHandler ist Quellform, Evidence Passing ist Lowering. Eine Laufzeit-Handler-Map ist kein Auflösungsmechanismus für statisch bekannte Rows (A-6).
Services referenzieren keine nativen FFI-Symbole oder Intrinsic-Endpunkte.

Fehler

Jeder Fehlertyp ist ein eigenes Row-Element Throw[E] (E-1).
Ob ein Fehler Kontrollfluss oder Wert ist, entscheidet die Aufrufstelle über catching (E-2).
Ein Trap ist auf Sprachebene nicht fangbar und nicht in ein Result verwandelbar (E-3).

Speicher

Allokation ist ein Effekt Alloc[A].
Der Default-Handler für Alloc trappt; Fallibilität ist Handler-Entscheidung (M-1).
Die Zielarena ergibt sich aus der memory-Policy des Typs, nicht aus dem Handler-Stack (M-2).
Für Arena-Werte gilt dieselbe positionale Escape-Regel wie für Borrows (M-3).

Reinheit

Pure und Deterministic sind abgeleitete Labels aus der TruthProfile-Closure und nicht per Refinement setzbar (P-0).
Pure = leere Row ∧ kein RefMut/Out-Parameter ∧ §6.5 (P-1).
Deterministic = Row ⊆ {Alloc[_]} ∧ kein RefMut/Out-Parameter (P-2). Query-Caching hängt an Deterministic, nicht an Pure.
Die Effect Row liegt im TruthProfile als Payload, nicht als Bit; die Closure-Regeln lesen sie und setzen daraus exec_bits.
Effektbehaftete Funktionswerte dürfen angenommen, gespeichert und zurückgegeben werden; nur ihr Aufruf verlangt die Row-Elemente (P-3).

Lowering

Die Effect Row ist ein Übersetzungszeit-Artefakt und erscheint nicht zur Laufzeit (L-1).
Handler werden über Evidence Passing aufgelöst, nicht über eine dynamische Suche (L-2).
Abilities erfordern keine Erweiterung des Instruktions-Core (L-3).
Row-Unifikation und Handler-Auflösung liegen auf Stdlib-Ebene in JDL; Evidence-Layout und Unwinding dauerhaft in Zig.
Der Bootstrap Seed erhält die Kategorie Core-Service-IDs; das ist eine Schema-Änderung mit schemaVersion-Erhöhung (S-1).

Refinements und Runtime

Die Ausführungsreihenfolge von Refinements legt der Compiler fest.
Transactional impliziert atomares Rollback aller Operationen im Block.
Jedes deklarative Konstrukt ist zur Laufzeit ein composable Dictionary.
Serialisierbarkeit ist eine strukturelle Eigenschaft aller deklarativen Konstrukte.
Der CallGraph installiert Handler; er interpretiert keine Effektbeschreibungen (D-1).
Zig ist kein Bestandteil der JDL-Semantikschicht. Es stellt Ring-0-Substrate, Host-Integration und den Bootstrap-/Recovery-Pfad bereit.

11. Offene Punkte¶

11.1 Vor der Implementierung zu entscheiden¶

#	Frage	Warum jetzt
O-1	Temporäre und Arenen (§5.5) — aus welcher Arena kommt ein Zwischenergebnis ohne `memory`-Policy?	Betrifft praktisch jede Zeile Stdlib-Code
O-2	`with Storage.arena[A]` vs. Handler — geht der bestehende Arena-Scope im `Alloc`-Service auf, oder bleiben zwei Mechanismen?	Zwei Wege zum selben Ziel; die Arena-Crossing-Regeln hängen daran
O-4	Mehrfachaufruf von Thunks — darf ein Thunk-Parameter mehrfach laufen, und steht das im Typ? Bei `Retry` ist es der Sinn, bei einem Handler-Body ein Fehler. Rust trennt `FnOnce`/`Fn`; hier fällt es womöglich aus den Move-Regeln	Muss vor der Trailing-Block-Grammatik feststehen
O-5	Fehleridentität (§4.4) — nominal oder global wie Zig?	Betrifft Interop und Wire-Format
O-6	Divergenz und Trap in `Pure` (§6.3) — impliziert `Pure` Terminierung? Bricht ein Trap die Reinheit?	Der Proof Trace behauptet sonst Ungeprüftes
O-7	Row-Polymorphie in Feldpositionen — `type Job: struct { run: () ->{Db} () }`. Rows wandern damit in Datentypen, nicht nur in Signaturen	Der Punkt, an dem Row-Systeme erfahrungsgemäß kompliziert werden

11.2 Für Phase 2¶

Dynamische Service-Instanzen — Tags sind statisch. Für zur Laufzeit erzeugte Instanzen (Verbindungspools, first-class Referenzen) bräuchte es named handlers mit Escape-Sicherung. Koka löst das über Rang-2-Polymorphismus; JDL hat mit M-3 möglicherweise bereits einen ausreichenden Mechanismus.
Allgemeine Resumption — Aufhebung von A-4; erfordert Continuation-Capture und berührt Frame-Layout, Call/Return und Scheduler.
requires-Block im CallGraph (§9.1) — entfällt als Redundanz oder bleibt als geprüfte Zusicherung?
Cache und Deterministic (§8.5) — soll Cache auf deterministische Funktionen eingeschränkt werden?
Stabile Service-Kennungen über Prozessgrenzen (§9.3) — Voraussetzung für Hot Deployment serialisierter Graphen.
CircuitBreaker als weiteres Funktions-Refinement.
Dictionary-Schema-Validierung zur Laufzeit.
Netzwerk-Transport-Protokoll für serialisierte Graphen.
Hot-Deployment-Semantik und Sicherheitsmodell.
Formale Definition der Grenzen zwischen jdl- und jade-Namespace.

11.3 Erledigt gegenüber v0.2¶

E existierte zweimal (Result[R,E] und Effect[R,E,D]) und hätte Umwandlungsregeln gebraucht. Jetzt: ein Kanal, ein Umwandlungspunkt (catching), an der Aufrufstelle gewählt.
Verhältnis von Fehler, Trap und Abbruch war nicht formuliert. Jetzt: E-3.
NewStruct hatte keinen Arena-Operanden; welche Arena zur Laufzeit gemeint war, blieb unbestimmt. Jetzt: M-2 verankert es am Typ.
Ein eigenes Schlüsselwort für Handler-Installation wurde erwogen und ist nicht nötig: provide, registerHandler, Runtime.withHandler und env: decken Definition und alle drei Installationsreichweiten ab (§3.6, §3.7).
Die Vorbedingung für Retry musste nicht neu erfunden werden — Fallible + Pure ⇒ Retryable steht bereits in 04-axiomatik §2.2. Die Row macht Fallible entscheidbar.
Wer die erste JDL-Stdlib übersetzt, ist in jdl-engine-descriptor-model §9 bereits normiert: Drei-Stufen-Bootstrap mit Seed-Dialekt in Stage 1, Ring-1-Engines in Stage 2, JDL-Compiler als Normalpfad in Stage 3, D-Bootstrap als Trust Anchor und Recovery Path.

Anhang A — Vollständiges Beispiel¶

// spekulativ — dient der Anschauung, nicht als normative Syntax

tag Primary
tag Replica
tag ReqArena

service Db[i] {
    def query(sql: str) -> [Row]
    def exec(sql: str)  -> u64
}

provide Db[PostgresHandler] {
    def query(sql: str) ->{Net} [Row] = Net.request(url, sql) |> parseRows
    def exec(sql: str)  ->{Net} u64   = Net.request(url, sql) |> affected
}

type Report: struct {
    lines: [str]
    total: i64
} <{ memory: arena[ReqArena] }>

// Eine Instanz in der Row → unqualifizierter Aufruf
def loadEvents() ->{Db[Replica], Alloc[ReqArena]} [Row] =
    Db.query("SELECT * FROM events")

// Zwei Instanzen → Qualifikation verpflichtend
def refreshAndLoad(id: UserId) ->{Db[Replica], Db[Primary], Alloc[ReqArena]} [Row] {
    Db[Primary].exec(f"UPDATE seen SET at = now() WHERE id = {id}")
    Db[Replica].query(f"SELECT * FROM events WHERE user = {id}")
}

// Alloc taucht im Rumpf nicht auf — hergeleitet aus Reports memory-Policy
def buildReport() ->{Db[Replica], Alloc[ReqArena]} Report {
    val rows = loadEvents()
    Report { lines: rows |> map(fmtRow), total: rows |> length }
}

// Row-polymorpher Kombinator
def withRetry[T, g](body: () ->{g} T, n: u32) ->{g} T

// main tilgt die letzte Schuld: Row ist leer
def main(io: Io) -> ExitCode {
    Runtime.withHandler[Db[Primary]](PostgresHandler { url: cfg.primaryUrl }) {
    Runtime.withHandler[Db[Replica]](PostgresHandler { url: cfg.replicaUrl }) {
    Runtime.withHandler[Alloc[ReqArena]](ArenaHandler { size: 64.kib }) {
    Runtime.withHandler[Net](TcpHandler { io }) {

        withRetry(3) { buildReport() } |> render |> io.write
        ExitCode.Ok
    }}}}
}

Für flache Fälle ist die deklarative Form lesbarer:

CallGraph app() ->{Throw[AppError]} () {
    env: {
        Db[Primary]:     PostgresHandler { url: cfg.primaryUrl }
        Db[Replica]:     PostgresHandler { url: cfg.replicaUrl }
        Alloc[ReqArena]: ArenaHandler { size: 64.kib }
        Net:             TcpHandler { io }
    }

    withRetry(3) { buildReport() } |> render |> io.write
}

Der Abbau der Row über die Handler-Kette:

buildReport()                            ->{Db[Replica], Alloc[ReqArena]}
  withHandler[Db[Replica]](postgres)     ->{Net, Alloc[ReqArena]}
  withHandler[Alloc[ReqArena]](arena)    ->{Net}
  withHandler[Net](tcp)                  ->{}

Anhang B — Herkunft der Designentscheidungen¶

Entscheidung	Vorbild	Abweichung in JDL
Effekte im Pfeil, `I ->{A} O`	Unison, Frank	—
Leere Menge = leer	Unison	Frank liest sie als ambient/polymorph
Row-Variable explizit	Unison	Frank macht sie implizit
Keine „innerster Handler gewinnt"-Regel	—	Koka erlaubt doppelte Labels via scoped labels
Instanzen über Typ-Tags	—	Koka/Effekt nutzen named handlers als Werte
Evidence Passing	Koka	—
Nur tail-resumptiv + abortiv in Phase 1	Koka, Effekt (als Optimierung)	Hier als Beschränkung, nicht als Optimierung
Fehler als Mengenelement	Zig (`error{...}`)	Zigs Fehler sind flach ohne Nutzlast; hier mit
Explizite Allokatoren	Zig	Dort Parameter, hier Service mit Handler-Politik
Escape-Sicherung über Positionsregel	—	Koka braucht dafür Rang-2-Polymorphismus