nextgen-typing — The Hyperpolymath Type Theory Pipeline

Table of Contents

• What This Is
• The Main Chain
• Co-Products
• Research Section
• Key Architectural Decisions
• Calibration Calculi.

Tip	AI agents: read 0-AI-MANIFEST.a2ml first, then .machine_readable/6a2/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 code. It documents relationships between type-theoretic repos, tracks the pipeline roadmap, and hosts research artefacts that span multiple projects.

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.