Five approaches to building a language with every known level of type safety. A programming language development project.

Named after Aristotle’s Κατηγορίαι (Categories, ~350 BCE) — the first systematic attempt to classify the fundamental kinds of things that exist. He identified 10 categories. As of March 2026, type theory has independently arrived at 10 known levels of type safety. This is probably not a coincidence, and it is probably not the end.

Why This Exists

Type theory is one of the most practically important areas in computer science, and one of the least recognised.

Every time a compiler catches a bug before your code runs, that is type theory. Every time Rust prevents a use-after-free, or Haskell forces you to handle a missing value, or Idris proves your parser terminates — type theory is doing the work. It is the invisible engineering behind "it just works."

And yet:

• Most working programmers have never heard the term

• Most PL courses stop at generics (level 3 of 10)

• Most "type-safe" languages cover 3-4 levels at best

• The research that could eliminate entire categories of bugs sits in papers that practising developers will never read

This project exists to change that, one level at a time.

What this is

This is a programming language development project. We build compilers, type checkers, and tools. We use type theory the way a carpenter uses geometry — as a means to an end, not an end in itself.

We are language developers, not mathematicians. Where the mathematics is settled, we implement it. Where it is not, we document what we tried, what broke, and what we learned. If we get the maths wrong, we would rather be corrected than be silently wrong — that is literally the point of type safety.

What this is not

This is not an attempt to advance the state of mathematical type theory. People at CMU, Edinburgh, Gothenburg, Nottingham, and elsewhere have spent decades on that work and we stand on their shoulders gratefully. What we are doing is engineering: taking those ideas and finding out what happens when you try to put all of them into one language at once. Nobody has done that. We want to find out why.

The 10 Known Levels (as of March 2026)

Level	What It Catches	Example	First Appeared
1. Basic Types	Mixing incompatible primitives	1 + "hello" rejected at compile time	FORTRAN (1957)
2. Algebraic Data Types	Missing cases, impossible states	Option<T> forces you to handle None	ML (1973)
3. Parametric Polymorphism	Accidental type assumptions in generic code	fn id<T>(x: T) → T cannot inspect T	System F (1972)
4. Higher-Kinded Types	Incompatible abstractions	List and Option are both Functor — abstract over that	Haskell (1990)
5. GADTs	Ill-typed expressions in DSLs	Expr<Int> vs Expr<Bool> — the type system tracks your language’s types	GHC (~2005)
6. Dependent Types	Logical errors provable at compile time	Vec 3 Int — the length is in the type; head on empty is a type error	LF (1986), Coq, Agda, Idris
7. Linear / Affine Types	Resource leaks, double-free, use-after-close	File handle must be closed exactly once — compiler enforces it	Linear Logic (1987), Rust, Idris 2
8. Refinement Types	Violated preconditions	{x : Int `	x > 0}` — division by zero is a type error
9. Session Types	Protocol violations in communication	Send Int, then receive Bool, then close — out-of-order is a type error	Honda (1993), Scribble
10. Homotopy / Cubical Types	Unsound type equivalences	Bool ≃ Bool has exactly two valid equivalences — the type system knows	HoTT (2013), cubicaltt, Agda --cubical

No single production language covers all 10 today. Most cover 3-4. The best (Idris 2) covers 7. That gap is the challenge.

The Five Routes

We do not know which approach will work. So we try five, share what we learn between them, and document everything — including the failures.

Each route shares a common test suite (10 challenge programs, one per level) and interface type specification, so progress is directly comparable.

Route α (Alpha): Extend Idris 2

Start from the strongest existing foundation and push upward using elaborator reflection and compiler plugins.

• Levels 1-7: native in Idris 2

• Level 8: Refinement types via elaborator-generated dependent pairs

• Level 9: Session types via Brady’s published encoding

• Level 10: The wall — QTT and cubical type theory are different foundations

Key question: How far can you extend a language before you need to replace its core?

Route β (Beta): Dyadic Split

Two languages sharing syntax, parser, and module system that diverge at the type checker. Inspired by Ephapax’s region-linear fusion approach.

• β-1 (workhorse): QTT core (levels 1-7, plus 8 via elaborator)

• β-2 (prover): Cubical core (levels 8-10)

• Bridge: Shared ABI layer; proofs from β-2 compile to witnesses β-1 consumes

Key question: Can two type checkers share enough to feel like one language?

Route γ (Gamma): Aspect Injection

Keep a stable core language and weave type-checking aspects into the compilation pipeline at defined points. Each aspect is independent.

• Core: Dependent types + QTT (levels 1-7)

• Aspect 1: SMT-backed refinement checker (level 8)

• Aspect 2: Protocol verifier for session types (level 9)

• Aspect 3: Cubical checker for path equality (level 10)

Key question: Can independent type checkers compose when a single proof needs guarantees from multiple levels?

Route δ (Delta): Aggregate Bridge

Use existing best-in-class languages for each level range and bridge them through a shared ABI/FFI standard.

• Idris 2: levels 1-7

• F* or Liquid Haskell: level 8

• Scribble / multiparty session types: level 9

• Agda --cubical: level 10

Key question: Can type safety survive crossing a language boundary?

Route ε (Epsilon): Clean Slate

Design a new core calculus that unifies everything from the ground up.

• Drawing on Nuyts, Gratzer, Sterling on combining linearity with cubical

• No legacy constraints

• Highest risk, highest potential reward

Key question: Is there a consistent type theory that subsumes all 10 levels, or is the fragmentation fundamental?

How to Participate

1. Fork this repository

2. Pick a route (or propose a new one)

3. Work through the levels, documenting your decisions in docs/

4. Submit progress updates as PRs

5. Read other routes’ stumble journals — the failures teach more than the successes

There is no winner. The point is to map the territory.

If you are a type theorist

We need you. Not to do the engineering — we have that covered — but to tell us when we are wrong. If a route makes an unsound assumption, or misunderstands a theorem, or reinvents something that was solved in 1988, we want to know. Open an issue. The whole point of type safety is catching errors early, and that applies to our own work too.

If you are a language developer

This is your project. Each route is a self-contained language development effort with real compilers, real type checkers, and real design decisions. The challenge programs in shared/test-suite/ are concrete and testable. Pick a route and start building.

If you are just curious

Read the stumble journal. It is the most interesting part. Watching five different approaches hit five different walls teaches you more about type theory than any textbook.

Documentation

Document	Purpose
Design Decisions	ADR-style records for every fork in the road
Stumble Journal	What went wrong, why, and what we learned
Shine Journal	What worked unexpectedly well
Cross-Pollination	Discoveries from one route that helped another
Methodology	How we work — constraint-first development, LLM collaboration patterns

Methodology

This project uses Productive Meandering — a constraint-first development methodology for exploratory work where the destination is known but the path is not.

Every route is developed with LLM collaboration (primarily Claude), with full transparency about what the human decided, what the LLM suggested, and where they disagreed. We believe this transparency is more useful to the field than pretending either party did it alone. The docs/methodology/ directory contains field reports.

Progress

Route	L1	L2	L3	L4	L5	L6	L7	L8	L9	L10
α Extend	✓	✓	✓	✓	✓	✓	✓	✓	✓	✗
β Dyadic	.	.	.	.	.	.	.	.	.	.
γ Aspect	.	.	.	.	.	.	.	.	.	.
δ Aggregate	.	.	.	.	.	.	.	.	.	.
ε Clean	.	.	.	.	.	.	.	.	.	.

(✓ = passing, ~ = partial, . = not started, ✗ = proven impossible on this route)

Route α's row is enforced by CI: scripts/check-idris2-proofs.sh type-checks all 13 modules (verified under Idris 2 0.7.0 and 0.8.0) and rejects axiom smuggling. L8 and L9 pass via encodings (dependent pairs; Brady's indexed monad); L10 is route α's documented wall — see routes/alpha-extend/Level10_CubicalTypes.idr.

Route δ has a measurement bridge before it has an implementation: the typell verification kernel is a live aggregate-style engine mapped level-by-level in routes/delta-aggregate/TYPELL-BRIDGE.adoc.

Level 11 and Beyond

Important

State of the art as of March 2026. Type theory is not finished. The 10 levels above represent our best understanding of the distinct kinds of type safety that exist today. If you know of a level we have missed, or if one emerges after this date, please open an issue. We would rather discover we were wrong than remain confidently incomplete.

The following are active research areas that may constitute future levels. We track them so that routes can consider them early, and so that this project stays honest about what it does not yet know.

Candidate	What It Would Add	Key Researchers (as of 2026)	Maturity
Graded types	Semiring-indexed resource tracking (generalises linear)	Orchard, Liepelt, Wadler (Kent/Glasgow); Granule language	Working compiler
Effect types	Side effects tracked and controlled in the type system	Leijen (MSR, Koka); Lindley (Edinburgh, Frank); Pretnar (Ljubljana, Eff)	Production-ready (Koka)
Modal types	Necessity, possibility, temporality as type operators	Pfenning (CMU); Gratzer (Aarhus, MTT); Agda --guarded	30+ years of theory, limited implementations
Directed types	Types as categories, morphisms as programs	Riehl, Shulman (Johns Hopkins); North	Very early (2023 preprints, no implementation)
Capability types	Authority-based access control in the type system	Clebsch (Pony, now dormant); Aldrich (CMU, Wyvern)	Proven in Pony, language inactive
Observational equality	Alternative foundation for equality (not cubical)	Altenkirch (Nottingham); Pujet-Tabareau (consistent, 2022)	May replace Level 10 rather than extend it
Sized types	Termination guaranteed by structural size	Abel (Gothenburg); Agda team	Stable in Agda
Gradual types	Sound mixing of static and dynamic typing	Siek (Indiana); Greenman (Brown); Typed Racket	Mature theory, production use

If any of these crystallise into a distinct level during this project, we will extend the test suite and the progress matrix. The name Kategoria does not promise exactly 10 — it promises we will classify whatever we find.

TypeFix Zero / TF0 relation

TypeFix Zero is a proposed standalone calibration calculus for Kategoria/Katagoria.

Where Kategoria explores routes toward high-assurance type safety, TypeFix Zero intentionally does the opposite: it strips the design down to the smallest typed, Turing-complete core that remains mathematically honest.

TF0 contains:

universe/metaset stratification: Type i : Type (i + 1) function types natural numbers lambda abstraction and application one explicit fixed-point primitive

Its value to Kategoria is diagnostic. It provides a tiny object language for testing claims about:

universe hierarchies ordinary mathematical types the boundary between total and partial computation whether a proposed type-safety level depends on termination how much machinery is truly necessary before a language becomes Turing complete

TF0 should not be treated as a Kategoria implementation target. It is a baseline calculus used to compare, simplify, and falsify larger designs.

Acknowledgements

This project builds on decades of work by people who will never see this repository. The type theory that makes levels 1-10 possible was developed by Russell, Church, Curry, Howard, Martin-Löf, Girard, Wadler, Brady, Voevodsky, and hundreds of others. We are language developers applying their ideas. If we get something wrong, blame us, not them.

License

MPL-2.0 (Palimpsest License)

Author

Jonathan D.A. Jewell (hyperpolymath)