Types at the Implementation Boundary

Two answers to "is this type compatible with that one": compare the shapes, or compare the declared identities. The choice decides what a type name means, how cheap the check is, and whether a `UserId` can be handed to something expecting an `OrderId`.

A type system is sound relative to its formal model if every accepted program preserves the typing guarantees that model defines. That is a much narrower claim than "no bugs", and several widely used type systems break it on purpose.

Generic type arguments can be thrown away after checking, kept as runtime metadata, or compiled into separate specialised bodies. The choice decides what reflection can see, what casts cost, and which perfectly reasonable programs the language has to forbid.

One generic body becomes a separate compiled function per type it is used with. The type is then concrete, which is what makes inlining, known layouts and devirtualization possible — and the bill arrives as code size and compile time.

A type system can encode a resource protocol: who is responsible for a value, who may read it, who may write it, and when it must be released. The invariant that makes the proof work is aliasing XOR mutability — and it buys thread safety as a side effect.

To check a borrow, the compiler needs a region: the set of program points over which a reference must stay valid. Annotations exist because a signature is a contract and the checker will not look inside the caller — and non-lexical lifetimes were the change that made the rules match what programmers meant.

A type that says what a function does, not just what it returns. You already use several partial effect systems — checked exceptions, `async`, `const`, `unsafe` — and the complaints about function colouring are the honest cost of the idea.