The facts live beside the values

I keep moving the same invariant around. First it lived in a vector index. Then it moved onto the relationship between two fields. Tether made that relationship a named link the compiler could invalidate, and the next version let individual data structures mint types of their own. Each step made the fact more local, which left me wondering why the fact had to live inside the data structure at all.

A packet can have a length field and a byte string before anyone has checked that they agree. Logging that packet is fine. Printing it is fine. The agreement matters at a few specific operations, such as sending it on a wire that trusts the header. Encoding “valid packet” as a permanent top-level type makes every operation participate in a distinction many of them do not care about.

So here is another language sketch. Call it Rel; the name is dull on purpose. Values have ordinary types. The type checker also carries a changing set of facts about relationships between the values currently in scope.

A fact does not have to be a field#

The packet type in Rel is boring. The relationship gets a name, but declaring the relationship does not make every Packet satisfy it.

type Packet = {  length: Nat  body: Bytes}fact Sized(p: Packet) =  p.length == p.body.len

Sized is a proposition the checker understands. It is not stored in the record and it is not a hidden type parameter. A raw parser can produce a Packet without proving anything. A checked parser can publish the extra fact in its function contract.

fn readExact(input: Cursor, n: Nat)  -> bytes: Bytes  gives bytes.len == nfn decode(input: Cursor) -> p: Packet  gives Sized(p){  let length = input.readU16().toNat()  let body = readExact(input, length)  return Packet { length, body }}

The postcondition on readExact gives the checker body.len == length. That is enough to establish Sized(p) when the packet is returned. There is no proof term in the runtime object; the caller receives one value and one piece of compile-time knowledge about it.

Callers then say whether they care about that knowledge. An inspector accepts any packet. The sender asks for the relationship because it is about to serialize the header and body as one message.

fn inspect(p: Packet) {  print(p.length, p.body)}fn send(p: Packet)  needs Sized(p){  socket.writeU16(p.length)  socket.write(p.body)}let packet = decode(input)inspect(packet)  // only needs Packetsend(packet)     // Sized(packet) is known here

I like this more than inventing UncheckedPacket and CheckedPacket for every stage. The value did not change after decode. What changed was what the scope knew about it.

Facts have a lifetime#

This becomes useful once the value changes. Rel treats assignments as new value identities under the hood. A write throws away facts that mention the old value unless the checker can derive an equivalent fact for the new one.

var packet = decode(input)packet.body = packet.body.take(8)send(packet)// error: missing fact Sized(packet)packet.length = packet.body.lensend(packet) // okay

After the body is truncated, the old equality is gone. The packet still has type Packet, so code that only inspects it keeps working. send is the place that complains. Updating the length gives the checker enough information to recover the equality.

error: send needs Sized(packet)  required:    packet.length == packet.body.len  this fact was known after decode(input)  and forgotten when packet.body changed

Branches work the same way. A successful comparison adds a fact to the branch where it holds, and leaving that branch drops the fact again.

fn sendIfValid(packet: Packet) {  if packet.length == packet.body.len {    send(packet)  }  // Sized(packet) is no longer assumed here.}

This is close to the direction in Numbers are sets, where a branch narrows the possible values of a number. Rel keeps that temporary knowledge in a separate fact context instead of trying to turn every useful branch condition into a larger algebraic type.

Function types can move relationships too#

Relationships get more interesting when the values are not fields of the same record. Splitting a byte string creates two new values and several useful facts connecting them to the input.

fn split(bytes: Bytes, n: Nat)  -> (left: Bytes, right: Bytes)  gives {    left.len + right.len == bytes.len    left.len == min(n, bytes.len)  }

Neither result needs to become Bytes<n>. The caller gets ordinary byte strings plus whatever relationships the function promised. Keep both values and the facts remain available. Drop one value and facts that mention it can disappear with it.

At any line the checker is carrying two fairly different things. One is the familiar map from names to ordinary types. The other is a small graph of facts over the current value identities.

values  packet : Packet  left   : Bytes  right  : Bytesfacts  Sized(packet)  left.len + right.len == packet.body.len  left.len <= 8

Function calls check their needs facts and add their gives facts. Comparisons add facts to the successful path. Mutation invalidates facts incident to the changed value. Scope exit removes the rest. That is most of the language feature.

When a program really needs to store a proof, Rel can reify one explicitly. That is the move from A value can carry proof, kept as an escape hatch instead of the default representation for every checked relationship.

let proof = witness Sized(packet)// proof is an ordinary value now.// Most code never needs to do this.

The compiler should forget almost all of this#

A function body might accumulate dozens of equalities while parsing a header or walking a buffer. Most of them are implementation debris. Rel should export only the facts written in the public needs and gives clauses, then throw the local graph away when the function closes.

That follows the argument in Make the type checker forget: richer local reasoning is easier to tolerate when the compiler promises not to turn every temporary inference into global state. It also fits The proof budget. Equality, ordering, bounds, and linear arithmetic cover a lot of useful relationships without asking an editor to become an interactive theorem prover.

The part I have not settled is higher-order code. A generic function that never looks inside a packet should probably preserve facts about that packet automatically, even when it accepts callbacks. There is a sensible frame rule hiding in there, but I do not yet know what its surface syntax should be. I would rather leave that hole visible than invent three keywords and pretend the problem went away.

At runtime, a packet in Rel is still a number beside some bytes. In the editor, send(packet) is accepted after decode, rejected after the body changes, and accepted again once the length agrees. The extra thing lives only in the checker, for exactly as long as the program has reason to know it.