UNITYPE

01NAMES

Identity from structure, not from a name anyone chose.

H3 gives every hexagon on Earth a canonical ID that anyone can compute without asking anyone. unitype does it for types. Normalization gives each semantic type exactly one serialization, and a blake3 hash over those bytes is its identity — excluding names, prose and annotations, because none of those are what makes a type what it is.

So two systems that have never exchanged a schema can find out they hold the same type by comparing 32 bytes, and two people can find out by comparing a phrase.

$ unitype --project examples/demo ls types
demo::Circle    struct     wet-either-model
demo::Rect      struct     code-twice-wheat
demo::Shape     struct     escape-until-deposit
geo::Point     struct     proof-mystery-trouble
geo::Place      struct     zoo-page-aware
gfx::Marker     struct     run-spawn-replace
gfx::Vec2      struct     proof-mystery-trouble

geo::Point and gfx::Vec2 get the same three words because they hold the same data — which nobody told it. Types live in universes, and between universes nothing is compatible by accident: data crosses only through an explicit link that carries a witness anyone can read.

02PROPOSITIONS & PROOFS

Which implementation runs is a policy decision, not an architectural one.

A function signature is a proposition. An implementation of it is a proof. There can be many proofs of one proposition — compiled or interpreted, native or sandboxed — each declaring its own time and space cost. Both are checked against the signature at the boundary, so a proof that lies about what it proves is caught rather than trusted.

$ unitype run demo::sort \
    --args '[[5,3,9,1]]' --policy fastest -v
candidates:
  sort.rust_merge  here     O(n log n) / O(n)
  sort.sandboxed   sandbox  O(n log n) / O(n)
  sort.py_bubble   python   O(n^2)     / O(1)
chose sort.rust_merge in here

[1,3,5,9]

$ unitype run demo::sort \
    --args '[[5,3,9,1]]' --policy min-memory -v
candidates:
  sort.py_bubble   python   O(n^2)     / O(1)
  sort.rust_merge  here     O(n log n) / O(n)
  sort.sandboxed   sandbox  O(n log n) / O(n)
chose sort.py_bubble in python

[1,3,5,9]

Same proposition, same answer. One ran in-process in Rust; the other ran in Python over a pipe.

$ unitype conform
demo::sort  3 proofs, 7 cases  — all agree
  not checked here: sort.sandboxed
demo::reverse<T>  2 proofs, 5 trials  — free theorem holds

A generic proposition is a claim about every type. A proof of reverse<T> cannot look at a T, so every T it returns must be one it was given — and conform checks that from the signature alone, with nobody writing down an expected answer. A proof that sorts when it sees integers is caught.

03INSTRUMENTS

The loop closes: a type can be described, checked, addressed, named, bridged, generated and computed — in more than one language. 735 tests, including the subtyping, inference and shape laws as property tests.

04TRY IT

Rust 1.85 or newer.

$ cargo install unitype-cli
$ git clone https://github.com/CarterCole/unitype
$ cd unitype

# three universes, eleven types, nine proofs in three environments
$ unitype --project examples/demo check

# what every platform calls an HTTP request
$ unitype --project examples/http words http::request

http::request(req: http::Request) -> future<http::Response>

  address   ut1:cd212e2df458227e6cc86b268247421129122977094fe54b560f7a24a0d3a9f6
  words     essay-border-siren

  Called:
    python      requests.request          in python
    rust        reqwest::Client::execute  in rust
    sh          curl                      in shell
    typescript  fetch                     in browser
    typescript  fetch                     in node

curl is a program, fetch is a global, requests is a package you install — three different kinds of thing. Underneath they answer the same proposition, and essay-border-siren is what that proposition is called when you have to say it to a person.

05COMMITMENTS

The specification is normative, so this is implementable in any language. The Rust workspace is the reference, not the definition.

1. Names are not identity.Two structs called User in different universes are unrelated until someone links them; two identically-shaped types with different names have the same address.
2. Nothing crosses a universe boundary by accident.Subtyping stops at the boundary. Links are the explicit permission, and always carry a witness.
3. Costs are declared, not measured.An implementation states its complexity and the dispatcher believes it; a differential harness checks that all proofs actually agree.
4. A proof that lies is caught.Arguments and results are checked against the signature at the dispatch boundary, so a wrong shape fails loudly instead of propagating.
5. Word aliases are for people.Derived, stable, and lengthening on collision like an abbreviated git hash — but ut1: addresses remain the authority.
6. A type is an ordinary thing to compute with.A declaration is a value that validates, addresses and travels like any other, and a test keeps that description from drifting.

06UPLINK