01 — Refinements, Meta-Records und Tags¶

Status: Normativer Konsolidierungsentwurf
Ersetzt insbesondere: Profile als type-Alias auf Meta-Record

1. Meta-Records¶

Ein Meta-Record ist ein struktureller Compile-Time-Datensatz.

<{ own: Unique, share: Local }>

Er existiert ausschließlich für Compiler, Type Engine, Tooling und spätere Normalisierung. Er ist kein Runtime-Wert.

ASCII:

JDL Source
    |
    v
Meta-Record <{ own: Unique, share: Local }>
    |
    v
Type Engine
    |
    v
TruthProfile / Labels

2. Präfix- und Suffix-Form¶

Direkte Meta-Record-Schreibweise:

type <{
    own: Unique
    share: Local
}> DbConnection : struct {
    handle: HandleId
}

Refinement-Schreibweise:

type DbConnection : struct {
    handle: HandleId
} :> Own(Unique) :> Share(Local)

Beide Formen sind äquivalent, sofern Own und Share TypeFns sind, die Meta-Record-Fragmente erzeugen.

tag OwnPolicy : enum =
    | Unique
    | Shared
    | Weak

tag SharePolicy : enum =
    | Local
    | Send
    | Sync

typefn Own(policy: OwnPolicy) = <{ own: policy }>
typefn Share(policy: SharePolicy) = <{ share: policy }>

Auswertung:

Own(Unique)   => <{ own: Unique }>
Share(Local)  => <{ share: Local }>

Merge:

<{ own: Unique }> + <{ share: Local }>
    => <{ own: Unique, share: Local }>

4. Tags als Meta-Träger¶

Ein Tag kann ein Meta-Record tragen.

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

Das normalisiert zu:

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

Dieser Tag kann auf Definitionen angewendet werden:

type UserCache : struct {
    entries: Map[UserId, User]
} :> TaskLocal

Semantisch äquivalent:

type UserCache : struct {
    entries: Map[UserId, User]
} :> Own(Unique) :> Share(Local)

5. `profile` entfällt als Sprachkonstrukt¶

Bisherige Form:

type TaskLocal = <{ own: Unique, share: Local }>

Neue Form:

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

Begründung:

TaskLocal ist kein Werttyp.
Es gibt keine TaskLocal-Werte.
TaskLocal ist ein benannter Meta-Träger.
Also ist TaskLocal ein tag.

profile bleibt ein erklärender Begriff in der Dokumentation:

Profile = Tag mit gebundenem Meta-Record.

Kein eigenes Keyword. Kein Pseudo-Type. Keine kleine Ontologie-Katastrophe mit Hut.

6. Merge-Regeln¶

Wenn mehrere Meta-Record-Fragmente auf dieselbe Definition angewendet werden, entsteht ein normalisiertes Meta-Record.

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

type Cache : struct {
    entries: Map[str, str]
} :> TaskLocal :> Share(Send)

Hier kollidieren Share(Local) und Share(Send).

JDL unterscheidet drei Fälle:

Default Policy:
    darf überschrieben werden.

Explicit Policy:
    spätere explizite Policy darf frühere Default-Policy überschreiben.

Hard/Sealed Guarantee:
    darf nie überschrieben werden.
    Konflikt erzeugt Diagnostic.

Für v0.1 gilt konservativ:

M-1: Zwei widersprüchliche explizite Policies erzeugen einen Konflikt.
M-2: Ein Tag mit Meta gilt als explizite Policy, sofern nicht anders markiert.
M-3: Derived/sealed Labels entstehen nicht durch Merge, sondern durch Closure.
M-4: Derived/sealed Labels dürfen nie direkt im Meta-Record gesetzt werden.

7. Tag-Meta-Zyklen¶

Ungültig:

tag A :> B
tag B :> A

Diagnose:

Fehler: zyklische Tag-Meta-Anwendung.

A :> B
B :> A

Tags dürfen Meta tragen, aber Tag-Meta darf keinen Zyklus bilden.

8. Pipeline¶

Source
  |
  v
Refinement-Aufrufe
  |
  v
TypeFn-Auswertung
  |
  v
Meta-Record-Fragmente
  |
  v
Merge / Normalisierung
  |
  v
TruthProfile / Label Closure
  |
  v
Typecheck / IR / Generator

9. Normative Invarianten¶

R-1: `:>` akzeptiert nur Ausdrücke, die zu einem Meta-Record normalisierbar sind.
R-2: Tags dürfen Meta-Records tragen.
R-3: Wird ein Tag per `:>` angewendet, wird sein Meta-Record in das Ziel-Meta-Record gemerged.
R-4: Profile sind kein eigenes Sprachkonstrukt.
R-5: Profile werden als Tags mit Meta-Record modelliert.
R-6: Tag-Meta-Anwendung muss azyklisch sein.
R-7: Widersprüchliche Policies müssen deterministisch diagnostiziert werden.