Denotational Design

Denotational Design is the practice of deriving a programming interface from simple, compositional, implementation-independent meanings.

The methodology was developed and named by Conal Elliott. Its central move is not merely to assign semantics to an existing language or API. It is to let semantics guide the design of the API itself.

The design loop

Use this order:

1. Choose the semantic domain.
2. Identify the structure that matters in that domain.
3. Choose a small vocabulary of primitive operations.
4. Derive useful operations compositionally.
5. State the laws those operations obey.
6. Choose one or more representations.
7. Implement interpretations that preserve the structure.
8. Validate them with laws, models, and scenarios.

Representation-first design commonly starts at step 6 and attempts to reconstruct steps 1–5 afterward.

Designing a branch algebra

Return to branch positions. The desired meaning is a finite path in a binary branching structure.

One possible primitive algebra is:

$$\begin{array}{rl}\mathrm{root}& :()\to \mathsf{Branch}\\ \mathrm{grow}& :\mathsf{Branch}\times \mathsf{Direction}\to \mathsf{Branch}\\ \mathrm{path}& :\mathsf{Branch}\times \mathsf{Branch}\rightharpoonup \mathrm{List}(\mathsf{Direction})\end{array}$$

The partial arrow $\rightharpoonup$ means that the path observation exists only when the first branch is an ancestor of the second.

Useful operations follow:

$$\begin{array}{rl}\mathrm{left}(b)& =\mathrm{grow}(b,\mathsf{Left})\\ \mathrm{right}(b)& =\mathrm{grow}(b,\mathsf{Right})\\ is\_ancestor(a,b)& ⟺\mathrm{path}(a,b)\text{is defined}\\ from\_path(d_s)& =\mathrm{fold}(\mathrm{grow},\mathrm{root},d_s)\end{array}$$

This algebra does not mention vectors, integers, fractions, database keys, or bytes. Those choices come later.

Structure before convenience

The primitive vocabulary should reveal the structure downstream code depends on. It should not be a collection of every convenient method available on one implementation.

trait BranchManager {
    // not recommended: exposes machinery, not semantic observations
    fn storage(&self) -> &BranchTable;
    fn config(&self) -> &BranchConfig;
    fn raw_bits(&self) -> &[u64];
    fn grow_and_save(&mut self, right: bool);
}

A semantic API may still include effects when effects are part of the chosen domain. The rule is not “everything must be pure.” The rule is “every primitive must state a coherent meaning.”

Encoding is not methodology

Denotational Design does not require:

• Haskell
• tagless-final encoding
• object algebras
• free monads
• one AST
• pure functions only
• category-theory terminology in every API

These may be useful encodings or explanatory tools. None defines the method.

Type-class morphisms

One way to understand the method is through structure-preserving mappings.

Suppose an interface describes a semantic algebra. An implementation maps its abstract values and operations into a concrete representation. A valid implementation must preserve the relevant operations and laws.

If encode maps abstract branches into a concrete carrier, preservation of growth looks like:

$$\mathrm{encode}(\mathrm{grow}(b,d))={\mathrm{grow}}_{\mathsf{concrete}}(\mathrm{encode}(b),d)$$

The implementation is not merely a bag of methods with matching names. It is intended to be a morphism that respects the algebraic structure.

What counts as a good abstraction

A good DD abstraction has several properties:

• Its values have a simple intended meaning.
• Its primitives expose semantic observations or constructions.
• Larger behavior is derived from those primitives.
• Its laws do not depend on one representation.
• Independent implementations can interpret it.
• Operational details appear only where they become relevant.

Smallness alone is not enough. A tiny trait exposing get_manager() is still representation-first. A larger algebra may be justified when its operations form one coherent semantic structure.

Semantic values and abstract carriers

Not every concrete type is forbidden from a specification.

Use an associated type when the interpreter should choose the carrier:

trait BranchAlg {
    type Branch;
}

Use a concrete type when it is stable semantic vocabulary:

enum Direction {
    Left,
    Right,
}

The distinction is not “abstract good, concrete bad.” It is semantic vocabulary versus accidental machine representation.

The specification is the denotation, and it need not execute

The specification is the denotation: the mathematical meaning assigned to each construct. Its power comes from being free of the constraints of efficiency and even of executability.

The canonical example is FRP (Functional Reactive Programming): a Behavior a is defined as a function of continuous time,

$$[[\cdot ]]:\mathsf{Behavior}a\to (\mathbb{R}\to a)$$

That model is precise but not executable — you cannot enumerate the reals. A program may likewise denote a set of outcomes; neither model runs, and that is the point. The meaning is chosen for simplicity and precision, not for how it will compute.

Executability and efficiency are pushed entirely onto the implementation, a separate artifact held correct by homomorphism laws (type class morphisms) that relate it back to the meaning: the meaning function must carry each syntactic composition to the corresponding semantic one. As Conal puts it, the denotation gives "an unambiguous definition of exactly what to implement, while leaving a great deal of room for creativity about how."

In Rust, several artifacts express parts of this specification, and some of them happen to be executable. Executability is incidental; it is not what makes them a specification:

• prose states intended meaning
• traits state available primitives
• extensions state derivations
• laws state required equalities
• interpreters demonstrate realizability
• tests provide finite evidence

Read them together, with meaning and laws above concrete machinery in authority.

Further reading

• Denotational Design: from programs to meanings (BayHac 2014)
• Denotational design with type class morphisms
• Conal Elliott's writings and talks