JDL Notiz: Typalgebra, Records, Blueprints und semantische Typmaterialisierung¶

Status: Arbeitsnotiz / nach Review überarbeitet Datum: 2026-05-26 Ziel: Konsolidierung der Diskussion zu Alias, Newtype, Records, &, Blueprints, Funktionstypen, TypeKinds, Row-Polymorphismus, Effect Rows, Associated Types, Zero-field Newtypes und Variance.

Diese Notiz ist keine normative Spezifikation. Sie beschreibt den aktuellen Arbeitskonsens und soll später gegen die bestehenden JDL/Jade-Spezifikationen konsolidiert werden.

1. Grundthese¶

JDL sollte Typen nicht nur als Namen, sondern als algebraisch normalisierbare Beschreibungen behandeln.

Die zentrale Schichtung:

Record      = strukturelle Feldform, keine eigene nominale Identität
Struct      = nominaler Datentyp über einer Record-Form
Blueprint   = nominaler Beschreibungstyp über einer Record-Form
MetaRecord  = Compile-Time-Record für Policies, Refinements und TypeFacts
Alias       = transparenter Name für einen Typausdruck
Newtype     = neue nominale TypeId über einem Carrier
Tag         = reine Compile-Time-Bedeutung ohne Wert

Kurz:

Record definiert Form.
Struct/Blueprint definieren Interpretation.
Alias koppelt an einen bestehenden Typ.
Newtype entkoppelt durch neue nominale Identität.
Tag benennt Bedeutung ohne Runtime-Wert.

Der zentrale Entwurfsgrundsatz:

Struktur, Identität, Verhalten, Policy und Runtime-Bindung bleiben getrennte Ebenen.

Daraus folgt eine wichtige operative Regel für & und Re-Materialisierung:

Struct und Blueprint sind RecordShapes mit Identität und Interpretation.
Strukturelle Operationen wie & operieren auf der Record-Form-Schicht.
Identität und Interpretation kommen erst durch Materialisierung wieder dazu.

2. Alias und Newtype¶

Alias¶

type RawId = str

Ein Alias ist transparent:

RawId == str

Eigenschaften:

keine neue TypeId
keine neue Coherence-Heimat
keine neue Memory-Semantik
keine neue Protocol-Identität
nur ein weiterer Name für denselben Typausdruck

Aliases eignen sich als Carrier-Schablonen:

type IdCarrier = str :> NonEmpty :> MaxLen(64)

Newtype¶

JDL verwendet das eigene Keyword newtype für die Materialisierung einer neuen nominalen Identität über einer Form:

newtype UserId  = IdCarrier
newtype OrderId = IdCarrier

Ein Newtype erzeugt eine neue nominale Identität:

UserId != OrderId
UserId != IdCarrier

Eigenschaften:

neue TypeId
eigene Coherence-Heimat
eigener Protocol-/Methoden-Raum
gleiche zugrunde liegende Repräsentation wie der Carrier
Ring-0/Core-Facts werden übernommen oder neu aus dem Carrier abgeleitet
API, Provides und domänenspezifische Semantik werden nicht automatisch übernommen

Merksatz:

Alias = gleicher Typ, anderer Name.
Newtype = gleiche Repräsentation, anderer Typ.

newtype ist die einzige Form, einen Newtype zu erstellen. Die ältere ML-artige Schreibweise type X = X(Y) wird in JDL nicht mehr verwendet — sie ist didaktisch missverständlich (Namens-Wiederverwendung sieht wie Rekursion aus) und bietet keinen Mehrwert, weil JDL ADTs mit mehreren Konstruktoren über enum ausdrückt.

Spezialisierung bei der Newtype-Materialisierung¶

Bei der Materialisierung können Felder über & spezialisiert werden:

newtype EnrichedUser = User & { roles: [Role] }
newtype DefaultedUser = User & { name: str = "anonymous" }

Die rechte Seite des & kann strukturell erweitern (neue Felder hinzufügen) oder Default-Werte für existierende Felder vorbelegen. Default-Override ist die Standardbedeutung; feste Wertbindung (Konstantisierung von Feldern) wird nicht im Sprachkern abgebildet und ist Stdlib-Sache über Refinements.

Alias als Schablone, Newtype als Materialisierung¶

type IdCarrier = str :> NonEmpty :> MaxLen(64)

newtype UserId  = IdCarrier
newtype OrderId = IdCarrier
newtype PostId  = IdCarrier

IdCarrier definiert die wiederverwendbare Form. Die Newtypes materialisieren daraus eigenständige Domänen.

Alias liefert die Form.
Newtype erzeugt die Identität.

3. Record, Struct und Blueprint¶

Ein Record ist eine strukturelle Produktform:

{ name: str, age: i32 }

Ein Struct materialisiert eine Record-Form als Datentyp:

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

Ein Blueprint materialisiert eine Record-Form als Beschreibungstyp:

type RouteSpec: blueprint {
    method:  HttpMethod = .GET
    path:    str
    handler: (HttpRequest) -> HttpResponse
}

Der Unterschied liegt nicht in der Feldform, sondern im TypeKind und in der Interpretation:

Struct-Felder    = Laufzeitdaten
Blueprint-Felder = deklarative Beschreibung / Engine-Input
MetaRecord       = Compile-Time-Policy

Ein Record selbst ist noch kein nominaler Typ. Er ist ein Shape. Erst Struct, Blueprint oder Newtype materialisieren daraus einen konkreten Typ mit TypeDescriptor/TypeId.

Wichtig für strukturelle Operationen: Struct und Blueprint enthalten ihre Record-Form. Operationen wie & operieren auf dieser Form-Schicht, nicht auf der TypeKind-Wrapper-Schicht. Das Ergebnis von Struct & {...} oder Blueprint & {...} ist wieder ein RecordShape, der durch erneute Materialisierung (Newtype-Konstruktor, Struct-/Blueprint-Definition) eine neue Identität bekommen kann. So bleibt & eine Operation auf einer einzigen Schicht, statt eine pro TypeKind-Kombination.

4. Enum-Member-Kurzschreibweise¶

JDL kann eine führende-Punkt-Schreibweise für Enum-Member verwenden:

type AdminRouteSpec: blueprint {
    method:  HttpMethod  = .GET
    auth:    AuthPolicy  = .Required
    audit:   AuditPolicy = .Enabled
    cache:   CachePolicy = .Disabled
    path:    str
    handler: (HttpRequest) -> HttpResponse
}

Regel:

.Member ist nur erlaubt, wenn der erwartete Typ eindeutig ein Enum-Typ ist.

Desugaring:

.GET      => HttpMethod.GET
.Required => AuthPolicy.Required
.Enabled  => AuditPolicy.Enabled
.Disabled => CachePolicy.Disabled

Ohne erwarteten Enum-Typ ist .Member ein Compilerfehler.

5. Der `&`-Operator¶

& ist ein type-level Operator für strukturelle Komposition und Spezialisierung. Er operiert auf der Record-Form-Schicht: Struct, Blueprint und RecordShape reichen ihre Form an & durch, das Ergebnis ist wieder ein RecordShape.

Grundregel¶

A & B

bedeutet bei strukturellen Formen:

Nimm A als Basis.
Lege B darüber.
Bei kompatiblen Feldkollisionen gewinnt B.

Also: rechts überschreibt links, wenn die Kollision kompatibel ist.

Record-Merge¶

type Shape = { a: i32 } & { b: str }

normalisiert zu:

type Shape = { a: i32, b: str }

Kollisionsregeln:

Feld nur links: übernehmen
Feld nur rechts: übernehmen
gleiches Feld, gleicher Typ: rechter Default/Wert gewinnt
gleiches Feld, inkompatibler Typ: Compilerfehler

Beispiel:

{ method: HttpMethod = .GET }
& { method: HttpMethod = .POST }

normalisiert zu:

{ method: HttpMethod = .POST }

Leerer Record als neutrales Element¶

{} & { a: i32 } & { b: str }

normalisiert zu:

{ a: i32, b: str }

Algebraisch:

{} & A = A
A & {} = A

Der leere Record {} ist das neutrale Element für Record-&.

Alias vs. Newtype mit `&`¶

type Shape = { a: i32 } & { b: str }
    Alias, keine neue TypeId

newtype NamedShape = { a: i32 } & { b: str }
    Newtype, neue TypeId

Blueprint-Spezialisierung¶

type EffectBase[R, E, D]: blueprint {
    inputs: D
    run:    (D) -> Result[R, E]
    env:    D
}

newtype UserRegistrationEffect =
    EffectBase[User, UserError, UserDeps] & {
        run: deps => registerUser(deps)
    }
    :> Retry(max: 3)
    :> Timeout(30s)

Bedeutung:

EffectBase[...] definiert die Blueprint-Form.
& { run: ... } konkretisiert/spezialisiert diese Form.
newtype materialisiert daraus eine neue nominale Blueprint-Domäne.
:> setzt Policies auf diese Domäne.

Bei Blueprint-Spezialisierung über & sind zwei Fälle zu unterscheiden, die nicht vermischt werden dürfen:

Fall A — Konservative Spezialisierung des Blueprint-Typs. Wenn die Materialisierung als Spezialisierung desselben Blueprint-Typs gemeint ist, darf die rechte Seite nur existierende Felder vorbelegen oder kompatibel überschreiben. Der resultierende Newtype bleibt strukturell ein EffectBase[...].

Fall B — Erweiterter Newtype über erweitertem Shape. Wenn die rechte Seite neue Felder einführt, entsteht ein Newtype über einem erweiterten RecordShape. Der Newtype ist dann strukturell nicht mehr identisch mit EffectBase[...], sondern hat eigene Felder zusätzlich.

Beide Fälle sind legitim, aber sie haben unterschiedliche Konsequenzen für Type-Compatibility und Engine-Dispatch. Welcher Fall gemeint ist, ergibt sich aus den rechten &-Operanden — neue Felder verschieben automatisch von A nach B. Die Spec sollte das normativ benennen, damit Leser nicht in eine "Ausnahmeregel"-Lesart verfallen, obwohl es nur die Konsequenz der Record-Algebra ist.

6. Zero-field Newtypes, Tags und Witness Tokens¶

Ein Newtype über dem leeren Record {} erzeugt einen materialisierbaren Werttyp ohne Nutzdaten:

newtype AdminToken = {}

Eigenschaften:

eigene TypeId
runtime-materialisierbarer Wert
keine relevante Payload
typischerweise Unit-/Zero-size-Repräsentation
kann als Wert übergeben, verlangt oder gespeichert werden

Das ist nicht dasselbe wie ein Tag.

tag AdminOnly

Ein Tag ist eine reine Compile-Time-Bedeutung:

kein Wert
kein Layout
kein Konstruktor
keine Runtime-Materialisierung

Abgrenzung:

tag AdminOnly
    Bedeutung ohne Wert.
    Compile-time only.

newtype AdminToken = {}
    Wert ohne Nutzdaten.
    Runtime-materialisierbar.

Einsatzgebiete¶

Zero-field Newtypes eignen sich für:

Witness Values
Proof Tokens
Capability Tokens
State Tokens
API-Gates
kontrollierte Berechtigungsübergabe

Beispiel:

newtype AdminToken = {}

def deleteUser(token: AdminToken, id: UserId) -> Result[(), DeleteError]

Die Funktion verlangt einen konkreten Beweis-/Berechtigungswert. Dieser Wert trägt keine Nutzdaten, aber sein Typ ist relevant.

Regel:

Wenn keine Runtime-Existenz gebraucht wird: tag.
Wenn ein konkreter Beweis-/Berechtigungswert übergeben werden soll: zero-field Newtype.
Wenn ein Werttyp eine Bedeutung nur auf Type-Level tragen soll: phantom tag parameter.

Beispiel für Phantom-Tags:

tag Registered
tag Verified

type User[phantom State]: struct {
    id: UserId
    email: Email
}

Hier existieren Registered und Verified nicht als Werte. Sie klassifizieren den Typ auf Compile-Time-Ebene.

7. Funktionen als Typen¶

Funktionstypen sind normale Typausdrücke:

type RouteHandler = (HttpRequest) -> HttpResponse

Blueprint-Felder dürfen echte Signaturen haben:

type EffectBase[R, E, D]: blueprint {
    run: (D) -> Result[R, E]
}

Ein Funktionsfeld kann implementiert werden durch:

FQN-Funktionsreferenz
inline Blueprint-lokalen Funktionskörper

Beispiel mit FQN:

newtype UserRegistrationEffect =
    EffectBase[User, UserError, UserDeps] & {
        run: myapp::users::registerUser
    }

Beispiel inline:

newtype UserRegistrationEffect =
    EffectBase[User, UserError, UserDeps] & {
        run: deps => {
            deps.db.register(...)
        }
    }

Regel für Inline-Funktionen in Blueprints:

Sie dürfen keine äußeren lexikalischen Bindings capturen.
Sie dürfen nur referenzieren:
- eigene Parameter
- Blueprint-Felder
- FQN/importierte Symbole
- im Context verfügbare Services/Capabilities

Blueprint-Felder und Auflösung¶

Blueprint-Felder sind nach Initialisierung read-only. Sie tragen Compile-Time-Werte (Literale, FQN-Symbole, andere bereits aufgelöste Blueprint-Felder, Funktionswerte). Sie sind statische Konfiguration, kein veränderlicher Runtime-State.

Referenzen auf Blueprint-Felder aus Inline-Funktionen werden bei der Materialisierung des Newtypes aufgelöst und im resultierenden Funktionswert eingebacken. Die Auflösungs-Reihenfolge ist topologisch nach Abhängigkeiten zwischen den Feldern; zyklische Referenzen sind ein Compile-Fehler.

Echter mutierender State gehört nicht ins Blueprint, sondern in die Dependency-Row. Eine Funktion, die einen Cache oder eine DB-Verbindung braucht, deklariert das nicht als Blueprint-Feld, sondern als Service in D und greift über den deps-Parameter darauf zu. Damit bleiben Blueprints deklarative Beschreibungen statt Instanzen mit eingebautem State.

Ein capture-freier Funktionswert ist als CallDescriptor serialisierbar, wenn Parameter, Rückgabetyp, Constraints und referenzierte Symbole im Ziel-Context auflösbar sind. Da Blueprint-Feld-Referenzen bei Materialisierung substituiert werden, bleibt die Inline-Funktion auch nach Materialisierung capture-frei im lexikalischen Sinn.

Kernsatz:

Blueprint-Feld:
    echte Typsignatur, read-only, Compile-Time-Wert

Engine:
    verlangt Implementierung dieser Signatur

Implementierung:
    inline oder per FQN

State:
    explizit in der Dependency-Row, nicht im Blueprint

Auflösung:
    bei finaler Newtype-Materialisierung, topologisch, eingebacken

8. Type-Level-Normalisierung¶

Typausdrücke werden vor TypeId-Vergabe, Constraint-Prüfung und Descriptor-Erzeugung normalisiert.

Beispiele:

A | B | A        => A | B
{ a } & { b }    => { a, b }
type RawId = str; newtype UserId = RawId => UserId(str)

Aber:

newtype RawId  = str
newtype UserId = RawId

bleibt UserId(RawId), weil RawId ein Newtype ist.

Invarianten:

Alias wird aufgelöst.
Newtype bleibt nominale Grenze.
Union wird flach, dedupliziert und stabil geordnet.
Record-& wird kanonisch gemerged.
Refinements werden in kanonische MetaRecord-Form gebracht.

Normalisierung ist Grundlage für:

TypeId-Stabilität
CompilerDb-Cache-Keys
Coherence-Prüfung
Descriptor-Erzeugung
bessere Diagnostics

Ohne Normalisierung werden logisch gleiche Typen intern verschieden. Das ist keine Designfreiheit, das ist später ein Bug mit akademischem Hut.

9. TypeKind / Kinds / Bootstrap Seed¶

JDL braucht kein neues oberflächliches Kind-System. Die vorhandenen Ring-0/TypeEngine-TypeKinds bilden die semantischen Kinds des Typsystems.

TypeKind sagt: Was ist das?
Labels sagen: Was gilt dafür?
Protocols sagen: Was kann es?
Refinements sagen: Welche Policy wurde gesetzt?

Beispiele für TypeKinds:

Primitive
Struct
Enum
Union
Function
Tuple
Blueprint
Flags
RecordShape
MetaRecord
Protocol
Service
Newtype
Alias

TypeFns und Typalgebra prüfen gegen TypeKind + Ring-0-Facts.

Beispiele:

Pick/Omit verlangen RecordShape-kompatible Typen.
Blueprint-Spezialisierung verlangt Blueprint-kompatible TypeKinds.
Newtype verlangt einen materialisierbaren Carrier.
& verlangt kompatible strukturelle TypeKinds (operiert auf der Record-Form-Schicht).

Bootstrap Seed¶

JDL-Primitives entstehen nicht durch normale User-Typdefinitionen. Sie werden im Bootstrap Seed als kanonische TypeDescriptors registriert.

Ring 0 liefert unverhandelbare Facts:

Repräsentation
Größe
Alignment
Registerklasse
Immediate/Handle-Status
primitive Operationsklasse

Der Bootstrap Seed materialisiert daraus JDL-sichtbare TypeIds und Namen.

Aliases können zusätzliche Namen auf denselben Descriptor legen. Newtypes erzeugen neue TypeIds über einem Carrier.

Schichtung:

Ring 0 / Jade Core:
    Primitive Facts, TypeId, TypeKind, TypeDescriptor, JME, VM, Intrinsics

Bootstrap Seed:
    minimale JDL-Typen, Primitive-Namen, Result, Option, Loader-Diagnostics

Stdlib / JDL:
    Protocols, Effects, Rows, Associated Types, Profiles, Collections, Engines

Userland / Plugins:
    konkrete Blueprints, Services, Domain-Typen, externe Integrationen

10. Row-Polymorphismus¶

Row-Polymorphismus erlaubt strukturelle Constraints auf Typen, ohne den exakten nominalen Typ zu verlangen.

def getName[T](x: T) -> str
where T has { name: str } =
    x.name

Bedeutung:

T muss mindestens ein Feld name: str besitzen.
T darf weitere Felder haben.

Das trennt Struktur von Verhalten:

T: Serializable + Send   => Verhalten/Garantien
T has { name: str }      => strukturelle Anforderung

Nested Constraints sind möglich:

where T has {
    profile: { email: Email }
}

oder mit separatem Feldtyp-Constraint:

where T has { config: C }
where C: Serializable + Send

Der eigentliche Nutzen ist, dass Constraints auf unterschiedlichen Ebenen des Typs gezogen werden können:

TypeKind-Ebene:
    T ist Struct / Blueprint / RecordShape / Function / ...

Protocol-/Label-Ebene:
    T erfüllt Serializable + Send

Row-/Shape-Ebene:
    T hat bestimmte Felder

Feldtyp-Ebene:
    T.x hat Typ X oder erfüllt Constraint C

Nested-Shape-Ebene:
    T.a.b.c existiert mit bestimmter Struktur

Meta-/Refinement-Ebene:
    T oder ein Feld trägt bestimmte Policies

Effect-/Context-Ebene:
    D enthält bestimmte Services/Capabilities

Nutzen:

generische, stark typisierte APIs
präzise Field-Level-Constraints
Blueprints und Dependency-Rows
weniger künstliche Marker-Protocols

11. Verbrauchssemantik gehört nicht in die Typalgebra¶

Verbrauchssemantik (Move, Use-after-Move, Drop) ist nicht Teil der Typalgebra und entsteht nicht über Refinements. Refinements sind monoton-additiv: Sie verfeinern eine Typeigenschaft, sie tragen keine Konsumlogik.

Verbrauchssemantik in JDL entsteht aus Ownership-Labels (own: Unique, !Copyable) plus Bewegungsoperationen und wird vom Typechecker über die TruthProfile-Closure erzwungen.

Diese Mechanik gehört normativ in:

03-runtime.md (Runtime-Modell): Use-After-Move-Diagnose, Move/Drop-Semantik, User-Sicht
04a-label-inferenz-regeln.md (Label-Inferenz): Closure-Regeln, die aus own: Unique + Move die Verbrauchsableitung produzieren

In der Typalgebra wird sie ausdrücklich nicht behandelt.

12. Effect Rows¶

Effect[R, E, D] wird durch Row-Polymorphismus deutlich stärker.

R = Erfolgstyp
E = Fehlertyp
D = Dependency-/Capability-Row

Beispiel:

type UserDeps = {
    db:  UserDb
    log: Logger
}

def fetchUser(id: UserId) -> Effect[User, UserError, UserDeps]

Offene Dependency-Constraints:

def audit[D](event: Event) -> Effect[(), AuditError, D]
where D has {
    log: Logger
}

Bedeutung:

Die Funktion ist in jedem Context ausführbar,
der mindestens log: Logger bereitstellt.

Algebra:

D1 & D2 kombiniert Dependency-Rows.
D has { field: Service } prüft Mindestanforderungen.
Context C satisfies D, wenn C alle Felder aus D bereitstellt.

Row-Satisfaction wird statisch geprüft¶

Die Prüfung, ob ein Context die Dependency-Row eines Effects erfüllt, findet statisch bei der Effect-Composition statt — also dort, wo Effect und Context zusammengeführt werden, nicht erst bei Ausführung.

Wichtig: Row-Satisfaction prüft Service-Traits/Capability-Typen, nicht konkrete Provider. Wenn ein Effect D has { log: Logger } verlangt, prüft die Composition, ob der Context einen Service-Slot log: Logger besitzt. Welcher konkrete Logger zur Runtime dort gebunden ist (z.B. via Dispatch-Mode oder Plugin-Resolution), ist eine andere Schicht und wird nicht von der Row-Satisfaction abgedeckt. Effect-Composition tut keine Service-Lookups.

Trennung:

D beschreibt benötigte Fähigkeiten.
Context stellt konkrete Fähigkeiten bereit.
Row-Satisfaction prüft das statisch zur Composition-Zeit.
Engine interpretiert oder führt den Effect aus.
Konkreter Provider wird über Dispatch/Plugin gelöst, nicht über die Row.
E bleibt Fehlerkanal und wird über Union-Typen modelliert.

Effect Rows geben Effect[R, E, D] eine natürliche funktionale Richtung, ohne dass JDL dafür ein separates Effekt-Sprachsystem braucht.

13. Opaque, dyn und reified¶

JDL trennt drei Formen von Typinformation:

opaque:
    konkreter Typ ist statisch bekannt, aber nach außen verborgen

dyn P:
    konkreter Typ ist zur Compile-Zeit nicht bekannt;
    Runtime-Typinfo/Protocol-Bindung nötig

reified T:
    Typparameter wird explizit zur Laufzeit materialisiert

Diese Trennung ist wichtig:

Generics sind nicht automatisch dyn.
Opaque ist nicht dyn.
Reified ist explizit, nie implizit.

14. Associated Types¶

Associated Types sind Typplätze innerhalb eines Protocols, die zur Implementierung gehören.

protocol Generator {
    type Item
    def next(self) -> Option[Self.Item]
}

Implementierung:

provide Generator for UserStream {
    type Item = User
    def next(self) -> Option[User] = ...
}

Associated Types dürfen Constraints haben:

protocol Repository {
    type Entity
    type Id: Hashable + Equatable

    def get(self, id: Self.Id) -> Result[Self.Entity, RepoError]
}

Nutzen:

weniger generischer Parameterlärm
klarere API-Semantik
bessere Abstraktion
Engine-, Parser-, Generator-, Codec- und Repository-Modelle werden natürlicher

Regel:

Associated Types werden pro provide eindeutig festgelegt.
Sie sind Teil der Protocol-Implementierung.
Sie können Constraints tragen.

15. Variance¶

Variance beschreibt, wie sich ein generischer Typ verhält, wenn sein Typparameter durch einen spezielleren oder allgemeineren Typ ersetzt wird.

Das klingt schlimmer, als es ist. Die einfache Frage lautet:

Wenn A dort verwendbar ist, wo B erwartet wird,
gilt das dann auch für Container[A] und Container[B]?

Oder konkreter:

Wenn Email als str verwendbar ist,
ist dann Array[Email] auch als Array[str] verwendbar?

Die Antwort hängt davon ab, was der generische Typ mit T macht.

Wichtig — Querverweis zur Cast-Effekte-Spec: Die Prämisse "A ist als B verwendbar" ist nicht automatisch erfüllt, nur weil ein Refinement-/Newtype-Verhältnis besteht. Ob ein refinement-verfeinerter Typ wie Email = str :> ValidEmail strukturell als str gilt — also Email <: str für Variance-Zwecke — hängt am Cast-System und am Refinement-Subtyping. Die normativen Regeln dazu stehen in 07-cast-effekte-refinements.md. Diese Notiz behandelt Variance unter der Annahme, dass die Subtyping-Beziehung bereits durch das Cast-System etabliert ist.

Drei Fälle¶

1. Kovariant: Lesen ist sicher¶

Ein Typ ist kovariant in T, wenn Werte von T nur nach außen gegeben oder gelesen werden.

Beispiel:

ReadSeq[Email]

Wenn Email als str verwendbar ist, dann kann eine reine Lese-Sequenz von Email auch als Lese-Sequenz von str betrachtet werden.

ReadSeq[Email] <: ReadSeq[str]

Warum? Weil nur gelesen wird. Jeder gelesene Email-Wert ist auch ein str.

Typische kovariante Positionen:

Rückgabewerte
immutable/read-only Container
Output-Sequenzen
Result[R, E] in R und meist auch E

2. Kontravariant: Eingabe darf allgemeiner sein¶

Ein Typ ist kontravariant in T, wenn T nur als Eingabe konsumiert wird.

Das typische Beispiel ist eine Funktion:

(str) -> bool

Eine Funktion, die jeden str akzeptiert, kann auch dort benutzt werden, wo nur Email übergeben wird.

val acceptsString: (str) -> bool = s => s.len > 0
val acceptsEmail:  (Email) -> bool = acceptsString

Das ist sicher, weil jede Email auch als str gilt.

Umgekehrt ist es nicht sicher:

val acceptsOnlyEmail: (Email) -> bool = e => ...
val acceptsAnyString: (str) -> bool = acceptsOnlyEmail // Fehler

Eine Funktion, die nur Email korrekt behandeln kann, darf nicht als Funktion für beliebige str gelten.

Merksatz:

Bei Funktionen ist der Parameter kontravariant.
Je allgemeiner die Funktion akzeptiert, desto leichter kann sie eingesetzt werden.

3. Invariant: Keine automatische Ersetzung¶

Ein Typ ist invariant in T, wenn automatische Ersetzung unsicher wäre.

Das wichtigste Beispiel sind mutable Container.

type Email = str :> ValidEmail

val emails: Array[Email] = [...]
val strings: Array[str] = emails    // wenn das erlaubt wäre
strings.push("not-an-email")        // kaputt

Wenn Array[Email] als Array[str] gelten dürfte, könnte man einen beliebigen str in ein Array schreiben, das eigentlich nur gültige Emails enthalten darf.

Deshalb:

Mutable Container sind invariant.

Also:

Array[Email] ist nicht automatisch Array[str].

Funktionsregel¶

Für einen Funktionstyp:

(A) -> B

gilt:

A ist kontravariant.
B ist kovariant.

Einfach gesagt:

Input darf allgemeiner sein.
Output darf spezieller sein.

Result¶

Für:

Result[R, E]

ist die natürliche Regel:

R kovariant
E kovariant

Warum? Beide Typen werden aus Result heraus gelesen. Result konsumiert sie nicht durch Mutation.

Effect¶

Für:

Effect[R, E, D]

gilt als Ausgangspunkt:

R kovariant
E kovariant
D nicht über naive Variance, sondern über Row-Entailment

D beschreibt Anforderungen an den Context. Eine Berechnung, die weniger benötigt, kann in einem reicheren Context laufen.

Beispiel:

type NeedsLog = {
    log: Logger
}

type ProdDeps = {
    log: Logger
    db: UserDb
    cache: Cache
}

Ein Effect mit NeedsLog kann in einem Context mit ProdDeps ausgeführt werden, weil ProdDeps mindestens log bereitstellt.

Das ist keine simple Kovarianz oder Kontravarianz. Es ist Row-Satisfaction:

Context C satisfies D,
wenn C mindestens die Felder aus D bereitstellt.

Startregeln für JDL¶

Immutable/read-only Container:
    kovariant

Mutable Container:
    invariant

Funktionsparameter:
    kontravariant

Funktionsrückgaben:
    kovariant

Result[R, E]:
    R kovariant
    E kovariant

Effect[R, E, D]:
    R kovariant
    E kovariant
    D über Row-Entailment

Warum das wichtig ist¶

Variance verhindert, dass Generics mit Refinements, Rows und Funktionstypen unsicher werden.

Ohne klare Regeln passieren Dinge wie:

verfeinerte Werte werden durch allgemeine Schreiboperationen verletzt
Funktionen werden in falscher Richtung substituiert
Effects laufen in Contexts, die ihre Anforderungen nicht erfüllen

Kurz:

Variance sagt dem Compiler, wann generische Ersetzung sicher ist.

Das ist keine akademische Dekoration. Das ist Brandschutz.

16. Zusammenfassung¶

JDLs Typmodell lässt sich auf eine kleine Menge starker Regeln zurückführen:

Record definiert Form.
Alias gibt Namen.
Newtype gibt Identität (immer über das Keyword `newtype`).
Zero-field Newtype gibt materialisierbare Beweis-/Token-Werte ohne Payload.
Tag gibt compile-time Bedeutung ohne Wert.
& kombiniert oder spezialisiert strukturelle Formen (Record-Form-Schicht).
| beschreibt Alternativen.
:> setzt Refinements/Policies (monoton-additiv, keine Verbrauchssemantik).
TypeKind begrenzt gültige Typoperationen.
Row-Polymorphismus macht Struktur generisch.
Effect Rows machen Effekte zu echten algebraischen Bausteinen.
Row-Satisfaction ist statisch zur Effect-Composition.
Associated Types entlasten generische APIs.
Variance hält das Ganze typsicher (in Verbindung mit der Cast-Spec).
Verbrauchssemantik gehört nicht in die Typalgebra (siehe 03-runtime und 04a).

Der entscheidende Entwurfsgrundsatz:

Struktur, Identität, Verhalten, Policy und Runtime-Bindung bleiben getrennte Ebenen.

Das verhindert, dass Blueprints zu Structs mit Sonderbehandlung, Aliase zu halben Typen, Tags zu Runtime-Werten oder Effects zu magischen Funktionsaufrufen verkommen.

JDL Notiz: Typalgebra, Records, Blueprints und semantische Typmaterialisierung¶

1. Grundthese¶

2. Alias und Newtype¶

Alias¶

Newtype¶

Spezialisierung bei der Newtype-Materialisierung¶

Alias als Schablone, Newtype als Materialisierung¶

3. Record, Struct und Blueprint¶

4. Enum-Member-Kurzschreibweise¶

5. Der &-Operator¶

Grundregel¶

Record-Merge¶

Leerer Record als neutrales Element¶

Alias vs. Newtype mit &¶

Blueprint-Spezialisierung¶

6. Zero-field Newtypes, Tags und Witness Tokens¶

Einsatzgebiete¶

7. Funktionen als Typen¶

Blueprint-Felder und Auflösung¶

8. Type-Level-Normalisierung¶

9. TypeKind / Kinds / Bootstrap Seed¶

Bootstrap Seed¶

10. Row-Polymorphismus¶

11. Verbrauchssemantik gehört nicht in die Typalgebra¶

12. Effect Rows¶

Row-Satisfaction wird statisch geprüft¶

13. Opaque, dyn und reified¶

14. Associated Types¶

15. Variance¶

Drei Fälle¶

1. Kovariant: Lesen ist sicher¶

2. Kontravariant: Eingabe darf allgemeiner sein¶

3. Invariant: Keine automatische Ersetzung¶

Funktionsregel¶

Result¶

Effect¶

Startregeln für JDL¶

Warum das wichtig ist¶

16. Zusammenfassung¶

5. Der `&`-Operator¶

Alias vs. Newtype mit `&`¶