Zum Inhalt

JDL — Effect Rows, abortive Fehler und Throw-Semantik

Status: Konsolidierte Arbeitsnotiz, Orientierungsgrundlage Version: 0.2.2 Datum: 2026-10-05 Bezug: jdl-row-throw-review-brief.md (GPT-5.6 Sol), Gegenprüfung Befunde A–H, antwort-an-claude-row-throw-konsolidierung.md, Arbeitsgespräch 2026-10-05 (Rows als Typen) 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
[V] Vorschlag, ausgearbeitet, aber nicht entschieden (seit 0.2.1)
[E] entschieden in den Arbeitsgesprächen, in keinem Quelldokument ausgeschrieben (seit 0.2.2)

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].

Seit 0.2.0 außerdem, wie eine Row verwaltet wird: Sie ist ein Typ (§3.6), Protocols weisen benannte Row-Plätze aus (§4.5), geliefert wird sie per provide (§4.6), und was ein ganzer Aufrufgraph braucht, ist eine Abfrage (§4.7). Seit 0.2.1 gehört jede Row zu genau einer Phase (§3.7).

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
type Db : service {
    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.

Dieselbe feste Ordnung bestimmt seit 0.2.0 auch die Plätze des Bündels, das eine gelieferte Row zur Laufzeit ist (§4.6, G-8).

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].

[O] Seit 2026-10-05 werden Unions als Block deklariert, type X : union { A, B } (jdl-sprachreferenz §5.3). Die Schreibweise A | B in dieser Notiz steht für eine namenlose Union im Typausdruck; deren Form ist nicht entschieden.

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} Unit
    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.

Seit 0.2.0 ist release eine Protocol-Methode mit Row-Platz (§4.5). Y-3 gilt für einen Row-Platz genauso wie für eine Row-Variable [A]: Der Platz von Scopeable.release muss nicht-abortiv sein. Die Schreibweise bleibt offen (N-4).

3.6 Die Row ist ein Typ [D]

Eine Row ist ein Typ, gebaut auf der Grundart row. Die Rolle steht wie bei allen Typen hinter dem Doppelpunkt. Es gilt: Ein Doppelpunkt sagt, was für ein Ding etwas ist, ein Gleichheitszeichen sagt, welches Ding es ist.

type Needs     : row::Row                          // spekulativ
type ShopNeeds : row::Row = {Orders, Payments}     // spekulativ
type NoNeeds   : row::Row = {}                     // spekulativ
  • Zeile 1: eine Row, deren Inhalt noch festgelegt wird — die Form für Row-Plätze (§4.5).
  • Zeile 2: ein Name für genau diese Row.
  • Zeile 3: ausdrücklich keine Services.

Warum dort row::Row steht und nicht nur row, erklärt §3.7: Jede Row gehört zu genau einer Phase.

Die Rolle steht immer da [D]. Eine benannte Row trägt ihre Rolle ausgeschrieben, auch wenn ihr Inhalt schon feststeht. Ohne Rolle ließe sich die Art einer Row nicht einmal ableiten: type X = {} sähe genauso aus wie ein Alias für den leeren Record (jdl-typalgebra-records-blueprints-notiz §5). Bei einem nicht leeren Inhalt verrät die Schreibweise die Art zwar (ein Record hat name: Typ, eine Row nur Typen), aber eine Regel, die nur beim leeren Inhalt versagt, wäre eine Ausnahme. Mit der Rolle gilt eine Regel ohne Ausnahme, und wer die Zeile liest, sieht sofort, dass es um Erlaubnisse geht. type ShopNeeds : row::Row = {…} sagt Art und Inhalt in einer Zeile.

type Needs : {} ist nicht die Form. In ->{} bedeutet {} die leere Menge (R-3); dieselbe Klammer dürfte nicht zugleich „noch zu füllen" heißen.

Leerer Record und leere Row. Beide sind das neutrale Element ihrer Verknüpfung: Ein leerer Record ändert nichts, wenn man ihn mit & auflegt; eine leere Row ändert nichts, wenn man sie vereinigt. Die Analogie reicht aber nur so weit. & hat eine Richtung (rechts überschreibt links), die Vereinigung von Rows nicht. & ist deshalb kein Row-Operator; erweitert wird eine Row im Inhalt, etwa = {ShopNeeds, Logging}.

Regel W-1. Eine Row ist ein Typ der Rolle row::Row oder row::MetaRow (§3.7). Sie hat keine Werte; val x: ShopNeeds ist ein Fehler. Eine benannte Row trägt ihre Rolle immer ausgeschrieben.

Regel W-2. Ein Row-Name ist durchsichtig. Er ist eine Abkürzung, kein neuer Typ mit eigener Identität. Zwei Rows sind gleich, wenn ihre Phase gleich ist und ihr Inhalt nach Normalisierung (§3.2) gleich ist.

W-2 ist nötig, sonst wären {Orders, Payments} und ShopNeeds zwei verschiedene Rows, und der Teilmengentest aus §3.2 scheiterte an Namen statt am Inhalt.

Regel W-3. Diagnosen und Werkzeuge nennen immer die einzelnen Elemente, nie nur den Namen einer Row. Ein Name darf Autorität nicht verstecken.

W-3 ist keine Typregel, sondern eine Anforderung an Diagnosen und den Sprachserver. ->{ShopNeeds} liest sich harmlos und enthält vielleicht Payments; wer eine Signatur prüft, muss sehen können, was darin steckt.

Meta ist kein Row-Element [N] jdl-meta-phase §2.1. Eine Row als Typ kann Meta daher nie enthalten. Das folgt aus der Bauart und braucht keine eigene Prüfung.

Was damit wegfällt. Ohne Row als Typ bräuchte JDL eigene Regeln dafür, wie man Rows benennt, übergibt und von einer Implementierung festlegen lässt. Mit Row als Typ ist all das schon da, weil Typen es können.

Trusted Core. Die TypeKinds sind im Zig-Kern fest verdrahtet (jdl-blueprint-spec BP-12). row gehört deshalb dort hinein; das ist eine Kernänderung, keine Stdlib-Sache. Als Typ bekommt eine Row einen Deskriptor und einen Hash und ist damit über die CompilerDB abfragbar (wie-jade-uebersetzt §6.6).

3.7 Laufzeit-Rows und Meta-Rows [D]

Das Problem. Die Phase einer Funktion steht am Pfeil, vor der Row: ->Meta{...} (jdl-meta-phase §2.1, MP-20). Solange jede Row an einem Pfeil hing, lieferte der Pfeil die Phase mit. Seit Rows Typen sind, gibt es Rows ohne Pfeil: benannte Rows, Row-Plätze, provide auf Rows, die Summe über einen Graphen, Einträge in der CompilerDB. Ohne eigene Phase wüsste niemand, ob eine solche Row in den Compiler gehört oder in die VM.

Die Elemente retten das nicht zuverlässig. Manche verraten die Phase (Fs darf nie in eine Meta-Row, jdl-meta-phase §3.3), viele passen in beide: {}, {Throw[E]}, {Storage}.

Die Entscheidung. Es gibt keine Row ohne Phase und keine Row, die in beiden Phasen gilt. Es gibt zwei getrennte Arten von Rows mit eigenen Regeln, je nachdem, was die Phase bedeutet.

row        die Grundart, ohne Phase      der TypeKind im Kern, selbst keine Row
Row        Laufzeit-Row                  Rolle row::Row
MetaRow    Meta-Row                      Rolle row::MetaRow

row ist damit nur die gemeinsame Grundlage, aus der die beiden Arten gebaut werden. Eine benutzbare Row ist immer eine Row oder eine MetaRow.

Wie die beiden Arten entstehen [V]. Arbeitsstand der Gespräche, als Form noch nicht festgelegt:

// spekulativ — Seed: einmal in JDL beschrieben, beim Prägen materialisiert
tag Phase : enum {
    Runtime
    Meta
}

def RowDefinition(phase: Phase = Runtime) ->Meta{} TypePatch { ... }

type Row     : row = {} :> RowDefinition()
type MetaRow : row = {} :> RowDefinition(phase = Meta)
  • Zeilen 2 bis 5: Die Phase ist eine Tag-Domain. Sie existiert zur Laufzeit nie als Wert, deshalb tag und nicht type (00-ontology-types-tags-phantoms §6). Und es ist dieselbe Phase, die am Pfeil steht: Das Meta hier ist das Meta aus ->Meta{. Nebenbei bekommt Runtime einen Namen; ob es schreibbar ist, war bisher offen (jade-service-typekind-arbeitsnotiz §8.4, jdl-meta-phase MP-15).
  • Zeile 7: Ein Refinement, das einer Row ihre Phase gibt.
  • Zeilen 9 und 10: Die beiden Rollen sind genau die zwei leeren Rows, die leere Laufzeit-Row und die leere Meta-Row.

Warum im Seed und nicht in Nephrit. Der Compiler vergleicht die Phase am Pfeil von sich aus mit der Phase der Row, ohne dass der Benutzer etwas dazu schreibt. Der Lader prüft, dass in der VM nur Laufzeit-Rows ankommen. Käme die Phase aus der Stdlib, hinge eine Prüfung des Kerns an Bibliothekscode. Das ist derselbe Grund, aus dem Alloc im Seed steht (07 §7.5). Geschrieben werden darf die Definition trotzdem in JDL, wie der Meta-Context (addendum-begriffe-und-motive G.2): einmal beschrieben, beim Prägen materialisiert, danach nur gelesen. Das braucht der Bootstrap ohnehin, denn der Meta-Evaluator muss wissen, was eine Meta-Row ist, bevor die erste Meta-Funktion läuft.

Regel W-12. Jede Row hat genau eine Phase. Die Grundart row ist selbst keine Row und steht nur im Seed. Es gibt keine Row, die in beiden Phasen gilt.

Regel W-13. Der Pfeil bestimmt die Art: ->{...} ist eine Row, ->Meta{...} eine MetaRow. Eine benannte Row der anderen Art an einem Pfeil ist ein Fehler.

Regel W-14. Die Phase gehört zur Identität einer Row. Die leere Row und die leere MetaRow sind verschiedene Typen mit verschiedenem Hash.

Trusted Core. Die Phase ist ein Bit im Row-Deskriptor. Einen dritten Zustand gibt es nicht, und einen weiteren TypeKind braucht es nicht. Das Bit geht in den Hash ein (W-14). Das Row-Bündel der VM (§4.6, G-8) enthält nur Bindungen von Laufzeit-Rows, und der Lader nimmt nur Laufzeit-Rows an (G-11). Benutzer können die Phase einer Row nicht überschreiben; sie ist ein Fakt des Seeds (vgl. jdl-meta-phase MP-10, MP-11).

[O] Der Übergang zwischen den Arten (N-15). Meta-Code darf gewöhnliche Funktionen aufrufen, „deren Row in seine Meta-Row passt" (jdl-meta-phase §3.4, MP-21). Das war ein Teilmengentest über eine einzige Art von Row. Mit zwei Arten ist es ein Übergang von einer Row in eine MetaRow. Bei einer leeren Row ist er harmlos. Bei Throw[E] braucht er eine Regel; betroffen ist etwa requireAtLeast (jdl-blueprint-spec §4.9), eine gewöhnliche Funktion mit ->{Throw[DiagnosticSet]}, die contribute aus der Meta-Phase aufruft. Vorschlag [V]: Die MetaRow legt fest, welche Laufzeit-Elemente sie übernimmt und was sie bei ihr bedeuten. Für Throw ist das naheliegend, denn Meta-Code läuft ohnehin auf einer VM im Compiler (addendum-begriffe-und-motive G.1); erst an der Grenze der Meta-Phase wird daraus eine Diagnose. Die Alternative — Meta ruft nur Funktionen mit leerer Row — widerspräche dem Ziel aus jdl-meta-phase §3.4, Hilfsfunktionen nicht für jede Phase zweimal zu schreiben.

[O] Rolle oder Basis (N-16). Hinter dem Doppelpunkt steht jetzt ein Typ, kein Schlüsselwort. Als Rolle gelesen ist MetaRow eine Art von Row und ihr eigener Inhalt belanglos. Als Basis gelesen ist NeedsMeta : row::MetaRow = {…} „MetaRow plus diese Elemente". Für Row und MetaRow ist beides gleich, weil ihr Inhalt leer ist. Auseinander gehen die Lesarten erst, wenn jemand eine nicht leere Row hinter den Doppelpunkt schreibt.

[O] Namensraum und Import (N-17). Unter welchem Namensraum die Seed-Einträge Row und MetaRow liegen, ist nicht festgelegt. Ein import im Rumpf eines Protocols, wie in der Gesprächsskizze, gibt es bisher nicht; Inline-Imports kennt die Sprache nur in Compile-Zeit-Rümpfen (jdl-meta-phase MP-12).


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.

Bei map legt jeder Aufruf g neu fest, über das übergebene f. Der Aufrufer wählt. Das unterscheidet map von einer Protocol-Methode, bei der die Implementierung festlegt (§4.5).

[O] Ob g mit §3.6 zu einem gewöhnlichen Typparameter mit Rolle wird ([T, Needs : row::Row]), zu einem Verweis auf die Row eines Parameters oder eine eigene Schreibweise behält, ist nicht entschieden (N-12).

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.

A-3 gilt für einen Row-Platz T.Needs in generischem Code genauso [A]: Dessen Inhalt ist im Rumpf ebenso unbekannt.

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 { | _ => 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.

A-7 gilt für T.Needs genauso [A].

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.

4.5 Row-Plätze in Protocols [D]

Das Problem. Eine Implementierung braucht oft Services, die das Protocol nicht vorhersehen kann: Eine gepufferte Datei braucht zum Schließen Fs, eine HTTP-Engine zum Starten einen Listener. Bisher stand dafür eine Row-Variable g an der Protocol-Methode. Der Benutzer musste sich ein nirgends deklariertes Konstrukt merken, und Vergessen oder Vertippen endete in einem schwer lesbaren Abgleichfehler.

Die Lösung. Das Protocol weist einen benannten Row-Platz aus.

protocol Scopeable {                              // spekulativ
    type Needs : row::Row
    def release(self) ->{Needs} Unit
}
  • Zeile 2: Der Protocol-Autor sagt ausdrücklich, dass jede Implementierung eigene Services mitbringen darf. Den Namen wählt er; Needs ist ein Beispiel. Die Rolle legt auch die Phase des Platzes fest (§3.7): Ein row::Row-Platz kann nur hinter einem Laufzeitpfeil stehen.
  • Zeile 3: Die Methode verweist auf diesen Platz.

Regel W-4. Eine Protocol-Methode darf Services ihrer Implementierung nur über einen Row-Platz zulassen, den das Protocol mit type <Name> : row::Row oder type <Name> : row::MetaRow ausweist. Ersetzt die Row-Variable an Protocol-Methoden.

Regel W-5. Die Implementierung schreibt ihre echte Row in die Signatur. Der Compiler leitet den Inhalt des Platzes daraus ab; eine eigene Zeile type Needs = … ist nicht nötig.

Regel W-6. Wer einen konkreten Typ benutzt, sieht den Platz nie; der Compiler setzt die echten Services ein. Nur generischer Code nennt den Platz, als T.Needs.

Wer was entscheidet. Zwei verschiedene Dinge heißen umgangssprachlich „binden":

festlegen, was die Row ist    die Implementierung, über ihre Signatur (W-5)
liefern, was sie verlangt     wer ein provide auf sie macht, meist ein Context (§4.6)

Fehler werden dort gemeldet, wo die Entscheidung fiel. Weist ein Protocol keinen Platz aus und bringt eine Implementierung trotzdem einen Service mit, lautet die Meldung sinngemäß: „Scopeable.release erlaubt keine eigenen Services, Fs ist hier nicht zulässig." Der Benutzer sieht sofort, ob das Protocol oder seine Implementierung zu ändern ist.

Kein eingebauter Platz. Anders als Self existiert ein Row-Platz nicht automatisch in jedem Protocol. Sonst wäre jede Protocol-Methode offen für beliebige Services, ohne dass ihr Autor das entschieden hat — dieselbe Magie, nur besser versteckt.

Vorbilder. Das Muster ist der assoziierte Typ (Rust type Item, Zugriff T::Item). JDL geht einen Schritt weiter: Rust verlangt type Item = u32; in jeder Implementierung, hier leitet der Compiler den Platz aus der Signatur ab (W-5), sodass Deklaration und Signatur nicht auseinanderlaufen können. Suchwort für Effekte als Protocol-Mitglied: associated effects (Flix, PLDI 2024).

dyn-Stellen. An einer dyn-Stelle ist die Implementierung unbekannt und damit auch der Inhalt des Platzes. Der Aufrufer muss aber vor dem Aufruf wissen, was er anfasst, sonst gäbe es Autorität, die in keiner Signatur steht.

Regel W-7. Eine dyn-Stelle eines Protocols mit Row-Platz legt den Inhalt des Platzes fest. Die Schreibweise ist offen (dyn-protocol-values §4.5).

Trusted Core. Beim dynamischen Dispatch muss der Verifier prüfen, dass die tatsächliche Implementierung nicht mehr verlangt, als die dyn-Stelle festlegt (G-9).

[O] Ob ein Row-Platz pro Protocol gilt (alle Methoden teilen sich einen) oder pro Methode, ist nicht entschieden (N-11).

4.6 provide auf Rows [D]

Geliefert wird eine Row, indem jemand ein provide auf sie macht. Damit sagt er: „Für diese Services stehe ich ein." In der Regel ist das ein Context. provide muss dafür nichts Neues lernen; die Row ist ein Typ wie jeder andere.

Regel W-8. Provided werden nur Service-Elemente. Ein Throw[E] wird nicht geliefert, sondern per catch eliminiert (E-1′). Ein provide auf eine Row deckt ihren Service-Teil ab.

Regel W-9. Gleicher Inhalt, gleiches provide. Wegen W-2 ist ein provide auf ShopNeeds dasselbe wie eines auf {Orders, Payments}. Steckt ein Service in zwei gelieferten Rows mit unterschiedlicher Bindung, ist das ein Konflikt; identische Bindungen zählen einmal.

W-9 ist dieselbe Algebra, die für Context-Components bereits entschieden ist (spec-context-model-refactored X-27).

Regel W-10. Eine gelieferte Row ist eine Bindung, kein Wert. Nutzercode kann sie nicht halten oder weiterreichen (W-1, A-5).

Trusted Core: Das Row-Bündel. Zur Laufzeit ist eine gelieferte Row ein Bündel von Bindungen, das die VM bei Aufrufen weiterreicht (Evidence Passing, A-6). Eine Row ist eine Menge und hat keine Reihenfolge; ein Bündel hat Plätze in fester Reihenfolge. Die Reihenfolge ist die feste Ordnung der Normalisierung (§3.2). Sie muss in Compiler und VM identisch sein, sonst landet Orders im Platz von Payments (G-8).

4.7 Die Summe über einen Aufrufgraphen [D]

Was ein ganzer Aufrufgraph braucht, schreibt niemand mehr von Hand hin. Der frühere requires-Block eines CallGraph war eine gepflegte Kopie dessen, was die Rows der aufgerufenen Funktionen ohnehin sagten (07 §9.1). Mit Rows als Typen rechnet der Compiler diese Summe aus.

Regel W-11. Zusammengezogen wird die Sicht auf einen Graphen, nicht die Signatur einer einzelnen Funktion. Jede Funktion deklariert ihre Row selbst. Die Summe aller Rows, die von einem Punkt aus erreichbar sind, ist eine Abfrage an die CompilerDB.

Der Unterschied ist wichtig. Leitete der Compiler die Rows einzelner Funktionen selbst ab, stünde in keiner Signatur mehr, was eine Funktion anfasst. So bleibt jede Signatur ehrlich, und nur der Überblick ist automatisch.

[O] Regel R-4 (07 §2.7) erlaubt modul-interne Effektinferenz. Nach einer späteren Entscheidung ist -> ohne {} nur Kurzschreibweise für die leere Row, und ein Rumpf, der mehr braucht, ist ein Fehler. W-11 setzt die zweite Lesart voraus. R-4 muss nachziehen (jdl-sprachreferenz §7.5).

Was daraus folgt:

  1. requires entfällt. Wer bindet — ein CallGraph, ein Context —, fragt die Summe ab, vergleicht sie mit seinem Angebot und meldet jeden fehlenden Service einzeln mit Namen.
  2. Rekursion ist kein Sonderfall. Weil jede Funktion ihre Row deklariert, ist das Zusammenziehen ein einfacher Durchlauf über die Signaturen. Ruft f die Funktion g und g wieder f, werden beide Signaturen gelesen und vereint. Ein Hin- und Herrechnen, bis es sich einpendelt, wäre nur bei abgeleiteten Rows nötig — ein weiteres Argument für die Deklarationspflicht.
  3. Die Summe bestimmt das Bündel. Die Summe eines Contexts ist genau das Row-Bündel, das die VM ihm mitgibt (§4.6).

Trusted Core: zur Laufzeit geladene Contexts. Deren Graph kennt der Compiler beim Bauen des Elternteils nicht. Der geladene Context bringt seine Summe deshalb in seinem Deskriptor mit, und beim Laden wird geprüft, ob der Elternteil sie decken kann. Passt es nicht, wird der Start abgelehnt (G-10, wie-jade-ausfuehrt §5.5).


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 Propagation mit try [E] (ersetzt die automatische Propagation aus 07 §4.1)

Ein Aufruf, der abbrechen kann, trägt try. Ohne catch reicht try den Fehler in die Row des Aufrufers weiter; mit catch behandelt es ihn (§7). Einen ?- oder =?-Operator gibt es nicht; =? ist ersatzlos entfallen (07 Invariante 12).

def parseUser(input: str) ->{Throw[ParseError], Throw[ValidationError]} User {
    val raw  = try parse(input)
    val user = try validate(raw)
    ret user
}
  • Zeilen 2 und 3: Beide Aufrufe können abbrechen und tragen deshalb try. Ihre Fehler wandern in die Row von parseUser.
  • Zeile 4: Ein Blockrumpf liefert keinen Wert von selbst; ret gibt ihn zurück.

Die Dreiteilung lautet damit:

throw          erzeugt
try            markiert und reicht weiter
try … catch    behandelt

Warum an jeder Stelle. Sichtbar soll beides sein: in der Signatur, was eine Funktion werfen kann, und im Rumpf, wo sie aussteigen kann. Eine automatische, unmarkierte Propagation machte nur die Signatur sichtbar; 07 §4.1 nannte genau das als Preis. Mit try an jeder abbrechenden Stelle wird dieser Preis nicht mehr gezahlt.

Regel T-3. Jeder Aufruf, der abbrechen kann, trägt try. Ohne catch wird der Fehler weitergereicht. [E] — Ein Aufruf ohne try, dessen Row ein nicht behandeltes Throw enthält, ist damit ein Fehler beim Übersetzen [A].

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 =                       // spekulativ
    try Ok(loadUser(id))
    catch { | val error => Err(error) }

Der Erfolgspfad steht in Ok(...), damit beide Zweige ein Result liefern (C-6, §7.5).

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(val value) => value
            | Err(val 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.

Der gebundene Wert ist damit ein Union-Wert zur Laufzeit. Wer ihn mit match nach seinem Mitgliedstyp unterscheiden will, braucht Typ-Arme; die sind vorgeschlagen, aber nicht entschieden (jdl-sprachreferenz §16.3).

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()
    | val 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 Der Name try [E] (2026-10-05)

Bis 0.2.1 stand hier ein Namensvorbehalt: try hieß in Zig und Rust „propagiere", in JDL „installiere Handler", während die Propagation ohne Schlüsselwort passierte. Mit §5.3 ist das aufgelöst. try markiert jede Stelle, an der abgebrochen werden kann, und reicht ohne catch weiter, wie in Zig. Mit catch installiert es zusätzlich einen Handler. Für Umsteiger stimmt die Richtung damit wieder, und für Anfänger benennt das Wort genau die Stelle, die sie sehen. Schließt N-10.


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.

Für einen Row-Platz gilt dasselbe wie für jede Row [A]: Ein generischer Aufruf mit T.Needs ist nur dann Pure, wenn der eingesetzte Inhalt leer ist. Die Labels werden nach der Substitution bestimmt, wie die Normalisierung (Y-2).

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.

10.5 Garantien für Rows als Typen [D]

Seit 0.2.0 kommen drei Garantien dazu (G-8 bis G-10), seit 0.2.1 eine vierte (G-11). Auch sie legen kein Format fest.

G-8 — kanonische Bündelordnung. Die Plätze eines Row-Bündels folgen der festen Ordnung der Normalisierung (§3.2). Compiler und VM berechnen dieselbe Ordnung nach derselben Regel. Der Verifier prüft, dass ein Aufruf das Bündel in dieser Ordnung übergibt.

G-9 — dyn-Dispatch hält die Row ein. Beim Dispatch über eine dyn-Stelle prüft der Verifier, dass die tatsächliche Implementierung nicht mehr verlangt, als die dyn-Stelle für ihren Row-Platz festlegt (W-7).

G-10 — geladene Contexts bringen ihre Summe mit. Ein zur Laufzeit geladener Context trägt die Summe seines Aufrufgraphen (§4.7) in seinem Deskriptor. Ring 0 prüft beim Laden, ob der Elternteil sie decken kann, und lehnt sonst den Start ab.

G-11 — in der VM nur Laufzeit-Rows. Jeder Row-Deskriptor trägt seine Phase (W-12). Ring 0 nimmt beim Laden nur Laufzeit-Rows an; ein Row-Bündel enthält nie eine Bindung aus einer Meta-Row. Seit 0.2.1.

Dazu gehört die Kernänderung aus §3.6: row steht in der fest verdrahteten TypeKind-Liste. Die beiden Rollen Row und MetaRow stehen im Seed (§3.7).


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).

Rows als Typen (seit 0.2.0)

  1. Eine Row ist ein Typ der Rolle row::Row oder row::MetaRow und hat keine Werte; eine benannte Row trägt ihre Rolle immer ausgeschrieben (W-1).
  2. Row-Namen sind durchsichtig; Gleichheit über Phase und normalisierten Inhalt (W-2). Diagnosen nennen die Elemente, nie nur den Namen (W-3).
  3. Services einer Implementierung lässt eine Protocol-Methode nur über einen ausgewiesenen Row-Platz zu (W-4). Den Inhalt leitet der Compiler aus der Signatur der Implementierung ab (W-5); sichtbar ist der Platz nur in generischem Code als T.Needs (W-6).
  4. Eine dyn-Stelle legt den Inhalt eines Row-Platzes fest (W-7).
  5. provide auf eine Row liefert nur Service-Elemente (W-8); gleicher Inhalt, gleiches provide, verschiedene Bindungen desselben Service sind ein Konflikt (W-9); eine gelieferte Row ist eine Bindung, kein Wert (W-10).
  6. Die Summe über einen Aufrufgraphen ist eine Abfrage; einzelne Signaturen bleiben deklariert (W-11).
  7. G-8 bis G-11 und row in der TypeKind-Liste gelten als Architekturanforderung an den Trusted Core.

Phasen von Rows (seit 0.2.1)

  1. Jede Row hat genau eine Phase; die Grundart row ist selbst keine Row (W-12).
  2. Der Pfeil bestimmt die Art einer Row; eine benannte Row der anderen Art ist dort ein Fehler (W-13).
  3. Die Phase gehört zur Identität einer Row; die leere Row und die leere MetaRow sind verschiedene Typen (W-14).

Aufrufstellen (seit 0.2.2)

  1. Jeder Aufruf, der abbrechen kann, trägt try; ohne catch wird weitergereicht (T-3).

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 und W-4
Row-Variable g an Protocol-Methoden jdl-blueprint-spec 0.5.2 §9.1 ersetzt durch Row-Platz (W-4 bis W-6)
requires-Block im CallGraph 07 §9.1, Sprachreferenz §19.1 gestrichen, Summe als Abfrage (W-11)
Propagation ohne Schlüsselwort 07 §4.1, Sprachreferenz §9.4 ersetzt durch T-3: try an jeder abbrechenden Stelle

Unverändert gültig bleiben insbesondere R-1 bis R-3, 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. R-4 steht nach §4.7 in Frage.


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 und Row-Plätze (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. Mit W-4 bekommt release einen Row-Platz.
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 — geschlossen 2026-10-05: try markiert jeden Aufruf, der abbrechen kann (§5.3, §7.7) —
N-11 Row-Platz pro Protocol oder pro Methode (§4.5) Entscheidet, wie viele Plätze ein Protocol wie RuntimeEngine ausweist und was eine dyn-Stelle festlegen muss.
N-12 g an gewöhnlichen Funktionen (§4.1). Zwei Kandidaten aus dem Gespräch vom 2026-10-05: ein Typparameter mit Rolle ([T, Needs : row::Row]) oder ein Verweis auf die Row eines Parameters (->{inner.Needs, …}). Der zweite spart die Wiederholung, verlangt aber eine sichtbar offene Row am Parameter, weil eine fehlende Row nach R-3 leer bedeutet. Betrifft jede Funktion höherer Ordnung in der Stdlib.
N-13 Schreibweise der Festlegung an einer dyn-Stelle (W-7) Ohne sie ist G-9 formuliert, aber nicht prüfbar.
N-14 R-4 gegen Deklarationspflicht (§4.7) W-11 setzt deklarierte Rows voraus.
N-15 Übergang von Row in MetaRow (§3.7) — Übergangsregel der MetaRow oder nur leere Row MP-21 und jdl-meta-phase §3.4 setzen einen Teilmengentest über eine Art von Row voraus. Betrifft jeden Aufruf einer gewöhnlichen Funktion aus Meta-Code, etwa requireAtLeast.
N-16 Rolle oder Basis (§3.7) — wie : row::MetaRow zu lesen ist Entscheidet, ob hinter dem Doppelpunkt nur Rollen aus dem Seed stehen dürfen oder auch gewöhnliche Rows.
N-17 Namensraum der Seed-Einträge Row/MetaRow, Import im Protocol-Rumpf (§3.7) Ohne Namensraum keine schreibbare Rolle.

Ausdrücklich nicht offen im Sinne eines Blockers: das Binärformat der Cleanup-Tabelle, die Wire-Darstellung von Fehlern, Concurrency-Failure-Policies, Cancellation-Semantik, das Format des Row-Bündels. 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. Seit 0.2.0 außerdem: §9.1 requires streichen (W-11), §2.7 R-4 gegen §4.7 abgleichen.

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. Die Punkte aus 0.2.0 sind in der Sprachreferenz 0.2.0 nachgezogen.

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, release mit Row-Platz (W-4).

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

jdl-meta-phase.md — §3.4 und MP-21 gegen §3.7 abgleichen: Der Aufruf gewöhnlicher Funktionen aus Meta-Code ist ein Übergang zwischen zwei Arten von Rows, kein Teilmengentest (N-15). MP-15 bekommt mit tag Phase einen Namen für Runtime.

Am 2026-10-05 bereits nachgezogen: jdl-sprachreferenz 0.2.1, jdl-blueprint-spec 0.5.4, 00-ontology-types-tags-phantoms, dyn-protocol-values v0.2, wie-jade-uebersetzt, wie-jade-ausfuehrt, spec-context-model-refactored, Markierungen in jdl-typalgebra-records-blueprints-notiz.


Änderungsprotokoll

v0.2.2 (2026-10-05) — Syntax nachgezogen. §5.3: Propagation mit try statt automatischer Propagation, neue Regel T-3 (Entscheidung aus den Arbeitsgesprächen); Beispiel mit try und ret; Dreiteilung angepasst. §7.7: Namensvorbehalt aufgelöst, N-10 geschlossen. §2.3: type Db : service statt service Db. §3.5: Unit statt (). §3.7: tag Phase in Blockform. §4.3, §6.2, §7.4: catch als Block mit Armen, neue Namen im Muster mit val. §6.3: val in Mustern. §6.2: Erfolgspfad in Ok(...); vorher passten die Typen der beiden Zweige nicht zusammen (C-6). Invariante 40 neu, Ersetzungstabelle ergänzt.

v0.2.1 (2026-10-05) — Rolle und Phase. §3.6: Benannte Rows tragen ihre Rolle immer ausgeschrieben (type X : row::Row = {…}); Begründung über die Verwechslung mit dem leeren Record; Abgrenzung leere Row gegen leeren Record, & ist kein Row-Operator; W-1 und W-2 angepasst. §3.7 neu: Laufzeit-Rows und Meta-Rows als zwei getrennte Arten, row nur als Grundart (W-12 bis W-14), Entstehung im Seed über tag Phase und RowDefinition als Vorschlag, Trusted Core; offen: Übergang (N-15), Rolle oder Basis (N-16), Namensraum (N-17). §4.5: Row-Plätze mit Phase (row::Row), W-4 angepasst. §10.5: G-11. Invarianten 30, 31, 36 angepasst, 37 bis 39 neu. N-12 um die Kandidaten aus dem Gespräch ergänzt. §14: Nachzug für jdl-meta-phase.

v0.2.0 (2026-10-05) — Rows als Typen. §3.6 neu: Rolle row, : gegen =, durchsichtige Namen (W-1 bis W-3), Trusted Core: row in der TypeKind-Liste. §4.5 neu: Row-Plätze in Protocols ersetzen die Row-Variable an Protocol-Methoden (W-4 bis W-7). §4.6 neu: provide auf Rows (W-8 bis W-10), Row-Bündel mit kanonischer Ordnung. §4.7 neu: Summe über einen Aufrufgraphen als Abfrage, requires entfällt (W-11), geladene Contexts bringen ihre Summe mit. §10.5 neu: G-8 bis G-10. Ergänzt: §1.1, §3.2 (Bündelordnung), §3.3 (Union-Schreibweise offen), §3.5 (Y-3 für Row-Plätze), §4.1 (g offen), §4.2 und §4.3 (A-3 und A-7 für T.Needs), §7.2 (Union-Wert, Typ-Arme), §8.2 (Labels nach Substitution). Invarianten 30 bis 36, zwei Ersetzungen, offene Punkte N-11 bis N-14, N-4 und N-8 erweitert. Widerspruch R-4 gegen Deklarationspflicht benannt.

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.