Make the type checker forget

The last two articles kept moving type information inward. First I put invariants on links between values. Then I let an individual data structure mint types that belong only to itself. There is an obvious way to keep going: let the local scope become more sophisticated until it is almost a tiny language of its own.

That sounds like a recipe for a miserable type checker. Every arena creates its own generic family. Every buffer has offsets tied to its identity. Functions accumulate equalities and bounds. A parser knows dozens of relationships between cursor positions, lengths, slices, and results. If all of that enters one global type problem, the feature has failed before the syntax is finished.

I think the useful direction is the reverse. Make local types more expressive because the compiler promises to forget them. A function or data scope can have a fresh inference graph, a refinement context, generated type families, value identities, and ownership proofs. When the scope closes, the checker exports a small summary and throws the working state away.

I wanted to see whether this was remotely compatible with a real compiler, so I went through Blot. It turns out Blot is a particularly convenient victim because it already made the most important architectural decision: refinement is not algebraic subtyping.

Blot already has two worlds#

Blot's ordinary inference engine follows Lionel Parreaux's Simple-sub shape: inference variables collect lower and upper bounds, levels control generalization, and biunification propagates subtype constraints. The point of that engine is boring but valuable: compact principal types with a polynomial algorithm.

The checker spec then puts a second set of knowledge beside that lattice. Stripped down, its full judgment looks like this:

Γ ; K ; Φ ; R ; Ω ⊢ e : A ! E ; CΓ  ordinary inferred typesK  compile-time valuesΦ  integer relationshipsR  value identities and array lengthsΩ  ownership pathsC  erasable lowering certificates

Phi is relational knowledge. R records identities such as a particular array and its length. Omega is ownership. Certificates authorize later lowering decisions. The spec is explicit that none of these participates in subtype propagation.

That separation exists for a good reason. Blot's branch narrowing does not push an intersection or a complement into a type variable. It computes a ground result, shadows the name in a child environment, and keeps the Simple-sub graph untouched. If branch refinements were allowed to mutate shared upper bounds, facts from one branch could leak into another. If arbitrary logical intersections and complements became ordinary positive types, the nice algebraic solver would quietly become a much nastier problem.

The current refinement implementation is deliberately small too. Its propositions are affine integer facts: equality with an offset, lower and upper bounds, strict ordering, and difference bounds. They become difference constraints such as x - y <= k. Entailment is shortest-path closure. The code even says why it recomputes closure instead of building a grand incremental theorem prover: the expected contexts are small.

That line feels like the opening. Keep making the contexts small on purpose.

A function can be a solver island#

Today it is natural to picture inference as one graph that lexical environments point into. A child scope changes name lookup, but inference variables still belong to the larger solver. That is exactly what you want while two expressions are jointly constraining one unknown. It is less obviously what you want after a function has a closed principal type.

I would make a function body an actual checking boundary. Recursive functions are the exception: a mutually recursive strongly connected component has to be one island because its members genuinely constrain each other. Blot already discovers recursive SCCs for other compiler work, so this is not a new graph problem.

check_scope(imported_summaries, body):  types = fresh Simple-sub graph  facts = fresh refinement graph  relations = fresh value identities  ownership = fresh ownership state  infer body  prove local obligations  settle public boundary  emit Runtime HIR  return ScopeSummary {    scheme,    effects,    families,    refinements,    ownership,    hir,  }  // types, facts, relations: gone

The important word is closed. A summary cannot contain a pointer to a live inference variable, a branch-local value identity, or a random node in the refinement graph. If the boundary needs polymorphism, quantify it. If it intentionally exports a generated identity, name that identity in the summary. Everything else dies with the island.

struct ScopeSummary {    scheme: ClosedType,    effects: ClosedEffects,    families: Vec<FamilySummary>,    refinements: Vec<BoundaryFact>,    ownership: OwnershipSummary,    hir: RuntimeHir,    dependencies: SummaryFingerprint,}

Callers constrain against the summary rather than reaching into the callee's graph. This is less magical than it sounds. Module interfaces already work this way: Blot's incremental spec refuses to cache an interface containing live inference variables or unbound rigid identities. I am proposing the same hygiene one level lower.

Now local generics become cheap enough to be interesting#

The previous article gave an arena its own Id. Push that harder and the arena should be allowed to own a generic type constructor, not merely one zero-argument brand. An arena might have Id<Payload>, Cursor<Mode>, a state type, and relationships between all of them.

Blot already has a nice answer to higher-kinded abstraction: a type constructor is just a compile-time function. The inference lattice does not need kinds because the function is evaluated and specialized before runtime typing needs to represent it. I would preserve that rule completely.

// Proposed Blot, not current syntax.const Arena = fn Element =>  @type.scope (fn Scope =>    const Id = fn Payload =>      @type.family (Scope, "Id", Payload)    const Cursor = fn Payload =>      @type.family (Scope, "Cursor", Payload)    return {      .Id = Id;      .Cursor = Cursor;      .insert = fn value => ...;      .get = fn id => ...;    }  )

@type.scope creates one fresh compile-time identity. @type.family creates a nominal family under it. Id itself is an ordinary compile-time closure over Scope, which means it can be passed to another type-level function without inventing a new kind system.

// A local generic is still an ordinary comptime function.const PairOf = fn Family => fn A => {  .left = Family A;  .right = Family A;}let arena = Arena Strconst TwoIds = PairOf arena.Id Int// TwoIds is a pair of IDs from this arena only.// Another arena has a different Id family.

This is the part I find more interesting than simply having path-dependent aliases. A data structure can manufacture a family of types, hand that family to generic compile-time code, receive a transformed family back, and still keep the whole construction confined to one generated scope.

Two arenas may both expose a function printed as Id. Their identities still differ because the constructor's real key is something like (scope, family, arguments), not the display name. Equality is then an integer-identity comparison plus argument comparison, which fits Blot's flat-arena direction much better than growing strings such as "Arena<some huge path>::Id<Int>" through the solver.

The existing nominal type is almost, but not quite, this#

Blot already has @type.seal. The current primitive constructs a sealed value from a text name and a carrier, and the Rust type representation eventually has an Opaque(String) case. That is useful for a normal nominal type such as Centimeter. It is the wrong identity source for a type generated by the third arena created at runtime.

I would split human naming from semantic identity and make generated families first-class in the internal type graph:

// Today, simplified:enum Type {    Variable(VariableId),    Rigid(VariableId),    // ...    Opaque(String),}// One possible direction:enum TypeNode {    // ... existing structural cases ...    Family {        scope: ScopeId,        family: FamilyId,        arguments: Vec<TypeId>,    },    Package {        scopes: Vec<ScopeId>,        body: TypeId,    },}

Start invariant. Variance across a locally generated family can come later if a real program needs it. A zero-argument, module-stable family can implement today's sealed nominal types, so this can be an extension of the existing mechanism instead of a second nominal system.

A runtime-created scope needs a package, not a runtime tag#

Compile-time-generated families are the easy half. The previous article wanted each runtime arena instance to mint its own handle family. That means the function returning an arena is hiding a fresh type name from its caller.

// Source view:let arena = makeArena Strlet id = arena.insert "brook"// Checker view, approximately:arena : exists s. Arena<s, Str>// Opening the package gives this lexical scope a fresh rigid name s.// id : Id<s, Str>// The s is erased before runtime.

Type theory has a familiar name for that package. I would avoid making arbitrary existential syntax part of Blot's source language at first, though. @type.scope can produce an internal package, and ordinary binding can open it automatically as a fresh rigid identity for the lexical lifetime of the unpacked value.

Put ten arenas in an array and each element is packaged. Pull one out and the checker opens one fresh local rigid. Pass the arena and its IDs together and the rigid remains shared across the values. Let the package die and the identity dies too. None of this requires a scope tag in WebAssembly. The brand exists for checking and specialization, then erases.

There is one compiler capability Blot is already circling around that would make the surface pleasant. A compile-time function currently cannot simply inspect the inferred type of an arbitrary runtime argument;@type.of evaluates its operand, which is intentionally not runtime reflection. Blot's own design notes need a checker-only version of this capability for resolving interfaces attached to inferred types. The same narrow mechanism could project arena.Id from a scoped value without turning every runtime type into inspectable data.

// compiler/src/primitives.rs@type.scope  : (Scope -> A) -> packaged A@type.family : (Scope, Text, TypeArgs) -> Type// Checker-only projection. This does not make runtime types reflectable.@type.member : (scoped_value, Text) -> comptime TypeConstructor

Refinement should get stronger by staying local#

Once functions are islands, I would be much less nervous about giving their refinement context more work. Not arbitrary theorem proving—just more facts in the fragment Blot already handles well. A parser function can have thirty cursor and length relations internally if the caller only receives two of them.

fn split(bytes, n)  requires 0 <= n  ensures left.len + right.len == bytes.len  ensures left.len == min(n, bytes.len)  => (left, right)

inside split:  i = min(n, bytes.len)  0 <= i  i <= bytes.len  left.len = i  right.len = bytes.len - i  cursor = i  remaining = bytes.len - cursor  ... 27 more temporary facts ...outside split:  left.len + right.len = bytes.len  left.len = min(n, bytes.len)

Closing an island becomes a projection problem. Keep only propositions whose identities are visible at the boundary: parameters, returned values, public fields, and intentionally exported generated scopes. Eliminate local temporaries. If a public fact is implied by the local graph, serialize the compact fact. If it is not, it does not get to escape merely because the implementation happened to assume it.

This resembles the useful boundary in Benjamin Cosman and Ranjit Jhala's Local Refinement Typing: infer rich intermediate refinements locally and ask programmers for signatures mainly at exported or cyclic boundaries. Liquid Types similarly showed that a decidable predicate vocabulary can infer refinements precise enough for useful safety properties without making every term carry a hand-written proof. I would borrow the locality, not transplant an SMT architecture wholesale into Blot.

Blot's difference constraints have another nice property here: they summarize. If the local graph knows a - b <= 4, b - c <= 7, and a hundred unrelated facts, it can export the entailed boundary relation a - c <= 11 without exposing b at all. The closure algorithm is already doing the mathematical part.

Relationships become part of the summary, not the main type#

This is where the three articles finally line up. A generated family answers where a value belongs. A local relationship answers what is currently true about that value. The principal algebraic type answers how the value can be used structurally. Ownership answers whether it may be moved or changed.

I would keep those as separate coordinates rather than trying to make one heroic type expression contain everything. Blot's experimental owned-region work is already written this way: store provenance, ordinary path-sensitive ownership, region-family derivation, and the destructive HIR operation form a proof stack. Region authority deliberately stays out of algebraic subtyping.

A proof-producing data structure could therefore own a little bundle of local systems. An arena owns its Id<T> family. A partitionable buffer owns an interval relationship algebra. A transaction owns row-view families and a liveness relation. A parser state owns source-position families and cursor ordering. Generic functions over the structure import only the pieces they name.

This could also be a compiler optimization#

So far this is a language argument. Blot gives it a compiler-performance reason too. Its current design notes include a nine-sample profile of a list-heavy compile: 23.6 ms overall, with 6.60 ms in checking, 14.4 ms preparing Runtime HIR, and 0.293 ms actually emitting WebAssembly.

list-heavy compiler profile, 9 sampleschecking                 6.60 mspreparing Runtime HIR   14.40 msemitting WebAssembly     0.293 mstotal                    23.60 msfinal HIR: 63 operations

I would not claim solver islands automatically make the 6.60 ms smaller. They add boundaries, summary construction, and potentially repeated instantiation. A monolithic graph can be efficient precisely because it shares work. This needs a benchmark, not a slogan.

The incremental case is more concrete. Today Blot's cache rules are primarily module-shaped, with some reuse for an unchanged top-level declaration prefix. A closed function summary gives the compiler a finer semantic dependency. Change a body, recheck its island, and compare its summary fingerprint. If the public summary did not change, callers have no new typing fact to observe.

fn parseHeader(input) =>  // edit implementation here  ...// Old body hash:  91d8...// New body hash:  44a1...// Public summary: 7b0c...  <- unchanged// Recheck parseHeader.// Reuse callers that only depend on summary 7b0c...

Generative identities have to participate in that fingerprint. Blot's incremental spec already says a cache hit is unsound if a reachable generative identity changed. A locally generated family makes that rule more common, not different.

The larger opportunity is the 14.4 ms HIR preparation. Blot's own next-step note says to progressively emit settled Runtime HIR during checking and delete request-local fact-map reconstruction. A solver island gives a clean commit point: once its summary and proofs are closed, build its HIR while the useful local identities are still in hand, then discard them instead of reconstructing their meaning later.

The actual Blot patch I would try first#

I would not start by adding @type.scope. The compiler architecture should prove that the boundary is useful before the source language depends on it.

// compiler/src/typecheck.rsstruct ScopeChecker {    types: ConstraintTypeArena,    variables: Vec<Variable>,    refinements: RefinementContext,    relations: RelationArena,    ownership: OwnershipState,}fn close(self, boundary: Boundary) -> ScopeSummary {    // reject escaping inference variables    // quantify permitted generics    // preserve generated ScopeIds intentionally    // project Φ down to boundary-visible identities    // close ownership and effects    // commit HIR}

Give every non-recursive function a ScopeChecker. Give each recursive SCC one shared checker. Imports arrive as immutable closed summaries. Generalization and settling happen before close returns. Any inference variable that still points outward without an explicit quantifier is a compiler error, not something silently retained in a parent graph.

Then move the refinement context in with it. Blot's TypeScript authority already creates child refinement contexts for branch proofs; the experiment is to make a function own the root of that context and to add a boundary-projection pass. The Rust compiler should eventually carry the same compact representation so there is still one semantic compiler rather than a clever editor checker and a different production checker.

Next, teach compiler/src/session.rs to cache the closed summary by the function's lowered body, imported summaries, compile-time dependencies, and reachable generative identities. Teach compiler/src/hir.rs to accept a closed island directly. Only after measuring that pipeline would I introduce type families in compiler/src/value.rs, typecheck.rs, and primitives.rs.

There is a limit, and I would enforce it#

I would also keep Blot's current refusal to put arbitrary refinement logic into the Simple-sub lattice. Locality makes stronger proof systems more tolerable; it does not make them free. Difference constraints and ground set algebra should remain the fast editor path. A future stronger solver could be invoked inside an island that asks for it, produce a small checked certificate, and disappear again.

Local generics should stay staged and predicative too. Blot already has explicit @forall for Rank-N use and refuses impredicative inference. A generated arena.Id does not require reopening that problem. It is a compile-time function closing over a rigid scope identity, and applications specialize to ordinary closed types.

Finally, a summary must be intentionally lossy. If callers can ask arbitrary questions about a function's internal proof graph, the graph is part of the interface and the island never closed. The compiler should make you name the relationships you want to preserve.

The strange end point is a simpler global checker#

If this works, the language gets locally weirder while the whole-program type problem gets more boring. A structure can create generic types. A function can build a dense little refinement graph. A region can have its own proof algebra. A recursive group can infer against itself. None of those graphs is automatically a graph the rest of the program has to carry.

The switchboard image at the top is a decent model for it. The operator establishes the connection that matters now. The rest of the board does not become one cable. When a local call is done, most of the patch cords can come out; what survives is the route that somebody outside actually needs.

That is the version of advanced types I want to try in Blot: not a type checker that can remember everything, but one with much better places to forget.