Scaling "Make Illegal States Unrepresentable"

The phrase “Make Illegal States Unrepresentable” has caught fire in the functional programming world after being coined by Yaron Minsky in 2011. It’s clear enough how to accomplish this for individual subsystems: given a component \(C\) with state \(C_S\), it’s just a matter of defining \(C_S\) so that illegal states literally cannot be represented by its type. This could be done with smart constructors, but refinement types potentially provide a better option for defining new types via predicates.

How do we scale this to multiple components? Here’s the rub: given subsystems \(C\) and \(D\) with state spaces \(C_S\) and \(D_S\), the space of valid states for \(C \times D\) is generally not \(C_S \times D_S\). This is because realistic systems usually have global as well as local constraints on the state space. Consider the example of two components that hold integer counters initialized to \(0\) where each counter can be incremented or decremented. The state space of each counter is \(\mathbb{Z}\). Now imagine there is a global constraint that the counters must add to \(0\). The resulting state space of the composite of two counters is no longer \(\mathbb{Z} \times \mathbb{Z}\) but rather some subscheme defined by the constraint \(x + y = 0\).

What becomes clear here is that components cannot unilaterally control their state as this would violate global constraints, and they cannot have knowledge of which global constraints must be enforced if they are intended to be standalone and modular. Components can attempt to signal state updates to other subsystems, but there is no a priori guarantee that these signals will be handled properly, which is what making illegal states unrepresentable is about to begin with! If components cannot unilaterally control their state without reference to the state of the remainder of the subsystems, does the state really belong to the components?

One possible solution, suggested before by various authors, is to make all system state external. All subsystems become stateless and an external agent or datastore enforces the constraints on the persistent state. Another possible solution is to consider actions that could update global state or not, depending on whether the new state was representable. The global state for a pair of counters would be a refinement type \(E_S \subseteq C_S \times D_S\), and one could consider an update monoid for \(E_S\). In any event there are solutions. It’s worth noting, however, that stateful components (e.g. objects) are not among them.