R3: Data: the type language closed under records and variants as Ty growthreq:R3
- Open, not triaged: variants: the tag select over records landed (decisions row 195 (d)); catchTag's residual, the caught tag subtracted from the error column, waits on decisions row 130
- Open, waits on a ruling (decisions row 124: recursive types as declarations of the application): recursive types are row 124 (open): nominal Σ_app declarations through Ty.app
- Open, not triaged: error payloads: the carrier (decisions row 120, part E1) and the face (part E2: one Data.TaggedError class per tag, printed and read back) landed; open: catchTag's residual over records (decisions row 130), int and number fields (row 121; a number field is refused by name as unreadable), a field typed by another class (refused by name), a record update of a class instance (it answers a structural object), and a host row answering a payload (R6, parked)
- Open, waits on a ruling (decisions row 108: the owner places the numbers slice; row 121 is ruled): int inhabited inside row 108's profile: ruled 2026-10-02 (decisions row 121); carried since decisions row 317, which removes the admission's int scan; the JSON wires since row 316; the computing rows (plus, minus, and lt and eq at int) since row 319; the Lean judgment and OCaml profile bound landed in row 321, and the TypeScript prelude refusal landed in row 322; the host truth record and comparison of an outside-profile result remain open (slice 7)
- Open, not triaged: the Schema and JSON images of app, null, undefined, number and bytes: unlowered or refused by name (decisions rows 121, 158, 160, 161)
- Open, after other work (a program that compares records (decisions row 126)): equality at records: eq stays refused at records until a program compares them (decisions row 126)
Requirement R3: First-order data typesabout:req:R3
This page explains requirement R3 in Effect4. It covers what the requirement asks for records and variants, why structured data types matter, and how the property is checked.
What the requirement asksabout:req:R3:what-it-asks
Requirement R3 asks that the static type language Ty closes under structured first-order data types (docs/core/system-map. §8, DB-15):
- Records: represented by a single constructor over field lists sorted in canonical name order (decisions row 119).
- Variants: tagged union representations with normalized membership (decisions row 130).
- Maps and tuples: pointwise and key-indexed compound data structures.
Every added constructor must provide its Fits membership rule, exact codecs, catamorphic folds, assignability order, and inhabitance characterization.
Why it mattersabout:req:R3:why-it-matters
Application workflows manipulate rich domain models including structured records, optional attributes, error payloads, and payload classes.
If the type system lacked direct representations for compound data, applications would need informal encodings that escape verification.
Closing Ty under records and variants provides thorough end-to-end verification for realistic application data structures.
How it is checkedabout:req:R3:how-it-is-checked
The requirement is checked by proving algebra, membership, codec, and inhabitance theorems across all constructors:
- Value membership under normalization is stated by
fits_normalizeandfits_subN(src/Effect4/Laws/Program/Typed/Membership.).lean - Semantic inhabitance equivalence is stated by
inhabited_iff_fitsin the same file. - Exact serialization embeddings are stated by
decode_iff(src/Effect4/Laws/Schema/Codec.) andlean ofSchema_exact(src/Effect4/Schema/Bridge.).lean - Error payload round-trip fidelity is stated by
errOf_valOfErr(src/Effect4/Laws/Program/Admit.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- Residual Program Typing proved, 2 nodes → No concept, Exact Codecs, Store Typing
- No concept proved, 7 nodes → Exact Codecs
- Store Typing proved, 5 nodes → Subtyping Algebra, No concept
- Exact Codecs proved, 6 nodes → No concept, Store Typing
- Subtyping Algebra proved, 2 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
checkInput_eq_none_iff | proved | — | — |
fits_normalize | proved | — | subN_trans, normalize_idem |
fits_subN | proved | — | subN_trans, fits_normalize |
inhabited_iff_fits | proved | — | subN_refl |
hom_eq_cata_ty | proved | — | — |
decode_iff | proved | — | — |
ofSchema_exact | proved | — | — |
readTerm_printTerm | proved | — | — |
type_metadata_exact | proved | — | — |
errOf_valOfErr | proved | — | errOf_payload |
admitModule_classDecls | proved | — | checkInput_eq_none_iff |
errOf_ne_boom_of_supported | proved | — | hom_eq_cata_ty, errOf_payload, isPayload_of_hasTy_record |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
frame_laws | proved | — | — |
member | proved | — | — |
codec_roundtrip | proved | — | decode_encode, member, hom_eq_cata_ty, normalize_idem |
subN_trans | proved | — | — |
normalize_idem | proved | — | — |
subN_refl | proved | — | — |
handles_of_payloadFieldTy | proved | — | — |
decode_encode | proved | — | — |