Notiz — Constraints in `where`, Meta-Phase und CompilerDB-Zugriff¶

Status: Ideensammlung, nicht normativ Herkunft: Gesprächsdurchgang, ausgehend von einem fremden Design-Text Geltungsbereich: Sprachebene, Meta-Phase, Trusted-Core-Auswirkungen

Nichts hier ist entschieden. Alle Codebeispiele sind spekulativ und dienen nur dazu, die Idee lesbar zu machen.

0. Wo das herkam¶

Ausgangsfrage: Wie schreibe ich Constraints besser — insbesondere für Querschnittsfunktionen wie Wire?

Zwischenerkenntnis, die den Rest getragen hat: Refinements sind Meta-Funktionen. Nicht ähnlich, dasselbe. Damit ist auch ein Meta-Constraint eine Meta-Funktion — sie sieht einen Typ an und urteilt.

Nicht gemeint ist T: X. Das nimmt an Auflösung und Typprüfung teil und ist etwas anderes; siehe Abschnitt 6.

Der ausgewertete Fremdtext wollte daraus ein eigenes System bauen (Constraint-Typ, Algebra, symbolische Propositionen, expliziter MetaContext). Die Diagnose des Textes war meist richtig, die vorgeschlagenen Mechanismen fast durchweg schon vorhanden oder unnötig. Abschnitt 8 hält fest, was bewusst nicht verfolgt wurde.

1. Constraints in `where`¶

Idee: where darf zusätzlich den Aufruf einer Meta-Funktion enthalten.

// spekulativ
def CanWire[T]() ->Meta{} bool {
    import jdl::meta
    val ok = meta.hasProvide(WireType, [T])
    if not ok {
        meta.diagnostic(DiagnosticEntry {
            summary: f"{meta.name(T)} hat kein WireType-Provide"
            severity: Error
        })
    }
    ok
}

def send[T: Serializable](value: T) ->{Throw[WireError]} ()
    where CanWire[T]()
= ...

Eigenschaften:

gewöhnliche Funktion, Phase am Pfeil, Rückgabe bool
Komposition ist ein Funktionsaufruf, kein neuer Mechanismus
kein Constraint-Typ, keine Algebra, kein neues Schlüsselwort

Grammatikseitig ist das genau eine Alternative mehr. Heute:

Relation ::= Name ":" KindConstraint

Ein Meta-Aufruf ist aber keine Relation. Sauberer wäre eine Ebene darüber:

WhereClause ::= "where" WhereTerm ("," WhereTerm)*
WhereTerm   ::= Relation | MetaCall

Dazu, getrennt von der Grammatik, als Typbedingung:

Ein MetaCall in WhereTerm muss zu einer Meta-Funktion
mit Rückgabetyp bool auflösen.

2. Warum `bool` reicht¶

Ein Constraint wird bei der Instanziierung geprüft, und dort ist T konkret. Es gibt nichts Offenes, über das symbolisch geredet werden müsste.

Reihenfolge — das ist keine Beobachtung, sondern die Bedingung, unter der bool reicht. Gehört normativ festgehalten:

1  Typauflösung        T wird aus der Aufrufstelle bestimmt
                       T: X nimmt teil und kann beschränken
2  Meta-Constraints    urteilen über das fertige T
3  Instanziierung      wenn 2 durchgeht

Folge: Ein Meta-Constraint kann die Auflösung nicht beeinflussen und trägt nie zur Kandidatenauswahl bei. Er darf das Ergebnis nur annehmen oder ablehnen.

Das ist die eigentliche Schutzwirkung des ganzen Modells: Beliebige Metaprogrammierung darf komplex sein, weil sie außerhalb der Typauflösung steht.

Nebenwirkung für Fehlermeldungen: „Typ nicht bestimmbar" und „Constraint verletzt" sind zwei verschiedene Fehler. Der zweite darf nie erscheinen, wenn der erste zutrifft.

3. Diagnostik statt Schweigen¶

Ein bool sagt nein und begründet nichts. Der Rumpf einer Meta-Funktion kann aber meta.diagnostic(...) aufrufen — mit Feldnamen, Ursache, Severity.

Das ist der eigentliche Unterschied zu T: X. Ein Protokollname kann nur „kein Provide" melden.

Konvention, die sich anbietet — als Erlaubnis, nicht als Pflicht:

Ein Meta-Prädikat darf Diagnostik erzeugen.
Liefert es false ohne Error-Diagnostik, synthetisiert der
Compiler eine Standardmeldung.

Eine Pflicht wäre schädlich: Dieselbe Funktion soll auch als gewöhnliches Prädikat befragbar sein, ohne beim bloßen Fragen zu brüllen. Außerdem vermeidet die schwache Form doppelte Meldungen bei Komposition.

4. `and` gegen `All` — die Abkürzungsfrage¶

and kürzt ab. Scheitert der linke Teil, läuft der rechte nicht, und seine Diagnostik entsteht nie.

// spekulativ — sammelt beide Gründe
def CanDistribute[T]() ->Meta{} bool =
    All([
        CanWire[T]()
        CanPersist[T]()
    ])

Der Listenaufbau erzwingt beide Aufrufe. All ist danach eine langweilige Faltung über bool.

and    wenn die zweite Prüfung die erste voraussetzt
All    wenn die Prüfungen unabhängig sind

Beispiel für and: IsStruct[T]() and HasSerializableFields[T](). Ohne Struct gibt es keine Felder, die zweite Meldung wäre Lärm.

Vorbehalt: Das hängt daran, dass Listenelemente strikt ausgewertet werden. Bei einer strikten Sprache ist das die Normalannahme, steht aber nirgends geschrieben. Für reproduzierbare Diagnostik gehört links-nach-rechts gleich mit festgelegt.

(Suchwörter in der Literatur für diese Unterscheidung: Either gegen Validation. Der Inhalt ist das, was oben steht.)

5. Warum nicht `:> Where(...)`¶

Zwei Gründe, der zweite ist der harte.

Ontologisch: 04-axiomatik-profiles-executables §1.2 sagt wörtlich, :> sei kein Query/Constraint. Bestehende Funktions-Refinements (Cache, Retry, Timeout, Transactional) sind alle Verhaltensänderungen, keine Vorbedingungen.

Mechanisch: Eine Refinement-Anwendung läuft einmal pro Deklaration — ApplyRefinement, PatchSet, Kohärenzprüfung, Materializer committed. Ein Constraint auf T muss pro Instanziierung neu urteilen. Das ist ein zweiter Lebenszyklus in einem Mechanismus, der für einen gebaut wurde.

Offen geblieben: Ob Typparameter der Deklaration in Refinement-Position überhaupt sichtbar sind, ist nirgends spezifiziert. Bei :> Cache(config) stellte sich die Frage nie.

6. `T: X` gegen `where f[T]()`¶

Beide bleiben, sie beantworten verschiedene Fragen.

T: X               Zugehörigkeit    Tabellenabfrage nach Provide
where f[T]()       Urteil           Meta-Funktion läuft

Zwei Unterschiede, die zählen:

Teilnahme an der Auflösung. T: X steht in der Typprüfung und kann bei mehreren Kandidaten mitentscheiden. Ein Meta-Constraint kommt an, wenn die Entscheidung gefallen ist.

Erlaubnis im Rumpf. T: Comparable sagt dem Typchecker, was T kann — compare darf aufgerufen werden. Ein bool aus einer Meta-Funktion sagt für den Rumpf nichts.

T: X               Bedingung und Erlaubnis
where f[T]()       nur Bedingung

Kein sauberes Prinzip: Die Grenze ist durchlässig. Retryable ist sealed und entsteht aus C-2 — ein Urteil, das wie ein Vertrag aussieht. Umgekehrt könnte eine Meta-Funktion im Rumpf nichts weiter tun als hasProvide aufzurufen.

Randnotiz: 13.2 hat heute die Prüffrage „brauche ich U, um den Constraint auf T auszudrücken?" als Kriterium für inline gegen where. Mit Meta-Aufrufen stimmt das nicht mehr — die gehören immer ins where, unabhängig von der Parameteranzahl.

Ebenfalls offen: Was gilt, wenn inline und where sich widersprechen? Vermutlich einfach beides muss gelten, wie bei zwei where-Relationen. Aufgeschrieben ist es nicht.

7. CompilerDB-Zugriff: explizite Fassade per Import¶

Bisher: implizites db.* im Meta-Rumpf. Der Fremdtext wollte daraus einen expliziten MetaContext-Parameter machen, was einen Wert erzeugt, der nicht entkommen darf — also ein neues Sprachkonzept.

Alternative, die nichts Neues braucht:

// spekulativ
def HasStableLayout[T]() ->Meta{} bool {
    import jdl::meta
    ...
}

Die Abhängigkeit steht sichtbar, nur nicht im Pfeil. Lokale Imports in Funktionsrümpfen gibt es bereits.

7.1 Symmetrie zu Intrinsics¶

Die Spec hatte die Symmetrie schon, nur ohne Namensraum auf der linken Seite:

Compile-Zeit:  Meta-Funktion  →  db.*         →  CompilerDB
Runtime:       def            →  intrinsic::  →  RuntimeBus

jdl::meta über jade::meta ist der fehlende Namensraum (Schichtung siehe 7.4). Denkbar, dass die Phase das Ziel des Intrinsics bestimmt, statt ein zweites Schlüsselwort einzuführen:

// spekulativ
def fields(of: TypeSubject) ->Meta{} [FieldDef] = intrinsic::meta::fields
def now() -> Timestamp                        = intrinsic::clock::now

7.2 Wo die Zig-Naht liegen könnte¶

Vorschlag: Eine primitive meta-Operation bildet genau eine CompilerDB-Query oder einen Patch-Konstruktor ab. Alles, was sich daraus zusammensetzen lässt, ist normales JDL.

fields()       → Query
hasProvide()   → Query
setMeta()      → Patch
diagnostic()   → DiagnosticPatch

Ebenfalls zu präzisieren: „Intrinsics in Meta-Code verboten" ist zu grob. Gemeint sein kann nur, dass Runtime-Intrinsics dort verboten sind. Meta-Intrinsics sind gerade die Grenze zur CompilerDB.

Die Zig-Oberfläche wäre damit exakt der bestehende Query-Katalog. Bequemlichkeit darüber ist JDL:

// spekulativ
def mutableFields(of: t: TypeSubject) ->Meta{} [FieldDef] =
    fields(of: t) |> filter(f => isMutable(f))

filter ist eine gewöhnliche Funktion mit leerer Row und in der Meta-Phase aufrufbar.

7.3 Bootstrap-Haken¶

Die Blattschicht von jade::meta muss reine Deklaration sein — Signatur plus Intrinsic-Verweis, kein Rumpf mit Logik. Sonst bräuchte der Evaluator fields, um fields auswerten zu können.

Die zweite Schicht darf Rümpfe haben, weil sie schon auf der ersten steht.

7.4 Gating¶

Zwei vorhandene Schichten, keine neue:

S-13: Runtime-Code ruft niemals Meta-Code auf. Der Import ist erlaubt, der Aufruf ist ein Typfehler.
Constitution mit OnImport-Trigger: „dieses Package sieht jade::meta::patch gar nicht erst."

Damit wird die Granularität zur Namespace-Frage — die Constitution kann nur auf dieser Ebene greifen. Drei Namespaces sind trennbar, einer ist es nicht.

Ringkonflikt. Die Constitution lässt Usercode heute nicht direkt auf jade:: zugreifen (user → jdl:: → jade::). Ein import jade::meta im Anwendercode bräche das. Zwei Auswege: eine phasenabhängige Ausnahme, oder — vermutlich besser — die User-Fassade eine Ebene höher legen:

User-Meta-Code
    ↓
jdl::meta::query / ::patch / ::diagnostic     Ring 2, normale Module
    ↓
jade::meta                                     Ring 1, dünne Blattschicht
    ↓
CompilerDB Query / Patch

Dann bleibt die Ringarchitektur unangetastet, und die privilegierte Schicht ist genau dort, wo ohnehin eine sein muss.

Wichtig dabei: Ring 1 sollte den Zugriff nicht von oben sperren. Deny gewinnt und ist nach unten nicht lockerbar — eine Ring-1-Regel würde jede Derive-Bibliothek in Ring 2 dauerhaft verbieten und aus „was die Stdlib kann, kann der User auch" ein Privileg machen. Selbstbindung pro Projekt, nicht Verbot von oben.

Randnotiz: Die Selektor-Form ist heute importeur-seitig (Import(from:, to:)). Für „Namespace X schützt sich gegen Zugriffe von außen" bräuchte es die andere Richtung mit offener Herkunft. Außerdem hat scope: zwei Lesarten — Aufenthaltsort gegen Autoritätsquelle.

8. Bewusst nicht verfolgt¶

Damit später nachvollziehbar ist, warum diese Wege offen liegen blieben.

Expliziter MetaContext-Parameter. Erzeugt einen Wert, der nicht entkommen darf. Braucht eine Nicht-Entkommens-Regel, also ein neues Sprachkonzept. Zusätzlich das Durchreichen bei jeder Komposition.

CompilerDB als Row-Element. Wäre in der Meta-Phase fast universell und trennt damit fast nichts. Die Row ist außerdem eine Auswahlmaschine — in der Meta-Phase gibt es keine Auswahl. Kein Handler installierbar, keine Tilgung, keine Senkung. „Ich fordere etwas an" gegen „ich hole es mir": nur das erste braucht die Row.

Constraint-Typ mit And/Or/Not und symbolischen Propositionen. Nur nötig, wenn Aussagen offen bleiben müssen — also wenn der Rumpf einer generischen Funktion gegen die deklarierten Constraints geprüft würde, bevor jemand sie aufruft. Bei Prüfung an der Instanziierung ist T konkret und bool reicht.

or und not in der Constraint-Oberfläche. Konjunktion ist geschenkt. Negation kostet: welche der drei Zustände not meint, Schichtung im Fixpunkt, negative Kanten im DepGraph. In allen gesichteten Beispielen kam not faktisch nicht vor — was aussah wie Negation (NoForbiddenHandles) war ein positiv formuliertes Prädikat mit verneinendem Namen.

Alloc als Meta-Row-Element. Das Element transportiert inhaltlich, was bei Erschöpfung passiert. In der Meta-Phase gibt es dafür genau eine Antwort: Übersetzung bricht ab. Nicht installierbar, nicht austauschbar, trennt nichts.

9. Randnotizen, die auffielen¶

Negation im Fixpunkt. 04a behauptet Reihenfolgeunabhängigkeit. C-6 liest aber eine negative Prämisse (not_proven(Copyable)) im Closure-Loop. Es funktioniert heute nur, weil Copyable ausschließlich von S-Regeln vor dem Loop gesetzt wird. Das ist eine Schichtungsregel, die befolgt, aber nicht aufgeschrieben ist. Sobald eine C-Regel Copyable ableitet, bricht C-6 still.

Sauberer als dokumentieren wäre, C-6 aus der positiven Closure herauszuziehen:

Phase S              strukturelle proven/excluded
Phase C              positive monotone Closure
Post-Closure         Share(Send) + not proven(Copyable) → MoveOnSend

Dann ist die Reihenfolgeunabhängigkeit tatsächlich gegeben statt nur zufällig erfüllt.

Rekursive Typen. Ein Prädikat, das in Felder absteigt, terminiert bei type Node : struct { next: Option[Node] } nicht. I-1 Totalität ist ohne einen Mechanismus dagegen eine Behauptung.

Korrektur gegenüber einer früheren Fassung dieser Notiz: „beim erneuten Auftreten vorläufig als erfüllt annehmen" ist keine allgemeine Lösung. Sie stimmt für monotone Eigenschaften wie AllFieldsSerializable, und sie ist offensichtlich falsch für IsAcyclic — dort ist genau das Wiederauftreten der Beweis für nein.

Der Evaluator sollte allgemeine Rekursion also nicht automatisch „lösen". Strukturtraversierung braucht entweder eine ausdrücklich zyklustolerante Query oder einen Kombinator mit expliziter Rekursionssemantik. Die CompilerDB behandelt Query-Zyklen ohnehin per Default als Fehler.

Meta-Allokation. Ohne Row muss etwas anderes entscheiden, wohin ein Wert alloziert wird. Mindestens zwei Lebensdauern:

Scratch    Zwischenlisten, Strings, Baugerüst — fällt am Aufrufende
Ergebnis   was in den PatchSet wandert — lebt bis zur Materialisierung

Die Signatur sagt nicht, welche gemeint ist. Kleine, lokale Escape-Frage: Was im Rückgabewert landet, überlebt.

TypeId. T kommt in der Meta-Funktion als Identität an, nicht als Name — die Auflösung ist vorher passiert. Die Leseseite der Fassade nimmt konsequent TypeSubject und nie str; kein lookup(name). Gleichnamige Typen aus verschiedenen Modulen sind über den vollqualifizierten Namen längst getrennt.

Diagnostik-Haken: Bei einem Alias liefert meta.name(T) den kanonischen Namen, nicht den, den der Benutzer getippt hat.

Offen: Eine TypeId ist ein Arena-Index und lauf-lokal. Für persistierte Ergebnisse über Compilerläufe hinweg braucht es einen stabilen Schlüssel — vermutlich das internierte Symbol plus normalisierte Struktur. Wird erst bei inkrementeller Übersetzung akut.

10. Anwendungsfall Wire¶

Wire zerfällt in drei Teile mit drei getrennten Adressen:

Ableiten    :> Derive([WireMessage])     Meta-Funktion erzeugt Patches
Prüfen      where CanWire[T]()           Meta-Funktion urteilt
Ausführen   Engine wählt Wire[Json]      Runtime, liest Descriptoren

Teil 1 und 3 standen schon. Teil 2 war die Lücke.

Beleg dafür in 04 §6.4 — unter dem Derive-Beispiel stehen drei Regeln in Prosa:

jedes Feld genau ein tag (via WireTags)
Tags eindeutig
Feldtyp selbst WireType oder verlustfrei darauf abbildbar

Für keine gab es einen Ort. T: WireType kann keine Tag-Eindeutigkeit prüfen. Die Regeln konnten nur fest im Compiler verdrahtet oder gar nicht durchgesetzt werden.

Verwandter Fall: Die Blueprint-Spec verdrahtet heute „jeder Typ in einem Blueprint-Feld implementiert Serializable" als Compiler-Regel. Solche Sätze sind der Grund, warum Querschnitts- funktionen im Compiler landen.

Faustregel, die sich aus der Aufteilung ergibt:

Urteil über einen Typparameter an der Aufrufstelle   →  where
Ableitung und Prüfung an einer Deklaration           →  :>

Bei Wire braucht es beides. Deshalb sah es lange nach einem fehlenden Mechanismus aus — es fehlte nur eine der zwei Hälften.

11. Was nachzuziehen wäre, falls das kommt¶

13.1   Grammatikzeile um MetaCall-Alternative erweitern
13.2   Prüffrage ergänzen: Meta-Aufrufe immer ins where
—      Reihenfolge Auflösung → Schranke → Meta-Constraint festhalten
—      Strikte Auswertung von Listenelementen festhalten
—      Konfliktregel inline gegen where
—      Sichtbarkeit von Typparametern in Refinement-Position

Alles klein. Der Rest dieser Notiz sind Beobachtungen, keine Aufgaben.

Notiz — Constraints in where, Meta-Phase und CompilerDB-Zugriff¶