TypeFn-Spezifikation — Prozedurale Typ-Funktionen¶
Status: Normativer Entwurf Erweitert: 03 — TypeFn-Semantik (Konsolidierung) Bezieht sich auf: CompilerDB-Spec, Ontologie (Tags & Phantoms), Refinements (00), Engine-Lifecycle, Design Constitution Autor: Elias
1. Zweck¶
typefn ist die JDL-Schnittstelle zur CompilerDB. TypeFns operieren zur Compile-Zeit auf TypeSubjects und Meta-Records: sie lesen Typstrukturen, validieren Kombinationen, konstruieren neue Typen und erzeugen MaterializationPatches. Nach der Compile-Zeit sind sie spurlos verschwunden.
Eine TypeFn schreibt nicht direkt in die CompilerDB. Schreibende db.*-Operationen erzeugen Patches, die erst nach erfolgreicher Auswertung durch den CompilerDB-Materializer atomar committed werden. Damit bleiben Proof Trace, Rollback, Cache und Diagnostics konsistent.
TypeFns sind das Compile-Zeit-Gegenstück zu Intrinsics (Runtime-Schnittstelle zum RuntimeBus). Beide sind kontrollierte Zugangspunkte zu tieferen Ringen.
2. Harte Constraints¶
Total Terminiert garantiert. Kein while, kein loop,
keine allgemeine Rekursion.
Deterministisch Selbe Eingabe → selbes Ergebnis.
Speicheragnostisch Keine Handles, keine Arenas, keine Allokation.
Nicht Turing-vollst. Strukturelle Rekursion über endliche Strukturen.
Keine Higher-Order Darf keine TypeFns zurückgeben.
Expression-basiert Letzter Ausdruck = Rückgabewert. Kein return.
Spurlos Existiert zur Runtime nicht.
2.1 Erlaubte Konstrukte¶
match Strukturelles Branching auf Tags, Enums, Varianten
if Prädikat-Branching auf boolean Bedingungen
val Immutable Let-Bindings
map, filter, fold Iteration über endliche Mengen
import Inline, full-qualified, nur Meta-Objekte
db.* TypeFnDbView im TypeFnContext (Section 5)
Literale str, i32, bool als Compile-Zeit-Werte
TypeFn-Aufrufe Komposition durch Aufruf
2.2 Verbotene Konstrukte¶
while, loop Unbegrenzte Schleifen
var Mutabler Zustand
return Explizite Rückgabe (expression-basiert stattdessen)
I/O Kein Dateisystem, kein Netzwerk
def-Funktionen Kein Aufruf von Runtime-Funktionen
Closures als Werte Keine First-Class-Funktionen
TypeFn als Rückgabe Muss zu konkretem Typ auflösen
Direktes <{}> Meta-Record-Literale nur innerhalb von TypeFns
3. Evaluationsmodell, Context und Target¶
3.1 TypeFnEvaluator¶
TypeFns werden nicht von der CompilerDB selbst evaluiert. Die CompilerDB ist Query-, Seed-, Descriptor- und Materialization-Substrate. Die Auswertung erfolgt durch einen TypeFnEvaluator beziehungsweise durch die TypeEngine/MetaEngine.
Stage 1 darf einen D-basierten Bootstrap-Evaluator verwenden. Ab Stage 2 ist der TypeFnEvaluator als Ring-1-JDL-Engine formulierbar. In beiden Fällen gilt derselbe semantische Vertrag:
TypeFn + TypeFnContext + Argumente
-> TypeFnResult
-> PatchSet / DiagnosticSet / TypeResult
-> CompilerDB-Materializer
-> committed Descriptoren und Meta-Records
Die Auswertung findet während der Meta-/Type-Resolution statt: nachdem TypeSubjects und Namen ausreichend aufgelöst sind, aber bevor Layout-Finalisierung, IR-Builder und Generator harte Annahmen über Typen, Provides oder Dispatch treffen.
3.2 TypeFnContext¶
Jede TypeFn wird in einem TypeFnContext evaluiert. In Source-Syntax wird dieser Context nicht als normaler Parameter geschrieben. Intern ist er jedoch explizit.
// kanonische Struktur, nicht user-facing Syntax
type TypeFnContext : struct {
db: TypeFnDbView
target: Option[TypeSubject]
phase: TypeFnPhase
namespace: ModulePath
proof: ProofTraceBuilder
}
db ist die im TypeFn-Body sichtbare Bindung auf context.db. Es ist keine globale Datenbank und kein frei austauschbarer Parameter. db ist eine eingeschränkte Fassade auf definierte CompilerDB-Queries und Patch-Erzeugung.
Die TypeFn darf den Context lesen, aber nicht verändern. Persistente Änderungen entstehen ausschließlich als Patches.
3.3 Refinement-Target und :>-Desugaring¶
Bei Refinement-TypeFns liefert der :>-Operator das Target-Subject.
wird intern zu:
Der Evaluator ruft die TypeFn mit context.target = User auf. Eine Refinement-TypeFn kann das Ziel über db.target() lesen.
typefn Share(policy: SharePolicy) -> MetaPatch {
val target = db.target()
db.setMeta(target, "share", policy)
}
Ordinary TypeFns, die nicht über :> angewendet werden, besitzen kein implizites Target und müssen TypeSubjects explizit als Argumente erhalten.
typefn HandlerMap(service: TypeSubject) -> TypeDescriptorPatch {
// service ist normaler Parameter, nicht context.target
}
Normativ gilt: :> ist kein normaler Funktionsaufruf. Es ist ein Meta-Operator zur Anwendung einer Refinement-TypeFn auf ein TypeSubject.
4. Refinements als TypeFn-Anwendungen¶
4.1 Grundprinzip¶
Refinements sind TypeFn-Anwendungen auf TypeSubjects. Ein TypeSubject ist jedes compile-time adressierbare Subjekt des Typsystems dessen Meta-Record durch die Type Engine verarbeitet wird: Primitive, Struct, Enum, Union, Function, Protocol, Blueprint und abgeleitete Descriptor-Subjects.
Der :>-Mechanismus bleibt einheitlich. Was zulässig ist, entscheidet nicht die Syntax, sondern die TypeFn-Prämissen, der TypeKind des Subjects und die Ring-0-Facts.
// Struct: werthaltender Typ mit Speicher- und Share-Policy
type CacheEntry : struct {
key: str
value: str
} :> Memory(Value) :> Share(Send)
// Blueprint: deklarative Ausführungsbeschreibung mit Engine-/Lifecycle-Policy
type Cache : blueprint {
entries: [CacheEntry]
maxSize: u32
} :> Queryable() :> ResourceLimits { maxTasks: 4 }
Runtime-orchestrierende Refinements wie Retry, Timeout, ResourceLimits, Parallel, OverrunPolicy oder Metrics sind nur auf Blueprints beziehungsweise Engine-Subjects zulässig. Speicher-, Ownership-, Share-, Drop-, Derive-, Operator- und FFI-Descriptor-Refinements bleiben auf den jeweils kompatiblen TypeSubjects zulässig.
Jedes Refinement ist die Anwendung einer TypeFn. Die TypeFn validiert die Kompatibilität mit dem Ziel-Subject und erzeugt einen MetaPatch nur bei Erfolg. Kein committed Meta-Record-Eintrag ohne Beweis.
4.1.1 Ring-0-Facts primitiver VM-Typen¶
Primitive VM-Typen besitzen axiomatische Ring-0-Facts. Dazu gehören Repräsentation, Größe, Alignment, Registerklasse, Immediate-/Handle-Status und die VM-interne Operationenklasse. Diese Facts werden vom Bootstrapper gesetzt und können von TypeFns gelesen, aber nicht überschrieben werden.
type i32 : primitive {
// Darstellung der Bootstrap-Facts, keine user-facing Feldsyntax
size: 4
align: 4
memory: Value
class: SignedInteger
}
Eine TypeFn darf zusätzliche Meta-Record-Informationen für i32 ableiten oder Protocol-Bindungen validieren, aber sie darf size, align, memory oder class nicht verändern.
i32 :> Derive([Renderable]) // zulässig, sofern Provide/Derive-Regeln erfüllt sind
i32 :> Memory(Ref) // Fehler: Ring-0-Fact `memory: Value` ist axiomatisch
Damit bleibt :> ein einheitlicher Mechanismus, ohne die VM-Fundamente zu verhandelbaren Benutzeraussagen zu degradieren.
4.2 Keine direkte Meta-Record-Manipulation¶
Die <{}> Syntax ist nicht Teil der user-facing Sprache. Meta-Records können ausschließlich über TypeFns gelesen und über MaterializationPatches vorbereitet werden. Die <{}> Notation lebt weiter als Darstellungsformat in Compiler-Diagnostics, REPL-Ausgaben, jade doc und Spezifikationsdokumenten.
4.3 Beispiel¶
typefn Own(policy: OwnPolicy) -> MetaPatch {
import jdl::protocols::Sync
val target = db.target()
if policy == Shared {
val mutableFields = db.fields(of: target)
|> filter(f => db.isMutable(f))
if not mutableFields.isEmpty() and not db.hasProvide(Sync, [target]) {
db.diagnostic(DiagnosticEntry {
summary: "Own(Shared) erfordert Sync auf Typen mit mutablem Zustand"
explanation: mutableFields |> map(f => f.name) |> join(", ")
severity: Error
})
db.Never
}
}
db.setMeta(target, "own", policy) // erzeugt MetaPatch; Commit durch Materializer
}
5. Der db-Parameter¶
db ist in jeder prozeduralen TypeFn als vordefinierter Name verfügbar. Source-seitig wird db nicht deklariert. Semantisch ist db jedoch ein Feld des TypeFnContext und damit ein expliziter, kontrollierter Evaluationsparameter.
db ist eine TypeFnDbView, nicht die rohe CompilerDB.
5.1 Leseseite¶
db.target() -> TypeSubject Aktuelles Refinement-Target; Fehler außerhalb von `:>`
db.fields(of: TypeSubject) -> [FieldDef] Felder eines Struct/Blueprint
db.typeOf(field: FieldDef) -> Type Typ eines Feldes
db.name(t: TypeSubject) -> str Name eines Subjects
db.typeParam(t: TypeSubject, index: i32) -> Type N-ter Typparameter
db.phantomParam(t: Type, name: str) -> Tag Phantom-Parameter-Wert
db.refinements(of: TypeSubject) -> [Refinement] Refinements eines Subjects
db.meta(of: TypeSubject, field: str) -> Option[Tag] Konkreter Meta-Record-Eintrag
db.metaRing(field: str) -> Ring Ring-Level eines Meta-Record-Feldes
db.hasProvide(protocol, args) -> bool Existiert ein Provide?
db.variants(of: TypeSubject) -> [VariantDef] Varianten eines Enum/Union
db.isMutable(field: FieldDef) -> bool Feld mutabel?
db.isConcreteType(t: Type) -> bool Typ vollständig aufgelöst?
db.isStruct(t: Type) -> bool Ist ein Struct?
5.2 Schreibseite¶
db.setMeta(target, field: str, value: Tag) -> MetaPatch
MetaPatch erzeugen; Commit durch Materializer
db.createStruct(name: str, fields) -> TypeDescriptorPatch
Neuen Struct vorbereiten
db.createEnum(name: str, variants) -> TypeDescriptorPatch
Neuen Enum vorbereiten
db.fnType(params, returnType) -> TypeDescriptorPatch
Funktionstyp vorbereiten
db.constructType(base, args) -> TypeDescriptorPatch
Generische Instanziierung vorbereiten
db.constructRefinement(r, args) -> RefinementPatch
Refinement-Instanziierung vorbereiten
5.3 Diagnostics¶
db.diagnostic(entry: DiagnosticEntry) -> DiagnosticPatch Compiler-Diagnostic vorbereiten
db.Never -> Type Bottom-Typ nach Error
5.4 Query-/Patch-Semantik¶
Jeder lesende db.*-Aufruf bildet auf eine definierte CompilerDB-Query ab. Jeder schreibende db.*-Aufruf erzeugt einen MaterializationPatch.
db.target() -> Context Target
db.fields(of: T) -> Query GetFields(T)
db.meta(T, field) -> Query GetMeta(T, field)
db.ring0Fact(T, f) -> Query GetRing0Fact(T, f)
db.hasProvide(P,args)-> Query LookupProvide(P,args)
db.setMeta(...) -> MetaPatch
db.diagnostic(...) -> DiagnosticPatch
Die TypeFn-Auswertung sammelt Patches. Erst der Materializer prüft Ring-Level, Ring-0-Facts, Coherence-Regeln und Konflikte und committed die Patches atomar.
6. Ring-geschichtete Meta-Records¶
Der Meta-Record eines Typs ist in Ring-Ebenen geschichtet. Höhere Ringe können tiefere lesen, aber nicht überschreiben. db.setMeta erzeugt nur einen MetaPatch; der CompilerDB-Materializer prüft den Ring-Level automatisch beim Commit.
Ring 0 (JME): handle_type, arena_policy, memory_layout
Ring 1 (Type Engine): own, share, init, destruct, type_constraints
Ring 2 (User): queryable, versioned, metrics, custom
6.1 Evaluationsmodell¶
Phase 1 — Absicht (Top-Down): Der User deklariert Refinements auf einem kompatiblen TypeSubject.
Phase 2 — Beweis (Bottom-Up): Die Type Engine validiert anhand von TypeKind, Ring-0-Facts, Meta-Record, Feldtypen und vorhandenen Provides. Um Own(Shared) auf einem Struct zu beweisen, müssen die Feld-Typen zuerst aufgelöst sein. Runtime-orchestrierende Refinements wie Timeout oder Retry werden dagegen nur auf Blueprint- beziehungsweise Engine-Subjects akzeptiert.
6.2 Proof Trace¶
Jeder Meta-Record-Eintrag trägt einen Proof Trace — die Kette der TypeFn-Aufrufe und Validierungsschritte die zum Eintrag geführt haben. Verfügbar für Diagnostics und Tooling.
6.3 Escape-Hatch — @trust¶
@trust("Begründung") senkt die Severity einer TypeFn-Validierung von Error auf Warning. Der Proof Trace vermerkt die Override-Begründung. @trust kann Ring-Ebenen nicht überspringen.
7. Rückgabetypen und Auflösungsregel¶
-> TypeDescriptorPatch Konkreten Typ vorbereiten (HandlerMap, TypedClient)
-> MetaPatch Meta-Record-Einträge vorbereiten (Own, Share, Queryable)
-> Tag Tag-Wert erzeugen (CanActivate, SafetyLevel)
-> bool Typ-Prädikat prüfen (HasField, IsSerializable)
-> Diagnostic Invariante prüfen (validateNoMutables)
Jeder TypeFn-Aufruf muss zu einem konkreten Ergebnis auflösen. Nach der Evaluationsphase enthält die CompilerDB nur vollständig aufgelöste Typen. Kein Fixpoint, kein mehrfaches Durchlaufen.
8. Inline-Imports¶
TypeFn-Bodies können Meta-Objekte inline importieren. Full-qualified only, lokal zum Body, gecacht.
typefn Own(policy: OwnPolicy) -> MetaPatch {
import jdl::protocols::Sync // Protocol
import jdl::tags::SharePolicy // Tag
import jdl::diagnostics::DiagnosticEntry // Type
// ...
}
Erlaubt: Tags, Types, Protocols, Phantoms, andere TypeFns. Verboten: def-Funktionen, Services, Handles, Intrinsics.
9. MetaConsumer — wer liest den Meta-Record?¶
Jedes Refinement erzeugt via TypeFn einen MetaPatch. Nach erfolgreichem Commit existiert daraus ein Meta-Record-Eintrag. Wer den Eintrag konsumiert, wird über ein provide MetaConsumer definiert:
provide MetaConsumer[Retry] {
hook: LifecycleHook.AroundExecute
def apply(inner, config) =
(spec) => {
var attempts = 0
loop {
match inner(spec) {
| Ok(v) => Ok(v)
| Err(e) if attempts < config.maxRetries => attempts = attempts + 1
| Err(e) => Err(e)
}
}
}
}
Ring-0-Facts werden vom Bootstrapper als axiomatische Seeds gesetzt und von JME/VM konsumiert. Ring-1-Policies wie own, share oder drop werden durch TypeFns bewiesen und als Descriptor-/Meta-Patches materialisiert. Runtime-orchestrierende Ring-2-Einträge werden über MetaConsumer-Provides konsumiert — run() liest die materialisierten MetaConsumer-/Engine-Descriptoren aus der CompilerDB und wendet sie an.
Discoverability: die CompilerDB indexiert alle MetaConsumer-Provides. :> im IDE zeigt nur Refinements deren MetaConsumer für die aktuelle Engine existiert.
10. Bootstrap-Integration¶
Stage 1 (D): TypeFn-Bodies werden geparst und zu Bytecode kompiliert, aber nicht evaluiert. Für jdl::core nur einfache Refinements die der D-Compiler direkt auswerten kann.
Stage 2 (VM): Die VM evaluiert prozedurale TypeFn-Bodies über den TypeFnEvaluator gegen die vorbefüllte CompilerDB. db ist dabei die TypeFnDbView des TypeFnContext, nicht die rohe CompilerDB.
11. Zusammenfassung der Invarianten¶
I-1 Totalität Jede TypeFn terminiert.
I-2 Determinismus Selbe Eingabe → selbes Ergebnis.
I-3 Auflösung Jeder Aufruf löst zu konkretem Ergebnis auf.
I-4 Speicheragnostik Keine Handles, keine Arenas.
I-5 Keine Higher-Order Komposition durch Aufruf, nicht Rückgabe.
I-6 Spurlosigkeit Zur Runtime nicht existent.
I-7 CompilerDB-Scope Nur TypeFnDbView, kein I/O, kein RuntimeBus.
I-8 Context Jede TypeFn wird in einem TypeFnContext evaluiert.
I-9 Target `:>` liefert das Refinement-Target; gewöhnliche TypeFns haben kein implizites Target.
I-10 Patch-Semantik Schreibende db.*-Aufrufe erzeugen Patches, keine Direktmutation.
I-11 Validierung Kein committed Meta-Record-Eintrag ohne TypeFn-Beweis.
I-12 Ring-Schutz Höhere Ringe können tiefere nicht überschreiben.
I-13 Subject-Scope Refinements gelten auf kompatiblen TypeSubjects; runtime-orchestrierende Refinements nur auf Blueprint-/Engine-Subjects.