Zum Inhalt

JDL — Effect Rows, abortive Fehler und Throw-Semantik

Status: Konsolidierte Arbeitsnotiz, Orientierungsgrundlage Version: 0.1.0 Datum: 2026-09-05 Bezug: jdl-row-throw-review-brief.md (GPT-5.6 Sol), Gegenprüfung Befunde A–H, antwort-an-claude-row-throw-konsolidierung.md Quellen: 07-cast-effekte-refinements.md v0.3, jdl-sprachreferenz.md v0.1.0, 04a-label-inferenz-regeln.md, 04-axiomatics-truthprofile.md, 02-typsystem.md, 03-runtime.md, 05-vm-instruction-set.md, 06-generator-und-code-emission-v2.md, 13-ir-spec.md

0. Über dieses Dokument

0.1 Kennzeichnung

Marke Bedeutung
[N] bestehend normativ belegt, Fundstelle genannt
[A] aus bestehendem Material ableitbar, aber nirgends ausgeschrieben
[O] offen
[D] neue Entscheidung dieser Konsolidierung

Jede [D]-Entscheidung, die eine bestehende Invariante aus 07 §10 ersetzt, nennt deren Nummer. Die Ersetzungstabelle steht in §12.2.

0.2 Prioritätsregel

Diese Notiz ist Arbeitsstand, keine Norm. Sie hat Vorrang vor 07 v0.3 und der Sprachreferenz nur an den Stellen, die sie ausdrücklich als [D] markiert. Überall sonst gelten die Quelldokumente.

0.3 Was hier keine Syntax ist

Syntaxbeispiele in dieser Notiz dienen der Anschauung. Wo eine Form noch nicht normiert ist, steht // spekulativ. Auf spekulative Formen wird keine Folgerung gestützt.

1. Zweck und Geltungsbereich

1.1 Was diese Notiz festlegt

Zwei Dinge, und alles, was zwingend daran hängt:

Die Effect Row ->{...} als allgemeines Sprachkonzept — ihre Algebra, ihre Handler-Semantik, ihr Verhalten unter Polymorphie.

Throw[E] als abortiven Fehlerkanal innerhalb dieser Row — Erzeugung, Propagation, Behandlung, Materialisierung, Verhältnis zu Result[T, E].

1.2 Was sie nicht behandelt

Nicht behandelt werden: Concurrency-Failure-Policies, Cancellation-Semantik, Mission-Control-Diagnostik, Wire-Format für Remote-Fehler, ABI-Details, konkrete Retry-Theorie.

Diese Themen berühren die Row, hängen aber an Entscheidungen, die hier nicht fallen. Sie kommen nur als Anschlussstelle vor.

1.3 Voraussetzungen, die noch fehlen

jdl-sprachreferenz §21 führt zwei Lücken vor allen anderen: Kontrollfluss — while, break, continue, return sind in keinem Quelldokument spezifiziert — und Pattern Matching — Destrukturierung, Guards und Exhaustiveness sind nicht normiert.

Beide sind Voraussetzung für eine vollständige try/catch-Spezifikation. Was ein return innerhalb eines try-Blocks tut, ist nicht beantwortbar, solange return nicht existiert.

Diese Notiz definiert deshalb für try/catch nur die semantische Beziehung zwischen Throw, Handler, Row-Elimination und Fehlerwert. Grammatik und Exhaustiveness-Regeln übernimmt die spätere Kontrollfluss- und Pattern-Spec.

2. Handlerklassen und Abortivität

Dieser Abschnitt steht vorn, weil §3 bis §10 daran hängen.

2.1 Das Problem: die Row war nicht ehrlich

Bisher galt: Handlerklassen sind Eigenschaften des Handlers (07 §3.8, jdl-sprachreferenz §8.8). Ein Handler ist tail-resumptiv, abortiv oder allgemein.

Daraus folgt ein Loch. Ein abortiver Handler bricht bis zu seiner Installationsstelle ab, nicht bis zum Aufrufer der Operation. Regel M-1 (07 §5.1) erlaubt ausdrücklich einen fehlbaren Alloc-Handler. Wirft der, werden alle Frames dazwischen abgeräumt — und deren Rows enthalten kein einziges Throw.

Damit war die Aussage „diese Funktion hat kein Throw in der Row, also kehrt sie zurück" falsch. Auf genau dieser Aussage ruhen aber Fallible, jede spätere Terminierungsgarantie und die Frage, an welchen Stellen der Generator Cleanup-Kanten emittieren muss.

2.2 Abortivität ist eine Eigenschaft der Operation [D]

Regel K-1. Eine Service-Operation ist abortiv, wenn ihr Rückgabetyp Never ist oder ihre Signatur einen abortiven Effekt deklariert. Andernfalls ist sie tail-resumptiv.

Der Mechanismus steckte schon in der Spec, nur unbenannt: 07 §4.1 deklariert def throw(err: e) -> Never. Der Rückgabetyp Never ist die Abortivitätsmarke — eine Operation, die nichts zurückgeben kann, setzt die Continuation ihres Aufrufers nicht fort.

Der Vorteil gegenüber der bisherigen Fassung: Die Klasse ist aus der Service-Deklaration ablesbar, nicht erst aus dem Handler. Der Aufrufer weiß beim Lesen der Signatur, was ihn erwartet.

Regel K-2. Handler bekommen keine Klasse. Ein Handler implementiert die Operationen seines Service und erbt deren Klasse. Ersetzt die Tabelle in 07 §3.8 und jdl-sprachreferenz §8.8.

2.3 Abortive Effekte gehören in die Operationssignatur [D]

07 §3.1 hält fest, dass Operationssignaturen innerhalb einer service-Deklaration keine Row tragen: Eine Operation ist eine Anfrage an die Umgebung, und welche Effekte bei ihrer Beantwortung anfallen, steht in der Signatur des Handlers.

Das stimmt für resumptive Effekte und ist für abortive falsch. Wenn eine Operation abbrechen kann, endet der Kontrollfluss des Aufrufers, nicht der des Handlers. Diese Information muss beim Aufrufer ankommen.

Regel K-3. Eine Operationssignatur darf abortive Effekte deklarieren. Sie und nur sie erscheinen in der Row des Aufrufers der Operation. Nicht-abortive Effekte des Handlers bleiben bei der Installationsstelle. Präzisiert 07 §3.1.

// spekulativ — Schreibweise der Operationsrow offen
service Db {
    def query(sql: str) ->{Throw[DbError]} [Row]
    def exec(sql: str)  ->{Throw[DbError]} u64
}

Damit trägt eine Funktion, die Db.query aufruft, {Db, Throw[DbError]} — nicht nur {Db}. Der Handler darf zusätzlich Net brauchen; das geht die Installationsstelle an, den Aufrufer nicht.

Die Aufteilung liest sich als: Was den Aufrufer abbricht, steht bei der Operation. Was der Handler zum Arbeiten braucht, steht beim Handler.

2.4 Handler-Bodies dürfen nicht heimlich abbrechen [D]

Regel K-4. Die Row eines Handler-Rumpfs darf keine abortiven Effekte enthalten, die nicht bereits in der Signatur der implementierten Operation deklariert sind. Formal: row(handler.op) \ declared(op) ist eine nicht-abortive Row (§3.5).

Ohne K-4 ist K-3 wirkungslos — ein Handler könnte an der Operationssignatur vorbei werfen und wäre wieder ein unsichtbarer Ausgang.

Was damit gewonnen ist: Die Row ist jetzt ehrlich.

Throw[_] ∈ effektive Row(f)   ⟺   f kann abortiv enden

Beide Richtungen. Das ist die Aussage, auf der §8 und §10 aufbauen können.

2.5 Was das M-1 kostet [D]

Regel M-1 (07 §5.1, Invariante 28) lautete: Der Default-Handler für Alloc[A] trappt bei Erschöpfung; Fallibilität ist eine Handler-Entscheidung, keine Eigenschaft der Operation. Das Versprechen war „derselbe Code, anderer Handler" — im JadeOS-Kernel ein Handler, der Result liefert.

Dieses Versprechen ist mit einer statischen Row nicht einlösbar. Ob eine Operation abbrechen kann, ist Teil ihrer Signatur und damit Teil jeder Row, die sie erreicht. Ein Handler kann das nicht nachträglich ändern, ohne die Row zur Lüge zu machen.

Regel M-1′. Erschöpfung von Alloc[A] trappt. Ersetzt M-1 (Invariante 28).

Konsequenz, offen benannt: Ein Ziel, das Allokationsfehler behandeln muss, braucht eine Operation, die das deklariert — und dann trägt jede allozierende Funktion Throw[OomError] in der Row. Das ist teuer und war genau der Grund für M-1.

Warum das trotzdem die bessere Seite des Tauschs ist: M-1 hat das Problem nicht gelöst, sondern versteckt. Der Abbruch fand statt; er stand nur nirgends. Ein sichtbarer teurer Vertrag ist einem unsichtbaren billigen vorzuziehen, besonders in einer Sprache, deren Constitution auf beweisbaren Grenzen aufbaut.

Die Beschränkung ist additiv aufhebbar. Falls JadeOS später einen fehlbaren Allokationspfad braucht, ist das eine zweite Operation oder ein zweiter Service, keine Änderung am Row-Modell.

2.6 Handlerklassen, korrigierte Fassung [D]

Klasse Bedingung Beispiele Kosten
Tail-resumptiv Rückgabetyp ≠ Never, keine abortiven Effekte deklariert Alloc, Fs, Api indirekter Call
Abortiv Rückgabetyp Never oder abortive Effekte deklariert Throw[E], Db.query Unwinding
Allgemein Continuation gespeichert, mehrfach oder später fortgesetzt Generatoren, Backtracking Continuation-Capture

Regel A-4′. Phase 1 unterstützt tail-resumptive und abortive Operationen. Allgemeine Resumption wird abgelehnt. Der einzige eingebaute abortive Effekt ist Throw[E]. Präzisiert A-4 (Invariante 20).

2.7 Throw ist kein Service [D]

07 §4.1 deklariert service Throw[e] { def throw(err: e) -> Never }. Das ist zirkulär — ein Service, dessen einzige Operation den Effekt erzeugt, der den Service benennt.

Regel E-1′. Throw[E] ist ein Row-Element, kein deklarierbarer Service. Es gibt keine service Throw-Deklaration und keinen Nutzer-Handler dafür. Der einzige Weg, ein Throw[E] zu erzeugen, ist der Ausdruck throw (§5.1); der einzige Weg, es zu eliminieren, ist catch (§7). Präzisiert E-1 (Invariante 24).

E-1 selbst bleibt unverändert: Jeder Fehlertyp ist ein eigenes Row-Element, keine Menge innerhalb eines Service-Parameters.

3. Row-Algebra

3.1 Elemente und Identität [N] 07 §2.3, §3.4

Eine Row ist eine ungeordnete Menge von Elementen. Ein Element ist entweder ein getaggter Service Db[Primary] oder ein Fehlerkanal Throw[E].

Zwei Elemente sind identisch, wenn Servicename und Tag beziehungsweise Fehlertyp identisch sind. Db[Primary] und Db[Replica] sind verschieden. Identität von Fehlertypen ist nominal, solange O-5 nicht anders entschieden ist — siehe §13.

3.2 Die vier Grundoperationen

Union bei Komposition [N] 07 §2.3:

{Db, Throw[A]} ∪ {Net, Throw[B]}  =  {Db, Net, Throw[A], Throw[B]}

Subset als Abschwächung [N] 07 §2.3: Eine Funktion mit kleinerer Row ist überall einsetzbar, wo eine größere erwartet wird. Die Umkehrung gilt nicht.

Difference als Elimination [A]: Eine Handler-Installation oder ein catch entfernt genau die Elemente, die es behandelt.

{Db, Throw[A], Throw[B]}  ⊖  {Throw[A]}  =  {Db, Throw[B]}

Diese Operation muss nicht als Nutzersyntax erscheinen, wird aber vom Solver gebraucht.

Normalisierung [A]: Duplikatfreiheit, Union-Verteilung nach §3.3, feste Ordnung für Vergleich und Fingerprint.

3.3 Union-Verteilung über Throw [D]

Strukturelle Uniontypen verteilen sich über Throw:

Throw[A | B]  ≡  Throw[A], Throw[B]

Nominale Typen tun das nicht. Ein Enum bleibt atomar:

type CheckoutError: enum {
    Unauthorized
    OutOfStock { sku: Sku }
}

bleibt Throw[CheckoutError] und zerfällt nicht in seine Varianten.

Regel Y-1. Throw verteilt über strukturelle Union, nicht über nominale Typen. Der Unterschied ist die Grenze zwischen „mehrere Fehlerkanäle" und „ein Fehlerkanal mit mehreren Fällen".

Das ist keine Sonderregel für Rethrow, sondern eine Typnormalisierung. Es beantwortet den Fall aus Befund E: Ein Catch-all, der einen Wert vom Typ A | B weiterwirft, erzeugt wieder {Throw[A], Throw[B]} und nicht Throw[A | B].

3.4 Normalisierung läuft nach der Substitution [D]

Y-1 hat eine Nebenwirkung. Enthält eine Row Throw[E] mit E als Typvariable, ist die Elementanzahl nicht bekannt — bei E := A | B werden aus einem Element zwei.

Regel Y-2. Eine Row mit Throw[V] für eine ungebundene Typvariable V gilt als nicht normalisiert. Normalisierung findet nach der Typsubstitution statt. Row-Vergleich, Unifikation und Fingerprint arbeiten nur auf normalisierten Rows.

Ohne Y-2 fällt der erste generische Rethrow auf die Nase.

3.5 Beschränkte Row-Variablen: nicht-abortive Rows [D]

Union, Subset, Difference und Normalisierung reichen nicht. Zwei Stellen erzwingen eine fünfte Fähigkeit.

Cleanup. Scopeable.release hat in 03-runtime §2 die Signatur -> (), also leere Row. Eine gepufferte Datei kann so nicht schließen; Flushen braucht Fs. Cleanup braucht also eine Row-Variable — darf aber nach §7.6 nicht abbrechen, sonst braucht die Sprache sofort Double-Fault-, Suppression- und Prioritätsregeln.

Handler-Bodies. K-4 verlangt dasselbe.

Regel Y-3. Das Row-System kennt eine Beschränkung von Row-Variablen auf nicht-abortive Rows: eine Row, deren Elemente sämtlich tail-resumptiv sind. Die Nutzersyntax ist offen.

// spekulativ — Schreibweise offen
def release[g](self, r: R) ->{g} ()
    where g: NonAbortive

Die Beschränkung ist eine Eigenschaft der Variable, keine Mengenoperation. g \ Throw[_] wäre eine mögliche Schreibweise, aber nicht die einzige, und die Wahl ist hier nicht nötig.

4. Row-Polymorphie

4.1 Offene Rows [N] 07 §2.3

Eine Row-Variable macht eine Funktion polymorph über die Effektmenge:

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

map führt keine eigenen Effekte ein und muss nichts über Throw, Db oder Net wissen. Genau das erspart der Stdlib eine mapResult/tryMap/traverseResult-Familie.

Die leere Row bedeutet leer, nicht „unbestimmt" — Unison-Lesart, nicht Frank-Lesart (07 §2.4, Invariante 8). Polymorphie braucht eine explizite Variable.

4.2 Qualifikationspflicht [N] 07 §3.5

A-1: genau ein Element des gesuchten Service in der Row ⇒ unqualifizierter Aufruf zulässig. A-2: mehrere Elemente ⇒ Fehler, keine „innerster Handler gewinnt"-Regel. A-3: Row-Variable vorhanden ⇒ Qualifikation verpflichtend, auch bei nur einer sichtbaren Instanz.

Die Begründung von A-3 ist der Kern: Es ist statisch nicht bekannt, ob g ein weiteres Element desselben Service enthält. Die konservative Regel garantiert, dass sich die Bedeutung eines Rumpfes nie dadurch ändert, dass ein Aufrufer etwas hinzufügt.

4.3 Keine stillschweigende Elimination bei offener Row [D]

Dieselbe Begründung greift für catch.

def run[g](body: () ->{g, Throw[A]} T) ->{g} T {
    try body() catch error => fallback()      // spekulativ — unzulässig
}

g kann weitere Throw[X] enthalten. Ein unqualifiziertes Catch würde sie stillschweigend verschlucken und die deklarierte Row ->{g} zur Lüge machen.

Regel A-7. Ein Handler — Service-Handler wie catch — darf nur Elemente eliminieren, die zum Zeitpunkt der Prüfung namentlich bekannt sind. Enthält die behandelte Row eine Variable, muss die eliminierte Menge explizit benannt werden. Folgt A-3 in Begründung und Wirkung.

4.4 Rows in Feldpositionen [N] jdl-sprachreferenz §19.3

Die Fehlerkonvention gilt auch für Funktionstypen in Feldposition; damit ist O-7 aus 07 §11.1 geschlossen.

Für Throw folgt daraus eine Feinheit, die festgehalten gehört: Ein Feld vom Typ (T) ->{Throw[E]} T transportiert eine abortive Verpflichtung in Daten. Wer den Wert speichert, speichert die Verpflichtung mit; sie wird erst beim Aufruf fällig, und zwar in der Row des Aufrufers (P-3, 07 §6.6, Invariante 35).

Das ist konsistent und braucht keine neue Regel. Es verschärft aber die offene Spannung aus jdl-sprachreferenz §19.3 zwischen „Blueprints sind effektfrei" und Rows in Feldpositionen — siehe §13.

5. Throw[E]

5.1 throw als Ausdruck [D]

Regel T-1. throw ist ein Sprachausdruck, keine Bibliotheksfunktion.

e : E
──────────────────────────────
throw e  :  Never   ->{Throw[E]}

Never ist der Bottom-Typ (jdl-sprachreferenz §3.4, jdl-primitives-spec §4.2). Er sorgt dafür, dass throw in beliebiger Position typprüft — insbesondere in einem Zweig eines if oder match, dessen anderer Zweig einen Wert liefert.

Ein kleines Sprachkonstrukt ist hier gerechtfertigt, weil throw den Kontrollflusscharakter sichtbar macht. Throw.raise(e) sähe aus wie ein gewöhnlicher Aufruf und wäre einer.

5.2 Auflösung über den Typ des Werts [D]

Ein Sonderfall, der sonst durchrutscht: A-3 verlangt Qualifikation, sobald eine Row-Variable im Spiel ist. Für throw gilt das nicht.

Regel T-2. throw e wird über den Typ von e aufgelöst, nicht über die Row. throw unterliegt der Qualifikationspflicht aus A-3 nicht.

Das ist dieselbe Konstruktion wie M-2 bei Alloc (07 §5.2, Invariante 29): Wo es keine benennbare Aufrufstelle für eine Qualifikation gibt, entscheidet der Typ. Bei throw ist die Auflösung sogar eindeutiger — der Typ des geworfenen Werts ist immer bekannt.

5.3 Automatische Propagation [N] 07 Invariante 12

Ein gewöhnlicher Aufruf propagiert nicht behandelte Throw[E] automatisch in die Row des Aufrufers. Es gibt keinen ?- oder =?-Operator; =? ist ersatzlos entfallen.

def parseUser(input: str) ->{Throw[ParseError], Throw[ValidationError]} User {
    val raw  = parse(input)
    val user = validate(raw)
    user
}

Die Dreiteilung lautet damit:

throw          erzeugt
normaler Call  propagiert
try/catch      behandelt

try bedeutet in JDL nicht „Propagation einschalten". Das ist ein bewusster Bruch mit Zig und Rust und in §7.7 als Namensrisiko vermerkt.

Der Preis, offen benannt (07 §4.1): Zigs try macht an jeder Stelle im Rumpf sichtbar, wo eine Funktion aussteigen kann. Hier verschwindet das. JDL tauscht Aufrufstellen-Sichtbarkeit gegen Signatur-Sichtbarkeit. Nach K-3 und K-4 ist die Signatur-Seite dieses Tauschs jetzt wenigstens vollständig.

5.4 Mehrere unabhängige Throw [N] 07 §4.1

E-1 bleibt: Jeder Fehlertyp ist ein eigenes Row-Element. Damit ist die Row-Vereinigung die Fehlermengen-Vereinigung, und es gibt keinen zweiten Mengenmechanismus.

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

5.5 Nominal und strukturell

Ein nominaler Fehlertyp ist ein Kanal mit mehreren Fällen. Eine strukturelle Union ist mehrere Kanäle. Y-1 hält die beiden auseinander.

Praktisch heißt das: Ein Domain-Error wird als enum deklariert und bleibt ein Element. Eine Union entsteht typischerweise nur dort, wo ein catch mehrere Kanäle zusammenfasst (§7.2).

6. Fehler als Wert

6.1 Drei Rollen, ein Typ [N] 07 §2.5, §4.2

E              normaler Wert
Result[T, E]   Fehler als Daten
Throw[E]       derselbe Typ als abortiver Kontrollfluss

Damit entfällt die übliche ideologische Frage „Exceptions oder Result?". Es gibt nicht zwei Sorten Fehlertypen, sondern zwei Rollen für denselben nominalen Typ.

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

6.2 Kontrollfluss zu Daten

catch materialisiert den Fehlerwert:

val result =
    try loadUser(id)
    catch error => Err(error)      // spekulativ

6.3 Daten zu Kontrollfluss

Umgekehrt kann ein Result wieder geworfen werden. Das ist gewöhnlicher Stdlib-Code, keine Sprachform:

provide Result[T, E] {
    def orThrow(self) ->{Throw[E]} T =
        match self {
            | Ok(value) => value
            | Err(error) => throw error
        }
}

6.4 catching entfällt als Sprachform [D]

07 §4.2 und jdl-sprachreferenz §9.3 führen catching { ... } als spekulative Form; die Sprachreferenz listet sie als Lücke 7.

Regel E-2′. Der Umwandlungspunkt von Kontrollfluss zu Daten ist catch. catching ist, wenn es gebraucht wird, eine gewöhnliche Stdlib-Funktion auf Basis von catch und keine Sprachform. Schließt jdl-sprachreferenz Lücke 7.

Begründung: Zwei Sprachformen für dieselbe Row-Elimination sind eine zu viel, und catching war in verschachtelten Fällen die klammerlastigere.

7. try / catch

Dieser Abschnitt definiert Semantik, keine Grammatik. Siehe §1.3.

7.1 Was catch ist [D]

Regel C-1. catch installiert einen abortiven Handler für eine bestimmte Menge von Throw-Elementen. Es ist eine Handler-Installation, kein Pattern Match auf den Rückgabewert.

Die Oberfläche darf dieselben Muster verwenden wie match — JDL braucht keine zweite Pattern-Sprache für Fehler. Semantisch sind es zwei verschiedene Dinge: match arbeitet auf Werten, catch auf dem Kontrollflusskanal.

7.2 Row-Elimination und Typ des Catch-Werts [D]

Regel C-2. Ein catch über die Menge S entfernt genau S aus der Row des try-Ausdrucks.

Auf der Wertseite wird der gefangene Fehler materialisiert. Fängt ein Catch {Throw[A], Throw[B], Throw[C]}, hat der gebundene Wert den Typ A | B | C.

Regel C-3. Die Union entsteht auf der Wertseite. Die Effektseite bleibt {Throw[A], Throw[B], Throw[C]} und wird nicht zu Throw[A | B | C] zusammengezogen.

Y-1 garantiert, dass beide Richtungen zusammenpassen: Wer den Wert vom Typ A | B | C weiterwirft, erzeugt wieder drei Elemente.

7.3 Geschlossene und offene Row [D]

Regel C-4. Ist die Throw-Menge des try-Ausdrucks geschlossen und vollständig bekannt, ist ein unqualifiziertes catch zulässig; es eliminiert diese Menge.

Enthält sie eine Row-Variable, muss die behandelte Menge explizit benannt werden. Ein unqualifiziertes catch ist dann ein Fehler. Folgt A-7.

// spekulativ — Schreibweise der Qualifikation offen
try body()
catch[AuthError] { ... }

Die Diagnostik sollte sich an EFF-AMB-001 (07 §3.5) anlehnen und die Alternative direkt vorschlagen.

7.4 Partielle Behandlung innerhalb eines E [D]

Ein Throw[E] ist auf Row-Ebene ein Element für den gesamten Typ E, nicht für einzelne Enum-Varianten. Behandelt ein Catch nur AuthError.InvalidToken, darf Throw[AuthError] nicht aus der Row verschwinden.

Regel C-5. Sobald ein catch einen Fehlertyp E behandelt, muss es E erschöpfend behandeln. Nicht behandelte Fälle müssen explizit weitergeworfen werden. Es gibt keine Variantenmengen innerhalb von Throw[E] und damit kein zweites Row-System.

try authenticate(token)
catch {
    | AuthError.InvalidToken => fallback()
    | error                  => throw error      // spekulativ
}

Bewusst nicht gewählt: die eliminierte Menge aus der Erschöpfungsanalyse der Arme abzuleiten. Das machte den Funktionstyp von einer Pattern-Analyse abhängig — die Signatur einer Funktion würde sich ändern, weil jemand einen Match-Arm hinzufügt.

C-5 hängt an einer Exhaustiveness-Definition, die es noch nicht gibt (jdl-sprachreferenz §16.2). Bis dahin ist die Regel formuliert, aber nicht prüfbar.

7.5 Typ des Gesamtausdrucks [D]

Regel C-6. try E catch H ist ein Ausdruck. Der Typ des Erfolgspfads und die Typen aller Catch-Zweige müssen sich zu einem gemeinsamen Typ vereinigen. Never-Zweige — etwa ein reines Rethrow — nehmen an der Vereinigung nicht teil.

Der Erfolgsfall erscheint nicht als Ok(...). Erfolg bleibt normaler Kontrollfluss.

7.6 Kein finally [D]

Regel C-7. JDL bekommt kein finally. Deterministisches Cleanup läuft über with (Scopeable, 03-runtime §2, 13-ir-spec WithScope) und über die Drop-Semantik.

Implizites Cleanup — Drop, release, Destruktion — darf keinen abortiven Effekt erzeugen. Formal: die Row eines Cleanup-Pfads ist nicht-abortiv im Sinne von Y-3.

Damit entfallen suppressed errors, Cause-Ketten und Double-Fault-Regeln aus dem Sprachkern. Wer einen fehlbaren Abschluss braucht, ruft ihn explizit auf und behandelt ihn.

7.7 Namensvorbehalt [O]

try heißt in Zig und Rust „propagiere", in JDL „installiere Handler" — während die Propagation ohne Schlüsselwort passiert. Für Umsteiger ist das genau falsch herum, und für Anfänger ist ein Wort, das eine unsichtbare Sache benennt und eine sichtbare nicht, keine Hilfe.

Der Name ist nicht entschieden. Kandidaten wären eine Postfix-Form ohne try oder ein anderes Wort für die Handler-Installation. Das gehört in die Kontrollfluss-Spec.

8. Labels

8.1 Fallible [D]

Regel L-F. Fallible gilt genau dann, wenn die effektive Row mindestens ein Throw[E] enthält.

Throw[_] ∈ row(T)   ⇔   Fallible

Die Äquivalenz — beide Richtungen — ist erst durch K-3 und K-4 wahr. Vor dieser Notiz galt nur die Hinrichtung, und die Rückrichtung wurde stillschweigend mitbenutzt.

Never, Trap, Cancellation und Prozessabbruch sind ausdrücklich nicht Fallible. Die vier Arten des Fehlschlagens aus jdl-sprachreferenz §9.1 bleiben getrennt.

8.2 Pure und Deterministic [D]

P-1 bleibt unverändert (07 §6.3, Invariante 32): Pure verlangt leere Row und keine RefMut/Out-Parameter. Eine Funktion mit Throw[E] ist damit nicht Pure. Das ist begrifflich richtig — ein Abbruch ist beobachtbar.

P-2 wird erweitert:

Regel P-2′. Deterministic verlangt row ⊆ {Alloc[_], Throw[_]} und keine RefMut/Out-Parameter. Ersetzt P-2 (Invariante 33).

Begründung: Ein Parser ist deterministisch — dieselbe Eingabe liefert denselben AST oder denselben ParseError. Ohne diese Erweiterung wäre praktisch keine fehlbare Funktion Deterministic, und da Query-Caching an Deterministic hängt und nicht an Pure, wäre das Label für die halbe Stdlib unbrauchbar.

Anforderung P-2a. Ein Cache über einer Deterministic-Funktion muss den Abbruch mitcachen: Ein Treffer auf einen zuvor geworfenen Fehler muss denselben Throw[E] erneut erzeugen, nicht einen Wert liefern.

Die Treppe bleibt: Pure ⇒ Deterministic.

8.3 Retryable entfällt aus der Label-Axiomatik [D]

Die bestehende Regel ist unerfüllbar:

Pure      ⇒ row = {}
Fallible  ⇒ Throw[_] ∈ row
────────────────────────────
Fallible ∧ Pure  ist leer

Sie steht in 07 §6.3 (Zeile 818), 04a C-2 und 04-axiomatics-truthprofile §7 — dort zusätzlich mit want_retry-Prämisse — und in 02-typsystem Zeile 759 in einer vierten, wieder anderen Fassung (Fallible + Concurrent).

Inhaltlich ist sie außerdem verkehrt herum. Bei einer deterministischen Funktion ist Retry sinnlos: gleiche Eingabe, gleicher Fehler. Retry lohnt genau bei nichtdeterministischen Effekten.

Regel L-R. Retryable wird als abgeleitetes Label gestrichen. Ersetzt C-2 in 04a und die Ableitung in 07 §6.3 und 04-axiomatics-truthprofile §7. Die Fassung in 02-typsystem Z. 759 entfällt ebenfalls.

Retry bleibt vorerst eine Eigenschaft von Handlern, Engines, CallGraphs oder expliziten Funktions-Refinements. Was Retry tatsächlich braucht, ist „hat vor dem Fehlschlag nichts Irreversibles committet" — eine Commit-/Rollback-Eigenschaft, für die es kein Label gibt. Diese Notiz erfindet sie nicht nebenbei.

9. Ownership und Payload-Escape

9.1 Warum die Return-Analogie nicht reicht

Bei return ist die Grenze der unmittelbare Aufrufer, und die Escape-Prüfung ist lokal. Bei throw unter offener Row steht der Handler statisch unbekannt weit außen. „Der Payload muss die Throw-Grenze legal verlassen können" ist damit lokal nicht prüfbar, wenn die Grenze selbst unbekannt ist.

M-2 verschärft das: Die Zielarena eines Werts folgt aus der memory-Policy seines Typs (07 §5.2, Invariante 29). Eine Escape-Kopie landete also wieder in derselben Arena.

9.2 Unwind-stabile Payloads [D]

Die Lösung ist, die Prüfung vom Ort auf den Typ zu verschieben.

Regel H-1. Der Payload eines Throw[E] muss unwind-stabil sein: gültig über beliebig viele verlassene Frames hinweg, bis ein Handler ihn konsumiert oder er materialisiert wird.

Zulässig sind damit Typen, deren Besitz- und Speichermodell einen ungebundenen Escape erlaubt — Werte, vollständig besessene unveränderliche Daten, Rc beziehungsweise stabil besessene Handles.

Nicht zulässig sind Borrows in einen lokalen Frame, Referenzen auf Stack-Lokalität und Werte, die an eine Arena gebunden sind, deren Lebensdauer kürzer sein kann als die Unwind-Distanz.

Regel H-2. throw e konsumiert einen nicht trivial kopierbaren Payload. Es ist ein Move, kein Borrow.

9.3 Ableitbar, kein neues Keyword [D]

Unwind-Stabilität ist keine neue Nutzer-Eigenschaft. Sie folgt aus der memory-Policy des Typs (M-2) und den bestehenden Besitzwrappern Ref/RefMut/Move/Out (04-axiomatik §7.1).

Regel H-3. Unwind-Stabilität ist ein abgeleitetes Label der TruthProfile-Closure, nicht per Refinement setzbar. Es gibt kein Nutzer-Keyword dafür. Bei Verstoß entsteht eine Diagnostik an der throw-Stelle.

Damit ist die Prüfung wieder lokal: Sie hängt am Typ von e, nicht an der Handlerdistanz.

10. Anforderungen an IR, Proto, Verifier und Runtime

Dieser Abschnitt legt Garantien fest, keine Formate. Wie Proto, Generator und VM sie codieren, wird später entschieden.

10.1 Ausgangslage

05-vm-instruction-set §6.5/§6.10: Die Core-Terminatoren sind Jmp, JmpIf, Return, Trap, Halt. Es gibt keinen abortiven Kontrollfluss.

06-generator §4.10: Proto enthält Bytecode, Konstantenpool, Registerzahl, Register-Layout, Upvalue- und Argumentzahl, optional Debug-Info. Keine Cleanup-Information.

05-vm-instruction-set §6.9: Drop ist eine explizite Instruktion, und der Verifier prüft Use-after-move und Use-after-drop.

Daraus folgt: Ein Throw darf Frames nicht einfach wegwerfen. Zwischen Throw-Stelle und Handler müssen die richtigen Drops und release-Aufrufe genau einmal laufen.

10.2 Die Garantien

G-1 — hinreichende Unwind-Information. Jeder ausführbare Frame trägt genügend statische Information, dass die Runtime für einen abortiven Ausgang den korrekten Cleanup-Pfad bestimmen kann.

G-2 — Exactly-once Cleanup. Jeder erforderliche Drop- und Cleanup-Schritt läuft auf dem Unwind-Pfad genau einmal. Kein doppelter Drop, kein ausgelassener.

G-3 — kein normaler Nachfolgecode. Der Unwind-Pfad führt keinen Code aus, der nur bei normaler Rückkehr gültig wäre.

G-4 — Unwind-Ziel aus der Evidence. Die Runtime erreicht das Unwind-Ziel, das die Evidence des abortiven Effekts bezeichnet. Es findet keine dynamische Handler-Suche statt.

G-4 ist gegenüber der Vorlage bewusst umformuliert. „Die Runtime bestimmt den nächsten passenden Handler" wäre eine dynamische Suche und damit genau die Laufzeit-Handler-Map, die A-6 und L-2 abgeschafft haben (07 §3.7 und §7.2, Invarianten 22 und 37). Das Ziel steht statisch fest; es muss nur erreicht werden.

G-5 — Verifier-Abdeckung. Der Verifier prüft zusätzlich zu 05-vm-instruction-set §7: gültige Unwind-Ziele, vollständige Cleanup-Abdeckung auf jedem Unwind-Pfad, keine doppelte Freigabe, kein Use-after-drop auf Exceptional Paths, konsistente Frame-Metadaten.

G-6 — kein Opcode-Zoo. Aus G-1 bis G-5 folgt kein neuer Exception-Opcode. Cleanup Tables, Landing Pads, Exception Regions, Frame-Unwind-Descriptoren und PC-Range-Tabellen sind mögliche Umsetzungen und bleiben Implementierungsdetail.

10.3 Verhältnis zu Invariante 38

L-3 („Abilities erfordern keine Erweiterung des Instruktions-Core") bleibt gültig. Unwinding ist nach Invariante 39 ohnehin Runtime-Sache in Zig.

Aber: Proto-Format und Verifier müssen wachsen. G-1 verlangt statische Information pro Frame, die es heute nicht gibt; G-5 verlangt Verifier-Regeln, die es heute nicht gibt. Das ist keine Verletzung von L-3, aber es ist Arbeit am Trusted Core.

10.4 Was das für die Reihenfolge heißt [D]

Anforderung G-7. Die Cleanup-Repräsentation muss feststehen, bevor der Generator geschrieben wird. Die Platzierung von Drop hängt daran.

Das ist der einzige Punkt dieser Notiz mit Terminwirkung. Alles andere ist Sprachdesign und lässt sich auf Papier reparieren; G-7 nicht.

Nach K-3 und K-4 hat die Anforderung übrigens einen erfreulichen Nebeneffekt: Cleanup-Kanten sind nur an Aufrufen nötig, deren Row abortive Elemente enthält. Ohne K-4 hätte der Generator an jedem Aufruf einer Service-Operation mit einer Unwind-Kante rechnen müssen.

11. Grenzen: Task, FFI, Remote

Nur die Materialisierungsregel. Alles Weitere gehört in eigene Notizen.

Regel B-1. An Grenzen, über die kein Stack-Unwinding möglich oder sinnvoll ist, wird Throw[E] materialisiert — zu einem Wert. Auf der anderen Seite kann der Fehler wieder in lokalen Throw-Kontrollfluss überführt werden.

Diese Grenzen sind mindestens:

Task-Grenze. Ein Throw kann nicht durch den Stack eines bereits weitergelaufenen Parent-Tasks unwinden. Der Task-Ausgang trägt das Ergebnis als Wert; await kann daraus lokal wieder einen Throw[E] erzeugen und trägt die entsprechende Row.

FFI-Grenze. JDL-Unwind läuft nicht über fremde ABIs. Ein Export mit durchlässigem Unwind ist verboten; die Grenze wird über einen Adapter auf Status- oder Fehlercodes abgebildet. In Gegenrichtung erzeugt ein Wrapper aus einem fremden Fehlerwert ein Throw[E].

Remote-Grenze. Ein Fehler, der eine Netzgrenze überquert, wird materialisiert, übertragen und auf der Gegenseite rekonstruiert. Das setzt eine stabile nominale Identität des Fehlertyps voraus, die nicht an eine lokale Runtime-TypeId gebunden ist — also O-5, siehe §13.

Nicht Gegenstand dieser Notiz: Failure-Policies bei Parallelität — fail-fast, collect-all, race, supervise — und Cancellation. Beide dürfen Throw[E] nicht überladen. Mehrfachfehler sind Wertsache, Cancellation ist ein Scheduler-Kontrollsignal.

12. Invarianten

12.1 Neue und präzisierte Invarianten dieser Notiz

Abortivität

  1. Abortivität ist eine Eigenschaft der Operation, nicht des Handlers. Rückgabetyp Never oder ein deklarierter abortiver Effekt macht eine Operation abortiv (K-1, K-2).
  2. Eine Operationssignatur darf abortive Effekte deklarieren; nur diese erscheinen in der Row des Aufrufers. Nicht-abortive Handler-Effekte gehören zur Installationsstelle (K-3).
  3. Der Rumpf eines Handlers darf keine abortiven Effekte enthalten, die die Operation nicht deklariert (K-4).
  4. Der einzige eingebaute abortive Effekt ist Throw[E] (A-4′).
  5. Throw[E] ist ein Row-Element, kein deklarierbarer Service. Erzeugung nur über throw, Elimination nur über catch (E-1′).
  6. Erschöpfung von Alloc[A] trappt; Fallibilität ist keine Handler-Entscheidung (M-1′).

Row-Algebra

  1. Throw verteilt über strukturelle Unions, nicht über nominale Typen (Y-1).
  2. Rows mit Throw[V] für eine ungebundene Typvariable sind nicht normalisiert; Normalisierung läuft nach der Substitution (Y-2).
  3. Das Row-System kennt eine Beschränkung auf nicht-abortive Row-Variablen (Y-3).
  4. Ein Handler darf nur namentlich bekannte Elemente eliminieren; bei offener Row muss die eliminierte Menge benannt werden (A-7).

Throw

  1. throw e : Never ->{Throw[E]}; throw ist ein Sprachausdruck (T-1).
  2. throw löst über den Typ des Werts auf und unterliegt A-3 nicht (T-2).
  3. catching ist keine Sprachform (E-2′).

try / catch

  1. catch ist eine Handler-Installation, kein Match auf den Rückgabewert (C-1).
  2. Ein catch über S entfernt genau S aus der Row (C-2).
  3. Die Union entsteht auf der Wertseite; die Effektseite bleibt getrennt (C-3).
  4. Geschlossene Throw-Menge ⇒ unqualifiziertes catch zulässig; offene Row ⇒ Qualifikation verpflichtend (C-4).
  5. Wer einen Fehlertyp behandelt, behandelt ihn erschöpfend oder wirft explizit weiter; es gibt kein zweites Row-System für Enum-Varianten (C-5).
  6. try/catch ist ein Ausdruck; alle Zweige vereinigen sich zu einem Typ, Never-Zweige ausgenommen (C-6).
  7. Kein finally. Implizites Cleanup darf nicht abortiv sein (C-7).

Labels

  1. Fallible ⟺ mindestens ein Throw[_] in der effektiven Row (L-F).
  2. Deterministic verlangt row ⊆ {Alloc[_], Throw[_]} (P-2′); ein Cache muss den Abbruch mitcachen (P-2a).
  3. Retryable entfällt als abgeleitetes Label (L-R).

Payload

  1. Throw-Payloads müssen unwind-stabil sein (H-1).
  2. throw konsumiert seinen Payload (H-2).
  3. Unwind-Stabilität ist abgeleitet, kein Nutzer-Keyword (H-3).

Trusted Core

  1. G-1 bis G-6 gelten als Architekturanforderung; das Format bleibt offen.
  2. Die Cleanup-Repräsentation steht vor dem Generator fest (G-7).

Grenzen

  1. Task-, FFI- und Remote-Grenzen materialisieren Throw (B-1).

12.2 Ersetzungen

Bestehend Fundstelle Status
Handlerklassen am Handler 07 §3.8, Sprachreferenz §8.8, Invariante 20 ersetzt durch K-1/K-2/A-4′
„Operationssignaturen tragen keine Row" 07 §3.1 präzisiert durch K-3
M-1 — Fallibilität ist Handler-Entscheidung 07 §5.1, Invariante 28 ersetzt durch M-1′
service Throw[e] 07 §4.1 ersetzt durch E-1′
catching als Umwandlungspunkt 07 §4.2, Invariante 25, Sprachreferenz §9.3 ersetzt durch E-2′
P-2 Deterministic, Row ⊆ {Alloc[_]} 07 §6.3, Invariante 33 ersetzt durch P-2′
Fallible ∧ Pure ⇒ Retryable 07 §6.3 Z. 818 gestrichen (L-R)
C-2 Fallible + Pure → Retryable 04a §C-2 gestrichen (L-R)
Fallible + Pure + want_retry → Retryable 04-axiomatics-truthprofile §7 gestrichen (L-R)
provide[T] Retryable ... Fallible + Concurrent 02-typsystem Z. 759 gestrichen (L-R)
Scopeable.release(...) -> () 03-runtime §2 nachzuziehen, Y-3

Unverändert gültig bleiben insbesondere R-1 bis R-4, A-1 bis A-3, A-5, A-6, E-1, E-2, E-3, M-2, M-3, P-0, P-1, P-3, L-1 bis L-3 sowie die Invarianten 7 bis 12, 14 bis 19, 21 bis 27, 29 bis 31, 34 bis 40.

13. Offene Punkte

Nur Punkte, die noch eine Architekturentscheidung verlangen. Spätere Implementierungsfragen stehen nicht hier.

# Frage Warum jetzt
N-1 Fehleridentität — nominal oder global wie Zig? (O-5, 07 §4.4) B-1 verlangt für Remote eine stabile Identität. Ohne Entscheidung kein Wire-Format und kein Plugin-Fingerprint für Fehlertypen.
N-2 Kontrollfluss — while, break, continue, return (Sprachreferenz Lücke 1) return im try-Block ist ohne return nicht definierbar. Blockiert C-6 in der Praxis.
N-3 Exhaustiveness (Sprachreferenz Lücke 2) C-5 ist ohne Exhaustiveness-Definition formuliert, aber nicht prüfbar.
N-4 Schreibweise nicht-abortiver Row-Variablen (Y-3) Betrifft jede Cleanup- und Handler-Signatur in der Stdlib. Semantik steht, Syntax nicht.
N-5 Schreibweise der Catch-Qualifikation (C-4) Hängt an N-3 und an der Trailing-Block-Grammatik.
N-6 Throw-Familien-Inferenz — Semantik steht (nur modulintern, R-4), Notation nicht. Throw[_] ist als Schreibweise vergeben: _ bedeutet in P-2′ und in 07 Z. 817 „Wildcard in einer Metaregel", in einer Signatur soll es „null oder mehr Elemente" heißen. Zwei Bedeutungen desselben Zeichens in derselben Position. Für Anfänger doppelt schlecht.
N-7 Blueprint-Effektfreiheit gegen Rows in Feldpositionen (Sprachreferenz §19.3) Ein Blueprint-Feld mit Throw in der Row transportiert eine abortive Verpflichtung in Daten. Die Auslegung ist nirgends festgehalten.
N-8 Scopeable nachziehen — acquire liefert heute Result[R, ScopeError], also v0.2-Stand; release hat leere Row. Beide Signaturen widersprechen dieser Notiz. Betrifft with, WithScope und jede Ressource.
N-9 Commit-/Rollback-Eigenschaft — Grundlage für ein späteres Retryable Nach L-R gibt es kein Retry-Label mehr. Ob eines zurückkommt, hängt daran. Kein Blocker.
N-10 Name für try (§7.7) Reine Oberflächenfrage, aber je später, desto teurer.

Ausdrücklich nicht offen im Sinne eines Blockers: das Binärformat der Cleanup-Tabelle, die Wire-Darstellung von Fehlern, Concurrency-Failure-Policies, Cancellation-Semantik. Diese Fragen haben feststehende Garantien (§10, §11) und mehrere zulässige Umsetzungen.

14. Was diese Notiz an anderen Dokumenten auslöst

Nachziehliste, nach Aufwand geordnet:

07-cast-effekte-refinements.md — §3.1 um K-3 ergänzen, §3.8 durch §2.6 ersetzen, §4.1 um E-1′ kürzen, §4.2 durch E-2′ ersetzen, §5.1 M-1 durch M-1′ ersetzen, §6.3 P-2 durch P-2′ und die Retryable-Zeile streichen, Invariantenliste §10 gegen §12.2 abgleichen, O-7 als geschlossen markieren.

jdl-sprachreferenz.md — §8.8 ersetzen, §9 um throw, try/catch und die Union-Regel erweitern, §9.3 auf E-2′ umstellen, Lücke 7 schließen, §20.3 auf P-2′ aktualisieren, Lückentabelle §21 gegen §13 abgleichen.

04a-label-inferenz-regeln.md — C-2 streichen, Fallible gegen L-F präzisieren.

04-axiomatics-truthprofile.md — §7 Retryable-Beispiel ersetzen; es ist als Beispiel für derived Labels weiterhin brauchbar, nur mit einer erfüllbaren Prämisse.

02-typsystem.md — Z. 759 provide[T] Retryable entfernen.

03-runtime.md — Scopeable nach N-8 nachziehen.

05-vm-instruction-set.md / 06-generator-und-code-emission-v2.md / 13-ir-spec.md — G-1 bis G-7 als Anforderungsabschnitt aufnehmen. Keine Formatfestlegung, aber die Garantien gehören dort hin, wo sie eingelöst werden.

Änderungsprotokoll

v0.1.0 — Erstfassung. Konsolidiert die Befunde A–H der Gegenprüfung und die Antwort von GPT-5.6 Sol. Zentrale Abweichung von der Vorlage: Befund A wird über Operationssignaturen gelöst (K-3, K-4) statt über eine Selbstverpflichtung der Handler; M-1 fällt dafür. G-4 ist umformuliert, weil die Vorlage eine dynamische Handler-Suche beschrieb, die A-6 und L-2 ausschließen. Neu gegenüber beiden Vorlagen: Y-2, P-2a, C-6, G-7.