systemet

Table of Contents

• 1. The wager
• 2. The five layers
• 3. The three gates
  • 3.1. 1. The Totality Gate (L1)
  • 3.2. 2. The Structural Gate (L2)
  • 3.3. 3. The Polarity Gate
• 4. What the theory makes cheap
  • 4.1. Disciplines as a one-line change of algebra
  • 4.2. Roles become tropes
  • 4.3. Effects erase only when proven harmless
  • 4.4. Dependent types, rows, and refinements without new relations
• 5. systemet vs the world
• 6. Status — read this honestly
• 7. Contributing
• 8. Licence

systemet is a stratified type theory. The name is system + ET, where ET stands for Equality Theory — because the one primitive relation the whole system keeps at the bottom is equality, and everything else is layered above it as discipline rather than added as new relations.

Important

systemet is the theory, not an implementation. It defines the semantics, the invariants, and the proof obligations. The reference kernel that implements systemet is a separate repository, anytype. A downstream product profile of that kernel is AffineScript. Repository Role systemet (this repo) The theory — Equality Theory. Semantic authority: the spec, invariants, and proof obligations. anytype The kernel — the reference engine that implements this theory. "Pick the algebra, get the discipline." AffineScript One opinionated product profile built on the anytype kernel (grade = affine + cost).

1. The wager

Modern type systems usually grow by adding new relations on types: equality evidence, roles, variance, subtyping, gradual escape hatches, region constraints. Each new relation has to cohere with every other one. Two features do not create two obligations; they create a square of interactions. Three create a grid. Eventually the compiler is no longer checking programs — it is managing a treaty between equality, subtyping, variance, effects, resources, inference, and runtime casts. systemet calls that failure mode the Coherence Cliff, and the underlying shape the anti-stack:

features accrete sideways as new type relations instead of stacking vertically as disciplined layers.

The systemet wager is one sentence:

Do not add a new type relation when a layer discipline will do.

So systemet keeps exactly one primitive relation at the bottom — equality — and moves expressive pressure upward into layers, not sideways into new relations.

2. The five layers

systemet is stratified. Each layer is defined in terms of the one below it; the relation set never grows.

Layer	Meaning	Theory status
L4 · effects ◇	Effect handlers under an erasure discipline	OPEN — the target is to prove when a Total + Effect-graded + Affine (TEA) handler erases completely
L3 · recursion ▶	Guarded recursion	sketched — rules owed in docs/theory/06
L2 · resources □	Graded-modal substrate over a pluggable grade algebra (semiring)	specified — this is where the discipline lives
L1 · equality	The totality cut: equality is conversion	specified — no coercions, no roles, no representational-equality calculus
L0 · runtime	Lowering target (e.g. WASM/C)	specified

The defining move is L1. In System F_c a great deal of expressive pressure is pushed into equality, which becomes a proof-carrying subsystem. systemet cuts earlier:

System Fc:  equality becomes a proof-carrying subsystem.
systemet:   equality remains conversion; discipline moves into layers.

3. The three gates

systemet works by refusing three tempting collapses. Each gate is a boundary, not an omission.

3.1. 1. The Totality Gate (L1)

At L1, type-level functions must terminate. Therefore equality is decidable by:

normalize
compare
done

No coercion language. No roles. No representational-equality proof calculus. No "trust me, these two types are the same at runtime." If a type-level function does not terminate, it does not belong at L1.

3.2. 2. The Structural Gate (L2)

systemet admits shallow structural subtyping exactly where it is just projection — CAR/CDR-style access from an additive product &, covering width-like behaviour for rows, variants, refinements, and record-like products.

Shallow CAR/CDR projection is allowed.
Deep co/contravariant rewriting is not.

Deep variance pushes structure through function spaces, resources, effects, lifetimes, and linearity — which is exactly where coherence starts to leak. The gate allows the shallow case and refuses the deep one.

3.3. 3. The Polarity Gate

systemet admits polarized casts, not a universal gradual any:

A -> ?     forward, lossless, forgetful
? -| A     backward, lossy, blame-graded

The forward direction is ordinary forgetting. The backward direction is not treated as a magical runtime check: it carries a blame grade !_{blame} that is part of the resource story. There is no universal any that silently punches a hole through the type system — only directed loss, explicit polarity, and graded blame.

4. What the theory makes cheap

4.1. Disciplines as a one-line change of algebra

Because the discipline lives at L2 over a pluggable grade algebra, a new discipline is a change of algebra, not a change of checker:

grade = Affine
grade = Cost * Nat
grade = Low <= High        (an information-flow lattice)
grade = [0,1]              (a probability-like grade)
grade = PrivacyBudget
grade = Latency x Billing

Same rules. Different algebra. Different discipline. A proposed grade is only admissible if it satisfies the laws the theory requires (the relevant operations and ordering) — "pick the algebra" is not "attach arbitrary metadata".

4.2. Roles become tropes

System F_c asks whether two types are representationally equal under a global role discipline. systemet avoids that question. Instead of a global coerce, it uses local, finite, model-checkable state transitions:

A@t1 -> A@t2 -> A@t3

A trope is a finite transition machine. The burden moves from global representational equality to explicit, local state movement: no coerce, no role inference, no hidden representational treaty. Each real API (file handles, sockets, transactions, streams, capabilities) gets a finite machine and a preservation obligation.

4.3. Effects erase only when proven harmless

A handler that is Total, Effect-graded, and Affine is a TEA handler. The L4 goal is to prove when such a handler erases completely. This is not "effects are free"; it is:

effects erase only when the layer discipline proves them observationally harmless.

4.4. Dependent types, rows, and refinements without new relations

They do not need new primitive relations. They live at L2 as structured uses of the graded substrate — which is the whole wager restated.

5. systemet vs the world

	systemet	Haskell / System Fc	Idris2	Rust
L1 equality	conversion	coercion proofs / equality evidence	conversion	trait & region solving
Coercions	none	yes	mostly none at the core	lifetime/representation-sensitive
L2 resources	pluggable semiring	limited / plugin-dependent	quantity discipline 0,1,ω	affine ownership
Roles	tropes A@t	global role system	none	lifetime / variance discipline
Deep variance	refused	controlled, external to this wager	limited	yes
Effects erase	TEA-purity target (open)	no general erasure theorem	no general erasure theorem	no general erasure theorem

6. Status — read this honestly

systemet is, at this commit, a theory written down with its tractable core machine-checked — not a proven theory.

• The semantics, the layering, the three gates, and the wager are specified in this repository — prose orientation in this README and EXPLAINME.adoc, formal specification per layer/gate in docs/theory/, with every proof obligation numbered in the citable ledger docs/theory/OBLIGATIONS.adoc (ET-1..ET-15). L3 guarded recursion is sketched, not fully specified — see docs/theory/06.

• The mechanized core (Lean 4, hermetic, no mathlib, gated in CI): the L2 grade-algebra law set (ET-4) with four instances + the product construction (ET-5) is proven; L1 hereditary substitution and the normalizer are total by construction (ET-1, core calculus) with stability nf_emb proven. ET-2’s soundness/completeness/decDefEq are open (statements recorded, never stubbed). Every gated theorem passes an axiom audit (nothing outside Lean’s three-axiom trusted base); docs/status/PROOF-STATUS.adoc is the dated evidence table, and CI fails if it drifts from the proof MANIFEST.

• L4 TEA-erasure is an open problem, not a result. Do not cite it as proven.

• There is no compiler here. The reference kernel is anytype, and it is itself at an early stage.

For the dated, signed honesty snapshot see AFFIRMATION; for the claim-to-artefact mapping see EXPLAINME; for the release gate see AUDIT.

7. Contributing

The useful contributions are theory and proof, not syntax:

• new L2 grade algebras (security lattices, differential-privacy budgets, latency/cost models, information-flow grades) with their laws;

• proofs — TEA erasure, trope preservation, shallow-structural soundness, the interaction of guarded recursion with grades;

• finite trope machines for real APIs (file handles, sockets, database transactions, web streams, WASM capabilities).

Open issues with one of: [ET-L2], [ET-L3], [ET-L4], [TROPE], [TEA].

8. Licence

Prose documentation is licensed CC-BY-SA-4.0; any code, configuration, and scripts are MPL-2.0. Per-file SPDX-License-Identifier headers are authoritative. The GitHub-detected licence is MPL-2.0 via the root LICENSE. Long-term attribution uses Quantum-Safe Provenance (PMPL Exhibit B where present).