unitype

An H3 for types. Every type gets one canonical form, a content address computed from its structure alone, and three words you can say out loud. Two systems that have never exchanged a schema can find out they hold the same type by comparing 32 bytes, and two people can by comparing a phrase. On top of the names, a function signature is a proposition and an implementation is a proof. One proposition can have many proofs, in Rust, Python, TypeScript or WebAssembly, and which one answers a call is a policy decision made when the call happens.

01 Identity from structure, not from a name 02 Two universes, one type, and nobody said so 03 Same proposition, same answer, another proof 04 The free theorem, checked from the signature 05 Across universes only by a link 06 One call, and every platform's name for it

Names from structure

Types, declarations, values and function bodies all serialize to plain JSON, so the representation, the wire format and the authoring format are the same thing. Normalization gives each type exactly one serialization: unions flatten and sort, and T?? collapses to T?. A blake3 hash of those bytes is the type's address, ut1:…. Names, prose and annotations are left out, because none of them is what makes a type what it is. Every List<i64> anywhere is provide-future-cave, with words drawn from the BIP-39 list the way intervalclock's aliases are.

Each declaration has three addresses:

• keyed, where field names count and their order doesn't, like a JSON object
• positional, where order counts and names don't, like a tuple or an argument list
• bag, where neither counts

geo::Point and gfx::Vec2 come out as the same three words because they hold the same data, and nobody told it that. Two declarations share a bag address exactly when some renaming and reordering turns one into the other.

Universes and links

Types live in universes, one per system or schema version, and inheritance inside a universe is nominal and checked. Between universes nothing is compatible by accident. Subtyping across them is always false, and data crosses only through an explicit link that says how, witnessed by a mapping anyone can read. Links can be derived from two declarations and composed along a path. An equivalence (the same data, renamed and reordered) loses nothing, so one link runs both ways.

Propositions and proofs

In the demo, sort : (xs: [i64]) -> [i64] has three proofs:

• a mergesort in native Rust, compiled into the command itself
• a bubble sort in Python, over a pipe
• the same Rust sort compiled to WebAssembly

Ask with --policy fastest and the Rust answers. Ask with min-memory and the Python answers, with the same result. Every answer is checked against the proposition at the boundary, so a proof that lies about what it proves is caught rather than trusted.

A WebAssembly proof gets memory, a budget and nothing else: no files, no sockets, no clock. Code you didn't write has somewhere to run where all it can do is answer.

A function can also skip proofs altogether. Written as a body in unitype's own total expression language, it needs nobody to prove it and runs in every target language once generated; demo::sorted checks that a list is in order that way.

Proofs checked against each other

sort and reverse have the same type, and only running both tells them apart. unitype conform runs every proof of a proposition against the others and exits 4 when they disagree. One example proves fetch_text(url) -> future<str> three ways: Python's urllib, Node's fetch and Rust's ureq. The case that earns its place is a page served as Latin-1. Node's shortest way to read text, response.text(), ignores the declared charset and returns caf�, and conform says so.

A generic proposition is checked from its signature alone. A proof of reverse<T> can't look inside a T, so every T it returns must be one it was given, and relabelling its inputs must commute with it. The harness checks that by passing tokens, with no expected answers written down anywhere, so a proof that quietly sorts when it sees integers is caught.

Code generation

Code generation targets TypeScript, Python and Rust. Each target is verified by running the generated code and comparing what it produces against what unitype says the value is. Generic declarations keep their type parameters and bounds, and a value takes the shape each language's own JSON gives it: a tuple is an array, a map is an object, and bytes are base64 text.

Stated honestly

More than 700 tests include property tests for the subtyping, inference and shape laws, plus golden vectors that pin the canonical form so it can't drift by accident. The WebAssembly sandbox sits behind a feature flag, because its engine is a large build for a capability not every workspace wants. types.cartercole.net is a static page that explains the idea. The names it shows were computed by the CLI, not in your browser.

About these pictures

figures/unitype.sh in this site's repository regenerates all six, and the tour, from the project as published. It builds the CLI from git archive of origin/main, never the working tree, so the hero is the real site from the repository's own site/ directory and the five terminals are transcripts of the README's own commands against examples/demo and examples/http. The WebAssembly proof is listed in them but not run, because that takes --features wasm, and conform says so. In the tour, the site is filmed a frame at a time on a stopped clock, the terminals are those transcripts typed back out, the generated code is what unitype gen wrote for the geo universe, and the count of passing tests is that commit's own cargo test. The voice is Orpheus, run locally.