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
Neverist 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 undjdl-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.
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 keineservice Throw-Deklaration und keinen Nutzer-Handler dafür. Der einzige Weg, einThrow[E]zu erzeugen, ist der Ausdruckthrow(§5.1); der einzige Weg, es zu eliminieren, istcatch(§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:
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.
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:
Nominale Typen tun das nicht. Ein Enum bleibt atomar:
bleibt Throw[CheckoutError] und zerfällt nicht in seine Varianten.
Regel Y-1.
Throwverteilt ü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 SchreibweiseA | Bin 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 TypvariableVgilt 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.
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::Rowoderrow::MetaRow(§3.7). Sie hat keine Werte;val x: ShopNeedsist 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
tagund nichttype(00-ontology-types-tags-phantoms§6). Und es ist dieselbe Phase, die am Pfeil steht: DasMetahier ist dasMetaaus->Meta{. Nebenbei bekommtRuntimeeinen Namen; ob es schreibbar ist, war bisher offen (jade-service-typekind-arbeitsnotiz§8.4,jdl-meta-phaseMP-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
rowist 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 eineRow,->Meta{...}eineMetaRow. 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
Rowund die leereMetaRowsind 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 einerRowin eineMetaRow. Bei einer leerenRowist er harmlos. BeiThrow[E]braucht er eine Regel; betroffen ist etwarequireAtLeast(jdl-blueprint-spec§4.9), eine gewöhnliche Funktion mit->{Throw[DiagnosticSet]}, diecontributeaus der Meta-Phase aufruft. Vorschlag[V]: DieMetaRowlegt fest, welche Laufzeit-Elemente sie übernimmt und was sie bei ihr bedeuten. FürThrowist das naheliegend, denn Meta-Code läuft ohnehin auf einer VM im Compiler (addendum-begriffe-und-motiveG.1); erst an der Grenze der Meta-Phase wird daraus eine Diagnose. Die Alternative — Meta ruft nur Funktionen mit leererRow— widerspräche dem Ziel ausjdl-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 istMetaRoweine Art von Row und ihr eigener Inhalt belanglos. Als Basis gelesen istNeedsMeta : row::MetaRow = {…}„MetaRow plus diese Elemente". FürRowundMetaRowist 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ägeRowundMetaRowliegen, ist nicht festgelegt. Einimportim 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-phaseMP-12).
4. Row-Polymorphie¶
4.1 Offene Rows [N] 07 §2.3¶
Eine Row-Variable macht eine Funktion polymorph über die Effektmenge:
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]Obgmit §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.
- Zeile 2: Der Protocol-Autor sagt ausdrücklich, dass jede Implementierung eigene Services
mitbringen darf. Den Namen wählt er;
Needsist ein Beispiel. Die Rolle legt auch die Phase des Platzes fest (§3.7): Einrow::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::Rowodertype <Name> : row::MetaRowausweist. 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 percatcheliminiert (E-1′). Einprovideauf eine Row deckt ihren Service-Teil ab.Regel W-9. Gleicher Inhalt, gleiches
provide. Wegen W-2 ist einprovideaufShopNeedsdasselbe 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:
requiresentfällt. Wer bindet — ein CallGraph, ein Context —, fragt die Summe ab, vergleicht sie mit seinem Angebot und meldet jeden fehlenden Service einzeln mit Namen.- Rekursion ist kein Sonderfall. Weil jede Funktion ihre Row deklariert, ist das
Zusammenziehen ein einfacher Durchlauf über die Signaturen. Ruft
fdie Funktiongundgwiederf, 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. - 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.
throwist ein Sprachausdruck, keine Bibliotheksfunktion.
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 ewird über den Typ voneaufgelöst, nicht über die Row.throwunterliegt 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 vonparseUser. - Zeile 4: Ein Blockrumpf liefert keinen Wert von selbst;
retgibt ihn zurück.
Die Dreiteilung lautet damit:
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. Ohnecatchwird der Fehler weitergereicht.[E]— Ein Aufruf ohnetry, dessen Row ein nicht behandeltesThrowenthä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.
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¶
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:
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.catchingist, wenn es gebraucht wird, eine gewöhnliche Stdlib-Funktion auf Basis voncatchund keine Sprachform. Schließtjdl-sprachreferenzLü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.
catchinstalliert einen abortiven Handler für eine bestimmte Menge vonThrow-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 MengeSentfernt genauSaus der Row destry-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 zuThrow[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 unqualifiziertescatchzulässig; es eliminiert diese Menge.Enthält sie eine Row-Variable, muss die behandelte Menge explizit benannt werden. Ein unqualifiziertes
catchist dann ein Fehler. Folgt A-7.
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
catcheinen FehlertypEbehandelt, muss esEerschöpfend behandeln. Nicht behandelte Fälle müssen explizit weitergeworfen werden. Es gibt keine Variantenmengen innerhalb vonThrow[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 Hist 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 überwith(Scopeable,03-runtime§2,13-ir-specWithScope) 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.
Falliblegilt genau dann, wenn die effektive Row mindestens einThrow[E]enthält.
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′.
Deterministicverlangtrow ⊆ {Alloc[_], Throw[_]}und keineRefMut/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 denselbenThrow[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:
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.
Retryablewird als abgeleitetes Label gestrichen. Ersetzt C-2 in04aund die Ableitung in07§6.3 und04-axiomatics-truthprofile§7. Die Fassung in02-typsystemZ. 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 ekonsumiert 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
Drophä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 einedyn-Stelle prüft der Verifier, dass die tatsächliche Implementierung nicht mehr verlangt, als diedyn-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
- Abortivität ist eine Eigenschaft der Operation, nicht des Handlers. Rückgabetyp
Neveroder ein deklarierter abortiver Effekt macht eine Operation abortiv (K-1, K-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).
- Der Rumpf eines Handlers darf keine abortiven Effekte enthalten, die die Operation nicht deklariert (K-4).
- Der einzige eingebaute abortive Effekt ist
Throw[E](A-4′). Throw[E]ist ein Row-Element, kein deklarierbarer Service. Erzeugung nur überthrow, Elimination nur übercatch(E-1′).- Erschöpfung von
Alloc[A]trappt; Fallibilität ist keine Handler-Entscheidung (M-1′).
Row-Algebra
Throwverteilt über strukturelle Unions, nicht über nominale Typen (Y-1).- Rows mit
Throw[V]für eine ungebundene Typvariable sind nicht normalisiert; Normalisierung läuft nach der Substitution (Y-2). - Das Row-System kennt eine Beschränkung auf nicht-abortive Row-Variablen (Y-3).
- Ein Handler darf nur namentlich bekannte Elemente eliminieren; bei offener Row muss die eliminierte Menge benannt werden (A-7).
Throw
throw e : Never ->{Throw[E]};throwist ein Sprachausdruck (T-1).throwlöst über den Typ des Werts auf und unterliegt A-3 nicht (T-2).catchingist keine Sprachform (E-2′).
try / catch
catchist eine Handler-Installation, kein Match auf den Rückgabewert (C-1).- Ein
catchüberSentfernt genauSaus der Row (C-2). - Die Union entsteht auf der Wertseite; die Effektseite bleibt getrennt (C-3).
- Geschlossene Throw-Menge ⇒ unqualifiziertes
catchzulässig; offene Row ⇒ Qualifikation verpflichtend (C-4). - Wer einen Fehlertyp behandelt, behandelt ihn erschöpfend oder wirft explizit weiter; es gibt kein zweites Row-System für Enum-Varianten (C-5).
try/catchist ein Ausdruck; alle Zweige vereinigen sich zu einem Typ,Never-Zweige ausgenommen (C-6).- Kein
finally. Implizites Cleanup darf nicht abortiv sein (C-7).
Labels
Fallible⟺ mindestens einThrow[_]in der effektiven Row (L-F).Deterministicverlangtrow ⊆ {Alloc[_], Throw[_]}(P-2′); ein Cache muss den Abbruch mitcachen (P-2a).Retryableentfällt als abgeleitetes Label (L-R).
Payload
- Throw-Payloads müssen unwind-stabil sein (H-1).
throwkonsumiert seinen Payload (H-2).- Unwind-Stabilität ist abgeleitet, kein Nutzer-Keyword (H-3).
Trusted Core
- G-1 bis G-6 gelten als Architekturanforderung; das Format bleibt offen.
- Die Cleanup-Repräsentation steht vor dem Generator fest (G-7).
Grenzen
- Task-, FFI- und Remote-Grenzen materialisieren
Throw(B-1).
Rows als Typen (seit 0.2.0)
- Eine Row ist ein Typ der Rolle
row::Rowoderrow::MetaRowund hat keine Werte; eine benannte Row trägt ihre Rolle immer ausgeschrieben (W-1). - Row-Namen sind durchsichtig; Gleichheit über Phase und normalisierten Inhalt (W-2). Diagnosen nennen die Elemente, nie nur den Namen (W-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). - Eine
dyn-Stelle legt den Inhalt eines Row-Platzes fest (W-7). provideauf eine Row liefert nur Service-Elemente (W-8); gleicher Inhalt, gleichesprovide, verschiedene Bindungen desselben Service sind ein Konflikt (W-9); eine gelieferte Row ist eine Bindung, kein Wert (W-10).- Die Summe über einen Aufrufgraphen ist eine Abfrage; einzelne Signaturen bleiben deklariert (W-11).
- G-8 bis G-11 und
rowin der TypeKind-Liste gelten als Architekturanforderung an den Trusted Core.
Phasen von Rows (seit 0.2.1)
- Jede Row hat genau eine Phase; die Grundart
rowist selbst keine Row (W-12). - Der Pfeil bestimmt die Art einer Row; eine benannte Row der anderen Art ist dort ein Fehler (W-13).
- Die Phase gehört zur Identität einer Row; die leere
Rowund die leereMetaRowsind verschiedene Typen (W-14).
Aufrufstellen (seit 0.2.2)
- Jeder Aufruf, der abbrechen kann, trägt
try; ohnecatchwird 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 | trytry 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.