Lattice Algebra in KindScript

·2 min read
#programming#type-theory#visualization

This post demonstrates the new interactive learning features on this site. Below are embedded flashcards, interactive diagrams, and a downloadable Anki deck.

The Containment Lattice

KindScript's CodeLoc type forms a three-level containment hierarchy. This visualization shows how directories contain files, which contain declarations.

DIRECTORYFILEDECLARATIONdir: /src/domainfile: /src/domain/order.ts...file: /src/domain/event.tsdecl: order.ts#Orderdecl: order.ts#LineItemdecl: event.ts#Eventdecl: event.ts#Emitsubsumes(dir, file) = true    subsumes(file, decl) = true    subsumes(dir, decl) = true
Directory (coarsest)
File
Declaration (finest)

Every line in the diagram represents the subsumes relation — the upper element contains the lower element.

The Powerset Lattice

Oxide (the Rust formalization) uses a classic powerset lattice structure. Regions are elements of P(Loans), ordered by subset inclusion.

{a, b, c}{a, b}{a, c}{b, c}{a}{b}{c}∅← top (everything)← 2-element subsets← singletons← bottom (nothing)meet({a,b}, {b,c}) = {a,b} ∩ {b,c} = {b}join({a}, {c}) = {a} ∪ {c} = {a,c}

Oxide's region algebra is this structure: P(Loans) ordered by ⊆. Meet = ∩, Join = ∪. A complete Boolean algebra.

This is a complete Boolean algebra — the strongest kind of lattice. It has complements, distributes over arbitrary unions and meets, and every subset has a join and meet.

Set Operations

The carrier algebra resolves to sets of code locations. Three core operations compose these sets:

Union

unionLocs

Set A
file/src/domain/order.ts
file/src/domain/event.ts
union
Set B
dir/src/domain
=
Result
dir/src/domain
removedorder.ts
removedevent.ts

The directory subsumes both files after merge, so canonicalization removes them.

Union merges two sets and canonicalizes the result — removing locations that are subsumed by coarser locations already in the set.

Intersection

intersectLocs

Set A
dir/src/domain
intersect
Set B
decldomain/order.ts#Order
file/src/infra/db.ts
=
Result
decldomain/order.ts#Order
removed/src/infra/db.ts

meet(dir, decl) = decl (dir contains it) — meet(dir, infra/db.ts) = null (different tree)

Intersection computes the pairwise lattice meet of elements from both sets, keeping only non-null results.

Exclusion

excludeLocs

Set A
file/src/a.ts
file/src/b.ts
file/src/c.ts
exclude
Set B
file/src/b.ts
=
Result
file/src/a.ts
file/src/c.ts
removed/src/b.ts

Each base location is checked: is it subsumed by any excluded location? If yes, it's dropped.

Exclusion removes elements from the base set that are subsumed by any element in the excluded set.

Key Insight: Form Independence

The checker operates on these resolved location sets uniformly — it never inspects the CarrierExpr that produced them. This is form independence: architectural properties don't depend on whether code is organized by folders, annotations, globs, or packages.

In Oxide (Rust's formalization), the same principle holds: the borrow checker validates ownership invariants against concrete loan sets, not against how those regions were inferred. Safety is a property of the resolved set, not of the expression that computed it.

Want to Review These Later?

You can download all the flashcards from this post as an Anki deck, or use the built-in spaced repetition system at /learn.

Flashcards Available

This post includes 5 flashcards for spaced repetition. Download the deck to import into Anki.

Download Anki Deck
How to import into Anki
  1. Download the .txt file above
  2. Open Anki and click Import
  3. Select the downloaded file
  4. Choose Basic card type
  5. Ensure fields map to Front and Back
  6. Click Import