Universes as Context

In earlier posts, we introduced the idea that rules depend on context: a general ownership rule may be refined by jurisdiction or restricted by organizational policy.

We treated context informally — as layers that add meaning.

Now we give it a precise structure.

The Problem with Informal Context

When context is informal, several questions remain difficult to answer:

• When can facts from one context be used in another?
• How do we know that a refinement is compatible with the general system?
• What happens when two contexts overlap or conflict?

As long as context is described only in natural language, these questions are resolved by convention — or not at all.

We need something more precise.

Introducing Universes

In Spine, a universe defines the context in which facts, rules, and effects are interpreted.

A universe is not a runtime container. It is a structural boundary that determines what is available, what is meaningful, and how elements relate.

The concept draws from universe polymorphism in dependent type theory — where types live at different levels, and the system tracks which level each element belongs to.

Spine extends this idea beyond types: universes organize not just types, but facts, rules, effects, and resources.

A Business Example

Let's make this concrete with our Asset System.

We define three universes, each building on the previous:

General

The base universe defines the core concepts: assets, agents, ownership, transfer. It expresses the abstract rules that any instance of this system must satisfy.

Here, the transfer rule is straightforward: ownership may change from one agent to another, with the usual constraints.

Jurisdiction

A jurisdiction universe refines the general system by adding legal structure.

In one jurisdiction, certain asset classes may not be transferable. In another, transfers above a threshold require regulatory approval. The jurisdiction does not replace the general rules — it narrows and extends them.

Organization

An organization universe adds further specificity: internal policies, approval workflows, delegation limits.

A company operating under a given jurisdiction inherits its constraints, and may add its own.

What Universes Provide

This structure gives us several things at once:

Scoping

Facts defined in one universe are only available where that universe is in scope. An organization-specific approval rule does not leak into the general system.

Refinement

A child universe may add rules, narrow constraints, or introduce new facts. It cannot weaken its parent — only strengthen it.

Compatibility

Because the relationship between universes is explicit, the system can check that refinements are compatible. An organization rule that contradicts its jurisdiction's requirements is a type error, not a runtime surprise.

A Geometric Example

The business example is intuitive, but universes are not limited to normative rules.

Consider a system that reasons about locations on Earth.

The base universe defines positions on a sphere — latitude, longitude, distances along great circles.

But real applications need projections: Mercator for navigation charts, local tangent planes for engineering, custom coordinate grids for specific regions.

Each projection is a universe. It inherits the concept of position from the base, but provides a different interpretation — a different way of computing distance, area, and direction.

A fact like "the distance between A and B is 500 meters" is meaningful only within the universe that defines how distance is measured.

Universes and Resources

In the previous post, we introduced resource tracking: the idea that some facts are consumed on use.

Universes interact with this naturally.

A linear ownership fact belongs to a particular universe. Transferring it to a different context is not free — it requires an explicit mapping between universes, which the type system checks.

For example: moving an asset from one jurisdiction to another may require demonstrating that the receiving jurisdiction accepts the transfer. This is not a runtime check — it is a type-level obligation, verified at compile time.

Universes and Effects

Effects are also universe-aware.

An effect valid in the general universe may not be sufficient in a jurisdiction that requires additional preconditions.

Conversely, an effect defined at the organization level may be unavailable outside that organization's context.

This means that the space of possible behaviors is not just constrained by rules and resources — it is also shaped by which universe the system is operating in.

Not Configuration, Not Modules

It may be tempting to think of universes as configuration files or module systems.

They are neither.

Configuration is external and unstructured. Modules organize code. Universes organize meaning — they determine what facts, rules, effects, and resources signify in a given context.

A module can be imported. A universe defines the conditions under which something is interpretable at all.

Universe Polymorphism

One of the most useful properties of this structure is polymorphism.

A function or rule can be written to work across any universe that provides the required structure.

For example: an audit rule that checks whether all transfers satisfy their preconditions can be defined once and applied in any jurisdiction — general, specific, or organization-level — as long as the required facts and constraints are present.

This is universe polymorphism: code that is generic over the context in which it operates, with the type system ensuring that the context provides everything needed.

A Subtle Shift

With universes in place, the system gains a new kind of structure.

We no longer describe one system. We describe a family of systems — related by refinement, parameterized by context, and connected through explicit universe relationships.

The same core model can be instantiated in different legal environments, different geometric interpretations, or different organizational settings — with the type system ensuring coherence at every level.

Looking Ahead

We now have the full set of ingredients: facts, rules, effects, invariants, time, space, uncertainty, processes, spatial structure, resources, and universes.

In the next post, we will turn from describing systems to verifying them — asking not just whether a system is well-structured, but whether it satisfies the properties we care about.

This will connect Spine to the world of formal verification: tools like Z3, TLA+, mCRL2, BigraphER, and PRISM, and how they fit into a language where correctness has been part of the design from the beginning.