nextgen-typing — Type Theory Pipeline

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> :toc: :icons: font

Tip	AI agents: read 0-AI-MANIFEST.a2ml first, then .machine_readable/descriptiles/STATE.a2ml.

What This Is

nextgen-typing is the coordination monorepo for the hyperpolymath type theory research and production pipeline. It does not contain compiler or application code; it documents and coordinates the pipeline, and hosts the cross-project formal-verification proofs in verification/proofs/. It documents relationships between type-theoretic repos, tracks the pipeline roadmap, and hosts research artefacts that span multiple projects.

Type Research: Connections and Meanings

The dashed arrows describe conceptual uses and research obligations. They do not certify package dependencies, integration, equivalence or proved transport. Residual Evidence Types is work in progress: its minimal Agda core now checks presence without value identification, plus narrow Echo and Epistemic interface comparisons. The guide links the exact proof receipts; the finite explorer and broader composition/revision programme remain separate obligations.

Family	The question it asks
Echo Types	Which possible origins remain compatible after information loss?
Epistemic Types	Who has access to a claim, with what evidence and soundness conditions?
Tropical Types	How do declared resource bounds compose?
Residual Evidence Types	Which explanations satisfy the observation and evidence, and what holds for all of them?
Choreographic Types	What is preserved when a global protocol is projected to its participants?

Read the shared glossary, connection obligations, ownership guide and first residual milestone. It distinguishes residual from residue, evidence from sound proof, and presence from value identification and causal role. These families answer complementary questions; they are not a ranking of type-system strength.

Naming note (2026-09-09): tropical-resource-typing now resolves on GitHub to tropical-types; the historical katagoria name below resolves to ideas-to-alphas. kategoria is a distinct language-development repository.

The Main Chain

katagoria  →  typell  →  typed-wasm  →  PanLL
 (research)   (kernel)   (target)    (eNSAID env)

Repo	Status	Role
katagoria	✅ Active	Research origination. Type theory prototypes, Idris2/Lean proof-of-concepts, and reading notes before promotion to production.
typell	✅ Active	TypeLL — open-ended progressive type verification kernel. Powers PanLL’s neurosymbolic intelligence. Port 7800.
typed-wasm	✅ Active	Dual role: (1) TypeLL type safety for WasmGC linear memory, and (2) aggregate library — shared binary conventions for AffineScript and Ephapax cross-language calls.
PanLL	✅ Active	eNSAID reference implementation. Downstream consumer of TypeLL. Binary Star: human (Panel-L) + machine (Panel-N) + world (Panel-W).

TypeFix Zero / TF0 sits beside this chain as a calibration calculus rather than a production stage. It is upstream of design judgement, not downstream infrastructure:

TypeFix Zero → Kategoria/Katagoria design tests → TypeLL partiality/totality boundary checks

It should not be placed between Kategoria/Katagoria and TypeLL as a required dependency. It is a small reference object used to test claims about universes, ordinary types, fixed points, and Turing completeness.

Co-Products

Repo	Relationship
affinescript (nextgen-languages/)	Compiles to typed WasmGC. Row polymorphism, algebraic effects, QTT surface syntax — all TypeLL-grounded.
ephapax (nextgen-languages/)	Compiles to typed WasmGC. Dyadic linear/affine type system.
protocol-squisher	Transport semilattice with max-composition is a tropical optimisation problem. Adapter path finding = Dijkstra over a max-plus semiring.

Research Section

Repo	What’s There
tropical-resource-typing	Isabelle/HOL: max-plus semiring, comm_semiring_1, dioid. Lean 4: speculative session types, soundness + QTT refinement. Research PDF. Proof document. Handover guide.

Key Architectural Decisions

• TypeLL is open-ended — not capped at any fixed number of levels.

• typed-wasm has dual role — TypeLL application AND aggregate library (ADR-004).

• Tropical grading separates billing from budget — spec_branch uses max not +. QTT overestimates wall-clock time; tropical grades give the tighter bound.

See docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and ROADMAP.adoc for full detail.

Calibration Calculi.

TypeFix Zero is a proposed standalone calibration calculus for the type-theory pipeline.

It is not a production language and not a replacement for TypeLL. Its role is to mark the lower bound of the estate’s “typed but Turing-complete” design space:

stratified universes / metasets: Type i : Type (i + 1) ordinary function types: A → B natural numbers as the minimal observable data type lambda abstraction and application one explicit fixed-point primitive: fix : (A → A) → A

The key distinction is that TF0 separates:

a total mathematical fragment suitable for proof-like reasoning an explicitly partial fragment introduced only through fix

This makes TF0 useful as a test object for TypeLL, Kategoria/Katagoria, and typed-Wasm discussions: it exposes exactly where Turing completeness enters and exactly where proof-theoretic totality stops.

Status: proposed standalone repository; design-stage.