Let the data structure invent its own types

The last two articles kept moving type information closer to the data that gives it meaning. First came relationship types: instead of making a byte string globally become Bytes<n>, let a packet say that its length field and body happen to agree. Then Tether turned those relationships into named links that mutation could invalidate and repair locally.

There is still one global thing left in that design that bothers me: the types themselves. A program tends to declare NodeId, Offset, or Handle once, somewhere above the values that actually own those names. Then every instance of the data structure speaks the same type language.

I want to try the opposite. Treat a data structure as a scope. Let an individual arena, graph, buffer, or table invent types that only make sense inside that particular value, and let its relationships use those local types directly.

The arena should own the word Id#

An arena is the smallest example I know where the missing distinction is obvious. The ordinary version returns an integer-shaped handle. We can wrap that integer in a nominal Id, but two arenas of the same type still produce the same Id type.

type Id = Nattype Arena<T> = {  items: Vec<T>}fn insert<T>(arena: &mut Arena<T>, value: T) -> Id {  let id = arena.items.len  arena.items.push(value)  return id}fn get<T>(arena: &Arena<T>, id: Id) -> &T {  return &arena.items[id]}let left = Arena<String>::new()let right = Arena<String>::new()let zero = left.insert("zero")right.get(zero) // type-checks

The last line is not necessarily an out-of-bounds access. That almost makes the bug worse. Slot zero may exist in both arenas, so the program quietly reads a completely different object. The handle has enough type information to say "I am an arena ID" and not enough to say which arena made it.

A phantom type parameter can encode the missing owner if we already have a name for it. The awkward part is that the identity we want does not exist until the arena value exists. I do not want callers inventing a global UserArenaTag just so one runtime object can distinguish its handles from another runtime object.

So in this version of Tether, scope means the structure may declare types of its own. Every construction of Arena creates a fresh family of those types.

type Arena<T> = scope {  type Id = private Nat  items: Vec<T>  relation Live(id: Id) =    id.raw < items.len  fn insert(self: &mut Self, value: T)    -> id: self.Id    ensures self.Live(id)  fn get(self: &Self, id: self.Id) -> &T    requires self.Live(id)}

Id is backed by a natural number, but that representation is private to the scope. Outside the arena, the useful name is not merely Id. It is left.Id, right.Id, or whichever stable value produced it.

let left = Arena<String>::new()let right = Arena<String>::new()let zero = left.insert("zero")left.get(zero)   // okay: zero is left.Idright.get(zero)  // error: expected right.Id

error: handle belongs to a different scope  expected: right.Id     found: left.Id  zero was created by left.insert(...)

This is the first rule: two values constructed from the same data-structure declaration do not automatically share its inner nominal types. The declaration gives them the same shape of local type system, not the same type identities.

A local type is not a local proof#

The distinction gets more useful with a buffer. An offset should belong to one buffer forever, but being in bounds is a fact that can stop being true when the buffer changes. Those are different jobs, so I would give them different language constructs.

type Buffer = scope {  type Offset = private Nat  bytes: Bytes  relation InBounds(at: Offset) =    at.raw < bytes.len  relation Ordered(a: Offset, b: Offset) =    a.raw <= b.raw  fn offset(self: &Self, n: Nat)    -> Option<at: self.Offset>    ensures Some(at) => self.InBounds(at)  fn byte(self: &Self, at: self.Offset) -> Byte    requires self.InBounds(at)}

buffer.Offset says where the offset came from. It prevents using an offset minted by one buffer with another buffer. buffer.InBounds(at) says something more temporary: given the buffer's current byte length, this particular offset is safe to dereference.

That separation matters the first time the buffer shrinks. The offset does not magically become an offset into some other object. Its local type is still valid. The relationship that justified a read is what disappears.

let at = buffer.offset(20)?let before = buffer.byte(at) // okaybuffer.truncate(8)let after = buffer.byte(at)// error: buffer.InBounds(at) is no longer known

This plugs directly into Tether's existing write-footprint model. A call that may write buffer.bytes invalidates caller facts whose predicates mention that field. The checker does not need a registry of every offset ever minted. It only needs to forget the InBounds facts currently present in the local proof graph.

The scope should appear in function types#

Once a value can create types, ordinary function signatures need one small dependent feature. A later parameter has to be able to mention the scope introduced by an earlier parameter.

fn checksum(  buffer: &Buffer,  start: buffer.Offset,  end: buffer.Offset,) -> U32  requires {    buffer.InBounds(start)    buffer.InBounds(end)    buffer.Ordered(start, end)  }

This is intentionally narrower than "all values may appear in all types." The path buffer is a stable name for one scope during the call, and the other parameters can select types and relationships from it. That is enough to write most APIs I care about without turning Tether into a fully dependently typed language.

Scala already demonstrates how useful this shape can be. Its documentation on inner classes uses a graph whose nested Node type is path-dependent: a node from one graph instance is not simply a node from every graph instance. Scala 3 also has dependent function types where a result type can depend on a parameter value. Tether is borrowing that instinct rather than claiming that instance-dependent types are new.

Moving a scope is not creating one#

Path syntax creates an immediate practical question. If the type is called arena.Id, what happens when arena is moved into another variable? I would not make the source variable name the real identity. It is only how the programmer refers to an identity the compiler already tracks.

let arena = Arena<String>::new()let zero = arena.insert("zero")let moved = move arenamoved.get(zero) // okay: moving preserves the scope identitylet copy = moved.clone()copy.get(zero)  // error: copy generated a fresh Id type

Internally, imagine that construction creates an unforgeable name rho. Moving the arena carries rho with it. A shared reference points at the same rho. A clone creates a fresh name, say sigma, because the copied arena can diverge immediately afterward.

The clone rule is especially important for graphs and slot maps. If a copied graph silently accepted every handle from the original graph, the type system would be saying the two structures are one scope even while their contents evolve independently. A graph-specific fork operation can return a remapping from old handles to new handles when that conversion is genuinely useful.

Persistent immutable structures are the interesting countercase. Two versions may intentionally share one logical identity even though they are different values. I would leave that as an explicit library-level choice rather than pretending "one runtime object" is always the correct definition of a scope. The compiler needs a notion of generated identity; libraries still get to decide when identities are preserved.

Scopes nest naturally#

Once ordinary data structures are scopes, packaging dependent values stops needing a separate exotic box. An outer structure can contain an inner scope, then let later fields and relationships refer to types that inner value generated.

type SeededArena<T> = scope {  arena: Arena<T>  first: arena.Id  relation FirstIsLive =    arena.Live(first)}

first cannot accidentally refer to some arena outside the record because its type literally selects arena.Id from the sibling field in the same structure. The relationship then records that the handle is live in that arena's current state.

This also gives the language a boring answer to the old "how do I return the thing and a value whose type depends on the thing?" problem. Return a scoped record containing both. The outer structure is the stable name that keeps the dependency together.

Collections are harder but not mysterious. A Vec<Arena<T>> contains elements with different hidden scope identities. Pull one element out and the checker opens its identity as a fresh local abstract name for as long as that element is in scope. In type-theory terms there is an existential package hiding in the implementation. I would rather the compiler handle that packaging than make everyday arena users write existential syntax themselves.

The compiler model can stay small#

The surface feature sounds stranger than the lowering. A scoped structure can be translated into the sort of phantom brand people already encode by hand. Construction introduces a fresh type-level identity, and all local types receive that identity as a hidden parameter.

// source modelnew Arena<T>// checker modelexists scope rho. Arena<T, rho>arena.Id// becomesId<rho>arena.Live(id)// becomesLive<rho>(arena, id)

fn insert<T, rho>(  arena: &mut Arena<T, rho>,  value: T,) -> id: Id<rho>fn get<T, rho>(  arena: &Arena<T, rho>,  id: Id<rho>,) -> &T

At runtime, rho can usually disappear. The arena handle is still the same integer it would have been before. The new information exists for type checking, relation tracking, and diagnostics.

There is precedent for that branded implementation technique too. The GhostCell paper uses branded types to tie cells to a matching permission token, building the brand from phantom types and rank-2 polymorphism. It is a clever library encoding of a fresh identity that the Rust type system can track without runtime tagging.

OCaml attacks freshness from another angle in its module system. A generative functor produces type components that are different across separate applications. That is very close to the semantic move here; the proposed difference is mostly where I want programmers to encounter it. Applying a module constructor is a natural generative boundary in OCaml. I want constructing an ordinary data structure to be one too.

The type case is the structure#

I like this feature because it changes what a data declaration means without asking every type in the language to become more complicated. A normal record says, "these values travel together." A Tether scope says one extra thing: "inside this value, these are the names by which some values are allowed to relate."

An arena can own Id. A graph can own Node and Edge. A buffer can own Offset. A database transaction can own a Row view that cannot be confused with a row borrowed from another transaction. Those types do not need globally unique names because their owner already gives them one.

The relationships from the previous article then sit inside the same scope instead of floating beside it. The local type answers "which world does this value belong to?" The local relation answers "what is true in that world right now?" Mutation can preserve the first while invalidating the second.

The hero image for this article is a printer's type case, which is almost too literal. The case is the structure. The compartments tell you where each piece belongs. The pieces are only useful because the case gives them an arrangement. I think some program data wants the same privilege: not merely to contain values, but to define the little type vocabulary in which those values make sense.