anytype

Table of Contents

• 1. What this is
• 2. The one mechanism that matters: pluggable grades
• 3. What the kernel implements (and how far)
• 4. Quick start
• 5. Repository map
• 6. anytype vs the world
• 7. Relationship to systemet and AffineScript
• 8. RSR integration
• 9. Contributing
• 10. Licence

anytype is the reference kernel for systemet (Equality Theory): a small, parameterised type checker whose discipline you choose by choosing the algebra at the resource layer. The wager it implements is one sentence — do not add a new type relation when a layer discipline will do.

Important

Why "anytype" and not "EveryType". This kernel was first drafted under the name EveryType. That name over-claimed: it suggested a universal "every type" relation, which is exactly the System-Fc trap this design refuses. The honest claim is the opposite of universal coercion — pick any resource algebra you like, and the same kernel gives you that discipline. Hence anytype. (See AFFIRMATION.adoc for the no-overclaim posture.) Repository Role anytype (this repo) The kernel — the reference engine that implements Equality Theory. "Pick the algebra, get the discipline." systemet The theory — Equality Theory. Semantic authority: spec, invariants, proof obligations. AffineScript One opinionated product profile of this kernel (grade = affine + cost).

1. What this is

anytype is a kernel for building disciplined type systems by changing the algebra at the resource layer (L2), rather than by bolting on new type relations. It is the implementation side of the split:

• the theory — what the layers mean, which collapses are refused, and what must be proven — lives in systemet;

• the engine — the checker, the pluggable grade machinery, the runtime/ABI seam — lives here.

anytype pins systemet upstream and may extend, not redefine it. If implementation pressure ever demands a change to the theory, that is an ADR in systemet, not a quiet edit here.

2. The one mechanism that matters: pluggable grades

The whole point of the kernel is that a new discipline is a one-line change of the L2 grade algebra, checked by the same rules:

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

A candidate grade is admissible only if it satisfies the laws the checker requires (the relevant semiring/ordering operations). "Pick the algebra" is not "attach arbitrary metadata". The laws a grade must satisfy are systemet’s to define; the checking against them is anytype’s to perform.

3. What the kernel implements (and how far)

These are the layers of Equality Theory as the kernel sees them. For what each layer means, read systemet; this table is only the implementation status.

Layer	Kernel responsibility	Implementation status
L4 · effects ◇	Effect handlers; detect when a Total+Effect-graded+Affine (TEA) handler erases	not started — depends on systemet’s open TEA-erasure result
L3 · recursion ▶	Guarded recursion checking	not started
L2 · resources □	The graded-modal substrate + the pluggable grade-algebra interface	built (MVP) — Anytype.Grade.Algebra is an ordered-semiring record whose laws are proof fields; instances exist for affine {0,1,ω} (AffineScript’s discipline) and exact-usage ℕ. Same rules, distinct disciplines — demonstrated in the golden matrix.
L1 · equality	Equality as normalize + compare; the totality check that makes it decidable	built (MVP cut) — a bidirectional simply-graded λ-calculus whose type-index language has no recursion constructor, so type-level computation is total by construction (a syntactic gate, machine-checked via %default total, not a termination analysis). Conversion is normalise-and-compare at one site.
L0 · runtime	Lowering to a WASM/C target	not started

Warning

Honesty check. At this commit the kernel exists for the MVP cut only: a simply-graded λ-calculus (src/kernel/) with pluggable grade algebras, a process-boundary seam (anytype-check + the Zig anytype_check export), and real gates (just test, just proof-check-idris2, CI idris2-proof.yml). What it is not yet: no dependent types, no branching (if needs a grade join beyond the stated semiring+order laws), no L3 guarded recursion, no L0 lowering, no L4 effects (gated on systemet’s open TEA-erasure result), and the seam transport is a spawned process, not in-process linkage. Five RSR template modules under verification/proofs/idris2/ never compiled and are quarantined in scripts/check-idris2-proofs.sh rather than deleted. Do not cite anytype as a general-purpose type checker; cite it as a working demonstration that one set of rules yields distinct disciplines by choosing the algebra.

4. Quick start

# See the available repository tasks
just

# Validate the repository shape (this works today — it checks RSR structure)
just validate

# Build / test the kernel (placeholder targets until the kernel exists)
just test
just quality

5. Repository map

Path	What lives there
0-AI-MANIFEST.a2ml	Universal entry point for AI agents. Read this before making changes.
.machine_readable/	Project metadata, policies, contractiles, AI configs, 6A2 state, anchors.
src/	(Planned) anytype kernel implementation.
src/interface/	Typed ABI/FFI seam: Idris2 interface descriptions, Zig FFI, generated headers.
verification/	(Planned) proofs/tests that the kernel honours systemet’s obligations.
docs/	Status notes, decisions, diagrams, design records.
EXPLAINME.adoc	Engineering deep-dive: how README claims map to files, caveats, evidence.
AFFIRMATION.adoc	Dated honesty snapshot of what the kernel currently does and does not do.
AUDIT.adoc	Release audit gate.
Justfile	Task surface. Thin aliases delegate to the build/session machinery.

6. anytype vs the world

The interesting comparison is the theory — see systemet’s README for the full table. As an engine, anytype’s distinguishing bet is that the discipline is a parameter (the L2 grade algebra), not a fixed feature set:

	anytype	Haskell / System Fc	Rust
Discipline source	pluggable L2 grade algebra	fixed relation set (equality evidence, roles)	fixed (ownership, lifetimes, variance)
Coercions	none (equality is conversion)	yes	representation/lifetime-sensitive
Roles	tropes A@t (local finite machines)	global role system	lifetime / variance discipline

7. Relationship to systemet and AffineScript

• systemet is the theory anytype implements; it is the semantic authority. anytype must not silently diverge from it.

• AffineScript is one product profile of this kernel (grade = affine + cost), aimed at WASM contracts and edge functions. It is downstream of anytype.

8. RSR integration

This repository uses the Rhodium Standard Repository pattern: machine-readable metadata under .machine_readable/, the 0-AI-MANIFEST.a2ml agent entry point, just validate for repository shape, governance and release gates, and SPDX-based licensing. The RSR machinery is repository infrastructure — it is not part of the anytype kernel, and passing RSR validation proves nothing about the kernel’s correctness. See EXPLAINME.adoc#_rsr_integration.

9. Contributing

Most of the deep work is theory and proof and belongs in systemet. Engine-side contributions that belong here:

• the L2 grade-algebra interface and concrete grade instances (affine, cost, information-flow lattice, privacy budget) that satisfy systemet’s laws;

• the L1 conversion checker and its totality gate;

• the typed ABI/FFI seam (src/interface/).

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

10. Licence

Code, configuration, and scripts are licensed under the Mozilla Public License 2.0 (MPL-2.0); prose documentation under CC-BY-SA-4.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).