Spine Type System

Data is inert; context is sovereign.

Spine is a design discipline for organizing types in any sufficiently expressive typed language (Lean, Haskell, Rust, TypeScript, Java, F#, and others). It is not a programming language, runtime, or compiler plugin. The value of Spine is not custom machinery — every mechanism it relies on (newtypes, coercions, typeclasses, records) already exists in modern languages. The value is the rules for when and how to use that machinery so that types carry domain meaning, not just memory layout.

Most type systems enforce structural correctness: this function expects an int, you gave it a string. Spine enforces semantic correctness: this function expects a temperature, you gave it a distance — even though both are float64 underneath.

Why Spine Exists

The problem with raw primitives

When float64 means everything — temperature, distance, price, user score — the compiler cannot catch category errors. celsius + meters compiles in most languages. The bug surfaces at runtime, in a test, or in production.

The problem with ad-hoc wrappers

Wrapping primitives in domain types (newtype Celsius = Celsius Float) is a well-known pattern. But without discipline, wrappers inherit all operations from their root (Num, Add, + on everything), silently strip meaning at API boundaries, and collapse records and collections into the same abstraction.

What Spine adds

Spine combines ideas from F# units of measure, Haskell newtypes, Rust's newtype pattern, Perl's scalar/list context, and DDD value objects into one coherent discipline with named rules for:

Spine chains — linear refinement from bytes to domain semantics
Context separation — scalar, product, and aggregate operations never mix accidentally
Decay — automatic within a chain, explicit across categories
Dimensional arithmetic — opt-in, dimension-aware operations
Coalescing — named projections and reductions when complex values enter scalar context

The goal is code that is both semantically safe (meaningless combinations are compile errors) and extensible (new types and new operations without editing existing code). See Analyses for how this connects to the expression problem.

Core Principles

Principle	Rule
P1. Data is inert	All values resolve to fixed-width byte sequences. Bytes have no behavior — only types give them meaning.
P2. Context is sovereign	A value's valid operations are determined by the context in which it appears (scalar, product, or aggregate).
P3. Specificity flows one way	Types refine linearly: `Root ← D₁ ← D₂`. A more specific type substitutes for a less specific one within its chain, never the reverse.
P4. Semantic loss must be visible	Stripping a decorator tag or projecting a product field must be either a well-defined automatic decay or an explicit programmer action. Silent loss is a bug.
P5. Operations encode dimensional truth	Addition preserves dimension; cross-dimensional multiplication must be declared; meaningless operations (e.g. `UserID + UserID`) are opt-out by default.

Type Taxonomy

Every Spine-conformant type belongs to exactly one of three categories. Two distinctions (scalar vs. structured, fixed vs. collection) yield three categories — collapsing any two loses precision.

Scalar

A fixed-width interpretation of bytes.

Root Scalars (Float64, Int64, Char8) own arithmetic and comparison.
Decorators (Meters, Celsius, USD, UserID) refine a root without adding fields — only semantic constraints and domain methods. A decorator occupies exactly the same bytes as its root.

Product

A named record of heterogeneous fields: Particle { id, mass, position, velocity }.

Fixed, deterministic layout
Field access, projection, structural update
Not iterable, not a collection

Aggregate

A homogeneous collection: List<Particle>, String as List<Char>.

Variable length
Functor operations: map, fold, filter
Never directly operable as a scalar — must coalesce through a named reduction

Spine Chains, Decay, and Coalescing

Spine chains

A linear refinement sequence read right-to-left (each type IS-A its parent):

Bytes(8) ← Float64 ← Meters
                   ← Seconds
                   ← Temperature ← Celsius
                                 ← Fahrenheit

Celsius and Fahrenheit are siblings. Both decay to Float64. Neither converts to the other implicitly.

Implicit decay

When a function expects a root scalar and receives a decorator from that chain, the decorator automatically strips its semantic tag. This is covariant substitution within a single chain.

Explicit coalescing (`~`)

Required when:

A product enters scalar context (projection to a declared field)
An aggregate enters scalar context (named reduction: sum, average, count, custom)
Sibling decorators interact (both must decay to their common root first)

If the compiler cannot resolve the transition in a single step down one spine chain, the programmer must be explicit.

Source	`~` produces	Mechanism
Root scalar	Itself	Identity
Decorator	Its root	Strip semantic tag
Product	A scalar field	Declared projection
Aggregate	A single scalar	Named reduction (never defaulted)

Dimensional Arithmetic

Operations on decorated types must respect what those operations mean, not just what the hardware can compute.

Operation	Types	Result	Declared?
`a + b`	`D × D`	`D`	No — additive closure
`a - b`	`D × D`	`D`	No
`a * s`	`D × Root`	`D`	No — scalar scaling
`a / s`	`D ÷ Root`	`D`	No
`a * b`	`D₁ × D₂`	`D₃`	Yes — cross-dimensional product
`a * b`	`D × D`	`Root` or `D²`	Optional
`a < b`	`D × D`	`Bool`	No — same dimension only
`a + b`	`D₁ × D₂`	—	Error

Opt-in by default (§5.7): Decorators support no arithmetic unless explicitly granted. UserID does not inherit Int64 + Int64. This is the reverse of most languages, where all numbers support all operations.

Base vs. derived dimensions (§5.8): Meters is a base dimension. SquareMeters is derived and should self-document its origin (Meters × Meters). This identity metadata lets tooling validate that dimensional rules and derivation declarations are consistent.

Evolution: v1 through v4

Spine evolved through four specification versions. Earlier Lean prototypes remain in the repository as historical reference; v4 is the current design discipline.

Version	Focus	Key idea
v1	Vertebra/Scalar/Decorator/Aggregate model	Strict context rules; operators belong to root scalars only; `Coe` for automatic context decay
v2	Unified "everything is an Aggregate"	Coalescing (`~`) operator driven by a `Coalescable` typeclass
v3	DSL and macros	`spine` / `view` commands for ergonomic syntax in Lean
v4	Design discipline (language-agnostic)	Drops implementation artifacts; adds dimensional arithmetic rules, base/derived dimension metadata, JSON schema, and code generation

The honest conclusion from v1–v3: the mechanisms already exist in every modern typed language. v4 captures the rules and provides tooling (schema + codegen) to practice them consistently.

Repository Layout

spine/
├── CONTEXT.md               # AI assistant orientation (conventions, layout, workflow)
├── specifications/          # Formal specs (v1–v4); v4 is canonical
├── spine_schema.json        # JSON Schema for .spine.json domain files
├── examples/                # Domain definitions conforming to the schema
├── analyses/                # Research essays (expression problem, type-level derivations, …)
├── spine-codegen/           # Node.js generator: .spine.json → Lean 4
├── generated/               # Codegen output (gitignored; regenerate locally)
├── SpinePrelude.lean        # Shared typeclasses for generated domains
├── SpineTypes.lean          # v1 prototype
├── SpineV2.lean             # v2 prototype (coalescing)
├── SpineV3.lean               # v3 prototype
├── SpineV3Dsl.lean            # v3 DSL macros
├── SpineDslExample.lean      # DSL usage example
└── lakefile.lean            # Lake package for Lean libraries

Quick Start

Prerequisites

Node.js (for code generation)
Lean 4 with Lake (for building generated domains)

Generate Lean code from a domain definition

node spine-codegen/generate.mjs examples/physics_domain_v4.spine.json

Optional namespace override:

node spine-codegen/generate.mjs examples/physics_domain_v4.spine.json --namespace Physics

Output lands in generated/ (e.g. generated/PhysicsDomain.lean). The generator emits:

Root scalar structures
Decorator types with Coe instances (implicit decay)
Opt-in dimensional arithmetic typeclasses (DimensionalAdd, DimensionalScale, DimensionalMul)
Cross-dimensional multiplication rules
Product types with coalescing views
Aggregate type aliases with named reduction views
Structural validity proofs (wrap/unwrap roundtrips)

Build the Lean project

lake build

Type-check a standalone prototype (no Lake)

lean SpineTypes.lean

Examples

The examples/ directory contains language-agnostic domain definitions in .spine.json format. Each file is a complete, machine-readable model of a domain's types, spine chains, dimensional rules, products, and aggregates. The schema (spine_schema.json) validates these files; the codegen turns them into target-language modules.

`physics_domain_v4.spine.json`

Purpose: A end-to-end reference domain demonstrating every major Spine v4 concept in a physics simulation context. Use this as the template when defining new domains.

Rationale: Physics is the canonical test case for dimensional typing. Distances, times, masses, forces, and energies have well-understood dimensional relationships. A physics domain exercises additive closure, scalar scaling, cross-dimensional products, derived dimensions, sibling decorators, opt-out arithmetic, products with views, and aggregate reductions — all in one file.

Root scalars

Type	Width	Encoding	Operations
`Float64`	8 bytes	IEEE 754	Full arithmetic, comparison
`Int64`	8 bytes	Two's complement	Arithmetic, comparison, bitwise

Two separate spine chains root at different scalars, showing that domains can mix floating-point physical quantities with integer identifiers.

Spine chains and decorators

Float64 chain — physical quantities:

Decorator	Role	Operations	Derivation
`Meters`	Base dimension: distance	add, sub, scale, compare	—
`SquareMeters`	Derived: area	add, sub, scale, compare	`Meters × Meters`
`Seconds`	Base dimension: duration	add, sub, scale, compare	—
`MetersPerSecond`	Derived: velocity	add, sub, scale, compare	`Meters ÷ Seconds`
`Kilograms`	Base dimension: mass (min ≥ 0)	add, sub, scale, compare	—
`Newtons`	Derived: force	add, sub, scale, compare, neg	`Kilograms × MetersPerSecond`
`Joules`	Derived: energy	add, sub, scale, compare	`Newtons × Meters`
`Temperature`	Abstract temperature	add, sub, scale, compare	—
`Celsius`	Sibling decorator	(same as parent)	parent: `Temperature`
`Fahrenheit`	Sibling decorator	(same as parent)	parent: `Temperature`

The chain demonstrates:

Base dimensions (Meters, Seconds, Kilograms) with no derivedFrom metadata
Derived dimensions with explicit derivedFrom origins matching dimensional rules
Sibling decorators (Celsius / Fahrenheit) sharing a parent but not converting to each other
Constraints (Kilograms has min: 0) for domain validation metadata

Int64 chain — identifiers:

Decorator	Role	Operations
`EntityID`	Opaque identifier	None — opt-out arithmetic
`ParticleID`	Particle-specific ID	None — inherits opt-out from parent chain

This pair demonstrates §5.7: identifiers are decorators on an arithmetic-capable root, but they deliberately grant no operations. ParticleID + ParticleID should not compile.

Dimensional rules

Explicit cross-dimensional products declared in the schema:

Meters × Meters          → SquareMeters
Meters ÷ Seconds         → MetersPerSecond
Kilograms × MetersPerSecond → Newtons
Newtons × Meters         → Joules
SquareMeters ÷ Meters    → SquareMeters  (non-commutative)

The generator validates that every derivedFrom declaration has a matching entry in dimensionalRules (§5.8 consistency check).

Products

Particle — a point particle in a 1D simulation:

Field	Type
`id`	`ParticleID`
`mass`	`Kilograms`
`position`	`Meters`
`velocity`	`MetersPerSecond`

Default coalesce: id (entering scalar context yields the particle's identifier)
Named views: ParticleAsMass, ParticleAsPosition, ParticleAsVelocity — alternative projections without modifying the Particle type itself

Views are Spine's answer to the expression problem's "add new operation" axis: each view is a standalone coalescing strategy.

Aggregates

ParticleSystem — List<Particle> with named reductions:

Reduction	Strategy	Result type
`TotalMass`	sum	`Kilograms`
`AverageMass`	average	`Kilograms`
`ParticleCount`	count	`Int64`
`CenterOfMass`	custom expression	`Meters`

Aggregates never have a default coalescing strategy (§6.4). Every reduction must be explicitly named — this prevents silent semantic loss when a collection is treated as a scalar.

What you learn from this example

How to structure a complete domain in JSON
How base and derived dimensions relate
How to opt out of arithmetic for identifier types
How products expose multiple coalescing views
How aggregates declare reductions with different strategies
How the codegen turns all of this into verified Lean 4 code

To define a new domain (e.g. finance, healthcare), copy this file, change the domain field, and model your types following the same patterns.

Analyses

The analyses/ directory contains research essays that connect Spine v4 to broader programming language theory:

File	Topic
`expression-problem.md`	Expression problem — foundational analysis
`expression-problem-v2.md`	Expression problem — with type-level Java proofs
`type-level-derivation-analysis.md`	Encoding `derivedFrom` metadata in target type systems
`java-expression-problem-enhancements.md`	How type-level derivations enhance the Java story

These are written to be readable standalone — you do not need to read the Lean code or run the generator to follow the argument.

`expression-problem.md` — Spine and the Expression Problem (baseline)

The problem (Wadler, 1998): Can you add both new data types and new operations over those types without modifying existing code, while preserving type s 8000 afety?

Traditional approaches fail on one axis:

OOP (virtual methods): easy to add types, hard to add operations
FP (algebraic data types + pattern matching): easy to add operations, hard to add types

Spine's answer: Not a clever encoding, but a discipline with three extensibility mechanisms:

Open spine chains — new decorators slot into existing chains without modifying them. Adding Kelvin to the temperature chain requires no changes to Celsius or Fahrenheit.
Standalone coalescing views — new operations on products and aggregates are new view/reduction classes, not edits to existing types. PersonAsHeight and PersonAsTaxPayer are separate projections of Person.
Opt-in arithmetic registry — dimensional rules are declared, not inherited. A new rule Force × Distance → Energy adds an operation without modifying Force or Distance.

Why opt-in arithmetic is the key mechanism: The expression problem's deepest trap is accidental inheritance — a new type (UserID) inheriting Int64 + Int64, or a new rule applying to types it shouldn't. Spine's default is silence-is-denial: no operation exists unless explicitly granted.

Practical walkthroughs in three languages:

Language	Domain	What it demonstrates
Rust	Physics	Newtypes, trait-based opt-in `Add`/`Mul`, `From` for decay
Haskell	Finance	`newtype` without `Num`, explicit conversion functions, aggregate reductions
Java	Geometry	`record` decorators, sealed spine chains, factory methods for cross-dimensional products

Visitor pattern comparison: The essay includes a detailed side-by-side against the Visitor pattern. Visitor solves "add new operations" via double dispatch but requires editing the visitor interface for every new type, produces untyped Double results, and enforces no dimensional safety. Spine's coalescing views are standalone, return semantically typed results (SquareMeters vs Meters), and prevent meaningless combinations at compile time. Visitor still wins for uniform dispatch over closed heterogeneous collections — a deliberate trade Spine makes consciously rather than by default.

`expression-problem-v2.md` — Spine and the Expression Problem (with type-level derivations)

This is an evolution of expression-problem.md with one major addition: type-level dimensional proofs in Java.

The baseline Java example uses factory methods (MetersPerSecond.from(Meters, Seconds)) where the derivation relationship exists only in the programmer's head. v2 introduces:

DimensionMul<Right, Out> and DimensionDiv<Right, Out> interfaces — relational proofs that the compiler verifies
Decorators implement these interfaces to prove their cross-dimensional operations
Generic algorithms like PhysicsEngine.computeCompound(L, R) that work for any types satisfying the dimensional proof

Rationale for the v2 analysis: Structural extensibility (not editing existing files) is necessary but not sufficient for generic domain libraries. Without type-level proofs, every generic function must take concrete types or decay to untyped Float64. With proofs, a physics engine can be written once and work across any types whose dimensional relationships are declared in the schema.

The Visitor comparison and Rust/Haskell walkthroughs are preserved from v1. The Java section is expanded to show how Meters implements DimensionMul<Meters, SquareMeters> so the compiler enforces that Meters * Meters yields exactly SquareMeters.

Relationship between the two files: Read expression-problem.md for the foundational argument. Read expression-problem-v2.md when you want to see how type-level derivation metadata strengthens the Java story.

`type-level-derivation-analysis.md` — Encoding derivations in target type systems

Explores four strategies for encoding derivedFrom metadata from the JSON schema directly into target language type systems, so compilers validate dimensional derivations rather than relying solely on schema checks or codegen:

Approach	Mechanism	Strength	Trade-off
1. Phantom origin tags	Marker traits/interfaces (`DerivedFrom<Mul<Meters, Meters>>`)	Broadest applicability; introspectable identity	Compiler knows the claim, not the proof
2. Associated types / type families	Relational proofs (`DimensionMul<RHS, Output>`)	Compiler verifies operations match rules	Derived type loses standalone identity tag
3. Structural exponents	Const generics (`Quantity<L, M, T>`)	Mathematical perfection	Collapses nominally distinct types (Torque ≡ Joules) — conflicts with P2
4. Reflection / annotations	Runtime metadata (`@DerivedFrom`)	Works in RTTI languages	Not compile-time validated by the language

Recommendation: Combine approaches 1 and 2. Code generators emit marker traits for identity (what a type is) and associated types for operations (what a type does). This elevates derivedFrom from JSON metadata to a mathematically proven compiler constraint while preserving Spine's nominal decorator architecture.

`java-expression-problem-enhancements.md` — Java expression problem enhancements

A focused comparison of how each type-level approach enhances Spine's expression problem solution in Java:

Baseline: Solves both axes structurally via isolated record types and opt-in methods. Simple and idiomatic, but derivations exist only in factory implementations.
Approach 1 (phantom tags): Types self-document their origin; generic consumers can require structural derivation (Area extends DerivedFrom<Mul<L, L>>).
Approach 2 (relational proofs): Enables generic operations (compute(L, R) bounded by DimensionMul) without modifying existing types.
Combined approach: Decorators declare identity (approach 1); operands provide relational proofs (approach 2). Enables bounded generic extensibility — new algorithmic libraries that operate over a Spine domain using dimensional semantics, not untyped dispatch.

Specifications

Formal specifications live in specifications/. Read them in order to understand the design evolution:

File	Version	Summary
`spine_type_system_v1.md`	0.1	Vertebra/Scalar/Decorator/Aggregate model; strict context separation; no operator overloading across decorator boundaries
`spine_type_system_v2.md`	0.2	Unified aggregate model with coalescing
`spine_type_system_v3.md`	0.3	DSL and macro-based syntax exploration
`spine_type_system_v4.md`	0.4 (current)	Language-agnostic design discipline; dimensional arithmetic; base/derived dimensions; practicing Spine in Lean, Haskell, Rust, TypeScript, Java

spine_type_system_v4.md is the canonical reference. All new domain models, codegen output, and analyses assume v4.

Relationship to Prior Art

System	What it covers	What Spine adds
F# Units of Measure	Dimensional arithmetic with compiler enforcement	Products, aggregates, coalescing, context rules
Haskell newtypes	Spine chains via wrap/unwrap	Dimensional arithmetic enforcement, opt-in operations
Rust newtype pattern	Decorators with `From`/`Into` decay	Cross-context rules, dimensional product registry
Scala opaque types	Decorator wrapping	Context separation, coalescing discipline
Perl scalar/list context	Context determines behavior	Type safety
DDD Value Objects	Wrap domain values	Formal operation rules, decay paths

Spine's contribution is combining these into one coherent discipline.

Practicing Spine

The minimum viable practice in any language:

Never use a raw numeric type for a domain value. Wrap it. Celsius, not float.
Never define arithmetic on a wrapper unless the operation is dimensionally meaningful.
When two wrappers interact, make the decay explicit. Don't let the compiler silently strip meaning.
Distinguish records from collections. They are not the same thing.
When a complex value must become a scalar, name the projection. "Person as ID" and "Person as height" are different operations.

In this repository

Language	How	Where
Lean 4	`structure` + `Coe` + `Coalescable` + dimensional typeclasses	`SpinePrelude.lean`, generated domains
JSON → Lean	Define domain in `.spine.json`, run codegen	`examples/`, `spine-codegen/`
Lean (historical)	Hand-written prototypes and DSL	`SpineTypes.lean` through `SpineV3Dsl.lean`

See specifications/spine_type_system_v4.md §7 for guidance on Haskell, Rust, TypeScript, Java, and other languages.

Development Conventions

v4 is canonical. New work should follow specifications/spine_type_system_v4.md.
Domains are defined in JSON conforming to spine_schema.json, then generated — not hand-written boilerplate.
Generated code is not edited. Regenerate from the .spine.json source.
generated/ is gitignored. Run the codegen locally after cloning.

Document	Topic
`specifications/spine_type_system_v4.md`	Full v4 specification
`analyses/expression-problem.md`	Expression problem — foundational analysis
`analyses/expression-problem-v2.md`	Expression problem — with type-level Java proofs
`analyses/type-level-derivation-analysis.md`	Encoding derivations in target type systems
`analyses/java-expression-problem-enhancements.md`	Java-specific enhancement analysis
`examples/physics_domain_v4.spine.json`	Reference domain definition
`spine_schema.json`	JSON Schema for domain files
`CONTEXT.md`	AI assistant context for this repository

Latest commit

History

Folders and files

Repository files navigation