Zum Inhalt

JDL — Sprachreferenz

Status: Konsolidierungsentwurf Version: 0.2.3 Datum: 2026-10-06 Geltungsbereich: Sprachoberfläche von JDL — Syntax, Konzepte, Regeln Zielgruppe: Sprachimplementierung, Spec-Arbeit, Tooling


0. Über dieses Dokument

0.1 Zweck

Dieses Dokument sammelt die Syntax und die tragenden Konzepte von JDL an einem Ort. Es ist als Anker gedacht: ein Stand, gegen den man andere Dokumente prüfen kann, statt sie gegeneinander zu prüfen.

Es ersetzt keine Entwurfsdokumente. Wo ein Dokument die Begründung einer Entscheidung enthält, bleibt es die Quelle; hier steht nur das Ergebnis.

0.2 Kennzeichnung

Jede Aussage in diesem Dokument trägt eine von vier Marken. Die Marke sagt, wie belastbar die Aussage ist.

Marke Bedeutung
[N] Normativ in einem bestehenden Dokument belegt. Quelle ist genannt.
[A] Aus Beispielen in bestehenden Dokumenten abgeleitet, aber nirgends als Regel formuliert. Fundstelle ist genannt.
[O] Offen. Entweder nicht spezifiziert, oder zwei Dokumente widersprechen sich.
[Entscheidung] Beim Verfassen oder in den Arbeitsgesprächen entschieden und hier zuerst aufgeschrieben; gesammelt in §0.4.

Es gibt in diesem Dokument keine erfundene Syntax. Wo etwas fehlt, steht [O] und eine Beschreibung der Lücke — keine Füllung.

0.3 Prioritätsregel

Bei Widerspruch zwischen Quellen gilt:

  1. 12-design-constitution — Charta
  2. 07-cast-effekte-refinements v0.3 — Effect Row, Casts, Services, Refinements
  3. 04a-label-inferenz-regeln v0.6 — Labelzustände und Inferenz
  4. Übrige normative Dokumente
  5. Arbeitsnotizen und Tutorials

Die Reihenfolge ist der Grund, warum manche Beispiele in 01-grundlagen in diesem Dokument anders aussehen: Sie sind nicht falsch geworden, sie sind nicht nachgezogen.

0.4 Getroffene Entscheidungen

Die folgenden Punkte waren beim Verfassen offen und wurden entschieden. Sie sind hier gesammelt, weil sie noch in keinem anderen Dokument stehen oder hier zuerst stehen.

Punkt Entscheidung Wirkt auf
Compile-Zeit-Funktionen typefn entfällt; Compile-Zeit-Auswertung ist def mit Meta am Pfeil, ->Meta{} (früher: in der Row; jetzt jdl-meta-phase MP-20) §15
Enum-Schreibweise Blockform statt führender \| §5.2
Fehlerkonvention Durchgängig Throw[E] in der Row, auch in Feldpositionen §9, §19
Union-Schreibweise (2026-10-05) Blockform type X : union { A, B } statt A \| B §5.3
Rows als Typen (2026-10-05) Row als Typ; : nennt die Rolle, = den Inhalt; die Rolle steht immer da §7.7
Laufzeit- und Meta-Rows (2026-10-05) Jede Row hat genau eine Phase: row::Row oder row::MetaRow; row allein ist nur die Grundart §7.7
Row-Plätze in Protocols (2026-10-05) benannter Platz type Needs : row::Row statt einer Row-Variable g an Protocol-Methoden §11.7
Bedarf eines Aufrufgraphen (2026-10-05) Summe der deklarierten Rows als Abfrage; requires entfällt §19.1
Eine Engine, mehrere Blueprints (2026-10-05) Union der Blueprint-Typen im Spec-Platz §19.2
Drei Rollen mit Feldern (2026-10-05) Record = Daten, Blueprint = Absicht, Struct = Verhalten; der Record ist der dümmste Container §5.10
& nach Rolle (2026-10-05) Was & bedeutet, sagt die Rolle links: Record zusammenlegen, Blueprint partiell anwenden §5.10
Newtype-Schreibweise (2026-09-14) newtype entfällt; : hinter dem Namen stiftet einen neuen Typ (type UserId : str), = ist ein Alias §5.4
Syntax aus den Arbeitsgesprächen (nachgezogen 2026-10-05) Unit statt (); Blockrumpf ohne Wert, ret; try an jeder abbrechenden Stelle; catch als Block mit Armen; val für neue Namen im Muster, keine Guards; Service als Rolle type X : service; val implizit, := leitet den Typ ab; Komma optional §1.2, §2.1, §3.3, §6.1, §8.1, §9.3, §9.4, §16, §17.3

Sichtbarkeit, @compiler und mod.jdl (§18) sind nicht hier gesammelt: Sie stehen bereits in spec-namespaces-und-module (D-13, D-14, D-18).

Die dritte Entscheidung schließt den offenen Punkt O-7 aus 07 §11.1 mit und berührt Constitution §8.2 („Blueprints sind effektfrei"). Siehe §19.3.

Die Begründungen der Entscheidungen vom 2026-10-05 stehen in jdl-effect-rows-und-throw §3.6, §3.7 und §4.5 bis §4.7, jdl-blueprint-spec §9 sowie 00-ontology-types-tags-phantoms §3a und §7a.


1. Lexikalische Struktur

1.1 Kommentare [N] 01-grundlagen §15

// Zeilenkommentar

/// Dokumentationskommentar über einer Deklaration.
/// Von LSP und Docs-Generator auswertbar.
def registerUser(name: str) ->{UserDb, Throw[UserError]} User

Ein Blockkommentar ist nicht spezifiziert. [O]

1.2 Trennzeichen

Das Zeilenende trennt — in Structfeldern, Parameterlisten und Blöcken. Kommas sind dort nicht nötig. [N] 01-grundlagen §4

Einzeilig bleibt das Komma möglich, etwa union { A, B }. Innerhalb von Klammern trennt ein Zeilenumbruch wie ein Komma; das gilt für Enum-Varianten, Tupel, Parameter und Feldlisten. [Entscheidung]

:: trennt Namensräume, . greift auf Member zu. Namensräume werden nie mit . getrennt. [N] spec-namespaces-und-module §2

users::service::findUser(email)    // Namespace
user.email                         // Member

1.3 Zahlenliterale [N] jdl-primitives-spec §2

Numerische Literale sind typenlos und werden aus dem Kontext inferiert. Ohne Kontext gilt: Ganzzahl → i64, Gleitkomma → f64.

42u8            // Suffix überschreibt Inferenz
3.14f32
0xFF            // hexadezimal
0b1010_1010     // binär
0o755           // oktal
1_000_000       // Underscore als Trenner
0xFF_00_FF

Verboten sind führender Underscore (_42), abschließender Underscore (42_) und Underscore direkt nach dem Präfix (0x_FF).

Ein Gleitkommaliteral braucht einen Dezimalpunkt. Wissenschaftliche Notation ist nur zusammen mit einem Punkt gültig:

1.0    3.14    1.0e10    1.5e-3    1.0E10     // gültig
1e10                                          // Fehler: kein Dezimalpunkt

Der Lexer entscheidet allein am Dezimalpunkt, ob ein Literal ganzzahlig oder gleitkommig ist. Kein Lookahead auf e.

1.4 Unit-Literale [O] — Widerspruch

jdl-primitives-spec §3 legt fest, dass ein Unit-Literal ein Methodenaufruf auf einem Zahlenliteral ist. Der Lexer liest IntLiteral.Identifier, der Parser senkt 5000.ms zu (5000).ms().

5000.ms
1.5.s
100.px

01-grundlagen §1 schreibt dagegen ohne Punkt:

val defaultTimeout = 5000ms

Und 07 §8.1 verwendet wiederum die Punktform (24.hours, 100.ms).

Zwei von drei Fundstellen sprechen für die Punktform, und nur sie hat eine Begründung (kein Sonderwissen des Lexers über Einheitennamen). Die punktlose Form in 01-grundlagen ist vermutlich nicht nachgezogen — normiert ist es nirgends.

Es gibt kein sprachliches Sonderwissen über einzelne Einheiten. Unit-Methoden sind gewöhnliche Methoden in der Stdlib; die Orphan-Regel (§11.4) verhindert, dass Nutzercode eigene auf Primitiven definiert.

1.5 Stringliterale [N] 01-grundlagen §11

val msg = f"Hallo, {alice.name}! Du bist {alice.age} Jahre alt."   // interpoliert

val pattern = r"\d+\.\d+"                                          // roh, keine Escapes
val path    = r"C:\Users\alice\Documents"

val sql = """
    SELECT name, email
    FROM users
"""                                                                // mehrzeilig

val query = f"""
    SELECT name FROM users WHERE age >= {minAge}
"""                                                                // mehrzeilig interpoliert

Die Einrückung mehrzeiliger Literale wird normalisiert.

1.6 Logische Operatoren [N] 01-grundlagen Änderungstabelle

and, or, not sind die bevorzugte Schreibweise. &&, ||, ! bleiben gültig.


2. Werte und Bindungen

2.1 val und var [N] 01-grundlagen §1

val name = "Alice"         // immutabel
var counter = 0            // mutabel
counter = counter + 1      // ok
name = "Bob"               // Fehler: val ist immutabel

Seit den Arbeitsgesprächen [Entscheidung]: var muss ausdrücklich stehen, val darf entfallen. name : str = "Alice" ohne Schlüsselwort ist ein val; val auszuschreiben bleibt erlaubt. := lässt den Typ ableiten, etwa val result := ….

2.2 Kein const [N] 01-grundlagen §1

Ein val mit Literalzuweisung ist für den Compiler als Compile-Zeit-Konstante erkennbar. Für explizite Garantien dient das Typsystem (§5.6).


3. Primitive Typen

3.1 Zahlen [N] jdl-primitives-spec §1

Gruppe Typen
Vorzeichenbehaftet i8 i16 i32 i64
Vorzeichenlos u8 u16 u32 u64
Gleitkomma f32 f64
Plattformgröße isize usize

isize und usize sind eigenständige nominale Typen, keine Aliase auf i64/u64. Auf 64-Bit-Plattformen existieren verlustfreie Casts in der Stdlib, die implizit angewendet werden. Kein Code darf von einer impliziten Identität ausgehen.

i128 und u128 sind nicht im Core. Sie wären Stdlib-Typen auf Basis von u64-Paaren.

3.2 bool [N] jdl-primitives-spec §1.2, §4.3

Genau zwei Bewohner, true und false. Kein numerischer Typ. Konversionen zu Integern sind Stdlib-Konvention über CastTo, nicht Sprachsemantik.

3.3 Unit [N] jdl-primitives-spec §4.1

Der Typ mit genau einem Bewohner. Die Schreibweise ist durchgängig Unit; () als Schreibweise für Unit entfällt [Entscheidung]. () bleibt nur die leere Parameterliste.

def log(msg: str) ->{LogService} Unit

3.4 Never [N] jdl-primitives-spec §4.2

Der Bottom-Typ — kein Bewohner, nicht konstruierbar. Funktionen mit Rückgabetyp Never kehren nie zurück. Ein Wert vom Typ Never ist zu jedem anderen Typ kompatibel.

3.5 Overflow und Float-Semantik [O]

Die Overflow-Semantik von Add, Sub, Mul auf Integern ist eine Entscheidung der Stdlib-Protokollimplementierungen und offen (jdl-primitives-spec §1.3).

NaN-Verhalten und die Frage, ob f32/f64 Equatable und Comparable implementieren, sind ebenfalls offen (§1.4).


4. Zusammengesetzte Typen

4.1 Dynamisches Array [T] [N] jdl-primitives-spec §5.1

val names: [str] = ["Alice", "Bob", "Charlie"]
var list: [str] = []
list.push("Dave")

val first = names[0]
val slice = names[1..3]     // 1..3 ist ein Range[i32]; Ergebnis ist eine Kopie

Übergabe an eine Funktion ist eine Kopie. Kein implizites Borrowing.

4.2 Fixgröße-Array [T; N] [N] jdl-primitives-spec §5.1

N ist eine Compile-Zeit-Konstante und ein Literal-Typ.

val rgb: [u8; 3] = [255u8, 128u8, 0u8]

4.3 Tuple [N] jdl-primitives-spec §5.1

val pos: (f64, f64) = (52.52, 13.405)
val (lat, lon) = pos
val x = pos.0

Normativ: (T) mit genau einem Element ist kein Tupeltyp, sondern ein gruppierter Ausdruck. Der Parser akzeptiert (T) nur zur Gruppierung oder als Beginn einer Funktionssignatur, wenn -> folgt.

4.4 Map und Set [N] jdl-primitives-spec §5.2

Beides sind reine Stdlib-Typen ohne privilegierte Literalsyntax.

val scores = Map.from([("Alice", 42), ("Bob", 17)])
val unique = names |> Set.from

Set[T] verlangt T: Hashable + Equatable. Das ist eine normative Constraint.

4.5 Nicht vorgesehen [N] jdl-primitives-spec §5.3

Anonyme Structs und strukturelle Typen sind nicht vorgesehen. JDL ist durchgehend nominal. Feld-Destrukturierung im Pattern Matching (§16) ist kein struktureller Typ, sondern ein lokales Parser-Feature auf nominalen Typen.


5. Typdeklarationen

5.1 Struct [N] 01-grundlagen §4

type User: struct {
    name:  str
    email: str
    age:   i32
}

val alice = User { name: "Alice", email: "alice@example.com", age: 30 }

Zeilenende trennt die Felder; Kommas sind nicht nötig.

5.2 Enum — Blockform [Entscheidung]

Varianten stehen in einem Block. Diese Form ersetzt die bisherige Schreibweise mit führendem |.

type Role: enum {
    User
    Admin
    Moderator
}

type Option[T]: enum {
    Some(T)
    None
}

type UserError: enum {
    NotFound      { id: str }
    InvalidEmail  { email: str, reason: str }
    AlreadyExists { email: str }
}

Eine Variante ist entweder nackt, trägt eine positionale Nutzlast in runden Klammern, oder benannte Felder in geschweiften Klammern.

Reichweite der Blockform. Das Zeichen | hatte in JDL fünf Rollen:

Rolle Beispiel Stand
Enum-Varianten type Role: enum { ... } Blockform, entschieden
Tag-Enums tag OwnPolicy : enum { ... } Blockform — Lesart der allgemeinen Entscheidung, dass Rümpfe in {} stehen statt mit = und \|
Union von Typen type X : union { A, B } Blockform, entschieden (2026-10-05, §5.3)
Function Unions type Cmd = \| def f(...) -> T offen [O]
Match-Arme match x { \| Ok(val v) => ... } \| bleibt [A] — catch schreibt seine Arme entschieden so, „wie match“

Offen ist damit nur noch die Function Union (§6.5).

5.3 Union von Typen [N] 01-grundlagen §5 — Schreibweise [Entscheidung] (2026-10-05)

Eine Union fasst bestehende Typen zu einem Typ zusammen. Die Mitglieder stehen in einem Block, wie die Varianten eines Enums.

type StringOrNumber : union { str, i64 }

type AnyError : union {
    UserError
    IoError
    DbError
}
  • Zeile 1: einzeilig trennt ein Komma.
  • Zeilen 3 bis 7: mehrzeilig trennt der Zeilenumbruch, wie bei Enum-Varianten und Structfeldern.

Diese Form ersetzt die frühere Schreibweise type X: union = A | B.

Unions werden automatisch flach und entfernen Duplikate [N]:

type A : union { X, Y }
type B : union { Y, Z }
type C : union { A, B }      // äquivalent zu union { X, Y, Z }

Union gegen Enum. Gleiche Klammern, andere Bauanleitung: Im Enum-Block erfindet man Namen, nämlich die Varianten. Im Union-Block nennt man Typen, die anderswo schon deklariert sind. Steht in einem Union-Block ein Name, der kein Typ ist, ist das ein Fehler. Die Fehlermeldung sollte genau das sagen, statt über einen unbekannten Variantennamen zu klagen; das ist eine Anforderung an die Werkzeuge, keine Sprachregel.

[O] Namenlose Unions im Typausdruck. Entschieden ist die Deklaration. Wie eine Union ohne eigenen Namen in einem Typausdruck geschrieben wird — etwa als Typ eines gefangenen Fehlers, A | B | C in jdl-effect-rows-und-throw §7.2 —, ist offen.

[O] Literal-Unions. Ob type HttpSuccessCode = 200 | 201 | 204 (§5.6) ebenfalls die Blockform bekommt, ist offen.

Wie man einen Union-Wert wieder auseinandernimmt, steht in §16.3.

5.4 Newtype — Schreibweise [Entscheidung] (2026-09-14), Bedeutung [N] 02-typsystem §4

type UserId  : str      // neuer Typ, aufgebaut wie str
type OrderId : str      // noch ein neuer Typ, ebenfalls wie str
type RawId   = str      // kein neuer Typ: RawId ist str
  • Zeilen 1 und 2: UserId und OrderId sind verschiedene Typen, obwohl beide wie str aufgebaut sind. Wo eine UserId erwartet wird, passt weder eine OrderId noch ein nackter str.
  • Zeile 3: ein Alias. RawId ist nur ein zweiter Name für str.

Ob ein neuer Typ entsteht, entscheidet das Zeichen hinter dem Namen: Ein Doppelpunkt stiftet einen neuen Typ, ein Gleichheitszeichen nicht. Das Schlüsselwort newtype entfällt; es sagte nur ein zweites Mal, was der Doppelpunkt schon sagt. Überholt sind damit type UserId = UserId(str) aus 02-typsystem §4 und newtype UserId = IdCarrier aus jdl-typalgebra-records-blueprints-notiz §2.

Ein Newtype ist ein eigener nominaler Typ. Er ist zugleich das Mittel, um die Orphan-Regel (§11.4) für fremde Typen zu umgehen.

[O] Werte erzeugen. Wie ein Wert eines Newtypes entsteht, ist mit der neuen Form nicht festgelegt. 02-typsystem §4 schrieb UserId("u-123"); dort kam der Name des Konstruktors aus der Deklaration type UserId = UserId(str).

[O] Blueprint-Profile. Ob ein Profil : oder = schreibt, also einen neuen Typ stiftet oder derselbe Blueprint bleibt, ist offen (jdl-blueprint-spec §3.6, Punkt 8).

5.5 Refinement-Typ [N] 02-typsystem §4

type Email = str :> ValidEmail

Anders als ein Newtype ist der Wert weiterhin der Basistyp und überall dort einsetzbar, wo dieser erwartet wird.

[O] Refinement-Typ gegen Refinement. Nach §5.4 ist Email ein Alias, also str. Nach jdl-blueprint-spec §8.1 erzeugt ein Refinement keinen neuen Typ, sondern landet als Patch auf dem bestehenden Typ. Zusammen hieße das: ValidEmail gälte für jeden str im Programm. Ob ein Refinement-Typ eine eigene Art Typ ist oder ob 02-typsystem §4 hier überholt ist, ist nicht entschieden.

5.6 Literal-Typen [N] 01-grundlagen §1, jdl-primitives-spec §6

type MaxRetries = 3                        // genau ein Bewohner
type HttpSuccessCode = 200 | 201 | 204     // Union von Literalen

Normativ ist die Beziehung zu Enums: Enums sind konzeptuell Literal-Typ-Unions auf Wertebene. Dasselbe Prinzip auf Typebene ist Literal-Matching in Meta-Funktionen (§15).

5.7 Meta-Präfix an einer Deklaration [N] 08-grammar-sketch §7

type <{
    derive: [Equatable, Hashable]
    memory: Value
    share:  Sync
    drop:   Trivial
}> Point: struct {
    x: f64
    y: f64
}

Dieselbe Information ist als Suffix schreibbar (§14.1).

5.8 Tag-Deklaration [N] 08-grammar-sketch §4

Ein Tag ist ein Typ ohne Werte — er existiert nur, um Rollen zu unterscheiden.

tag RequestArena
tag Primary
tag Replica

tag RequestArena : ArenaKind          // Zugehörigkeit zu einer Tag-Domäne

tag TaskLocal
    :> Own(Unique)
    :> Share(Local)

Tag-Enums haben dieselbe Blockform wie Enums (§5.2).

tag OwnPolicy : enum {
    Unique
    Shared
    Weak
}

5.9 Row-Deklaration [Entscheidung] (2026-10-05)

Eine Row ist ein Typ. Sie beschreibt eine Menge von Effekten und hat keine Werte. Ihre Rolle steht immer da und nennt zugleich ihre Phase. Einzelheiten stehen in §7.7.

type ShopNeeds : row::Row = {Orders, Payments}     // spekulativ

5.10 Record, Blueprint, Struct [Entscheidung] (2026-10-05)

Drei Rollen haben benannte, getypte Felder. Sie unterscheiden sich nicht in der Form, sondern darin, was man mit ihnen tun darf. Ausgearbeitet ist das in 00-ontology-types-tags-phantoms §3a; hier steht nur die Kurzfassung.

Record      Daten        hält nur Daten, kann nichts hinzulernen, reist überall hin
Blueprint   Absicht      beschreibt, was eine Engine tun soll; lebt nur in der Meta-Phase
Struct      Verhalten    hält Werte, kann provided werden und Protocols implementieren

Was & bedeutet, sagt die Rolle links.

Record & {…}       Formen zusammenlegen
Blueprint & {…}    partielle Applikation des Rezepts (Profil)
Struct & {…}       Fehler — Vorschlag, siehe unten

& auf einem Blueprint und _ im Aufruf sind derselbe Gedanke in zwei Phasen (jdl-partielle-applikation CALL-4). Zwei Unterschiede folgen aus dem Zweck und sind gewollt [A]:

  1. Im Aufruf muss jede offene Stelle als _ dastehen (PA-1). Bei & {} bleibt offen, was man nicht nennt; geprüft wird erst, wenn die Engine das Rezept einlöst. Ein Aufruf will am Ende vollständig sein, ein Rezept will angepasst werden.
  2. Ein var-Feld darf ein späteres Profil neu setzen. Ein bei _ festgelegter Parameter verschwindet dagegen aus der Signatur (PA-4).

[O] & auf einem Struct. Vorschlag: ein Fehler mit Hinweis. Ein Erweitern wäre Vererbung durch die Hintertür, weil ein neuer Typ kein provide erbt; ein Feld user: User sagt dasselbe ehrlich. Wer Daten ableiten will, leitet die Form als Record ab. Ein Fehler lässt sich später zu einer Bedeutung lockern, eine erlaubte Bedeutung nicht mehr zurücknehmen.


6. Funktionen

6.1 Deklaration [N] 01-grundlagen §2 — Blockrumpf [Entscheidung]

// Ausdrucksform
def double(x: i32) -> i32 = x * 2

// Blockform — der Rückgabewert steht hinter ret
def greet(name: str) -> str {
    val msg = f"Hello, {name}!"
    ret msg
}

Ein Blockrumpf hat keinen eigenen Wert; der letzte Ausdruck ist nicht der Rückgabewert. Zurückgegeben wird mit ret, das auch als vorzeitiger Ausstieg dient. Die =-Form bleibt bestehen, und if, match und try bleiben Ausdrücke. Das ersetzt die Regel aus 01-grundlagen §2, nach der der letzte Ausdruck zurückgegeben wurde.

6.2 Funktionstypen und Regel C-1 [N] 07 §1.3

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

type Mapper[T, U] = ((T) -> U)
type Thunk[T]     = (() -> T)
type G            = (User) ->{Db} UserSummary

val summary = user -> UserSummary        // Cast: linke Seite ist ein Wert

T -> U ist kein Funktionstyp. Damit muss der Parser nie raten.

6.3 Generics [N] 01-grundlagen §2, 02-typsystem §4a

def identity[T](x: T) -> T = x

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

Die Grammatik der Typparameter steht in §13. Ob die Row-Variable g hier als Typparameter mit Rolle row::Row weiterlebt, ist offen (§7.7).

6.4 Benannte Argumente [N] 01-grundlagen Änderungstabelle

f(name = "Alice")

Gleichnamige Argumente dürfen kurz stehen: makeReport(title) statt makeReport(title = title) [Entscheidung]. Ein _ an Argumentstelle macht den Aufruf zur partiellen Applikation (jdl-partielle-applikation PA-1).

Ob benannte und positionale Argumente mischbar sind und ob Parameter Vorgabewerte haben dürfen, ist nicht spezifiziert. [O] — 07 §8.1 zeigt Vorgabewerte allerdings in Structfeldern (only: CachePolicy = CachePolicy.Always), was für Funktionsparameter nichts festlegt.

6.5 Function Unions [N] 01-grundlagen §14 — Schreibweise [O] siehe §5.2

Ein Wert dieses Typs ist genau eine der Operationen samt ihrer Argumente. Nützlich für Aktor-Nachrichten und RPC.

type UserCommand =
    | def register(name: str, email: str, age: i32) ->{Throw[UserError]} User
    | def find(email: str)                          ->{Throw[UserError]} User
    | def list()                                    ->{Throw[UserError]} [User]

7. Die Effect Row

7.1 Grundprinzip [N] 07 §2.1

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

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

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

Die Row ist keine versteckte Parameterliste. Es wird nichts hineingereicht. Sie ist eine Bedingung an den Aufrufkontext — eine Schuld, die abgetragen wird: Jeder installierte Handler streicht ein Element, bis in main die leere Menge übrig bleibt.

7.2 Notationsregeln [N] 07 §2.2

Regel R-1. Ein Funktionstyp hat immer eine geklammerte Parameterliste.

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

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

7.3 Algebra [N] 07 §2.3

Die Row ist eine ungeordnete Menge.

Vereinigung bei Komposition:

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

Abschwächung: Eine Funktion mit kleinerer Row ist überall einsetzbar, wo eine größere erwartet wird. Die Umkehrung gilt nicht.

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

Row-Variablen erlauben Polymorphie über die Effektmenge:

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

map führt keine eigenen Effekte ein; es reicht durch, was der Aufrufer mitbringt.

An Protocol-Methoden gibt es keine Row-Variable mehr; dort tritt ein benannter Row-Platz an ihre Stelle (§11.7).

7.4 Die leere Menge bedeutet leer [N] 07 §2.4

JDL folgt der Unison-Lesart: ->{} verbietet ausdrücklich jeden Effekt. Polymorphie braucht eine explizite Variable ->{g}.

Der Preis ist real und bewusst gezahlt: Jede Funktion höherer Ordnung in der Stdlib trägt eine explizite Row-Variable. Genau das macht ->{} überhaupt erst zu einer Aussage.

7.5 Inferenz [N] 07 §2.7

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

[O] Widerspruch. Nach einer späteren Entscheidung ist -> ohne {} nur eine Kurzschreibweise für die leere Row; braucht der Rumpf etwa Fs, ist das ein Fehler, und die Row muss ausgeschrieben werden. Das verträgt sich nicht mit einer modul-internen Inferenz nach R-4. Die Summe über einen Aufrufgraphen (§19.1) setzt deklarierte Rows voraus; eine der beiden Regeln muss nachziehen.

7.6 Suspendierte Berechnungen [N] 07 §2.6

Ein Thunk, dessen Effekte im Typ stehen, ersetzt den früheren Effect-Wert:

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

Der Default hat sich gegenüber v0.2 umgedreht: Alles läuft sofort, Aufschieben ist der explizite Schritt. Die typische Fehlerklasse wechselt damit von „vergessen auszuführen, es passiert nichts" zu „vergessen zu suspendieren, es läuft zu früh".

Eine Trailing-Block-Form zur Vermeidung von () => an jeder Aufrufstelle ist vorgeschlagen, aber nicht entschieden:

withRetry(3) { loadUser(id) }        // spekulativ, 07 §2.6

7.7 Rows sind Typen [Entscheidung] (2026-10-05)

Eine Row ist ein Typ. Die Rolle steht wie bei allen Typen hinter dem Doppelpunkt. Es gilt eine Regel, die man einmal lernt und überall anwendet: 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. Das ist die Form für Row-Plätze in Protocols (§11.7).
  • Zeile 2: ein Name für genau diese Row.
  • Zeile 3: ausdrücklich keine Services.

Die Rolle steht immer da. Auch wenn der Inhalt feststeht, wird die Rolle ausgeschrieben. Ohne sie wäre type NoNeeds = {} nicht von einem Alias für den leeren Record zu unterscheiden; die Art einer Row ließe sich nicht einmal ableiten.

Jede Row hat genau eine Phase. row::Row ist eine Laufzeit-Row, row::MetaRow eine Meta-Row. Eine Row ohne Phase gibt es nicht, und keine Row gilt in beiden Phasen. row allein ist nur die Grundart, aus der die beiden gebaut werden; sie steht im Seed, nicht in Benutzercode. Der Pfeil bestimmt, welche Art an ihm stehen darf: ->{…} eine Laufzeit-Row, ->Meta{…} eine Meta-Row. Begründung und Seed-Skizze: jdl-effect-rows-und-throw §3.7.

type Needs : {} wäre missverständlich und ist nicht die Form: In ->{} heißt {} „gar nichts", hier sollte es „noch zu füllen" heißen. Gleiche Zeichen, entgegengesetzte Bedeutung.

Ein Row-Name ist durchsichtig. ShopNeeds ist eine Abkürzung, kein neuer Typ mit eigener Identität. Der Compiler setzt überall den Inhalt ein; zwei Rows sind gleich, wenn Phase und Inhalt gleich sind. Diagnosen nennen immer die einzelnen Services, nie nur den Namen.

Rows werden im Inhalt erweitert, nicht mit &.

type MoreNeeds : row::Row = {ShopNeeds, Logging}     // spekulativ

& hat eine Richtung (rechts überschreibt links), die Vereinigung von Rows nicht.

Eine Row hat keine Werte. val x: ShopNeeds ist ein Fehler.

Meta gehört nicht hinein. Meta ist die Phase vor der Row, kein Row-Element (jdl-meta-phase §2.1).

Geliefert wird eine Row per provide. Wer für die Services einer Row einsteht — in der Regel ein Context —, macht ein provide auf sie. Geliefert werden nur Services; Throw wird abgefangen, nicht geliefert. Einzelheiten in jdl-effect-rows-und-throw §4.6.

[O] Row-Variablen an gewöhnlichen Funktionen. Ob das g aus §7.3 als Typparameter mit Rolle row::Row weiterlebt, als Verweis auf die Row eines Parameters oder eine eigene Schreibweise behält, ist nicht entschieden (jdl-effect-rows-und-throw N-12).

[O] Übergang von Laufzeit- in Meta-Rows. Meta-Code ruft gewöhnliche Funktionen auf, wenn deren Row in seine Meta-Row passt (jdl-meta-phase MP-21). Mit zwei getrennten Arten von Rows ist das kein Teilmengentest mehr, sondern ein Übergang. Bei leerer Row harmlos, bei Throw[E] braucht es eine Regel (jdl-effect-rows-und-throw N-15).

[O] Rolle oder Basis. Ob : row::MetaRow als Art („eine Meta-Row") oder als Basis („MetaRow plus diese Elemente") zu lesen ist (jdl-effect-rows-und-throw N-16).

7.8 Inferenz gegen Summe [Entscheidung] (2026-10-05)

Zusammengezogen wird die Sicht auf einen Aufrufgraphen, nicht die Signatur einer einzelnen Funktion. Jede Funktion nennt ihre Row selbst. Was alle Funktionen unter einem Einstiegspunkt zusammen brauchen, ist eine Abfrage an die CompilerDB (§19.1).


8. Services

8.1 Deklaration [N] 07 §3.1

Was die Literatur Ability nennt, heißt in JDL service. Ein Service ist ein Typ mit der Rolle service, deklariert wie andere Typen [Entscheidung].

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

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

Zwei Punkte sind normativ:

  1. Der Instanz-Parameter [i] ist optional (§8.3).
  2. Die Operationssignaturen tragen kein Result. Der Fehler wandert in die Row des Handlers (§9).

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

[O] Widerspruch. 10-runtime-handles X.2.1 deklariert dieselben Capabilities als protocol Db { ... }. 07 §3.1 stellt fest: es gilt service, X.2.1 ist zu korrigieren. Der Widerspruch besteht in der Quelldatei fort.

8.2 Aufruf [N] 07 §3.2

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

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

Regel A-1. Enthält die Row genau ein Element des gesuchten Service, ist der Aufruf unqualifiziert zulässig.

8.3 Instanzen über Tags [N] 07 §3.4

Zwei Instanzen desselben Service werden über Typ-Tags unterschieden, nicht über Namen.

tag Primary
tag Replica

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

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

Ein Tag ist eine Rolle, keine Instanz: Derselbe Tag kann in verschiedenen Läufen von verschiedenen Handlern bedient werden — Produktion und Test — ohne dass die aufrufende Funktion sich ändert.

8.4 Mehrdeutigkeit [N] 07 §3.5

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

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

def refreshUser(id: UserId) ->{Db[Replica], Db[Primary]} Option[User] {
    val rows = Db[Replica].query(f"SELECT * FROM users WHERE id = {id}")
    ...
}

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

A-3 garantiert, dass sich die Bedeutung eines Rumpfes nie dadurch ändert, dass ein Aufrufer einen Service hinzufügt.

A-3 gilt für einen Row-Platz wie T.Needs (§11.7) genauso [A]: Sein Inhalt ist im generischen Rumpf ebenso unbekannt wie der einer Row-Variable.

8.5 Ein Service ist eine Forderung, kein Wert [N] 07 §3.3

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

Abgrenzung zu Capabilities. Ein Service ist eine Forderung: steht im Pfeil, wird vom umgebenden Handler aufgelöst, Nutzercode hält ihn nie. Eine Capability[T] mit rights und attenuate ist ein Wert: unfälschbar, explizit weitergereicht, abschwächbar, an ein konkretes Objekt gebunden. Beide greifen ineinander, dürfen aber nicht zusammengezogen werden.

8.6 Handler-Definition [N] 07 §3.6

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

Der Instanz-Tag steht hier bewusst nicht. Ein Handler ist polymorph in der Instanz — derselbe PostgresHandler bedient Primary wie Replica; welche Rolle er erfüllt, entscheidet die Installation. Die Klammer in provide Db[...] ist damit eindeutig der Handlertyp.

Es gibt kein resume und kein Operations-Matching. Ein Handler ist eine gewöhnliche Methodenimplementierung (Folge von A-4, §8.8).

[O] Widerspruch zur Schreibweise. 01-grundlagen §13 und 02-typsystem §1 schreiben die Service-Handler-Bindung als provide UserDb for InMemoryUserDb { ... }. 07 §1.1 und §3.6 schreiben provide UserDb[PostgresHandler] { ... }. Nach der Prioritätsregel gilt die Klammerform. Die for-Form bleibt der Protocol-Implementierung vorbehalten (§11.2).

8.7 Handler-Installation — drei Formen [N] 07 §3.7

Global:

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

Bereichsbegrenzt — eine gewöhnliche Stdlib-Funktion mit Block, kein Schlüsselwort:

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

Deklarativ — im Blueprint (§19.1):

env: {
    Db[Primary]:     PostgresHandler { pool }
    Db[Replica]:     PostgresHandler { replicaPool }
    Alloc[ReqArena]: ArenaHandler { size: 64.kib }
}

Regel A-6. withHandler ist die Quellform, Evidence Passing das Lowering. Eine Laufzeitsuche „Capability-Typ → Handler-Wert" entfällt als Auflösungsmechanismus für statisch bekannte Rows.

Abgrenzung zu with. with expr as name { body } ist der Ressourcen-Scope: verlangt eine Scopeable[R]-Instanz, senkt zu acquire + Body + release (auch auf Fehlerpfaden). with bindet einen Wert und lässt die Row unverändert; eine Handler-Installation bindet keinen Wert und entfernt ein Element aus der Row. Zwei verschiedene Operationen — daher withHandler als eigene Funktion.

8.8 Handler-Klassen [N] 07 §3.8

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

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

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


9. Fehler

9.1 Die vier Arten des Fehlschlagens [N] 07 §4.3

Art Fangbar Ort
Option-Abwesenheit n/a — kein Fehlschlag Wert
Throw[E] ja, über Handler Sprachebene
Trap nein Engine; invalidiert den lokalen Scope
Abbruch nein Prozessende

9.2 Throw[E] [N] 07 §4.1

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

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

Zigs Fehlermengen und die Effect Row haben dieselbe Algebra: beides Mengen, beide vereinigen sich bei Komposition, beide erlauben Teilmengen-Coercion. Der Fehlerkanal ist kein Fremdkörper in der Row, sondern ein Spezialfall dessen, was sie ohnehin tut.

9.3 Der Aufrufer entscheidet [N] 07 §2.5, §4.2

Regel E-2. Es gibt genau einen Fehlerkanal und genau einen Umwandlungspunkt. Der Umwandlungspunkt wird vom Aufrufer gewählt, nicht vom Autor der Funktion.

val idResult =                                // : Result[UserId, ConvError]   // spekulativ
    try Ok(user -> UserId)
    catch { | val error => Err(error) }

Der Umwandlungspunkt ist catch. Die frühere Form catching entfällt als Sprachform; wer sie braucht, schreibt sie als Stdlib-Funktion auf Basis von catch (jdl-effect-rows-und-throw §6.4, E-2′).

Result[T, E] verschwindet nicht aus der Sprache — es hört auf, ein Mechanismus des Rückgabetyps zu sein, und wird zu dem, was der Umwandlungspunkt liefert.

9.4 =? existiert nicht, try markiert [N] 07 Invariante 12 — try [Entscheidung]

Der frühere Propagationsoperator ist ersatzlos entfallen. Jeder Aufruf, der abbrechen kann, trägt try; ohne catch wird der Fehler weitergereicht und erscheint in der Row der aufrufenden Funktion (jdl-effect-rows-und-throw §5.3, T-3). So ist beides sichtbar: in der Signatur, was geworfen werden kann, und im Rumpf, wo.

// v0.2
def createUser(...) -> Result[User, UserError] =
    val validEmail =? validateEmail(email)
    ...

// heute
def createUser(...) ->{Throw[UserError]} User {
    val validEmail = try validateEmail(email)
    ...
}

9.5 Trap [N] 07 §4.3

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

9.6 Option und Optionalzugriff [N] 01-grundlagen §8

val street = user?.address?.street          // -> Option[str]
val city   = user?.address?.city ?? "N/A"   // ?? ist Nil-Coalescing

Option und Result sind kanonisch in jdl::core definiert und werden ohne expliziten Import in den Scope gebracht (§18.6).

9.7 Fehleridentität [O] 07 §4.4, O-5

Ob Fehlertypen nominal oder global identifiziert werden, ist offen. Betrifft Interop und Wire-Format.


10. Allokation

10.1 Allokation ist ein Effekt [N] 07 §5.1

Eine Allokation verändert globalen Zustand und kann fehlschlagen. Sie gehört damit in die Row.

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

Andernfalls wanderte Result in jede Konstruktion zurück — und damit =? durch die Hintertür. Die praktische Folge: derselbe Code, anderer Handler. Auf dem Desktop trappt eine erschöpfte Arena; im Kernel oder auf eingebetteten Zielen liefert ein anderer Handler ein Result.

10.2 Auflösung über den Typ [N] 07 §5.2

Alloc unterscheidet sich grundlegend von Db, Fs und Api: Es wird nicht vom Nutzer aufgerufen, sondern vom Compiler. Ein Struct-Literal hat keine Aufrufstelle, an der man qualifizieren könnte.

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

tag ReqArena

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

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

Das Alloc[ReqArena] in der Signatur steht dort nicht, weil der Rumpf es erwähnt — es wird aus der memory-Policy von Report hergeleitet und gegen die Deklaration geprüft.

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

10.3 Arenapolymorphie [N] 07 §5.3

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

Eine Funktion, die in irgendeiner Arena baut, entschieden vom Aufrufer.

10.4 Escape-Regeln [N] 07 §5.4

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

Ausdrücklich dieselbe Maschinerie, keine zweite.

10.5 Temporäre [O] 07 §11.1, O-1

Aus welcher Arena ein Zwischenergebnis ohne memory-Policy kommt, ist offen. Betrifft praktisch jede Zeile Stdlib-Code.

10.6 Arena-Scope vs. Handler [O] 07 §11.1, O-2

Ob der bestehende with Storage.arena[A]-Scope im Alloc-Service aufgeht oder zwei Mechanismen bestehen bleiben, ist offen.


11. Protocols

11.1 Deklaration [N] 02-typsystem §1

protocol Equatable {
    def equals(self, other: Self) -> bool
}

protocol Comparable: Equatable {
    def compare(self, other: Self) -> Ordering
}

Self existiert in jedem Protocol automatisch als Alias für den implementierenden Typ.

Abgrenzung zu service: protocol beschreibt das Verhalten eines Typs; service eine Capability in Effektkontexten. Protocols erscheinen nicht in der Row, Services nicht als Typ-Constraint.

11.2 Die drei Formen von provide [N] 07 §1.1

provide Equatable for User        // Protocol-Implementierung für einen Typ
provide User                      // Methoden direkt am Typ
provide UserDb[PostgresHandler]   // Service-Handler-Bindung

Die vierte Form aus v0.2, provide Target from Source für Konversionen, ist entfallen. Konversion ist ein gewöhnliches Protocol (§12).

provide User {
    def isAdult(self) -> bool = self.age >= 18
}

Seit 2026-10-05 kann provide auch eine Row liefern (§7.7). Ob das eine vierte Form ist oder unter eine der bestehenden fällt, ist mit der Schreibweise offen. [O]

11.3 Derive [N] 02-typsystem §1

type User: struct {
    name:  str
    email: str
} :> Derive([Equatable, Hashable, Inspectable])

11.4 Coherence — die Orphan-Regel [N] 02-typsystem §1, spec-namespaces §10

Eine Protocol-Implementierung ist nur erlaubt, wenn P oder T im selben Package oder Modul definiert ist. Für fremde Typen nutzt man Newtypes (§5.4).

Das hält Dispatch eindeutig und verhindert, dass zwei Bibliotheken unterschiedliche Semantik für dieselbe Kombination (P, T) einschleusen.

11.5 Operator-Überladung [N] 02-typsystem §2

Operatoren sind semantisch frei. Was ein Operator tut, bestimmt der Typ über ein Protocol. Die Bindung geschieht über ein Meta-Record am Protocol.

protocol <{ operator: "+" }> Add {
    def add(self, other: Self) -> Self
}

protocol <{ operator: "-" }> Neg {
    def negate(self) -> Self
}

Unäre und binäre Operatoren mit demselben Symbol werden über die Stelligkeit unterschieden — negate(self) gegen sub(self, other).

11.6 Protocol-Typen in Signaturen [N] 02-typsystem §1.5

In Parameterposition ist ein Protocol ein implizites Generic. In Rückgabeposition ist es ein opaquer Rückgabetyp.

11.7 Row-Plätze [Entscheidung] (2026-10-05)

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. Dafür weist das Protocol einen benannten Row-Platz aus, den jede Implementierung füllt.

protocol Scopeable {                              // spekulativ
    type Needs : row::Row
    def release(self) ->{Needs} Unit
}
  • Zeile 2: Der Protocol-Autor sagt ausdrücklich: „Hier darf jede Implementierung eigene Services mitbringen." Den Namen wählt er selbst; Needs ist nur ein Beispiel. row::Row legt fest, dass der Platz hinter einem Laufzeitpfeil steht.
  • Zeile 3: Die Methode verweist auf genau diesen Platz.

Diese Form ersetzt die frühere Row-Variable g an Protocol-Methoden. Ein Einbuchstaben-Name, den man sich merken muss und der nirgends deklariert ist, entfällt damit.

Drei Regeln:

  1. Die Implementierung schreibt ihre echte Row. Im provide steht def release(self) ->{Fs} Unit wie bei jeder Funktion. Der Compiler leitet Needs = {Fs} daraus ab. Eine eigene Zeile type Needs = … braucht es nicht.
  2. Wer einen konkreten Typ benutzt, sieht den Platz nie. Der Compiler setzt dort die echten Services ein.
  3. Nur generischer Code schreibt den Platz hin, als T.Needs, gelesen: „was immer T braucht".

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

Kein eingebauter Platz. Anders als Self (§11.1) existiert ein Row-Platz nicht automatisch in jedem Protocol. Sonst wäre jede Protocol-Methode offen für beliebige Services, ohne dass der Autor das entschieden hat.

Das Vorbild ist der assoziierte Typ (Rust type Item in Iterator, Zugriff T::Item). Suchwort für die Übertragung auf Effekte: associated effects (Flix).

[O] Pro Protocol oder pro Methode. Ob sich alle Methoden eines Protocols einen Platz teilen oder jede Methode ihren eigenen hat, ist nicht entschieden.

[O] dyn-Stellen. An einer dyn-Stelle ist die Implementierung unbekannt und damit auch der Inhalt des Platzes. Der Platz muss dort festgelegt werden; die Schreibweise ist offen (dyn-protocol-values §4.5).


12. Casts

12.1 Konversion ist ein Protocol [N] 07 §1

Konversion ist CastTo[T], gebunden an den Operator ->.

12.2 Drei Modi [N] 07 §1.4

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

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

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

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

12.3 Anwendung [N] 07 §1.5

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

Bemerkenswert: Der Cast sieht bei allen drei Modi gleich aus. Der Unterschied steht in der Row der aufrufenden Funktion, und beim Modus Try zusätzlich im try, das jede abbrechende Stelle trägt (§9.4) [A].

12.4 Primitive Widening [N] 07 §1.6

Verbreiterung — etwa i32 zu i64 — ist eingebaut und braucht keinen provide-Block. Verengungen brauchen immer einen expliziten Cast.


13. Typparameter und Constraints

13.1 Grammatik [N] 02-typsystem §4a

TypeParam      ::= Qualifier* Name (":" KindConstraint)?
Qualifier      ::= "phantom" | "reified"
KindConstraint ::= Protocol ("+" Protocol)*

TypeParamList  ::= "[" TypeParam ("," TypeParam)* "]"
WhereClause    ::= "where" Relation ("," Relation)*

Die Reihenfolge innerhalb eines Parameters ist fix. where folgt nach der vollständigen Parameterliste.

Die Grammatik gilt einheitlich für type, def und provide.

13.2 Inline oder where [N] 02-typsystem §4a

Prüffrage: Brauche ich Parameter U, um den Constraint auf T auszudrücken? Wenn ja → where. Wenn nein → inline.

type SortedList[T: Comparable]: struct { ... }
def lookup[T: Comparable + Hashable](key: T) -> Option[T]

provide Displayable for T where T: Equatable + Printable { ... }

13.3 phantom und reified [N] 08-grammar-sketch §5

Ein Parameter kann phantom oder reified sein, aber nicht beides.

type ManagedUser[phantom State: UserState]: struct { ... }
def describe[reified T](value: T) -> str

type Bad[phantom reified T]: struct { ... }     // ungültig

13.4 Typestate über Phantom Types [N] 02-typsystem §4

type UserPhase: enum {
    Registered
    Verified
    Active
}

type ManagedUser[phantom P: UserPhase]: struct {
    id:   UserId
    name: str
}

def register(name: str) ->{Throw[UserError]} ManagedUser[UserPhase.Registered]
def verify(u: ManagedUser[UserPhase.Registered], code: str)
    ->{Throw[UserError]} ManagedUser[UserPhase.Verified]
def activate(u: ManagedUser[UserPhase.Verified]) -> ManagedUser[UserPhase.Active]

Der Compiler verhindert ungültige Übergänge, weil Registered und Verified verschiedene Typen sind.


14. Meta-Records und Refinements

14.1 Zwei Schreibweisen [N] 08-grammar-sketch §7

Dieselbe Information steht als Präfix <{ ... }> oder als Suffix :> Ausdruck.

Refinements ::= Refinement+
Refinement  ::= ":>" TypeLevelExpr

MetaPrefix  ::= "<{" MetaField* "}>"
MetaField   ::= Identifier ":" TypeLevelExpr
type User: struct { ... } :> Share(Local)

tag <{
    own:   Unique
    share: Local
}> TaskLocal

14.2 Compile-Zeit und Laufzeit [N] 07 §9.2

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

Serialisierbarkeit ist damit eine strukturelle Eigenschaft, keine Feature-Anforderung.

14.3 Funktions-Refinements [N] 07 §8

Querschnittsbelange stehen im Meta-Record, nicht in der Logik. Die Funktion beschreibt was sie tut, das Refinement wie sie sich verhält.

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

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

Vorhandene Refinements: Cache, Retry, Timeout, Transactional.

Der Cache-Schlüssel wird automatisch erzeugt — Funktionssignatur als Namensraum, Hash der Parameter als Schlüssel. Parameter müssen Hashable implementieren; der Compiler prüft das statisch.

14.4 Refinements und die Row [N] 07 §8.5

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

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

Ob Cache auf deterministische Funktionen eingeschränkt wird, ist offen (07 §11.2).


15. Compile-Zeit-Funktionen

15.1 Form [Entscheidung]

Compile-Zeit-Auswertung ist eine gewöhnliche Funktion mit Meta am Pfeil, vor der Row (jdl-meta-phase §2.1, MP-20). Das Schlüsselwort typefn entfällt.

def Share(policy: SharePolicy) ->Meta{} MetaPatch { ... }     // spekulativ im Rumpf

Ein schreibendes Refinement liefert einen Patch, keinen fertigen Meta-Record (jdl-meta-phase §4.7).

Damit gelten für Compile-Zeit-Funktionen alle Regeln aus §6, §7 und §13 unverändert — Parametergrammatik, Row-Algebra, Constraints. Es gibt keine zweite Sprache im Sprachkörper.

[O] In den Quelldokumenten nicht nachgezogen. 08-grammar-sketch §6 führt typefn weiterhin als eigenständige Deklarationsform. jdl-typefn-spec ist inzwischen durch jdl-meta-phase ersetzt.

15.2 Was Compile-Zeit-Code darf [N] jdl-meta-phase §3

Compile-Zeit-Code terminiert, ist deterministisch und greift auf keine Resources, Handles oder Services der Laufzeit zu (MP-1 bis MP-3). Den Determinismus sichert die Meta-Row; Allokation läuft normal.

Ob der Rumpf darüber hinaus gewöhnliches JDL ist, die frühere Liste verbotener Konstrukte also durch den Totalitätsbeweis ersetzt wird, ist dort ein Vorschlag [O] (jdl-meta-phase §3.2, MP-22).

15.3 Auswertung gegen die CompilerDB [N] jade-compiler-db-spec §9, jdl-meta-phase §4.7, §6

Compile-Zeit-Code bekommt Zugriff auf die CompilerDB — Leseseite, Schreibseite und Diagnostics. Schreiben heißt Patchen (MP-8). Meta-Records sind ring-geschichtet; die Beweisspur einer Ableitung liegt getrennt im ProvenanceStore (jdl-meta-phase §6.2).

15.4 Typ-Patterns [O] jdl-primitives-spec §6

Musterabgleich auf Typebene ist architektonisch beschlossen, aber nicht normativ spezifiziert:

def Flatten[T]() ->Meta{} Type =
    match T {
        | [Inner] => Flatten[Inner]
        | _       => T
    }

Betroffen sind Shape-Matching, Protocol-Constraint-Matching und Literal-Typ-Matching. Die Beispiele in jdl-primitives-spec §6 stehen noch in typefn-Schreibweise.

Nicht zu verwechseln mit den Typ-Armen in §16.3: Dort wird ein Wert einer Union nach seinem Mitgliedstyp unterschieden, hier ein Typ nach seiner Form.


16. Pattern Matching

16.1 Grundform [N] 01-grundlagen §7 — Arme mit | [A] siehe §5.2

def handleResult(res: Result[User, UserError]) -> str =
    match res {
        | Ok(val user)                           => f"OK: {user.name}"
        | Err(UserError.NotFound { id })         => f"Nicht gefunden: {id}"
        | Err(UserError.AlreadyExists { email }) => f"Existiert bereits: {email}"
        | Err(val e)                             => f"Fehler: {e}"
    }

Neue Namen im Muster tragen val [Entscheidung], etwa Some(val x). Ob ein Name gebunden oder verglichen wird, entscheiden so weder die Namensauflösung noch die Groß-/Kleinschreibung. Benannte Felder einer Struktur muss man nicht neu binden; der Zugriff über den Feldnamen reicht.

Match ist exhaustiv — der Compiler meldet fehlende Arme.

16.2 Nicht normierte Formen [O] jdl-primitives-spec §6

Die folgenden Formen sind architektonisch beschlossen, aber nicht normativ spezifiziert:

  • Exhaustiveness-Regeln für alle Musterformen

Entschieden ist inzwischen [Entscheidung]:

  • Feld-Destrukturierung gibt es für nominales Matching auf die Felder eines Records. Der Typ kommt vom Subjekt, das Muster nennt nur Felder; ... steht für „die übrigen Felder“ (.. ist der Spannungsoperator). _ ist kein Feldmuster, sondern bleibt der Auffangarm.
  • Guards (| … if …) gibt es nicht.

Das ist die größte einzelne Lücke in der Sprachoberfläche.

16.3 Typ-Arme für Unions [O] — Vorschlag aus dem Arbeitsgespräch 2026-10-05

Eine Union (§5.3) ist ohne eine Möglichkeit, sie wieder auseinanderzunehmen, nur halb nutzbar. Vorgeschlagen, aber nicht entschieden, sind Typ-Arme: Ein Arm nennt einen Mitgliedstyp der Union, und im Arm hat das Subjekt genau diesen Typ.

match spec {                                       // spekulativ
    | EntrypointSpec                     => { spec.port ... }
    | RemoteEntrypointSpec { host, ... } => { ... }
}
  • Zeile 1: spec hat einen Union-Typ.
  • Zeile 2: Der Arm nennt einen Mitgliedstyp. Im Arm ist spec ein EntrypointSpec, also geht spec.port ohne neue Bindung. Suchwort: type narrowing.
  • Zeile 3: Optional werden zugleich Felder zerlegt, ... für den Rest.

Vorgeschlagene Regeln:

  1. Ein Arm darf nur Typen nennen, die in der Union stehen.
  2. Jedes Mitglied braucht einen Arm, oder es gibt einen _. Weil Unions flach sind, ist diese Vollständigkeitsprüfung einfach.
  3. Die Verengung gilt nur, wenn das Subjekt ein Name ist. Bei match load() { ... } gibt es nichts zu verengen; dann wird erst gebunden.
  4. Typ-Arme gelten überall, nicht nur in der Meta-Phase. catch unterscheidet bereits nach Fehlertypen (jdl-effect-rows-und-throw §7.2); ohne Typ-Arme in match gäbe es zwei Mechanismen für dieselbe Sache.

Trusted Core. Zur Laufzeit muss ein Union-Wert wissen, welches Mitglied er gerade ist. DynValue ist bisher die einzige Wertekategorie mit Tag (addendum-begriffe-und-motive, dyn-protocol-values §5.4). Ein Union-Wert braucht ebenfalls eine Markierung, wie ein Enum seine Variantennummer. Naheliegend ist, dass die VM eine Union intern wie ein Enum behandelt, dessen Varianten fremde Typen tragen: eine Darstellung und ein Dispatch statt zwei. Für Unions aus Blueprints spielt das keine Rolle, weil sie nur in der Meta-Phase leben; es betrifft Unions zur Laufzeit wie AnyError oder den Wert eines catch.


17. Ausdrücke und Kontrollfluss

17.1 if als Ausdruck [N] 01-grundlagen §6

def validateAge(age: i32) ->{Throw[UserError]} i32 =
    if age >= 0 and age <= 150 then
        age
    else
        throw UserError.InvalidAge { age }

Die Inline-Form if cond then x else y ist in der Änderungstabelle von 01-grundlagen als neu vermerkt.

17.2 for [A] 01-grundlagen §2

Belegt ist nur die Form über eine Sammlung, und zwar allein durch ein Beispiel:

for item in xs {
    out.push(f(item))
}

17.3 Kontrollfluss [Entscheidung] — Rest [O]

Aus den Arbeitsgesprächen entschieden, in keinem Quelldokument ausgeschrieben:

  • ret gibt aus einem Blockrumpf zurück und ist zugleich der vorzeitige Ausstieg (§6.1).
  • loop liefert den Wert, den break mitgibt. while und for liefern immer Unit, weil sie auch ohne break enden können. Beide sind Zucker über loop; ein break mit Wert ist in ihnen vorerst nicht erlaubt.
  • Zwei Syntax-Ebenen: Deklarationen (type, def, import, provide) stehen oben, alles andere ist Ausdruck. Einen eigenen Anweisungsbegriff gibt es nicht.
  • ret in with verlässt nur den with-Block, nicht die Funktion (§17.6).

Weiterhin offen:

  • continue
  • die Benennung der Schleifenformen
  • Bereiche außerhalb des Index-Kontexts (1..3 ist nur als Range[i32] beim Slicing belegt)

17.4 Pipelines [N] 01-grundlagen §9

val adminNames =
    users
    |> filter(u => u.active and u.role == Role.Admin)
    |> map(_.name)
    |> sort

17.5 Lambdas [N] 01-grundlagen §10

users |> filter(u => u.active)        // knapp
users |> filter(_.active)             // Platzhalter
users |> map { u =>                   // Block
    val name = u.name.trim()
    f"{name} ({u.role})"
}

[O] Zwei Bedeutungen von _. Seit der partiellen Applikation macht ein _ an Argumentstelle einen Aufruf zur partiellen Applikation (jdl-partielle-applikation PA-1). filter(_.active) und map(_.name) (§17.4) benutzen _ dagegen als Platzhalter einer Lambda. Nach dem Wortlaut von PA-1 steht dort kein _ an Argumentstelle, sondern ein Ausdruck, der _ enthält; für Leser ist der Unterschied aber kaum zu sehen. Ob die Platzhalterform bleibt, ist nicht entschieden. Ebenfalls offen ist, ob die Blockform einer Lambda wie ein Blockrumpf ret braucht (§6.1).

17.6 with — Ressourcen-Scope [N] 07 §3.7

with expr as name { body }

Verlangt eine Scopeable[R]-Instanz. Senkt zu acquire + Body + release, auch auf Fehlerpfaden; im IR die Extended-Operation WithScope. with bindet einen Wert und lässt die Row unverändert — im Gegensatz zur Handler-Installation (§8.7).

ret im with-Block verlässt nur den Block, nicht die Funktion [Entscheidung]. Wer den Wert braucht, bindet ihn: val x = with … { … ret … }.


18. Module und Sichtbarkeit

18.1 Dateipfad ist Modulname [N] spec-namespaces-und-module §3

Eine Datei users/service.jdl definiert das Modul users::service. Es gibt keine Moduldeklaration innerhalb der Datei; der Pfad ist die Quelle der Wahrheit.

Zirkuläre Modulabhängigkeiten sind ein harter Compilerfehler.

18.2 Sichtbarkeit [N] spec-namespaces-und-module §4, D-13

pub und package gibt es nicht. Alles ist standardmäßig unsichtbar; was ein Modul nach außen gibt, steht in seiner Constitution (constitution.jdl, spec-constitution-system). An der Deklaration steht kein Schlüsselwort.

def validateEmail(email: str) -> bool
def findUser(email: str) ->{Throw[UserError]} User
type User: struct { ... }

Der Preis ist bewusst gezahlt: Wer eine Datei aufschlägt, sieht nicht, ob eine Definition freigegeben ist. Der Ausgleich liegt beim Compiler, der meldet, wenn sich der Fingerabdruck der Oberfläche ändert (spec-namespaces-und-module §4, addendum-begriffe-und-motive G.3).

18.3 Importformen [N] spec-namespaces-und-module §8

import users::service                          // Modul als Name im Scope
import users::service as user_service

import users::service : User, findUser         // Symbole
import users::service : User as AppUser
import users::service::UserService             // Kurzform für : UserService

Es gibt keinen Wildcard-Import. Explizit ist Pflicht.

Imports dürfen innerhalb von Funktionen stehen. Ausnahme: keine lokalen Imports von service-Typen.

18.4 Relative Referenzen [N] spec-namespaces-und-module §8.2

import parent::middleware : Middleware      // Parent-Namespace
import package::model     : User, UserId    // Root des aktuellen Packages

parent:: in einem Top-Level-Modul ist ein Compilerfehler.

18.5 internal als Importbarriere [N] spec-namespaces-und-module §5

Ein Modulpfad, der ein Segment internal enthält, ist außerhalb des Packages nicht importierbar. Eine Freigabe in einem internal-Modul bedeutet daher: sichtbar innerhalb des Packages, nicht extern.

Bemerkenswert: internal ist kein Schlüsselwort, sondern ein Pfadsegment. Die Barriere liegt im Dateisystem, nicht in der Deklaration.

18.6 Tiny Prelude [N] spec-namespaces-und-module §10.1, D-1, D-2

Result und Option sind kanonisch in jade::core definiert und stammen aus dem Seed. Sie werden samt ihren Varianten (Some, None, Ok, Err) automatisch in den Scope gebracht. Das ist kein Wildcard-Import von jade::core.

Primitive Builtins (i8..i64, u8..u64, f32, f64, bool, str, Unit) sind keine Prelude-Importe, sondern Sprach-Builtins.

[O] spec-namespaces-und-module §7 führt den Einheitstyp noch als () (§3.3).

18.7 Namenskonflikte [N] spec-namespaces-und-module §11.1

Bringen zwei Importe dasselbe Symbol unqualifiziert in den Scope, ist das ein Compilerfehler. Ein Alias löst es auf.

18.8 Reservierte Namensräume [N] spec-namespaces-und-module §12

Namensraum Bedeutung
jdl:: Root der user-facing Stdlib (Nephrit)
jade:: reserviert für privilegierte System-/Runtime-Module

jade:: und jdl:: bilden zusammen mit dem Seed ein Coherence-Package (spec-namespaces-und-module §15.2, D-6).

@compiler entfällt [N] spec-namespaces-und-module §13, D-18. Ziel- und Build-Fakten kommen aus der @cfg-Prädikatsprache oder aus db.target() in der Meta-Phase, Layoutfragen aus der Meta-Schicht. @ bedeutet damit nur noch eine Sache: Annotation (addendum-begriffe-und-motive G.4). @intrinsics ist ebenfalls kein Namensraum.

18.9 mod.jdl [N] spec-namespaces-und-module §6, D-14

mod.jdl ist der Ort, an dem etwas für den ganzen Ordner deklariert wird, keine API-Kontrolle. Freigaben stehen in constitution.jdl (§18.2).


19. Deklarative Konstrukte

19.1 CallGraph [N] 07 §9.1 — requires entfällt [Entscheidung] (2026-10-05)

Der CallGraph ist kein Interpreter, sondern ein deklarativer Ort der Handler-Installation.

Regel D-1. Die Grenze zwischen „läuft nicht" und „läuft" ist der Handler, nicht der Graph.

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

    handleRequest(req)
}

07 §9.1 stellte fest, dass ein requires-Block eine Redundanz zur Row ist, und ließ offen, ob er entfällt oder als geprüfte Zusicherung bleibt. Entschieden: Er entfällt.

Was ein Graph insgesamt braucht, ist die Summe der deklarierten Rows aller Funktionen, die von seinem Einstiegspunkt aus erreichbar sind. Diese Summe schreibt niemand ab; sie ist eine Abfrage an die CompilerDB. Wer bindet — ein CallGraph, ein Context —, vergleicht sie mit seinem Angebot, und jeder fehlende Service wird einzeln mit Namen gemeldet.

Zusammengezogen wird dabei nur die Sicht auf den Graphen. Die Row jeder einzelnen Funktion bleibt deklariert (§7.8). Begründung und Folgen: jdl-effect-rows-und-throw §4.7.

Weil der CallGraph eine echte Datenstruktur ist, sind Verhaltens-Refinements möglich, ohne den Compiler zu berühren:

CallGraph app(...) { ... }
    :> Retry(max: 3, backoff: Exponential)
    :> Serializable

19.2 Blueprints und Engines [N] 12-design-constitution §8

Ein Blueprint ist eine deklarative Struktur ohne eigene Ausführung. Eine Engine interpretiert Blueprints. Ein Descriptor beschreibt, was eine Engine an Fähigkeiten verlangt und bietet. Wie sich der Blueprint von Record und Struct unterscheidet, steht in §5.10.

Eine Engine, mehrere Blueprints [Entscheidung] (2026-10-05). Eine Engine kann mehrere Blueprint-Typen bedienen, indem im Spec-Platz ihres Protocols eine Union dieser Typen steht (§5.3). Es gibt dafür kein mehrfaches provide desselben Protocols auf demselben Träger. Einzelheiten: jdl-blueprint-spec §9.4.

19.3 Rows in Feldpositionen [Entscheidung, mit offener Flanke]

Die Fehlerkonvention gilt durchgängig — auch für Funktionstypen in Feldposition:

type ParserSpec[T]: blueprint {
    grammar:    GrammarSpec[T]
    validation: Option[(T) ->{Throw[ValidationError]} T]
}

Das schließt O-7 aus 07 §11.1 mit ab: Rows wandern damit in Datentypen, nicht nur in Signaturen.

[O] Zu klärende Spannung. Constitution §8.2 legt fest, dass Blueprints effektfrei sind. Ein Blueprint-Feld mit nichtleerer Row braucht dafür eine Auslegung — etwa, dass die Effektfreiheit für die Auswertung des Blueprints gilt und nicht für die Signaturen der Funktionen, die er transportiert. Diese Auslegung ist nirgends festgehalten.


20. Labels

20.1 Was ein Label ist [N] 04a-label-inferenz-regeln

Ein Label ist eine abgeleitete Eigenschaft eines Typs oder einer Funktion. Labels, die dem Compiler Rechte geben, können nicht gesetzt werden — sie müssen bewiesen werden.

20.2 Drei Zustände [N] 04a §Negationsmodell

Zustand Bedeutung
proven(X) Beweis liegt vor
excluded(X) X gilt nachweislich nicht
unproven(X) kein Beweis vorhanden — kein Fehlerzustand

Der Unterschied zwischen excluded und unproven ist zentral: unproven heißt nicht „falsch", sondern „nicht gezeigt".

Jedes abgeleitete Label trägt eine verpflichtende Provenienz — Regel, Prämissen und Herkunft bis auf ein konkretes Feld.

20.3 Pure und Deterministic [N] 07 §6

Regel P-1. Pure verlangt eine leere Row und keine RefMut/Out-Parameter.

Regel P-2. Deterministic verlangt Row ⊆ {Alloc[_]} und keine RefMut/Out- Parameter.

Die beiden bilden eine Treppe, keine Skala: Pure ⇒ Deterministic. Wer aus Pure herausfällt, landet eine Stufe tiefer, nicht im Nichts.

Alloc hat diesen Freibrief, weil das Query-Caching nicht fragt, ob eine Funktion Speicher angefasst hat, sondern ob bei gleicher Eingabe dasselbe herauskommt. Hinge Caching an Pure, wäre es seit Einführung von Alloc für fast die ganze Stdlib unbenutzbar.

20.4 Was die Row nicht sieht [O] 07 §6.5

Drei Dinge sind nicht durch die Row erfasst und in 07 als zu entscheiden markiert: Divergenz, Trap-Verhalten in Pure, sowie ein dritter dort genannter Punkt. Solange sie offen sind, behauptet der Proof Trace an diesen Stellen Ungeprüftes.


21. Bekannte Lücken

Zusammenfassung aller [O]-Stellen dieses Dokuments, nach Größe geordnet.

# Lücke Abschnitt
1 Kontrollfluss — ret, loop/break, while/for entschieden; offen: continue, Namen der Schleifenformen, Bereiche §17.3
2 Pattern Matching — Destrukturierung und Guards entschieden; Exhaustiveness-Regeln nicht normiert §16.2
3 Reichweite der Blockform — nur noch die Function Union offen §5.2
4 Typ-Patterns auf Typebene nicht normiert §15.4
5 provide für Service-Handler — zwei Schreibweisen in Umlauf §8.6
6 Unit-Literale — Punktform gegen punktlose Form §1.4
7 catching — geschlossen: entfällt als Sprachform, Umwandlungspunkt ist catch §9.3
8 Blueprints effektfrei gegen Rows in Feldpositionen §19.3
9 requires im CallGraph — geschlossen 2026-10-05, entfällt §19.1
10 Temporäre und Arenen (O-1) §10.5
11 Arena-Scope gegen Handler (O-2) §10.6
12 Fehleridentität (O-5) §9.7
13 Divergenz und Trap in Pure (O-6) §20.4
14 Overflow- und Float-Semantik §3.5
15 Vorgabewerte für Funktionsparameter §6.4
16 Blockkommentare §1.1
17 protocol Db gegen service Db in 10-runtime-handles §8.1
18 Typ-Arme für Unions — Vorschlag liegt vor, nicht entschieden; Trusted Core: Union-Werte brauchen eine Markierung §16.3
19 Row-Plätze — einer pro Protocol oder einer pro Methode §11.7
20 Row-Variable g an gewöhnlichen Funktionen — Typparameter mit Rolle, Verweis auf die Row eines Parameters oder eigene Schreibweise §7.7
21 R-4 gegen Deklarationspflicht der Row §7.5
22 Namenlose Unions im Typausdruck und Literal-Unions §5.3
23 Übergang von Laufzeit- in Meta-Rows — Übergangsregel oder nur leere Rows §7.7
24 Rolle oder Basis hinter : row::MetaRow §7.7
25 & auf einem Struct — Vorschlag: Fehler mit Hinweis §5.10
26 Struct-Typen in Record-Feldern und die Schreibweise eines Funktionsverweises als Daten §5.10, Ontologie §3a
27 newtype gegen :/= — geschlossen 2026-10-06: : stiftet einen neuen Typ, newtype entfällt; offen bleibt, wie ein Wert eines Newtypes entsteht §5.4
28 Zwei Bedeutungen von _ — Lambda-Platzhalter gegen Lücke der partiellen Applikation §17.5
29 Struct-Literale — Felder mit : (hier durchgängig) oder mit = wie in Blueprint-Profilen §5.1
30 () in spec-namespaces-und-module §7 — dort noch Schreibweise des Einheitstyps §18.6
31 Refinement-Typ gegen Refinement — type Email = str :> ValidEmail als Alias träfe jeden str §5.5

Die ersten beiden sind von anderer Art als der Rest: Sie betreffen Konstrukte, die jedes JDL-Programm braucht. Seit 0.2.2 ist bei beiden der größere Teil entschieden; offen ist, was in ihrer Zeile steht. Alle übrigen sind Widersprüche oder Feinheiten.


22. Quellen und Aussortierung

22.1 Vollständig eingeflossen — Aussortierungskandidaten

Der Inhalt dieser Dateien ist, soweit er die Sprachoberfläche betrifft, hier aufgegangen. Sie enthalten darüber hinaus Begründungen; wer die behalten will, behält die Datei als Archiv.

Datei Bemerkung
08-grammar-sketch.md Deckt weniger ab als der Titel verspricht. Der abgedeckte Teil ist hier enthalten; typefn in §6 ist überholt. Als Grammatikquelle ersetzt.
jdl-typefn-spec.md Beschreibt vollständig ein Konstrukt, das mit der Entscheidung in §15.1 entfällt. Wird nicht migriert, sondern ersetzt — §2 (erlaubte und verbotene Konstrukte) und §5 (CompilerDB-Zugriff) sind vorher zu retten. Erledigt durch jdl-meta-phase.
jdl-primitives-spec.md Vollständig eingeflossen außer §6 (Pattern Matching, ausstehend) und §7 (offene Punkte), die hier als Lücken geführt sind.
spec-namespaces-und-module.md Vollständig eingeflossen.

22.2 Teilweise eingeflossen — bleiben bestehen

Datei Was hier steht Was dort bleibt
07-cast-effekte-refinements.md Syntax und Regeln von Cast, Row, Services, Throw, Alloc, Refinements Begründungen, Literaturvergleiche, Lowering (§7), Invariantenliste (§10), Anhänge. Bleibt normative Quelle.
01-grundlagen.md Basissyntax Lehrpfad und durchgehendes Beispiel. Enthält überholte Stellen: =?, Effect[R,E,D], deps-Erwähnung, provide ... for bei Services.
02-typsystem.md Protocols, Operatoren, Typparameter, Newtypes, Phantoms Ausführliche Beispiele, Konstruktionslebenszyklus. Enthält überholte =?- und Result-Stellen.
04a-label-inferenz-regeln.md Nur die Zustände und die Treppe Pure/Deterministic Die vollständigen Regelwerke S, C und die Closure-Axiome. Bleibt normative Quelle.
12-design-constitution.md Nur Blueprint/Engine/Descriptor in Kurzform Ring-Modell, IR-Invarianten, Constitution-as-Descriptor. Bleibt Charta.

22.3 Nicht herangezogen

Diese Dateien wurden geprüft und tragen zur Sprachoberfläche nichts bei, das nicht schon aus den obigen Quellen kommt: jade-emergente-eigenschaften.md, jade-vision.md, 10-source-audit.md, 09-migration-checklist.md, README.md, index.md.

d-nogc-cheatsheet.md ist vollständig D-spezifisch und für JDL gegenstandslos.


Änderungsprotokoll

Version 0.2.3 (2026-10-06) — §5.4: Newtype in der Schreibweise vom 2026-09-14, type UserId : str; newtype entfällt. Offen bleiben die Erzeugung eines Werts und die Schreibweise von Blueprint-Profilen. §5.5: Widerspruch zwischen Refinement-Typ und jdl-blueprint-spec §8.1 benannt. §0.4 und §21 entsprechend (Lücke 27 geschlossen, 31 neu).

Version 0.2.2 (2026-10-05) — Syntax auf den Stand der Arbeitsgespräche gebracht, soweit entschieden. §1.2: Komma optional, Zeilenumbruch trennt. §2.1: val implizit, :=. §3.3: Unit statt (). §5.2: Tag-Enums in Blockform (Lesart), Match-Arme mit | bestätigt, offen nur die Function Union. §5.4: Widerspruch newtype gegen :/= benannt. §5.8: Tag-Enum in Blockform. §6.1: Blockrumpf ohne Wert, ret. §6.4: Kurzform für gleichnamige Argumente, Verweis auf partielle Applikation. §8.1: type X : service, Unit. §8.4: Unit. §9.3: catching entfällt, catch als Block mit Armen. §9.4: try an jeder abbrechenden Stelle. §12.2, §17.1: throw statt Throw.throw. §12.3: try beim Try-Cast. §14.3: try, ret. §15.1, §15.4: ->Meta{} am Pfeil, MetaPatch. §16.1, §16.2: val in Mustern, Feld-Destrukturierung mit ..., keine Guards. §17.3: Kontrollfluss nach den Entscheidungen, Rest offen. §17.5: zwei Bedeutungen von _ als offener Punkt. §17.6: ret im with-Block. §18.2, §18.5, §18.8, §18.9: Sichtbarkeit über constitution.jdl, @compiler entfällt, mod.jdl als Deklarationsort, jeweils als [N] nach spec-namespaces-und-module, das diese Punkte bereits führt. §18: alle Verweise auf die aktuelle Gliederung von spec-namespaces-und-module gebracht; §18.6 jade::core statt jdl::core nach dortigem D-1, Varianten im Prelude, () in dessen §7 als [O]. §15.1 bis §15.3: Verweise von jdl-typefn-spec auf jdl-meta-phase umgestellt, das jene ersetzt. §0.2: Marke [Entscheidung] in die Legende aufgenommen; sie war seit 0.1 in Gebrauch, aber nicht erklärt. §0.4 und §21 entsprechend; erste Zeile von §0.4 auf Meta am Pfeil berichtigt. Unverändert: Struct-Literale mit Doppelpunkt, newtype, if … then … else, Allokation in §10 und §8.7 (Speichermodell), Handler-Klassen in §8.8.

Version 0.2.1 (2026-10-05) — Zweiter Durchgang desselben Tages. §0.4: Rollen- und Phasenentscheidung der Rows, Trias, & nach Rolle. §5.9 und §7.7: Rolle immer ausgeschrieben (row::Row), Begründung über den leeren Record, jede Row mit genau einer Phase, row nur als Grundart, Gleichheit über Phase und Inhalt, Erweitern im Inhalt statt mit &; offen: Übergang, Rolle oder Basis. §5.10 neu: Record, Blueprint, Struct in Kurzform, & nach Rolle, & gegen _, Vorschlag „& auf Struct ist ein Fehler". §6.3, §11.7, §19.2 angepasst. §21: Lücke 20 angepasst, Lücken 23 bis 26 neu.

Version 0.2.0 (2026-10-05) — Ergebnisse des Arbeitsgesprächs vom 2026-10-05 eingearbeitet, sonst nichts. §0.4: fünf Entscheidungen ergänzt. §5.2: Union-Rolle als entschieden markiert, drei |-Rollen bleiben offen. §5.3: Blockform type X : union { A, B }, Abgrenzung Union gegen Enum, offen: namenlose Unions und Literal-Unions. §5.9 neu: Row-Deklaration. §6.3, §7.3: Hinweis auf Row-Plätze und die offene Zukunft von g. §7.5: Widerspruch zwischen R-4 und der Deklarationspflicht benannt. §7.7 neu: Rows sind Typen (Rolle row, : gegen =, durchsichtige Namen, keine Werte, provide auf Rows). §7.8 neu: Summe statt Inferenz. §8.4: A-3 gilt für T.Needs [A]. §11.2: provide auf Rows. §11.7 neu: Row-Plätze in Protocols statt g. §15.4: Abgrenzung zu Typ-Armen. §16.3 neu: Typ-Arme als Vorschlag mit Trusted-Core-Folge. §19.1: requires entfällt, Form B gestrichen. §19.2: eine Engine, mehrere Blueprints. §21: Lücke 9 geschlossen, Lücke 3 angepasst, Lücken 18 bis 22 neu.

Nicht nachgezogen sind die übrigen Entscheidungen seit 0.1.0, etwa zur Sichtbarkeit (pub/package), zu @compiler, zu Unit statt () und zum Blockrumpf ohne Wertsemantik. Die betroffenen Abschnitte geben weiterhin den Stand von 0.1.0 wieder. (Seit 0.2.2 nachgezogen.)

Version 0.1.0 — Erste Fassung. Zusammengetragen aus 07-cast-effekte-refinements v0.3, 01-grundlagen, 02-typsystem, jdl-primitives-spec, spec-namespaces-und-module, 08-grammar-sketch, 04a-label-inferenz-regeln, 12-design-constitution und jdl-typefn-spec.

Drei Entscheidungen sind erstmals hier festgehalten: typefn entfällt zugunsten von Meta in der Row, Enum-Varianten stehen in Blockform, und die Fehlerkonvention Throw[E] gilt durchgängig einschließlich Feldpositionen.