JDL — Sprachreferenz¶
Status: Konsolidierungsentwurf Version: 0.1.0 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 drei 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. |
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:
12-design-constitution— Charta07-cast-effekte-refinementsv0.3 — Effect Row, Casts, Services, Refinements04a-label-inferenz-regelnv0.6 — Labelzustände und Inferenz- Übrige normative Dokumente
- 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¶
Drei Punkte waren beim Verfassen offen und wurden entschieden. Sie sind hier gesammelt, weil sie noch in keinem anderen Dokument stehen.
| Punkt | Entscheidung | Wirkt auf |
|---|---|---|
| Compile-Zeit-Funktionen | typefn entfällt; Compile-Zeit-Auswertung ist def mit Meta in der Row |
§15 |
| Enum-Schreibweise | Blockform statt führender \| |
§5.2 |
| Fehlerkonvention | Durchgängig Throw[E] in der Row, auch in Feldpositionen |
§9, §19 |
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.
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
:: trennt Namensräume, . greift auf Member zu. Namensräume werden nie mit .
getrennt. [N] spec-namespaces-und-module §2
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:
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().
01-grundlagen §1 schreibt dagegen ohne Punkt:
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
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. () ist ein Alias; die textuelle Form Unit wird
bevorzugt, beide sind normativ gleichwertig.
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.
4.3 Tuple [N] jdl-primitives-spec §5.1¶
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.
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.
[O] Reichweite der Blockform noch offen. Das Zeichen
|hat in JDL fünf Rollen. Entschieden ist bisher nur die erste:
Rolle Beispiel Stand Enum-Varianten type Role: enum { ... }Blockform, entschieden Tag-Enums tag OwnPolicy: enum = \| Unique \| Sharedoffen Union von Typen type X: union = A \| Boffen Function Unions type Cmd = \| def f(...) -> Toffen Match-Arme match x { \| Ok(v) => ... }offen Die vier offenen Rollen sind in diesem Dokument im bisherigen Spec-Stand mit
|geschrieben. Sie sind nicht bestätigt.
5.3 Union von Typen [N] 01-grundlagen §5 — Schreibweise [O] siehe §5.2¶
Unions werden automatisch flach und entfernen Duplikate:
5.4 Newtype [N] 02-typsystem §4¶
type UserId = UserId(str)
type OrderId = OrderId(str)
findUser(UserId("u-123")) // ok
findUser(OrderId("o-456")) // Fehler: OrderId ist kein UserId
Ein Newtype ist ein eigener nominaler Typ. Er ist zugleich das Mittel, um die Orphan-Regel (§11.4) für fremde Typen zu umgehen.
5.5 Refinement-Typ [N] 02-typsystem §4¶
Anders als ein Newtype ist der Wert weiterhin der Basistyp und überall dort einsetzbar, wo dieser erwartet wird.
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 stehen im Spec-Stand mit |; Schreibweise [O] siehe §5.2.
6. Funktionen¶
6.1 Deklaration [N] 01-grundlagen §2¶
// Ausdrucksform
def double(x: i32) -> i32 = x * 2
// Blockform — letzter Ausdruck ist der Rückgabewert, kein return nötig
def greet(name: str) -> str {
val msg = f"Hello, {name}!"
msg
}
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¶
Die Grammatik der Typparameter steht in §13.
6.4 Benannte Argumente [N] 01-grundlagen Änderungstabelle¶
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.
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) -> i32ist exaktdef f(a: i32) ->{} i32.
7.3 Algebra [N] 07 §2.3¶
Die Row ist eine ungeordnete Menge.
Vereinigung bei Komposition:
Abschwächung: Eine Funktion mit kleinerer Row ist überall einsetzbar, wo eine größere erwartet wird. Die Umkehrung gilt nicht.
Row-Variablen erlauben Polymorphie über die Effektmenge:
map führt keine eigenen Effekte ein; es reicht durch, was der Aufrufer mitbringt.
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.
7.6 Suspendierte Berechnungen [N] 07 §2.6¶
Ein Thunk, dessen Effekte im Typ stehen, ersetzt den früheren Effect-Wert:
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:
8. Services¶
8.1 Deklaration [N] 07 §3.1¶
Was die Literatur Ability nennt, heißt in JDL service. Kein neues Schlüsselwort.
service Fs {
def readText(p: Path) -> str
def writeText(p: Path, s: str) -> ()
}
service Db[i] {
def query(sql: str) -> [Row]
def exec(sql: str) -> u64
}
Zwei Punkte sind normativ:
- Der Instanz-Parameter
[i]ist optional (§8.3). - 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-handlesX.2.1 deklariert dieselben Capabilities alsprotocol Db { ... }.07§3.1 stellt fest: es giltservice, 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.
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]} () =
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.
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]() -> Capaus10-runtime-handlesX.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 und02-typsystem§1 schreiben die Service-Handler-Bindung alsprovide UserDb for InMemoryUserDb { ... }.07§1.1 und §3.6 schreibenprovide UserDb[PostgresHandler] { ... }. Nach der Prioritätsregel gilt die Klammerform. Diefor-Form bleibt der Protocol-Implementierung vorbehalten (§11.2).
8.7 Handler-Installation — drei Formen [N] 07 §3.7¶
Global:
Bereichsbegrenzt — eine gewöhnliche Stdlib-Funktion mit Block, kein Schlüsselwort:
Deklarativ — im Blueprint (§19.1):
env: {
Db[Primary]: PostgresHandler { pool }
Db[Replica]: PostgresHandler { replicaPool }
Alloc[ReqArena]: ArenaHandler { size: 64.kib }
}
Regel A-6.
withHandlerist 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.
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.
Die Form catching ist in 07 §4.2 ausdrücklich als spekulativ geführt. [O]
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 [N] 07 Invariante 12¶
Der frühere Propagationsoperator ist ersatzlos entfallen. Ein Aufruf, dessen Fehler weitergereicht wird, steht ohne Sonderoperator da; der Fehler erscheint in der Row der aufrufenden Funktion.
// v0.2
def createUser(...) -> Result[User, UserError] =
val validEmail =? validateEmail(email)
...
// v0.3
def createUser(...) ->{Throw[UserError]} User {
val validEmail = 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
Resultverwandeln. 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¶
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).
11.3 Derive [N] 02-typsystem §1¶
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.
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.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 = user -> UserId // Try — wirft; Row trägt Throw[ConvError]
Bemerkenswert: Der Aufruf sieht bei allen drei Modi gleich aus. Der Unterschied steht in der Row der aufrufenden Funktion.
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
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 =
UserDb.getUserById(id)
:> Cache(CacheConfig { ttl: 24.hours, only: Ok })
def persistUserAndAudit(user: User) ->{UserDb, AuditLog, Throw[AppError]} User {
val saved = UserDb.insert(user)
AuditLog.write(saved.id)
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 in der Row. Das
Schlüsselwort typefn entfällt.
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 undjdl-typefn-specführentypefnweiterhin als eigenständige Deklarationsform. Diese Dokumente sind gegen die hier getroffene Entscheidung zu prüfen;jdl-typefn-specvermutlich vollständig zu ersetzen.
15.2 Was Compile-Zeit-Code darf [N] jdl-typefn-spec §2¶
Die Constraints aus der TypeFn-Spec gelten der Sache nach weiter, unabhängig von der Schreibweise. Erlaubt sind Typausdrücke, Verzweigung und Musterabgleich auf Typebene; verboten ist alles, was Laufzeitzustand berührt.
Der genaue Umfang steht in jdl-typefn-spec §2.1 und §2.2 und ist beim Umschreiben dieses
Dokuments zu übernehmen.
15.3 Auswertung gegen die CompilerDB [N] jdl-typefn-spec §5¶
Compile-Zeit-Code bekommt Zugriff auf die CompilerDB — Leseseite, Schreibseite und Diagnostics. Meta-Records sind ring-geschichtet; jede Ableitung hinterlässt einen Proof Trace.
15.4 Typ-Patterns [O] jdl-primitives-spec §6¶
Musterabgleich auf Typebene ist architektonisch beschlossen, aber nicht normativ spezifiziert:
Betroffen sind Shape-Matching, Protocol-Constraint-Matching und Literal-Typ-Matching. Die
Beispiele in jdl-primitives-spec §6 stehen noch in typefn-Schreibweise.
16. Pattern Matching¶
16.1 Grundform [N] 01-grundlagen §7 — Schreibweise der Arme [O] siehe §5.2¶
def handleResult(res: Result[User, UserError]) -> str =
match res {
| Ok(user) => f"OK: {user.name}"
| Err(UserError.NotFound { id }) => f"Nicht gefunden: {id}"
| Err(UserError.AlreadyExists { email }) => f"Existiert bereits: {email}"
| Err(e) => f"Fehler: {e}"
}
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:
- Feld-Destrukturierung —
match user { | { name, age } => ... } - Guards —
match user { | { age } if age >= 18 => ... } - Exhaustiveness-Regeln für alle Musterformen
Das ist die größte einzelne Lücke in der Sprachoberfläche.
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.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:
17.3 Nicht spezifiziert [O]¶
Zum Kontrollfluss fehlt in allen Quelldokumenten:
whileund andere bedingte Schleifenbreakundcontinuereturnals vorzeitiger Ausstieg — belegt ist nur „letzter Ausdruck ist Rückgabewert"- Schleifen als Ausdruck (Wert einer Schleife)
- Bereiche außerhalb des Index-Kontexts (
1..3ist nur alsRange[i32]beim Slicing belegt)
Das ist neben §16.2 die zweite große Lücke.
17.4 Pipelines [N] 01-grundlagen §9¶
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})"
}
17.6 with — Ressourcen-Scope [N] 07 §3.7¶
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).
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 Sichtbarkeitsstufen [N] spec-namespaces-und-module §4¶
| Form | Bedeutung |
|---|---|
| ohne Schlüsselwort | privat — nur innerhalb des Moduls |
package |
sichtbar in allen Modulen desselben Packages, nicht extern exportierbar |
pub |
exportiert und importierbar |
def validateEmail(email: str) -> bool // privat
package def normalizeEmail(email: str) -> str
pub def findUser(email: str) ->{Throw[UserError]} User
pub type User: struct { ... }
18.3 Importformen [N] spec-namespaces-und-module §5¶
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 §5.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.3¶
Ein Modulpfad, der ein Segment internal enthält, ist außerhalb des Packages nicht
importierbar. pub 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 §5.6¶
Result und Option sind kanonisch in jdl::core definiert und werden automatisch in den
Scope gebracht. Das ist kein Wildcard-Import von jdl::core.
Primitive Builtins (i8..i64, u8..u64, f32, f64, bool, str, ()) sind keine
Prelude-Importe, sondern Sprach-Builtins.
18.7 Namenskonflikte [N] spec-namespaces-und-module §8¶
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 §9¶
| Namensraum | Bedeutung |
|---|---|
jdl:: |
Root der user-facing Stdlib |
jade:: |
reserviert für privilegierte System-/Runtime-Module |
@compiler |
compiler-provided Queries und Primitive |
Namensräume mit @-Präfix sind für Compiler und Toolchain reserviert. @intrinsics ist
kein kanonischer Namensraum mehr; bestehende Verwendungen sind Altlast und auf
@compiler zu normalisieren.
18.9 mod.jdl [N] spec-namespaces-und-module §7¶
Optionale API-Kontrolle über Re-Exports. Nicht erforderlich; formt die öffentliche Oberfläche eines Packages.
19. Deklarative Konstrukte¶
19.1 CallGraph [N] 07 §9.1 — requires [O]¶
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.
07 §9.1 stellt fest, dass der requires-Block eine Redundanz zur Row ist, und lässt
offen, ob er entfällt oder als geprüfte Zusicherung bleibt. Beide Formen sind hier
abgebildet.
Form A — ohne requires:
CallGraph app(req: HttpRequest) ->{Throw[AppError]} HttpResponse {
env: {
Db[Primary]: PostgresHandler { pool }
Db[Replica]: PostgresHandler { replicaPool }
Alloc[ReqArena]: ArenaHandler { size: 64.kib }
}
handleRequest(req)
}
Form B — mit requires als geprüfte Zusicherung:
CallGraph app(req: HttpRequest) ->{Throw[AppError]} HttpResponse {
requires: [UserDb, LogService]
env: {
UserDb: PostgresUserDb { pool }
LogService: ConsoleLogger {}
}
handleRequest(req)
}
Weil der CallGraph eine echte Datenstruktur ist, sind Verhaltens-Refinements möglich, ohne den Compiler zu berühren:
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.
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.
Pureverlangt eine leere Row und keineRefMut/Out-Parameter.Regel P-2.
Deterministicverlangt Row ⊆{Alloc[_]}und keineRefMut/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 — while, break, continue, return, Schleifen als Ausdruck sind in keinem Dokument spezifiziert |
§17.3 |
| 2 | Pattern Matching — Destrukturierung, Guards, Exhaustiveness-Regeln nicht normiert | §16.2 |
| 3 | Reichweite der Blockform — vier der fünf \|-Rollen 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 als Form nicht festgelegt |
§9.3 |
| 8 | Blueprints effektfrei gegen Rows in Feldpositionen | §19.3 |
| 9 | requires im CallGraph — entfällt oder bleibt |
§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 |
Die ersten beiden sind von anderer Art als der Rest: Sie betreffen Konstrukte, die jedes JDL-Programm braucht, und sind nirgends geschrieben. 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. |
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.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.