A type-theoretic substrate is a semantic foundation for computing systems where types are not just annotations, but the core structural units of meaning and action. Instead of treating software as opaque applications, the system represents every capability as a typed term: something that declares what it is, what it accepts, and what it produces.

This gives:

• user inspectability: you can see what an agent thinks it is doing
• system predictability: agents can only compose workflows that type-check

This post sketches an early design for such a substrate, built as the semantic core of the Blue Note Computer project.

At the core, types are modeled as terms of a free algebra over a signature $\Sigma$.

Each type is either a constant (like $\mathrm{Unit}$ or $\mathrm{Int}$) or a constructor applied to child types (like $\mathrm{List}(\mathrm{Int})$ or $\mathrm{Function}(\mathrm{Int},\mathrm{String})$).

They are immutable, purely structural syntax trees. This means they can be:

• reasoned about structurally
• unified and substituted safely
• hashed and stored efficiently

Here’s how this algebra is implemented in types.py:

from dataclasses import dataclass, field

K_TYPE = "type"

@dataclass(frozen=True)
class Type:
    name: str
    params: tuple['Type', ...]
    metadata: dict = field(default_factory=dict)
    kind: str = K_TYPE

$\text{name} \to$ symbol in $\Sigma$

$\text{params} \to$ child terms

$\text{metadata} \to$ arbitrary annotations (not part of equality)

$\text{kind} \to$ implementation tag (also ignored in equality)

frozen=True $\to$ immutability, matching the free-algebra model

Equality is purely structural:

Metadata and kind are ignored. Hashing is computed from $(\text{name}, \text{params})$ only, so structurally equal types are guaranteed to hash the same.

Example:

Classic ADTs are encoded naturally in this system:

These follow standard cartesian closed category semantics: products, sums, and exponentials.

Effects can be modeled monadically:

There’s also a universal top type $\top$:

To support unification, we track free type variables:

This prevents infinite types when solving type equations.

The next step is to implement a full unification algorithm: solving $\tau_1 \stackrel{?}{=} \tau_2$ for the most general unifier (MGU) $\theta$.

This will power type inference and reasoning, letting the system plan and compose capabilities safely. Right now, the system already supports structural equality, hashing, and ADT construction.

This type algebra is the first building block of a new kind of computing system: one where types are the substrate of execution, not just annotations for compilers.

Even if I don’t build a full operating system, this core could be useful for:

• agentic planning and orchestration
• AI-native UI composition
• capability-based kernels
• safe modular tool systems

If this sort of thing interests you (Programming language theory or Human–Computer Interaction), I’d love to hear from you.