Chapter 3

The maths you need

Everything in the paper is built from about ten small ideas. None needs more than discrete maths; what makes the paper hard is that it uses the notation of type theory without introducing it. This chapter introduces exactly that notation, each idea with a code equivalent. Skim it once now; come back to it whenever a formula in chapters 4–9 stops you. Appendix A is the same material as a lookup table.

1. Functions are values, and composition reads right-to-left

A function f : X → Y takes an X and gives a Y. Functions are ordinary values here: you can store one, pass one, return one from another function. The paper leans on this constantly — an "undo" is just a stored function.

Composition f ∘ g means "do g first, then f": (f ∘ g)(x) = f(g(x)). Read it right to left. id is the function that returns its argument unchanged.

const compose = (f, g) => x => f(g(x))   // f ∘ g : g runs first
const id = x => x

Why it matters here: an undo stack is a composition of undo functions, and the right-to-left convention is exactly why "last in, first out" shows up as a formula rather than a rule.

2. Arrows: →, ⇝, ⇀, ↦

3. Pairs, projections, and let

X × Y is the type of pairs (x, y). pr₁ and pr₂ pick the first and second component. Γ × (Γ → Γ) is therefore "a state together with a function on states" — you will meet this pair on almost every page.

let (δ, g) = e(γ) in … destructures a pair, exactly like const [delta, g] = e(gamma).

type Pair<A, B> = [A, B]
const pr1 = <A, B>(p: Pair<A, B>) => p[0]
const pr2 = <A, B>(p: Pair<A, B>) => p[1]

4. Γ is just "the type of the whole world"

The paper writes Γ (capital gamma) for the context type — the type of everything a component can touch: registered routes, open timers, the service table, all of it. A particular state of the world is γ (small gamma). Nothing is assumed about its structure until chapter 6 gives it one. When you see Γ → Γ, read "a change to the world"; when you see γ₀, read "the world before the component arrived".

Confusingly for a Haskell reader, Γ here is not a typing environment. It is a runtime value type. The paper chose the letter deliberately (it reifies the typing context), but you can ignore that motivation.

5. Partial maps with preconditions, and "produces no transition"

A dictionary σ : K ⇀ V is defined on dom(σ) ⊆ K. Notation: σ(k) lookup; σ[k ↦ v] the dictionary with k set to v; σ ∖ k with k removed. An operation may carry a precondition (e.g. "k ∉ dom σ" for inserting). The paper's convention: if a precondition fails, the operation is an error and the state does not change — so every formula about "what transitions do" applies unchanged. You can mentally read every Σ ⇀ Σ as Σ → Maybe(Σ).

const set = (k, v) => (σ: Map) => {
  if (σ.has(k)) throw new Error('already provided')     // precondition: k ∉ dom σ
  const next = new Map(σ).set(k, v)                      // σ[k ↦ v]
  const undo = (σ2: Map) => { const m = new Map(σ2); m.delete(k); return m }   // σ′ ∖ k
  return [next, undo]
}

6. "The value type depends on the key": (k : K) ⇀ 𝒱ₖ

This is the one piece of genuinely dependent typing. 𝒱 is a family of types indexed by keys: 𝒱_db might be Database, 𝒱_http might be Server. A map of type (k : K) ⇀ 𝒱ₖ is a dictionary where each key has its own value type. TypeScript can only approximate this with an interface; Effect's Context.Tag is the same idea.

interface Services { db: Database; http: Server; logger: Logger }
// σ : (k : keyof Services) ⇀ Services[k]
declare function get<K extends keyof Services>(σ: Partial<Services>, k: K): Services[K] | undefined

The subscript on 𝒱ₖ, 𝒜ₖ, ℳₖ, ≃ₖ always means "the one belonging to key k".

7. Recursive types: μX. …

μX. F(X) reads "the type X such that X = F(X)". A linked list is μL. Maybe(A × L): either empty, or an element paired with the rest of the list. The paper uses it for two things: the effect iterator (a step that returns the rest of the steps — a generator) and the context (a state that contains a state). In TypeScript you write the recursion directly:

type Iter = (γ: Γ) => [Γ, (γ: Γ) => Γ, Iter | null]   // μℑ. Γ → Γ × (Γ→Γ) × Maybe(ℑ)

Maybe(X) is Nothing or Just(x); Either(E, X) is an error or a value.

8. Monoids and "respects the operation"

A monoid is a set with an associative binary operation and a unit: strings under concatenation with ""; numbers under + with 0; functions Γ → Γ under ∘ with id. That last one is the only monoid the paper really uses: "effects form a monoid" just means "you can sequence them, sequencing is associative, and doing nothing is an effect".

A homomorphism is a map between monoids that respects the operation: h(a ∘ b) = h(a) ∘ h(b) and h(unit) = unit. When the paper says track is a homomorphism (Thm 5), it means: tracking two effects one after the other gives the same result as tracking their composite. That is all. You may read "homomorphism" as "respects sequencing" throughout.

9. "Witnessed": a value bundled with a proof

Type-theory notation like

(e : Γ → Γ × (Γ → Γ)) × ((γ : Γ) → (δ : Γ) → (g : Γ → Γ) → ((δ, g) = e(γ) → g(δ) = γ))

looks fierce but says: "an effect function e, together with a proof that whenever e(γ) returns (δ, g), applying g to δ gives back γ". The × pairs the function with the proof; the chain of → is "for all γ, δ, g: if … then …". A witness is that proof. In engineering terms it is a contract the author promises and the runtime does not check (chapter 10 says so explicitly). When you see "witnessed", read "comes with a promise that its inverse works".

10. "Up to an equivalence": agreeing not to look

a ≃ b means "a and b are the same for our purposes". Two heaps that differ only in where blocks happen to sit; two states that differ in a counter nobody reads. An equivalence relation is reflexive, symmetric, transitive. Saying a result "holds up to ≃" means: replace every = by ≃ and the result is still true. Chapter 6 defines the paper's ≃ precisely: two values are equivalent if no experiment made of the allowed operations can tell them apart. That is a black-box notion you already know from algorithms (observational equivalence of data structures).

11. How to read one of the paper's definitions

1. Read the type line first — e.g. 𝔈Γ ≔ Γ → Γ × (Γ → Γ). Say it in words: "a function from a state to (a new state, a function on states)".
2. Ask what each component is for. Here: the new state is the effect's result; the function is its undo.
3. Only then read the formula, matching each symbol to its component.
4. Find the theorem that uses it and read its statement, not its proof. The proofs in this paper are short computations; you rarely need them.

The decorated letters are just names for types: 𝔈 (effect functions), ℑ (iterators), 𝔗 (pairs under twisted composition), 𝔇 (specifications), 𝔓 (provisions), ℭ (components), 𝔉 (fibers), 𝔑 (fiber names), 𝔐 (transformation monoids). A star (𝔈Γ*) means "witnessed"; a superscript set (ℑΓ^S) means "witnessed up to ≃_S".