The type between the fields

A packet arrives with a length field and some bytes. The first type you write is almost embarrassingly ordinary:

type Packet = {  length: U16  body: Bytes}

Everybody reading it can see the missing fact. length is supposed to agree with body.length, but the record says nothing about that agreement. So the dependently typed instinct is to move the length into the type of the body. Idris uses exactly this shape for its standard Vect n a example: n is an index, and the vector carries its length in its type.

That is a good representation when length is part of what a vector is. I am less convinced it should be the automatic answer whenever one value happens to constrain another. A packet body is still bytes when nobody cares about the header. The interesting fact appears only after those bytes are placed next to a declared length.

The index escapes the record#

Give the packet a type-level length and the missing invariant becomes explicit:

type Packet<n: Nat> = {  length: Nat<n>  body: Vector<n, Byte>}fn decode(input: Bytes) -> exists n. Packet<n>

Now body cannot have the wrong length. But n has become part of the packet's identity, so code that does not care about it still has to quantify over it, infer it, hide it, or carry an existential package around. Idris has dependent pairs for exactly the case where an index is only discovered at runtime: a value like (n ** Vect n Int) packages the number with the vector whose type mentions it.

None of that is a flaw in dependent types. It is the correct cost when callers need the index. The cost feels odd when the program only wanted to remember that two fields agree. Decode a packet, put it in a queue, log it, encrypt its body byte-for-byte, then send it elsewhere; most of those operations have no use for a type parameter naming the payload length.

The invariant belongs to the pair. That suggests a different place to put the type information: on the edge between the values that participate in it.

Put a type on the edge#

Imagine that a record can contain a named relationship alongside its fields. The fields keep their ordinary types, while the relationship names a proposition over them:

relationship LengthMatches(  declared: Nat,  actual: Nat,) = declared == actualtype Packet = {  length: U16  body: Bytes  relationship lengthMatches:    LengthMatches(length, body.length)}

LengthMatches is a type whose inhabitants witness equality between the declared length and the length computed from the byte string. The compiler can erase that witness after checking it, just as many proof terms disappear in dependently typed programs. What changes is the surface area: the relation lives inside Packet, and Bytes does not acquire an index merely because one record wants to compare its length with something else.

This is close to refinement typing. Jhala and Vazou describe refinement types as ordinary types narrowed by logical predicates, and dependent refinements have been used to express relationships such as vector bounds. A sufficiently expressive refinement system could encode the packet above today. I am not claiming new type theory here. The design question is whether the relationship deserves its own named slot in the data model rather than being smuggled into one endpoint's top-level type.

That distinction starts to matter once a record has several invariants. An image might relate width, height, pixel format, and byte count. A slice relates two offsets to each other and then relates the upper offset to a source buffer. Encoding every one of those facts as another index on the container can turn a fairly boring runtime object into a long type-level parameter list.

type Image = {  width: Nat  height: Nat  pixels: Bytes  relationship packed:    pixels.length == width * height * 4}type Slice = {  start: Nat  end: Nat  source: Bytes  relationship ordered: start <= end  relationship inBounds: end <= source.length}

Check once at the boundary#

A relationship type cannot make untrusted bytes truthful. The parser still has to establish the fact when data crosses into the typed world. That can be a runtime check, a consequence of an operation the checker already understands, or an explicit proof for a harder predicate.

fn decode(input: Bytes) -> Result<Packet, DecodeError> {  let length = input.readU16()  let body = input.readBytes(length)  prove LengthMatches(length, body.length)  return Packet { length, body }}

In this example, readBytes(length) already promises to return exactly that many bytes or fail, so the proof may be discharged without generating another comparison. A parser that reads an independently delimited body would perform the equality check there instead. Either way, callers receive an ordinary Packet after the boundary rather than an unchecked pair of values that must be compared again at every use.

Mutation makes the model more interesting. Write a new body and the old relationship witness is invalid, because it mentioned the previous body. The language can respond the same way a borrow checker responds when an alias stops being usable: make the record temporarily incomplete until the relationship is re-established, or require an update that preserves all affected relationships.

fn truncate(packet: Packet, n: Nat) -> Packet {  let body = packet.body.take(n)  return Packet {    length: body.length,    body,  }}

I have not worked out which mutation rule would feel best in a real language. Requiring every intermediate expression to satisfy every record invariant may be too strict for ordinary construction, while letting a broken relationship float arbitrarily far would defeat the point. A small scoped builder, where relationships must hold again when the value leaves the scope, seems plausible but needs actual use before I would trust it.

Some properties really are intrinsic#

This idea does not replace indexed types. If an algorithm's behavior genuinely depends on vector length, then Vector<n, A> gives the function exactly the handle it needs. Matrix multiplication is the obvious case: the dimensions participate in the operation's type, so hiding them inside a record relation would make the API worse.

Relationship types fit the other class of invariant, where ordinary values become constrained because a particular structure puts them together. File offsets, protocol headers, cached counts, AST source spans, image dimensions, and foreign-memory views are full of these local agreements. The values remain useful on their own; the structure is what gives the agreement meaning.

The packet is still the example I keep coming back to because the runtime object never needed to become exotic. It has a number and a byte string. The extra thing is one erased piece of evidence connecting them, sitting in the record exactly where the two values first became each other's problem.