Part I named the two hardnesses and put contracts in your hands. Now we begin the constraint stream in earnest, on the part of the system that can least afford to be wrong: the domain core. The goal of this chapter is a specific and slightly radical one. We are not going to detect illegal states with checks scattered through the code. We are going to arrange the model so that the illegal states have no representation at all — so that the wrong value is not caught, but unspeakable.
Every state a type permits is a state some code, somewhere, eventually produces. So the design question is not "how will I validate this?" but "what am I allowing to be said?" A type is a vocabulary. The narrower the vocabulary, the fewer the sentences — and a bug is always a sentence the domain forbids but the type allowed.
3.1 The Bag of Nullable Fields
Here is how an order is modelled when no one is watching the vocabulary. One class, all the fields any stage might need, a string to remember which stage we are in:
-- Every illegal combination is representable. The type says almost nothing.
class Order
feature
status: String -- "draft"? "placed"? "shipped"? who enforces this?
items: Array[Line_Item] -- empty is fine for a draft, nonsense once placed
total: Money -- meaningless until placed; some number anyway
tracking: Tracking_Id -- meaningless until shipped; nil the rest of the time
end
Count the illegal states this permits. An order with status = "shipped" and no items. An order with status = "draft" and a tracking id. An order marked "placed" whose total does not equal the sum of its items. A status of "shpiped" — a typo the type welcomes. Each of these is a sentence the domain forbids and the type cheerfully allows, so each one must be guarded against by hand, in every function that touches an order, forever. The model has pushed its entire correctness burden onto the code that uses it.
The string status is the tell. Whenever a field's value is supposed to control which other fields are meaningful, the type is being used to smuggle in a notion of "kind" that it cannot enforce. That is exactly the job of a sum type.
3.2 Sum Types: One of Several Shapes
A sum type says a value is exactly one of a fixed set of shapes, and each shape carries only the data that makes sense for it. Nex writes this directly with union: a name for the whole, then one line per shape naming the data that shape holds.
union Order
Draft(items: Array[Line_Item])
Placed(items: Array[Line_Item], total: Money)
Shipped(items: Array[Line_Item], tracking: Tracking_Id)
end
This is a closed set: union tells the compiler that no other shapes exist, so it can reason about the whole. Under the surface each variant becomes a distinct type — Draft, Placed, Shipped — and Order is their sealed parent; the concise form simply spares you writing the parent and each subclass by hand. You construct a variant by name, create Placed.make(xs, t), and read its data as ordinary fields.
But shape is only part of what a placed order must satisfy. A Placed should have at least one line, and its total should equal the sum of those lines — and those are not facts about shape, they are relationships among values. The union form states shape and nothing more; it synthesises no contracts. When a variant must also hold a relationship, write that hierarchy in the longhand the union is shorthand for, and hang the contract on the variant that needs it:
sealed deferred class Order
end
class Draft
inherit Order
feature items: Array[Line_Item]
create make(xs: Array[Line_Item]) do items := xs end
end
class Placed
inherit Order
feature
items: Array[Line_Item]
total: Money
create make(xs: Array[Line_Item], t: Money)
require
not_empty: xs.length > 0
total_matches: t = sum_of(xs)
do
items := xs
total := t
end
invariant
not_empty: items.length > 0
total_consistent: total = sum_of(items)
end
class Shipped
inherit Order
feature
items: Array[Line_Item]
tracking: Tracking_Id
create make(xs: Array[Line_Item], t: Tracking_Id) do
items := xs
tracking := t
end
end
The two forms describe the same three shapes; the longhand only adds what union leaves out — the require and invariant that make Placed's relationships as unbreakable as its shape. This is the book's own thesis surfacing in the language: reach for the concise union by default, and drop to the open longhand exactly where a shape needs a contract. Look now at what has become impossible. A Draft has no total and no tracking field — not "null", but absent, so no code can read a draft's tracking id because there is nothing to read. A Shipped has a tracking id and no way to exist without one. The illegal combinations of §3.1 are not rejected at runtime; they cannot be constructed, because there is no shape that holds them. The vocabulary no longer contains the forbidden sentences.
Notice also where types stop and contracts begin. That an order is one of three shapes is structural — the type carries it. But "a placed order has at least one line" and "its total equals the sum of its lines" are not structural facts about shape; they are relationships among values, and no arrangement of fields can express them. So the sum type hands them to contracts: the require refuses to build a bad Placed in the first place, and the invariant guarantees no later operation can drift it into an inconsistent one. This is the division of labour from Chapter 2, now doing structural work: the type makes the kinds unrepresentable; the contract makes the illegal relationships unreachable.
3.3 Constrained Types: Giving a Value a Standard
The same move works one level down, on individual values. A Line_Item's quantity is not just any integer — it is a positive one; a quantity of zero or minus three is not a small bug but a meaningless value. Rather than let a bare Integer carry it and re-check positivity everywhere, we give the quantity its own type — an Integer narrowed by the standard it must always meet:
-- A Quantity is an Integer that is known to be positive.
declare type Quantity = Integer where n: n > 0
This is a refinement type: the base type Integer, narrowed by a predicate. It is not a wrapper class — a Quantity is an Integer at runtime, with no field to unwrap and no boxing to pay for. What the refinement adds is a single, enforced promise: the predicate n > 0 is checked at every point where a plain Integer is narrowed into a Quantity — a typed binding, a parameter, a returned value. Widening back the other way is free, because a positive integer is still an integer.
let q: Quantity := 5 -- checked here: asserts 5 > 0
let doubled: Integer := q * 2 -- free: a Quantity is already an Integer
Once a value is a Quantity, its positivity travels with it. A function that takes a Quantity never checks that it is positive, because a bare integer could not have crossed into that type otherwise — the predicate is the type's promise to every routine that will ever hold it. The check happens once, at the narrowing gate, and never again. This is the same economy as a sum type, applied to a scalar: pay for the constraint where the value enters, collect the guarantee everywhere else — and, unlike a wrapper class, without a single .value to thread through the arithmetic.
This pattern — giving a primitive a type that enforces its standard — is how you retire "primitive obsession", the habit of representing every domain quantity as a raw Integer or String. A numeric bound like "positive" is a refinement, a one-liner; a value drawn from a fixed set is better a small class or a distinct type. A raw string can be an email address, a currency code, a typo, or an SQL injection; a Currency_Code that admits only the codes that exist can be none of those. Each such type is a small door closed for good.
3.4 Exhaustiveness: The Compiler Carries the Argument
Closing the set of shapes buys something beyond forbidding bad values: it lets the compiler guarantee you handled all the good ones. Because Order is sealed, a match over it must cover every case, or the program does not compile.
function describe(o: Order): String
do
match o of
when Draft as d then
result := "draft with " + d.items.length.to_string + " item(s)"
when Placed as p then
result := "placed, total " + p.total.to_string
when Shipped as s then
result := "shipped via " + s.tracking.to_string
end
end
Each when binds the matched value at its specific type — inside the Placed branch, p has a total; inside Shipped, s has a tracking — so the fields you may touch are exactly the fields that make sense for the case. There is no null to guard, because there is no field that does not belong.
Now imagine the domain grows a fourth state, Cancelled. You add it to the sealed hierarchy, and the compiler immediately marks every match that does not yet handle it — describe among them — as incomplete. The new requirement does not slip silently through code that predates it; the type system turns "handle the new case everywhere" from an act of memory into a checklist the compiler hands you. Exhaustiveness converts a change into a set of compile errors, which is the friendliest form a change can take. This is the constraint tradition paying a dividend: a closed set is not a cage but a guarantee that nothing was forgotten.
The escape hatch matters too. An else branch handles the remaining cases and switches off the exhaustiveness check — useful, but a deliberate loosening. Every else over a sealed type is a small decision to not be told about future cases, and should be written knowingly. Prefer enumerating; reach for else only when the ignored cases are genuinely uniform.
3.5 What Types Cannot Say
It is tempting, having seen how much types can forbid, to try to push everything into them. That temptation is worth resisting, because it leads to models so elaborate that the types become harder to understand than the bugs they prevent. The discipline is to know the line: use types for what types are good at, and hand the rest to contracts.
Types are good at shape and kind. They express that an order is one of three forms, that a quantity is its own type, that a shipped order has a tracking id. What they cannot express, without contortion, are relationships that hold among values at runtime: that a total equals a sum, that a discount never exceeds a subtotal, that a shipment's items are a subset of the order's. These are not facts about shape; they are arithmetic and logical claims, and the right tool for them is the contract — the require that refuses to build the bad value and the invariant that forbids the object from ever resting in a bad state.
So the constrained core is built from two materials working together. Sum types and constrained types set the vocabulary — the kinds and shapes that can be said at all. Contracts set the grammar — the relationships those values must satisfy to be legal. Between them they make the illegal states of §3.1 unrepresentable: the structural ones by absence, the relational ones by contract. The core is now the part of the program you are least afraid of, exactly as Chapter 1 promised.
3.6 The Edge of the Core
There is one objection left. All of this assumes the values arriving at the core are already the right types — that someone handed us a real Array[Line_Item] and a real Money, not a blob of JSON off the network or a row from a form. Inside the core, that assumption is exactly what lets the interior stop checking. But it has to be made true somewhere, and it cannot be made true inside the core, because the core deals only in values that are already trustworthy.
That "somewhere" is the boundary — the moment untrusted input becomes a typed value, once, and earns the right to enter. It is the first place the open world meets the closed core, and it deserves a chapter of its own. That is the next one: parse, don't validate.