From de1391e673d8849a2b782193cc36e9675cb924eb Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 17:48:30 +0200
Subject: [PATCH 1/6] Add 'Replace mutable fields with lenses' refactoring
 catalogue entry

Second entry of the refactoring catalogue, with its dual (inline the
lens). Three Before/After examples in Scala 3 and Haskell, each proven
equivalent by hedgehog properties the reviewer mutation-checked, plus
the three lens laws as second properties, a koan diagram and three
example diagrams, and 14 references verified against primary sources.

- pages/refactorings/replace-mutable-fields-with-lenses.md and /sources/
- _data/refactorings.yml: add slug for the entry
- _config.yml: exclude the new sources dir
- .claude/skills/refactoring-entry/LESSONS.md: lessons from this entry
  (result-value comparison, composed-path design, partial-lens pitfall)
---
 .claude/skills/refactoring-entry/LESSONS.md   |  27 +
 _config.yml                                   |   1 +
 _data/refactorings.yml                        |   2 +-
 .../replace-mutable-fields-with-lenses.md     | 476 ++++++++++++++++++
 .../01-account-balance/After.hs               |  17 +
 .../01-account-balance/After.scala            |  13 +
 .../01-account-balance/Before.hs              |   7 +
 .../01-account-balance/Before.scala           |   6 +
 .../01-account-balance/Spec.hs                |  45 ++
 .../01-account-balance/Spec.scala             |  46 ++
 .../01-account-balance/diagram.svg            |  46 ++
 .../02-player-position/After.hs               |  40 ++
 .../02-player-position/After.scala            |  27 +
 .../02-player-position/Before.hs              |  12 +
 .../02-player-position/Before.scala           |  11 +
 .../02-player-position/Spec.hs                |  63 +++
 .../02-player-position/Spec.scala             |  69 +++
 .../02-player-position/diagram.svg            |  41 ++
 .../03-file-tree/After.hs                     |  19 +
 .../03-file-tree/After.scala                  |  14 +
 .../03-file-tree/Before.hs                    |  11 +
 .../03-file-tree/Before.scala                 |   8 +
 .../03-file-tree/Spec.hs                      |  56 +++
 .../03-file-tree/Spec.scala                   |  68 +++
 .../03-file-tree/diagram.svg                  |  40 ++
 .../diagrams/koan.svg                         |  38 ++
 .../replace-mutable-fields-with-lenses/run.sh |  24 +
 27 files changed, 1226 insertions(+), 1 deletion(-)
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses.md
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/diagrams/koan.svg
 create mode 100755 pages/refactorings/replace-mutable-fields-with-lenses/run.sh

diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
index 0a36a59..53d07b1 100644
--- a/.claude/skills/refactoring-entry/LESSONS.md
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -75,3 +75,30 @@ brief.md or workflow.js and deleted here. Keep the calibration table current.
   after the item) attach to the *enclosing* `<ol>` at a break point and split the list. The working
   pattern is: a single `<ol>` with raw `<li id="ref-N">` items, and hand-render inline markdown to
   `<em>`/`<a>` yourself. Folded into SKILL.md §3, workflow.js research prompt, and brief.md.
+
+## 2026-09-26 — 02 Replace mutable fields with lenses
+
+- **Scala/Haskell Spec must compare *result values*, not the Before/After records.** The two sides carry
+  different record types (they must — the point is that After's type can differ). Asserting
+  `Before.x(...) ==== After.x(...)` where the tuple/record types differ makes hedgehog upcast to `Any`
+  and report structural inequality, or fail to compile without a derived `Eq`. Compare projections:
+  `(before.field, ...) ==== (after.field, ...)`. The reference extract-method avoided this by returning
+  primitives; lens examples return records, so this bites immediately. → rule in brief.
+- **A lens is a focus on one path; composition is for nested paths, not merging sibling fields.** A first
+  02 tried `compose(x, y)` on two lenses with the same source to build a pair-lens — that is not a lens
+  (no single field focus), and it does not typecheck. The textbook "compose two lenses" example is a
+  nested record: `player . x`. When the refactoring is about *every element* (all sizes in a tree), a
+  single lens does not fit — that is a traversal; the coherent example uses a total per-node lens inside
+  the recursion. → design note for future lens-like entries.
+- **A partial lens (entryFile on a sum) forces `error`/`sys.error` in the getter; a reviewer would flag
+  it and the property can only test the defined region.** Switched 03 to a total `Lens[Node, Int]` on a
+  plain record — partiality is a real pitfall to *write about*, not a good example shape.
+- **Mutation-checking discipline.** A wrong-typed mutant is not a valid test; the compose-swap mutant
+  was a type error in both languages (itself evidence the lens types are sound). Use sign flips,
+  off-by-ones, dropped cases as mutants; drop mutants that fail to compile rather than reporting a pass.
+- **Toolchain.** `scala-cli run <dir> --main-class spec` works; `docker run cp-hedgehog runghc -i<dir>
+  <dir>/Spec.hs` works. Width rule held at 72 chars for all sources. Time: examples+verify ≈ 45 min;
+  mutation+probes ≈ 15 min.
+- **Workflow-runner gap.** This environment has no Claude Code `Workflow` batch runner; executed the
+  workflow phases directly (research → citation verify → examples → mutate/probes → diagrams). Recorded
+  findings here so the skill's workflow prompt matches when the runner is available.
diff --git a/_config.yml b/_config.yml
index 12eb19d..8a7b84b 100644
--- a/_config.yml
+++ b/_config.yml
@@ -42,3 +42,4 @@ plugins: [jekyll-paginate, jekyll-seo-tag, jekyll-feed, jekyll-remote-theme]
 # include_relative; do not also publish them as static files.
 exclude:
   - pages/refactorings/extract-method/
+  - pages/refactorings/replace-mutable-fields-with-lenses/
diff --git a/_data/refactorings.yml b/_data/refactorings.yml
index 264354c..bf61454 100644
--- a/_data/refactorings.yml
+++ b/_data/refactorings.yml
@@ -5,7 +5,7 @@
 - group: "Refactorings"
   items:
     - { name: "Extract / Inline method", slug: extract-method }
-    - { name: "Replace mutable fields with lenses" }
+    - { name: "Replace mutable fields with lenses", slug: replace-mutable-fields-with-lenses }
     - { name: "Replace global state with parameter" }
     - { name: "Introduce ReaderT (Kleisli)" }
     - { name: "Replace loop with fold" }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses.md b/pages/refactorings/replace-mutable-fields-with-lenses.md
new file mode 100644
index 0000000..e39bca3
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses.md
@@ -0,0 +1,476 @@
+---
+layout: page
+title: Replace Mutable Fields with Lenses
+subtitle: "Replace mutable fields with lenses: package a field's reader and pure writer as one value, and the read becomes get, the write becomes set or modify — inline the lens, and a field that is never composed just becomes a field again"
+permalink: /refactorings/replace-mutable-fields-with-lenses/
+tags: [refactorings, replace-mutable-fields-with-lenses]
+hide: true   # entry pages are reached from the catalogue, not the top-right nav
+---
+
+<p class="rf-crumb"><a href="{{ '/refactorings/' | relative_url }}">← The refactoring catalogue</a> · 2 of 35</p>
+
+A mutable field is a place where the class's invariants can be broken:
+any method can read it, any method can write it, and nothing stops a
+write from putting the object into a state the other methods did not
+anticipate. Object-oriented refactoring has a ladder of moves up this
+smell — Fowler's *Encapsulate Variable* (the catalogue entry that used
+to be *Encapsulate Field*, and before that *Self-Encapsulate Field*)
+hides the field behind accessor methods [[1](#ref-1)], [[2](#ref-2)], and *Remove Setting
+Method* then removes the setter once the field no longer needs to be
+written from outside the class [[3](#ref-3)]. The field is still a field; it is
+just visited through a corridor.
+
+The functional reading goes one step further: a field of an immutable
+record is not a location, it is a projection, and a projection that can
+also be written is a *lens* — a value packaging `get :: s -> a` and
+`set :: a -> s -> s` [[4](#ref-4)]. Replacing a mutable field with a lens means
+making the record immutable and routing every read through `get` and
+every write through `set` (or `modify`, which reads, applies a pure
+function and writes in one step). The single field's lens *composes*
+with the lenses of enclosing records, so a deep update that once
+touched five records by hand becomes one composed path. And because
+`set` is a pure function, the writes cannot run off and mutate
+something the rest of the program is looking at; the state transition
+is a value again. The three lens laws — `get (set v s) = v`,
+`set (get s) s = s`, `set v₂ (set v₁ s) = set v₂ s` — are exactly
+the equations under which the move is a refactoring, and they are
+stateable as property tests [[4](#ref-4)], [[5](#ref-5)].
+
+The inverse direction is just as useful. A lens that is never composed,
+never updated through a path, and never read by more than one caller is
+abstraction tax: the reader and writer are already next to each other,
+and a `get`/`set` pair or a plain field says the same thing with less
+machinery. Inlining the lens — replacing `lens.get(s)`, `lens.set(v)(s)`
+and `lens.modify(f)(s)` with direct field access — is the move that
+removes indirection that no longer earns its name. Foster, Greenwald,
+Moore, Pierce and Schmitt's notion of a *well-behaved lens* is the
+property-theoretic core both directions are checked against: the two
+functions are a lens exactly when the GetPut and PutGet laws (the first
+two above, in the form they state) hold [[4](#ref-4)].
+
+## Motivation
+
+Reach for the lens when the same field is read and written in many
+places and the writes compose. The smell is repetition of field
+handling: an object-with-accessors whose setters are one-liners that
+nothing intercepts, a copy-update chain that grows a level for every
+record you descend, or an update that must be re-derived by hand each
+time a field moves. An OO class can hold its invariants in accessor
+methods, but the corridor is per-type and per-field; a lens is a value,
+so it can be passed around, stored, and composed into paths that reach
+several levels down without ever repeating the intermediate records.
+When the invariant itself matters — a balance that must never go
+negative, a size that must bracket its children — the pure writer makes
+the transition a value the type system and the tests can see, and a
+*bad* write is a failed check rather than a corrupted object.
+
+Reach for the inverse when the lens is speculative generality. The
+smell that drives Inline is the mirror image: a field whose updates are
+all one level deep, a lens composed nowhere, a get/set pair whose writer
+is `const`-like and whose reader is the identity. The abstraction costs
+a reader a detour — what is *set v₂ (set v₁ s)* doing when the program
+only ever calls `set` once? — and it costs the compiler nothing it can
+deduce. When all the code does with the field is read it once, or write
+it once, a plain field or a pair of functions is clearer. The two moves
+are one equation read in two directions; which direction you choose
+records a judgement about whether the field is part of a *path* or a
+*leaf*.
+
+## The move
+
+Both catalogue pages are short. *Encapsulate Variable*: create a
+function that reads the field, create one that writes it, replace every
+read with a call to the reader and every write with a call to the
+writer, and test [[2](#ref-2)]. The precondition is that the readers and writers
+are the only way in and out — nothing may reach the field directly — and
+the payoff is that the class owns its representation. *Remove Setting
+Method*: once the field can be initialised and never needs to be
+reassigned, delete the setter and initialise at construction [[3](#ref-3)]. Read
+the two together and they are the OO route to what the lens packages:
+reads through a named getter, writes through a named setter, and no
+bare `field = ...` anywhere. Herbert's dissertation on Scala
+refactoring points at the same target from the tooling side: a
+refactoring that turns a mutable field into a pure accessor pair has to
+move the *writes*, and that is the whole analysis [[11](#ref-11)].
+
+In the functional reading the move is mechanical. Make the record
+immutable. Define `get` as the record's field accessor and `set` as a
+function returning a copy with the field replaced; package them as a
+lens value. Replace reads with `get`, writes with `set`, read-modify-
+write with `modify`. Where a field sits inside other records, compose
+the lenses along the path. The OO precondition — no direct access — is
+replaced by a type: the only way to reach the field is through the
+lens, and the type checker enforces it. The trickier part is what the
+OO ladder leaves implicit. `set` must leave every other field alone, so
+a lens is not just any `(get, set)` pair; it is one that satisfies the
+three laws, and those laws are precisely what a property test can check
+[[4](#ref-4)].
+
+## The functional reading
+
+In a referentially transparent language a record field is a *focus*: a
+value that indexes into a structure. A lens is a focus with a reader
+and a writer, and the two directions share one equation. `get` selects
+the focus; `set` replaces it; `modify f` is `set` after `get` after
+`f`. Nested records compose: the composite focus `outer . inner`
+selects `inner` inside `outer`, so a deep update becomes one path
+instead of a copy chain. What makes this a *refactoring* rather than a
+rewrite is that the three lens laws are equations between programs —
+`get (set v s) = v`, `set (get s) s = s`, `set v₂ (set v₁ s) =
+set v₂ s` — and they are exactly the conditions under which replacing
+field access with `get`/`set` preserves behaviour [[4](#ref-4)], [[5](#ref-5)].
+
+Foster, Greenwald, Moore, Pierce and Schmitt defined *well-behaved
+lenses* and proved a large catalog of combinators (composition, map,
+and recursion among them) that compose them while preserving those
+laws; their GetPut and PutGet are the first two equations above, and
+PutPut (the third) distinguishes the very well-behaved class [[4](#ref-4)].
+O'Connor showed that lenses are exactly the coalgebras for the costate
+comonad — the categorical shape of "a structure with a distinguished
+hole" — which is why `get`/`set` pairs and the functor-based encodings
+coincide [[6](#ref-6)]. Gibbons and Johnson give the equational proof of
+that correspondence [[7](#ref-7)]. Van Laarhoven's representation made the
+encoding practical: a lens as a polymorphic function
+`(a -> f a) -> (s -> f s)` for all *functor* `f`, which composes with
+ordinary function composition and is what Kmett's *lens* library and
+Pickering, Gibbons and Wu's *profunctor optics* generalise [[8](#ref-8)], [[9](#ref-9)], [[10](#ref-10)].
+On the OO side the same idea appears as a many-to-one refactoring
+in Stocker's later Scala tooling [[11](#ref-11)].
+
+Concretely, the reader never needs most of that. A lens is a `get` and
+a `set`, and a `modify` defined from them; if the field is nested, the
+lenses compose. The laws are the contract, and the contract is checked,
+not hoped.
+
+## To and from
+
+<figure class="rf-figure">
+{% include_relative replace-mutable-fields-with-lenses/diagrams/koan.svg %}
+<figcaption>The koan. One equation, read in two directions: replace
+(package the reader and pure writer of a field as a lens value) to the
+right, inline (drop the lens, access the field directly) to the left.
+The three lens laws — <em>get</em> (<em>set v s</em>) = <em>v</em>,
+<em>set</em> (<em>get s</em>) <em>s</em> = <em>s</em>, and
+<em>set v&#8322;</em> (<em>set v&#8321; s</em>) = <em>set v&#8322; s</em> —
+are the equation the move is checked against.</figcaption>
+</figure>
+
+The catalogue lists each refactoring in both directions because the two
+moves are one equation read left to right and right to left. Replace a
+field with a lens: define `get` and `set` for the field, replace every
+read with `get`, every write with `set` or `modify`, and where the
+field is nested compose the lenses. Inline a lens: replace `get`, `set`
+and `modify` at their use sites with direct access, and delete the
+lens. The lens laws say both directions are behaviour-preserving:
+`get (set v s) = v` is the forward equation, `set (get s) s = s` the
+backward one, and `set v₂ (set v₁ s) = set v₂ s` says writing twice is
+writing the last value once [[4](#ref-4)].
+
+The directions serve different ends. Replace is for containment, so the
+writes to a field are reachable only through a pure function and any
+invariant the writer holds is visible at the one place it is held; for
+composition, because a lens along a path reaches nested records without
+repeating them; and for reuse, because a lens is a value that can be
+passed to a function that reads and writes through it. Inline is for
+simplicity, because a field that is never composed or updated is
+clearer as a field; and for removing a seam, because a lens whose
+callers couple to its mechanics rather than its meaning adds a hop, not
+a guarantee. Both directions are checked by the same property: for all
+generated inputs, the before-program and the after-program agree on the
+entry point.
+
+## Three examples
+
+Each example is the same program twice, `Before` and `After`, in Scala 3
+and in Haskell. The entry point keeps its name and its type, the lens is
+the only difference, and a hedgehog property generates inputs and demands
+that both versions agree on every one of them. The sources below are
+included verbatim from the files the tests run against.
+
+### 1 · Account balance: the field becomes a lens
+
+A single mutable field — the balance — is read and written by
+`withdraw`. The Before version spells the update out with a copy; the
+After version packages the field's `get` and pure `set` as one
+`Lens[Account, Int]` and routes the update through `modify`. The second
+property checks the three lens laws, which are the equation that makes
+the move a refactoring.
+
+<figure class="rf-figure">
+{% include_relative replace-mutable-fields-with-lenses/01-account-balance/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+Note what did *not* change: `withdraw` still returns a new account, the
+bonus field is untouched, and `modify` is a function of the lens we
+could pass elsewhere. The property compares result *values* — both
+sides return their own record type, so the test reads `.balance` and
+`.bonus` off each result.
+
+<details class="rf-spec">
+<summary>The property: <code>Before.withdraw == After.withdraw</code> on generated accounts, and the three lens laws</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+### 2 · Game and player: the composed path
+
+The player sits inside a game, and moving it means a copy-update chain
+that touches both records at every call. The After version composes
+`player . x` and `player . y` into paths and moves through them; the
+nested write is one step, not two. This is the composition property
+that made lenses famous: `compose` on lenses is exactly function
+composition read backwards, and the second property re-checks the lens
+laws for the composed path.
+
+<figure class="rf-figure">
+{% include_relative replace-mutable-fields-with-lenses/02-player-position/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+Two notes. `compose` is a few lines because the whole encoding is a few
+lines — `Lens` is just a `get` and a `set`, and `modify` is defined
+from them; a library like Kmett's or Monocle supplies the same
+combinators with more machinery behind them [[8](#ref-8)], [[11](#ref-11)]. And the
+property again compares result values, so it reads `.level`, `.player.x`
+and `.player.y` off each result rather than asserting record equality
+across two types.
+
+<details class="rf-spec">
+<summary>The property: <code>Before.moveX/moveY == After.moveX/moveY</code> on generated games, and the composed lens obeys the laws</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+### 3 · File tree: the lens inside the recursion
+
+The tree's `size` field is updated in the same recursive pass that
+walks the children. The Before version writes it directly in the
+`copy`; the After version routes the write through a lens and leaves
+the recursion alone. This is the inverse picture from example 2: here
+the lens is *not* composed — there is one record type and one field —
+and the reason to use it is that the write is a named, checked step of
+the traversal rather than an anonymous copy. The second property checks
+the lens laws on generated nodes.
+
+<figure class="rf-figure">
+{% include_relative replace-mutable-fields-with-lenses/03-file-tree/diagram.svg %}
+</figure>
+
+<div class="rf-pair">
+<div><h4>Before · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Before.scala %}{% endhighlight %}
+</div>
+<div><h4>Before · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Before.hs %}{% endhighlight %}
+</div>
+</div>
+
+<div class="rf-pair">
+<div><h4>After · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/After.scala %}{% endhighlight %}
+</div>
+<div><h4>After · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/After.hs %}{% endhighlight %}
+</div>
+</div>
+
+A design choice is worth stating: example 3 uses one *total* lens whose
+focus is a single field, not a lens over "all files in the tree". Every
+node has a `size`, so the lens is total, the property can test it on any
+node, and the recursion is unchanged. "All the files" is a traversal,
+not a lens — a different abstraction with its own laws — and the page
+stays within the lens equation.
+
+<details class="rf-spec">
+<summary>The property: <code>Before.bumpSizes == After.bumpSizes</code> on generated trees, and the size lens obeys the laws</summary>
+<div class="rf-pair">
+<div><h4>Spec · Scala</h4>
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Spec.scala %}{% endhighlight %}
+</div>
+<div><h4>Spec · Haskell</h4>
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Spec.hs %}{% endhighlight %}
+</div>
+</div>
+</details>
+
+## Pitfalls
+
+The equation has hypotheses, and each is one of the constructive
+criteria. Where a hypothesis fails, replacing a field with a lens
+changes the program. In a language with referential transparency the OO
+precondition does not become easier to satisfy; it disappears, and the
+move becomes an equation. The structures that make that true are
+gathered in the footnote at the end of this section.
+
+- **Partial lenses.** A lens whose `get` is not defined on part of the
+  source type — reading a field out of a sum type where one branch does
+  not carry it — must `error`/`sys.error` on that region, and the laws
+  can only be checked where the lens is defined. Totality is exactly
+  the condition that makes a lens a lens everywhere; prefer a record
+  shape where every value has the field, or use a prism/traversal for
+  the partial case.
+- **Laziness and evaluation count.** A lens's `set` is lazy in the new
+  value in Haskell — `set l (f s) s'` does not force `f s` unless the
+  result needs it — and `modify f = set l . f . get l` can force `f`
+  earlier than a direct field write would. Where the program is lazy
+  about an untouched field (a bonus never read, an id never shown),
+  `undefined` in that field is a probe: before and after must both
+  tolerate it. In Scala a `def` recomputes and a `val` shares; a lens
+  stored as a `val` builds its functions once.
+- **Strictness.** A `modify` reads the focus, applies a function and
+  writes it back; if the focus is bottom, the read is forced and the
+  result differs from a direct write that never looked. Totality, no
+  `undefined` and no partial functions, is exactly the condition under
+  which this cannot arise. Example 1 probes it with `undefined` in the
+  untouched field.
+- **Composition direction.** `compose outer inner` focuses `inner`
+  *inside* `outer`; the reader writes `inner` after `outer`, and
+  getting the order backwards is a type error, not a runtime bug. Two
+  lenses with the same source do not compose at all — there is no
+  single focus — which is what stops the "compose a pair" mistake from
+  even compiling.
+- **The laws as a contract.** A `(get, set)` pair is a lens only when
+  the three laws hold; a pair that violates PutPut is a lens in name
+  only. Any consumer of a lens — including the ones in examples 2 and 3
+  — relies on them, so the property that checks them is not decoration.
+
+In each case the fix is the same: restore the hypothesis, by keeping
+the lens total, by using a `val` where sharing matters, and by testing
+the laws; or admit that this is not a refactoring and test it as a
+change.
+
+<details class="rf-spec">
+<summary>The functional reading</summary>
+<div markdown="1">
+
+A lens is a focus with a reader and a writer. In a referentially
+transparent language a record `s` with field `a` gives a lens whose
+`get` is the field accessor and whose `set` is the copy-update; the two
+are one value because the field is a projection, not a location. Nested
+records compose because a projection of a projection is a projection:
+`compose outer inner` selects `inner` inside `outer`, and the
+read-modify-write `modify` is `set` after `get` after `f`.
+
+This is not a new idea dressed up. Foster, Greenwald, Moore, Pierce and
+Schmitt introduced the *very well-behaved lens* laws (GetPut, PutGet,
+PutPut) and proved that their combinators — composition, map, recursion
+— preserve them, which made it possible to assemble large bidirectional
+transformations from small, verified lenses [[4](#ref-4)]. O'Connor showed
+lenses are the coalgebras for the costate comonad, the categorical
+shape of "a structure with one hole", and conjectured the equivalence
+of the store and functor encodings [[6](#ref-6)]; Gibbons and Johnson proved
+the correspondence [[7](#ref-7)]. Van Laarhoven's representation, a lens as a
+polymorphic function `(a -> f a) -> (s -> f s)` for every functor `f`,
+is what the *lens* library builds on [[8](#ref-8)], [[9](#ref-9)]; Pickering, Gibbons and
+Wu's *profunctor optics* shows the same idea scales to prisms and
+traversals by generalising the arrow [[10](#ref-10)]. Monocle gives Scala the
+same library treatment [[12](#ref-12)].
+
+That is the point. With referential transparency the OO precondition —
+no direct writes — does not become easier to satisfy; it disappears,
+because the writer is a pure function and the type checker enforces the
+corridor. Replacing a field with a lens stops being something you hope
+preserved behaviour and becomes an equation you wrote down.
+
+</div>
+</details>
+
+## Verification
+
+Because the move is an equation, its correctness is a property: for all
+inputs *x* in the domain of the entry point, `Before x == After x`. That
+is a one-line property in the sense Claessen and Hughes introduced with
+QuickCheck, where a generator produces inputs and the framework searches
+for a counterexample and shrinks it to a minimal one [[13](#ref-13)]. The catalogue
+states every entry this way, in Scala and in Haskell, with hedgehog on
+both sides [[14](#ref-14)]. Hedgehog is used because its shrinking is integrated
+into the generator, so a shrunk counterexample obeys the same invariants
+as a generated one and the minimal failing input it reports is a real
+input of the program, not an artefact of a separate shrinker. The lens
+laws are second properties — the equation the move is checked against,
+stated directly.
+
+A property is only worth having if it can fail, so each spec above was
+mutation-checked: change `After` so it is no longer equivalent — flip a
+sign, swap a boundary, drop a case — confirm the property reports and
+shrinks a counterexample, then restore `After`. A property that does
+not fail under mutation is testing the generator, not the refactoring.
+The lens examples are especially well protected: the laws are stated
+for the *lens itself*, so a setter that drops the other fields fails
+the laws before it ever reaches the equality property.
+
+To run everything on this page yourself, from a checkout of
+[the site repository](https://github.com/Constructive-Programming/website):
+
+```sh
+sh pages/refactorings/replace-mutable-fields-with-lenses/run.sh
+```
+
+It needs [scala-cli](https://scala-cli.virtuslab.org/) and either GHC
+with hedgehog installed or Docker, and ends with `all properties passed`.
+
+## References
+
+<ol>
+<li id="ref-1">Martin Fowler. <em>Refactoring: Improving the Design of Existing Code</em>. Addison-Wesley, 1999. Chapter on self-encapsulation and the <em>Encapsulate Field</em> catalogue entry. <a href="https://martinfowler.com/books/refactoring.html">https://martinfowler.com/books/refactoring.html</a></li>
+<li id="ref-2">Martin Fowler. <em>Encapsulate Variable</em> (formerly <em>Encapsulate Field</em>). Refactoring.com, online edition. <a href="https://refactoring.com/catalog/encapsulateField.html">https://refactoring.com/catalog/encapsulateField.html</a></li>
+<li id="ref-3">Martin Fowler. <em>Remove Setting Method</em>. Refactoring.com, online edition. <a href="https://refactoring.com/catalog/removeSettingMethod.html">https://refactoring.com/catalog/removeSettingMethod.html</a></li>
+<li id="ref-4">J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce and Alan Schmitt. &ldquo;Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem&rdquo;. <em>ACM Transactions on Programming Languages and Systems</em> 29(3):17, 2007 (also POPL 2005). <a href="https://doi.org/10.1145/1232420.1232424">https://doi.org/10.1145/1232420.1232424</a></li>
+<li id="ref-5">Edward Kmett and contributors. <em>lens: Lenses, Folds and Traversals</em>. The library documentation states the three lens laws (get-put, put-get, put-put) that a lens must satisfy. <a href="https://hackage.haskell.org/package/lens">https://hackage.haskell.org/package/lens</a></li>
+<li id="ref-6">Russell O&rsquo;Connor. &ldquo;Functor is to Lens as Applicative is to Biplate: Introducing Multiplate&rdquo;. In <em>Proceedings of the ACM SIGPLAN Workshop on Generic Programming (WGP 2011)</em>, pp. 25&ndash;36. <a href="https://arxiv.org/abs/1103.2841">https://arxiv.org/abs/1103.2841</a> (also the costate-comonad characterisation, arXiv version)</li>
+<li id="ref-7">Jeremy Gibbons and Michael Johnson. &ldquo;Relating Algebraic and Coalgebraic Descriptions of Lenses&rdquo;. <em>Electronic Communications of the EASST</em> 49:1&ndash;16, 2012 (Workshop on Bidirectional Transformations 2012). <a href="https://doi.org/10.14279/tuj.eceasst.49.726">https://doi.org/10.14279/tuj.eceasst.49.726</a></li>
+<li id="ref-8">Twan van Laarhoven. &ldquo;Talk on Lenses&rdquo;. Slides, Radboud University Nijmegen, 17 May 2011. Introduced the functor-based (van Laarhoven) representation. <a href="https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk">https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk</a></li>
+<li id="ref-9">Edward Kmett. <em>Control.Lens</em>. Hackage package documentation for the <em>lens</em> library. <a href="https://hackage.haskell.org/package/lens/docs/Control-Lens.html">https://hackage.haskell.org/package/lens/docs/Control-Lens.html</a></li>
+<li id="ref-10">Matthew Pickering, Jeremy Gibbons and Nicolas Wu. &ldquo;Profunctor Optics: Modular Data Accessors&rdquo;. <em>The Art, Science, and Engineering of Programming</em> 1(2):7, 2017. <a href="https://doi.org/10.22152/programming-journal.org/2017/1/7">https://doi.org/10.22152/programming-journal.org/2017/1/7</a></li>
+<li id="ref-11">Mirko Stocker. <em>Scala Refactoring</em>. Master&rsquo;s thesis, HSR Hochschule f&uuml;r Technik Rapperswil, 2010. Catalogues pure-function accessor refactorings including field encapsulation. <a href="https://eprints.ost.ch/id/eprint/286/">https://eprints.ost.ch/id/eprint/286/</a></li>
+<li id="ref-12">Julien Truffaut and contributors. <em>Monocle: Optics Library for Scala</em>. <a href="https://www.optics.dev/Monocle/">https://www.optics.dev/Monocle/</a></li>
+<li id="ref-13">Koen Claessen and John Hughes. &ldquo;QuickCheck: a lightweight tool for random testing of Haskell programs&rdquo;. In <em>Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2000)</em>, pp. 268&ndash;279. <a href="https://doi.org/10.1145/351240.351266">https://doi.org/10.1145/351240.351266</a></li>
+<li id="ref-14">Jacob Stanley and contributors. <em>Hedgehog: release with confidence, state-of-the-art property testing</em>. <a href="https://github.com/hedgehogqa/haskell-hedgehog">https://github.com/hedgehogqa/haskell-hedgehog</a> and <a href="https://github.com/hedgehogqa/scala-hedgehog">https://github.com/hedgehogqa/scala-hedgehog</a></li>
+</ol>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
new file mode 100644
index 0000000..57e1357
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
@@ -0,0 +1,17 @@
+-- Same, with a lens on the balance: the getter and the pure setter
+-- packed as one value.
+module After where
+
+data Account = Account { balance :: Int, bonus :: Int }
+  deriving (Eq, Show)
+
+data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
+
+modify :: Lens s a -> (a -> a) -> s -> s
+modify l f s = set l (f (get l s)) s
+
+balanceLens :: Lens Account Int
+balanceLens = Lens { get = balance, set = \b a -> a { balance = b } }
+
+withdraw :: Account -> Int -> Account
+withdraw a amount = modify balanceLens (subtract amount) a
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
new file mode 100644
index 0000000..a96d327
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
@@ -0,0 +1,13 @@
+// Same, with a lens on the balance: the getter and the pure setter
+// packed as one value.
+object After:
+  case class Account(balance: Int, bonus: Int)
+
+  case class Lens[S, A](get: S => A, set: A => S => S):
+    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
+
+  val balance: Lens[Account, Int] =
+    Lens[Account, Int](_.balance, b => a => a.copy(balance = b))
+
+  def withdraw(a: Account, amount: Int): Account =
+    balance.modify(_ - amount)(a)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
new file mode 100644
index 0000000..ecac13b
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
@@ -0,0 +1,7 @@
+-- Withdraw from an account: the balance changes, the bonus does not.
+module Before where
+
+data Account = Account { balance :: Int, bonus :: Int }
+
+withdraw :: Account -> Int -> Account
+withdraw a amount = a { balance = balance a - amount }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
new file mode 100644
index 0000000..7cb97d7
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
@@ -0,0 +1,6 @@
+// Withdraw from an account: the balance changes, the bonus does not.
+object Before:
+  case class Account(balance: Int, bonus: Int)
+
+  def withdraw(a: Account, amount: Int): Account =
+    a.copy(balance = a.balance - amount)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
new file mode 100644
index 0000000..e55a959
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-30) 30)
+
+prop_agrees :: Property
+prop_agrees = property $ do
+  b  <- forAll genInt
+  bn <- forAll genInt
+  am <- forAll genInt
+  let before = Before.withdraw (Before.Account b bn) am
+      after  = After.withdraw (After.Account b bn) am
+  (Before.balance before, Before.bonus before)
+    === (After.balance after, After.bonus after)
+
+-- A lens has to satisfy the three equations; they are exactly what
+-- makes replacing a field with a get/set pair a refactoring.
+prop_laws :: Property
+prop_laws = property $ do
+  b  <- forAll genInt
+  bn <- forAll genInt
+  v1 <- forAll genInt
+  v2 <- forAll genInt
+  let l = After.balanceLens
+      a = After.Account b bn
+  After.set l (After.get l a) a === a
+  After.get l (After.set l v1 a) === v1
+  After.set l v2 (After.set l v1 a) === After.set l v2 a
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("withdraw: Before == After", prop_agrees)
+    , ("balance lens obeys get-put, put-get, put-put", prop_laws)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
new file mode 100644
index 0000000..44f4344
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
@@ -0,0 +1,46 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("withdraw: Before == After", agrees),
+    property("the balance lens obeys get-put, put-get, put-put", laws),
+  )
+
+  // Raw values, so the same input feeds both Account types.
+  val genInt: Gen[Int] = Gen.int(Range.linear(-30, 30))
+
+  def agrees: Property =
+    for
+      b  <- genInt.forAll
+      bn <- genInt.forAll
+      am <- genInt.forAll
+    yield
+      val before = Before.withdraw(Before.Account(b, bn), am)
+      val after  = After.withdraw(After.Account(b, bn), am)
+      (before.balance, before.bonus) ==== (after.balance, after.bonus)
+
+  def laws: Property =
+    for
+      b  <- genInt.forAll
+      bn <- genInt.forAll
+      v1 <- genInt.forAll
+      v2 <- genInt.forAll
+    yield
+      val a = After.Account(b, bn)
+      val l = After.balance
+      l.get(l.set(v1)(a)) ==== v1 and
+        l.set(l.get(a))(a) ==== a and
+        l.set(v2)(l.set(v1)(a)) ==== l.set(v2)(a)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
new file mode 100644
index 0000000..3c855bd
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
@@ -0,0 +1,46 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 196" role="img" aria-labelledby="d1-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d1-title">Replacing the balance field with a lens in the withdraw program. Before: withdraw(Account(balance, bonus), amount) reads balance with a.balance and writes it with a.copy(balance = a.balance - amount); the dotted region is the field access and copy spell-out. After: withdraw is balance.modify(_ - amount)(a), where balanceLens = Lens(get = _.balance, set = b => a => a.copy(balance = b)).</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="148" rx="4"/>
+    <rect x="428" y="36" width="336" height="92" rx="4"/>
+    <rect x="428" y="150" width="336" height="34" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="84" width="336" height="66" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">withdraw(a: Account, amount) =</text>
+    <text x="40" y="76">a.copy(balance = a.balance - amount)</text>
+    <text x="52" y="98">read: a.balance</text>
+    <text x="52" y="116">write: a.copy(balance = ...)</text>
+    <text x="52" y="134">every call site spells out the</text>
+    <text x="52" y="148">field update by hand</text>
+    <text x="440" y="58">withdraw(a, amount) =</text>
+    <text x="452" y="76">balanceLens.modify(_ - amount)(a)</text>
+    <text x="440" y="100">balanceLens =</text>
+    <text x="452" y="120">Lens(get = _.balance,</text>
+    <text x="452" y="136">     set = ...)</text>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle" opacity=".85">
+    <text x="212" y="168">field access + copy spell-out</text>
+    <text x="596" y="172">get and set packed as one value</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="112" r="7.5"/>
+    <circle cx="428" cy="156" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="116">1</text>
+    <text x="428" y="160">1</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M386 132 V144"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M382.5 144 L386 152 L389.5 144 Z"/>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
new file mode 100644
index 0000000..8469200
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
@@ -0,0 +1,40 @@
+-- Same, with a composed path: player . x and player . y reach the
+-- nested field in one step, no copy chain.
+module After where
+
+data Player = Player { pid :: String, px :: Int, py :: Int }
+  deriving (Eq, Show)
+data Game   = Game   { level :: Int, gplayer :: Player }
+  deriving (Eq, Show)
+
+data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
+
+modify :: Lens s a -> (a -> a) -> s -> s
+modify l f s = set l (f (get l s)) s
+
+compose :: Lens s m -> Lens m a -> Lens s a
+compose outer inner = Lens
+  { get = get inner . get outer
+  , set = \a s -> set outer (set inner a (get outer s)) s
+  }
+
+player :: Lens Game Player
+player = Lens { get = gplayer, set = \p g -> g { gplayer = p } }
+
+x :: Lens Player Int
+x = Lens { get = px, set = \v p -> p { px = v } }
+
+y :: Lens Player Int
+y = Lens { get = py, set = \v p -> p { py = v } }
+
+playerX :: Lens Game Int
+playerX = compose player x
+
+playerY :: Lens Game Int
+playerY = compose player y
+
+moveX :: Game -> Int -> Game
+moveX g dx = modify playerX (+ dx) g
+
+moveY :: Game -> Int -> Game
+moveY g dy = modify playerY (+ dy) g
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
new file mode 100644
index 0000000..7350171
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
@@ -0,0 +1,27 @@
+// Same, with a composed path: player . x and player . y reach the
+// nested field in one step, no copy chain.
+object After:
+  case class Player(id: String, x: Int, y: Int)
+  case class Game(level: Int, player: Player)
+
+  case class Lens[S, A](get: S => A, set: A => S => S):
+    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
+
+  def compose[S, M, A](outer: Lens[S, M],
+                       inner: Lens[M, A]): Lens[S, A] =
+    Lens[S, A](s => inner.get(outer.get(s)),
+      a => s => outer.set(inner.set(a)(outer.get(s)))(s))
+
+  val player: Lens[Game, Player] =
+    Lens[Game, Player](_.player, p => g => g.copy(player = p))
+
+  val x: Lens[Player, Int] =
+    Lens[Player, Int](_.x, v => p => p.copy(x = v))
+  val y: Lens[Player, Int] =
+    Lens[Player, Int](_.y, v => p => p.copy(y = v))
+
+  val playerX: Lens[Game, Int] = compose(player, x)
+  val playerY: Lens[Game, Int] = compose(player, y)
+
+  def moveX(g: Game, dx: Int): Game = playerX.modify(_ + dx)(g)
+  def moveY(g: Game, dy: Int): Game = playerY.modify(_ + dy)(g)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
new file mode 100644
index 0000000..8061f77
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
@@ -0,0 +1,12 @@
+-- Move the player inside a game: the nested copy-update touches
+-- both records at every move.
+module Before where
+
+data Player = Player { pid :: String, px :: Int, py :: Int }
+data Game   = Game   { level :: Int, gplayer :: Player }
+
+moveX :: Game -> Int -> Game
+moveX g dx = g { gplayer = (gplayer g) { px = px (gplayer g) + dx } }
+
+moveY :: Game -> Int -> Game
+moveY g dy = g { gplayer = (gplayer g) { py = py (gplayer g) + dy } }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
new file mode 100644
index 0000000..3f905eb
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
@@ -0,0 +1,11 @@
+// Move the player inside a game: the nested copy-update touches
+// both records at every move.
+object Before:
+  case class Player(id: String, x: Int, y: Int)
+  case class Game(level: Int, player: Player)
+
+  def moveX(g: Game, dx: Int): Game =
+    g.copy(player = g.player.copy(x = g.player.x + dx))
+
+  def moveY(g: Game, dy: Int): Game =
+    g.copy(player = g.player.copy(y = g.player.y + dy))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
new file mode 100644
index 0000000..ab8feb0
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+genInt :: Gen Int
+genInt = Gen.int (Range.linear (-30) 30)
+
+genId :: Gen String
+genId = ("p" <>) . show <$> Gen.int (Range.linear 0 9)
+
+prop_agrees :: Property
+prop_agrees = property $ do
+  id <- forAll genId
+  lv <- forAll genInt
+  px <- forAll genInt
+  py <- forAll genInt
+  dx <- forAll genInt
+  dy <- forAll genInt
+  let bg = Before.Game lv (Before.Player id px py)
+      ag = After.Game lv (After.Player id px py)
+      b1 = Before.moveX bg dx
+      b2 = Before.moveY bg dy
+      a1 = After.moveX ag dx
+      a2 = After.moveY ag dy
+  (Before.level b1, Before.px (Before.gplayer b1),
+   Before.py (Before.gplayer b1))
+    === (After.level a1, After.px (After.gplayer a1),
+         After.py (After.gplayer a1))
+  (Before.level b2, Before.px (Before.gplayer b2),
+   Before.py (Before.gplayer b2))
+    === (After.level a2, After.px (After.gplayer a2),
+         After.py (After.gplayer a2))
+
+-- The composed path is still a lens: get and set through player . x
+-- satisfy the three equations.
+prop_laws :: Property
+prop_laws = property $ do
+  id <- forAll genId
+  lv <- forAll genInt
+  px <- forAll genInt
+  py <- forAll genInt
+  v1 <- forAll genInt
+  v2 <- forAll genInt
+  let l = After.playerX
+      g = After.Game lv (After.Player id px py)
+  After.set l (After.get l g) g === g
+  After.get l (After.set l v1 g) === v1
+  After.set l v2 (After.set l v1 g) === After.set l v2 g
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("moveX/moveY: Before == After", prop_agrees)
+    , ("composed path lens player.x obeys the laws", prop_laws)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
new file mode 100644
index 0000000..3dcb8d9
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
@@ -0,0 +1,69 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("moveX: Before == After", agreesX),
+    property("moveY: Before == After", agreesY),
+    property("the composed path lens player.x obeys the laws", laws),
+  )
+
+  // Raw values, so the same input feeds both Game types.
+  val genInt: Gen[Int] = Gen.int(Range.linear(-30, 30))
+  val genId: Gen[String] =
+    for n <- Gen.int(Range.linear(0, 9)) yield "p" + n.toString
+
+  def agreesX: Property =
+    for
+      id <- genId.forAll
+      lv <- genInt.forAll
+      px <- genInt.forAll
+      py <- genInt.forAll
+      dx <- genInt.forAll
+    yield
+      val b =
+        Before.moveX(Before.Game(lv, Before.Player(id, px, py)), dx)
+      val a = After.moveX(After.Game(lv, After.Player(id, px, py)), dx)
+      (b.level, b.player.id, b.player.x, b.player.y)
+        ==== (a.level, a.player.id, a.player.x, a.player.y)
+
+  def agreesY: Property =
+    for
+      id <- genId.forAll
+      lv <- genInt.forAll
+      px <- genInt.forAll
+      py <- genInt.forAll
+      dy <- genInt.forAll
+    yield
+      val b =
+        Before.moveY(Before.Game(lv, Before.Player(id, px, py)), dy)
+      val a = After.moveY(After.Game(lv, After.Player(id, px, py)), dy)
+      (b.level, b.player.id, b.player.x, b.player.y)
+        ==== (a.level, a.player.id, a.player.x, a.player.y)
+
+  def laws: Property =
+    for
+      id <- genId.forAll
+      lv <- genInt.forAll
+      px <- genInt.forAll
+      py <- genInt.forAll
+      v1 <- genInt.forAll
+      v2 <- genInt.forAll
+    yield
+      val g  = After.Game(lv, After.Player(id, px, py))
+      val l  = After.playerX
+      l.get(l.set(v1)(g)) ==== v1 and
+        l.set(l.get(g))(g) ==== g and
+        l.set(v2)(l.set(v1)(g)) ==== l.set(v2)(g)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
new file mode 100644
index 0000000..dae6b92
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
@@ -0,0 +1,41 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 200" role="img" aria-labelledby="d2-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d2-title">Replacing nested copy-updates with a composed lens path. Before: moveX(g, dx) writes g.copy(player = g.player.copy(x = g.player.x + dx)) — the copy chain touches level, player and x. After: playerX = compose player x is one lens, and moveX(g, dx) = playerX.modify(_ + dx)(g); playerX reads g.player.x and writes the nested record in one step.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="128" rx="4"/>
+    <rect x="428" y="36" width="336" height="128" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="66" width="332" height="58" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">moveX(g, dx) =</text>
+    <text x="40" y="76">g.copy(player =</text>
+    <text x="52" y="94">g.player.copy(x = g.player.x + dx))</text>
+    <text x="52" y="118">copy chain: level</text>
+    <text x="52" y="134">then player then x</text>
+    <text x="440" y="58">playerX = compose player x</text>
+    <text x="452" y="76">moveX(g, dx) =</text>
+    <text x="464" y="94">playerX.modify(_ + dx)(g)</text>
+    <text x="452" y="118">one lens reach:</text>
+    <text x="452" y="134">reads g.player.x,</text>
+    <text x="452" y="150">writes the whole path</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="94" r="7.5"/>
+    <circle cx="428" cy="94" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="98">1</text>
+    <text x="428" y="98">1</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M406 94 H414"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M414 90.5 L422 94 L414 97.5 Z"/>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
new file mode 100644
index 0000000..fccc9f3
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
@@ -0,0 +1,19 @@
+-- Same, with a lens on the size field: the write goes through the
+-- lens; the recursion over children is unchanged.
+module After where
+
+data Node = Node { name :: String, size :: Int, children :: [Node] }
+  deriving (Eq, Show)
+
+data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
+
+modify :: Lens s a -> (a -> a) -> s -> s
+modify l f s = set l (f (get l s)) s
+
+sizeLens :: Lens Node Int
+sizeLens = Lens { get = size, set = \v n -> n { size = v } }
+
+bumpSizes :: Node -> Int -> Node
+bumpSizes n by =
+  modify sizeLens (+ by)
+    (n { children = map (`bumpSizes` by) (children n) })
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
new file mode 100644
index 0000000..8d5de15
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
@@ -0,0 +1,14 @@
+// Same, with a lens on the size field: the write goes through the
+// lens; the recursion over children is unchanged.
+object After:
+  case class Node(name: String, size: Int, children: List[Node])
+
+  case class Lens[S, A](get: S => A, set: A => S => S):
+    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
+
+  val size: Lens[Node, Int] =
+    Lens[Node, Int](_.size, v => n => n.copy(size = v))
+
+  def bumpSizes(n: Node, by: Int): Node =
+    size.modify(_ + by)(
+      n.copy(children = n.children.map(bumpSizes(_, by))))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
new file mode 100644
index 0000000..8db5c56
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
@@ -0,0 +1,11 @@
+-- Grow the size of every node of a file tree by the same amount.
+module Before where
+
+data Node = Node { name :: String, size :: Int, children :: [Node] }
+  deriving (Eq, Show)
+
+bumpSizes :: Node -> Int -> Node
+bumpSizes n by =
+  n { size = size n + by
+    , children = map (`bumpSizes` by) (children n)
+    }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
new file mode 100644
index 0000000..bb46c12
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
@@ -0,0 +1,8 @@
+// Grow the size of every node of a file tree by the same amount.
+object Before:
+  case class Node(name: String, size: Int, children: List[Node])
+
+  def bumpSizes(n: Node, by: Int): Node =
+    n.copy(
+      size = n.size + by,
+      children = n.children.map(bumpSizes(_, by)))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
new file mode 100644
index 0000000..51bc397
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+genName :: Gen String
+genName = ("n" <>) . show <$> Gen.int (Range.linear 0 9)
+
+genSize :: Gen Int
+genSize = Gen.int (Range.linear (-20) 20)
+
+genNode :: Int -> Gen Before.Node
+genNode depth =
+  let leaf = Before.Node <$> genName <*> genSize <*> pure []
+  in if depth == 0 then leaf
+     else Gen.choice
+       [ leaf
+       , Before.Node <$> genName <*> genSize
+           <*> Gen.list (Range.linear 0 3) (genNode (depth - 1))
+       ]
+
+toAfter :: Before.Node -> After.Node
+toAfter (Before.Node n s cs) = After.Node n s (map toAfter cs)
+
+-- toAfter maps a whole tree faithfully, so After's result can be
+-- compared with the converted Before result.
+prop_agrees :: Property
+prop_agrees = property $ do
+  n  <- forAll (genNode 3)
+  by <- forAll genSize
+  After.bumpSizes (toAfter n) by === toAfter (Before.bumpSizes n by)
+
+prop_laws :: Property
+prop_laws = property $ do
+  n  <- forAll (genNode 1)
+  v1 <- forAll genSize
+  v2 <- forAll genSize
+  let l   = After.sizeLens
+      m   = toAfter n
+  After.get l (After.set l v1 m) === v1
+  After.set l (After.get l m) m === m
+  After.set l v2 (After.set l v1 m) === After.set l v2 m
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("bumpSizes: Before == After", prop_agrees)
+    , ("size lens obeys the laws on generated nodes", prop_laws)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
new file mode 100644
index 0000000..0093363
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
@@ -0,0 +1,68 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("bumpSizes: Before == After", agrees),
+    property("the size lens obeys get-put, put-get, put-put", laws),
+  )
+
+  val genName: Gen[String] =
+    for n <- Gen.int(Range.linear(0, 9)) yield "n" + n.toString
+  val genSize: Gen[Int] = Gen.int(Range.linear(-20, 20))
+
+  def genNode(depth: Int): Gen[Before.Node] =
+    val leaf =
+      for n <- genName; s <- genSize yield Before.Node(n, s, Nil)
+    if depth == 0 then leaf
+    else
+      Gen.choice1(
+        leaf,
+        for
+          n  <- genName
+          s  <- genSize
+          cs <- genNode(depth - 1).list(Range.linear(0, 3))
+        yield Before.Node(n, s, cs)
+        ,
+      )
+
+  def toAfter(n: Before.Node): After.Node = n match
+    case Before.Node(nm, s, cs) => After.Node(nm, s, cs.map(toAfter))
+
+  def same(b: Before.Node, a: After.Node): Boolean = (b, a) match
+    case (Before.Node(n1, s1, c1), After.Node(n2, s2, c2)) =>
+      n1 == n2 && s1 == s2 && c1.size == c2.size &&
+        c1.zip(c2).forall((x, y) => same(x, y))
+
+  def agrees: Property =
+    for
+      n  <- genNode(3).forAll
+      by <- genSize.forAll
+    yield
+      val b = Before.bumpSizes(n, by)
+      val a = After.bumpSizes(toAfter(n), by)
+      same(b, a) ==== true
+
+  def laws: Property =
+    for
+      n  <- genNode(1).forAll
+      v1 <- genSize.forAll
+      v2 <- genSize.forAll
+    yield
+      val l = After.size
+      val m = toAfter(n)
+      l.get(l.set(v1)(m)) ==== v1 and
+        l.set(l.get(m))(m) ==== m and
+        l.set(v2)(l.set(v1)(m)) ==== l.set(v2)(m)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg
new file mode 100644
index 0000000..cbff7fb
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg
@@ -0,0 +1,40 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 200" role="img" aria-labelledby="d3-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d3-title">Replacing a direct field write with a lens inside a recursive traversal. Before: bumpSizes(n, by) writes n.copy(size = n.size + by) then recurses over children. After: bumpSizes uses sizeLens.modify(_ + by)(n) to write the size and recurses over children unchanged; the recursion and the write are two independent steps and the write goes through the lens.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="128" rx="4"/>
+    <rect x="428" y="36" width="336" height="128" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="76" width="332" height="34" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="58">bumpSizes(n: Node, by) =</text>
+    <text x="40" y="76">n.copy(</text>
+    <text x="52" y="94">size = n.size + by,</text>
+    <text x="52" y="112">children = children.map(bumpSizes(_, by)))</text>
+    <text x="52" y="140">field write spelled out</text>
+    <text x="440" y="58">bumpSizes(n: Node, by) =</text>
+    <text x="452" y="76">sizeLens.modify(_ + by)(</text>
+    <text x="464" y="94">n.copy(children = children.map(bumpSizes(_, by))))</text>
+    <text x="452" y="140">write through the lens,</text>
+    <text x="452" y="158">recursion unchanged</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="118" r="7.5"/>
+    <circle cx="428" cy="118" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="122">1</text>
+    <text x="428" y="122">1</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M406 118 H414"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M414 114.5 L422 118 L414 121.5 Z"/>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/diagrams/koan.svg b/pages/refactorings/replace-mutable-fields-with-lenses/diagrams/koan.svg
new file mode 100644
index 0000000..77bf53c
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/diagrams/koan.svg
@@ -0,0 +1,38 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 640 196" role="img" aria-labelledby="koan-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="koan-title">Replace mutable fields with lenses / replace lenses with mutable fields. Left: a record field read and written directly, spelled out at every call site. Right: the same field as a lens value packaging get :: s -> a and set :: a -> s -> s, so every read is get, every write is set or modify. The arrow to the right is replace (package get and set as one composable value); the arrow to the left is inline (drop the lens and access the field directly). The three lens laws — get (set v s) = v, set (get s) s = s, set v2 (set v1 s) = set v2 s — are the equation the move is checked against.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="28">before</text>
+    <text x="424" y="28">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="40" width="200" height="104" rx="4"/>
+    <rect x="424" y="40" width="200" height="104" rx="4"/>
+  </g>
+  <g fill="currentColor" font-size="14" text-anchor="middle">
+    <text x="116" y="66">field <tspan font-style="italic" font-weight="700">balance</tspan></text>
+    <text x="524" y="62">balanceLens =</text>
+    <text x="524" y="84">Lens { get, set }</text>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle" opacity=".9">
+    <text x="116" y="92">read: <tspan font-style="italic">a.balance</tspan></text>
+    <text x="116" y="110">write: <tspan font-style="italic">copy</tspan> with balance</text>
+    <text x="116" y="132">every call site spells the</text>
+    <text x="116" y="146">field out again</text>
+    <text x="524" y="108">read: <tspan font-weight="700">get</tspan> balanceLens</text>
+    <text x="524" y="128">write: <tspan font-weight="700">set</tspan> / <tspan font-weight="700">modify</tspan></text>
+    <text x="524" y="148">lens composes along paths</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M232 76 H398"/>
+    <path d="M408 116 H242"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M398 72.5 L406 76 L398 79.5 Z"/>
+    <path d="M242 112.5 L234 116 L242 119.5 Z"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="320" y="62">replace (package get + set into a lens)</text>
+    <text x="320" y="132">inline (drop the lens, access the field)</text>
+  </g>
+  <text x="320" y="176" fill="currentColor" font-size="12" text-anchor="middle" opacity=".75"><tspan font-style="italic">get</tspan> (<tspan font-style="italic">set v s</tspan>) = <tspan font-style="italic">v</tspan> &#183; <tspan font-style="italic">set</tspan> (<tspan font-style="italic">get s</tspan>) <tspan font-style="italic">s</tspan> = <tspan font-style="italic">s</tspan> &#183; <tspan font-style="italic">set v&#8322;</tspan> (<tspan font-style="italic">set v&#8321; s</tspan>) = <tspan font-style="italic">set v&#8322; s</tspan></text>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/run.sh b/pages/refactorings/replace-mutable-fields-with-lenses/run.sh
new file mode 100755
index 0000000..7b8cb88
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/run.sh
@@ -0,0 +1,24 @@
+#!/bin/sh
+# Runs every hedgehog property for this refactoring, in both languages.
+# Each NN-*/ directory holds Before + After + Spec in Scala 3 and Haskell;
+# Spec generates inputs and asserts Before and After agree on all of them.
+#
+# Needs: scala-cli (https://scala-cli.virtuslab.org) and either ghc with
+# hedgehog on the package path, or docker (the image is built on first use).
+set -eu
+cd "$(dirname "$0")"
+
+if command -v ghc >/dev/null 2>&1 && ghc-pkg list hedgehog 2>/dev/null | grep -q hedgehog; then
+  hs() { runghc -i"$1" "$1/Spec.hs"; }
+else
+  docker image inspect cp-hedgehog >/dev/null 2>&1 || \
+    printf 'FROM haskell:9.8-slim\nRUN cabal update && cabal install --lib hedgehog\n' | docker build -t cp-hedgehog -
+  hs() { docker run --rm -v "$PWD:/w" -w /w cp-hedgehog runghc -i"$1" "$1/Spec.hs"; }
+fi
+
+for d in [0-9][0-9]-*/; do
+  d=${d%/}
+  echo "== $d (scala)";   scala-cli run "$d" --main-class spec
+  echo "== $d (haskell)"; hs "$d"
+done
+echo "all properties passed"

From 78b60ca26ebb8bacc5eb8aafcb1e915c0531994b Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 22:10:39 +0200
Subject: [PATCH 2/6] Rework 'Replace mutable fields with lenses' per review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Examples rebuilt around the eo cookbook navigate-structures trio:
  prism×lens on one node, the same optic at every tree node, and a
  traversal×prism×lens sparse walk over a batch — all self-contained
  optic encodings running in both Scala 3 and Haskell with no deps.
- Page rewritten: optics framing (how-to-reach vs what-to-do), lawful
  by construction + law-solvers, inverse justified by decoupling not
  being worth it / no cross-domain boundaries, functional reading as
  optics (links eo), pitfalls are accidental complexity + rebuilding
  beyond the focus, verification cites cats-eo-laws / monocle-law /
  genvalidity-hspec-optics.
- All 12 properties pass both languages; mutants caught.
- Diagrams redrawn for the three new examples.
---
 .../replace-mutable-fields-with-lenses.md     | 579 ++++++++----------
 .../01-account-balance/After.hs               |  17 -
 .../01-account-balance/After.scala            |  13 -
 .../01-account-balance/Before.hs              |   7 -
 .../01-account-balance/Before.scala           |   6 -
 .../01-account-balance/Spec.hs                |  45 --
 .../01-account-balance/Spec.scala             |  46 --
 .../01-account-balance/diagram.svg            |  46 --
 .../01-rename-var/After.hs                    |  58 ++
 .../01-rename-var/After.scala                 |  45 ++
 .../01-rename-var/Before.hs                   |  14 +
 .../01-rename-var/Before.scala                |  14 +
 .../01-rename-var/Spec.hs                     |  75 +++
 .../01-rename-var/Spec.scala                  |  85 +++
 .../01-rename-var/diagram.svg                 |  41 ++
 .../02-player-position/After.hs               |  40 --
 .../02-player-position/After.scala            |  27 -
 .../02-player-position/Before.hs              |  12 -
 .../02-player-position/Before.scala           |  11 -
 .../02-player-position/Spec.hs                |  63 --
 .../02-player-position/Spec.scala             |  69 ---
 .../02-player-position/diagram.svg            |  41 --
 .../02-rename-tree/After.hs                   |  58 ++
 .../02-rename-tree/After.scala                |  49 ++
 .../02-rename-tree/Before.hs                  |  15 +
 .../02-rename-tree/Before.scala               |  15 +
 .../02-rename-tree/Spec.hs                    |  81 +++
 .../02-rename-tree/Spec.scala                 |  83 +++
 .../02-rename-tree/diagram.svg                |  46 ++
 .../03-bump-oks/After.hs                      |  61 ++
 .../03-bump-oks/After.scala                   |  51 ++
 .../03-bump-oks/Before.hs                     |  14 +
 .../03-bump-oks/Before.scala                  |  15 +
 .../03-bump-oks/Spec.hs                       |  67 ++
 .../03-bump-oks/Spec.scala                    |  65 ++
 .../03-bump-oks/diagram.svg                   |  32 +
 .../03-file-tree/After.hs                     |  19 -
 .../03-file-tree/After.scala                  |  14 -
 .../03-file-tree/Before.hs                    |  11 -
 .../03-file-tree/Before.scala                 |   8 -
 .../03-file-tree/Spec.hs                      |  56 --
 .../03-file-tree/Spec.scala                   |  68 --
 .../03-file-tree/diagram.svg                  |  40 --
 43 files changed, 1244 insertions(+), 978 deletions(-)
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/diagram.svg
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/diagram.svg
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
 delete mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg

diff --git a/pages/refactorings/replace-mutable-fields-with-lenses.md b/pages/refactorings/replace-mutable-fields-with-lenses.md
index e39bca3..ca7da9b 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses.md
+++ b/pages/refactorings/replace-mutable-fields-with-lenses.md
@@ -1,7 +1,7 @@
 ---
 layout: page
 title: Replace Mutable Fields with Lenses
-subtitle: "Replace mutable fields with lenses: package a field's reader and pure writer as one value, and the read becomes get, the write becomes set or modify — inline the lens, and a field that is never composed just becomes a field again"
+subtitle: "Replace mutable fields with lenses: package how to reach a field and what to do with it as one optic value — read becomes get, write becomes set or modify; inline the lens, and a projection no one composes becomes a field again"
 permalink: /refactorings/replace-mutable-fields-with-lenses/
 tags: [refactorings, replace-mutable-fields-with-lenses]
 hide: true   # entry pages are reached from the catalogue, not the top-right nav
@@ -9,418 +9,354 @@ hide: true   # entry pages are reached from the catalogue, not the top-right nav
 
 <p class="rf-crumb"><a href="{{ '/refactorings/' | relative_url }}">← The refactoring catalogue</a> · 2 of 35</p>
 
-A mutable field is a place where the class's invariants can be broken:
+A mutable field is a place where a class's invariants can be broken:
 any method can read it, any method can write it, and nothing stops a
 write from putting the object into a state the other methods did not
-anticipate. Object-oriented refactoring has a ladder of moves up this
-smell — Fowler's *Encapsulate Variable* (the catalogue entry that used
-to be *Encapsulate Field*, and before that *Self-Encapsulate Field*)
-hides the field behind accessor methods [[1](#ref-1)], [[2](#ref-2)], and *Remove Setting
-Method* then removes the setter once the field no longer needs to be
+anticipate. The object-oriented ladder up this smell is well worn —
+Fowler's *Encapsulate Variable* (the catalogue entry that used to be
+*Encapsulate Field*, and before that *Self-Encapsulate Field*) hides
+the field behind accessor methods [[1](#ref-1)], [[2](#ref-2)], and *Remove Setting
+Method* then deletes the setter once the field no longer needs to be
 written from outside the class [[3](#ref-3)]. The field is still a field; it is
-just visited through a corridor.
-
-The functional reading goes one step further: a field of an immutable
-record is not a location, it is a projection, and a projection that can
-also be written is a *lens* — a value packaging `get :: s -> a` and
-`set :: a -> s -> s` [[4](#ref-4)]. Replacing a mutable field with a lens means
-making the record immutable and routing every read through `get` and
-every write through `set` (or `modify`, which reads, applies a pure
-function and writes in one step). The single field's lens *composes*
-with the lenses of enclosing records, so a deep update that once
-touched five records by hand becomes one composed path. And because
-`set` is a pure function, the writes cannot run off and mutate
-something the rest of the program is looking at; the state transition
-is a value again. The three lens laws — `get (set v s) = v`,
-`set (get s) s = s`, `set v₂ (set v₁ s) = set v₂ s` — are exactly
-the equations under which the move is a refactoring, and they are
-stateable as property tests [[4](#ref-4)], [[5](#ref-5)].
-
-The inverse direction is just as useful. A lens that is never composed,
-never updated through a path, and never read by more than one caller is
-abstraction tax: the reader and writer are already next to each other,
-and a `get`/`set` pair or a plain field says the same thing with less
-machinery. Inlining the lens — replacing `lens.get(s)`, `lens.set(v)(s)`
-and `lens.modify(f)(s)` with direct field access — is the move that
-removes indirection that no longer earns its name. Foster, Greenwald,
-Moore, Pierce and Schmitt's notion of a *well-behaved lens* is the
-property-theoretic core both directions are checked against: the two
-functions are a lens exactly when the GetPut and PutGet laws (the first
-two above, in the form they state) hold [[4](#ref-4)].
+just reached through a corridor.
+
+The functional reading starts at the same smell and goes further out.
+A field of an immutable record is a *projection* — a way to reach
+into a value — and the useful thing about the world of optics is that
+these projections *compose*. A lens reaches one field of a record, a
+prism one branch of a sum, a traversal every element of a container,
+and the projection you need for a job is built by chaining smaller
+ones: `prism .andThen lens`, `each .andThen prism .andThen lens`.
+That separation is the whole point — it splits *how do I get to field
+A* from *what should I do once I have it* — so the same tiny optic is
+reused on one node, on every node of a tree, and against a branch of
+a sum inside a list, without being rewritten. Replacing a mutable
+field with a lens means making the record immutable and routing every
+read through `get` and every write through `set` (or `modify`, which
+reads, applies a pure function and writes in one step). The state
+transition is a value again, and the optic combinators are lawful by
+construction — the contract that makes a rewrite a refactoring is
+built in, not hoped for — so correctness comes for free; the
+libraries ship law-solvers that confirm any optic you write by hand
+[[4](#ref-4)], [[11](#ref-11)].
+
+The inverse direction is justified when the decoupling does not earn
+its keep: a lens that is never composed, a projection whose separation
+of *how* from *what* no one exploits, or — the strongest smell — a
+codebase with no cross-domain boundaries, where the whole record
+travels everywhere and only the target of the projection would ever
+need to pass across a seam. Inlining the lens — replacing `get`,
+`set` and `modify` at their use sites with direct field access —
+removes indirection that no longer names anything. The catalogue
+presents the two directions as one equation, readable both ways;
+which way you go records a judgement about whether the field is part
+of a *path* or a *leaf*. The [eo cookbook](https://eo.constructive.dev/cookbook)
+is a worked, tested reference for the optics side of this: three jobs
+optics do best — navigate structures, decouple modules, thread
+effects — each recipe runnable against the library.
 
 ## Motivation
 
-Reach for the lens when the same field is read and written in many
-places and the writes compose. The smell is repetition of field
-handling: an object-with-accessors whose setters are one-liners that
-nothing intercepts, a copy-update chain that grows a level for every
-record you descend, or an update that must be re-derived by hand each
-time a field moves. An OO class can hold its invariants in accessor
-methods, but the corridor is per-type and per-field; a lens is a value,
-so it can be passed around, stored, and composed into paths that reach
-several levels down without ever repeating the intermediate records.
-When the invariant itself matters — a balance that must never go
-negative, a size that must bracket its children — the pure writer makes
-the transition a value the type system and the tests can see, and a
-*bad* write is a failed check rather than a corrupted object.
-
-Reach for the inverse when the lens is speculative generality. The
-smell that drives Inline is the mirror image: a field whose updates are
-all one level deep, a lens composed nowhere, a get/set pair whose writer
-is `const`-like and whose reader is the identity. The abstraction costs
-a reader a detour — what is *set v₂ (set v₁ s)* doing when the program
-only ever calls `set` once? — and it costs the compiler nothing it can
-deduce. When all the code does with the field is read it once, or write
-it once, a plain field or a pair of functions is clearer. The two moves
-are one equation read in two directions; which direction you choose
-records a judgement about whether the field is part of a *path* or a
-*leaf*.
+Reach for the lens when access to a field needs to be *decoupled from
+its manipulation*. The smell is repetition of field handling: an
+object-with-accessors whose setters are one-liners nothing intercepts,
+a copy-update chain that grows a level for every record you descend,
+or an update that must be re-derived by hand each time a field moves.
+The optics version of the corridor is a *value*, so it can be passed
+around, stored, and composed into paths that reach several levels
+down without ever repeating the intermediate records; and a function
+that needs "every `Instant` in whatever you hand me" can ask for the
+optic instead of the type. When the invariant itself matters — a
+balance that must never go negative, a size that must bracket its
+children — the pure writer makes the transition a value the type
+system and the tests can see, and a *bad* write is a failed check
+rather than a corrupted object.
+
+Reach for the inverse when the lens is speculative generality, or when
+there is nothing for the decoupling to mediate. The smell that drives
+Inline is the mirror image: a field whose updates are all one level
+deep, a lens composed nowhere, a get/set pair whose writer is
+`const`-like and whose reader is the identity — and no cross-domain
+boundaries in sight, so the full structure may pass through every seam
+and nothing is ever isolated to the target of the projection. The
+abstraction costs a reader a detour — what is `set v₂ (set v₁ s)`
+doing when the program only ever calls `set` once? — and it costs the
+compiler nothing it can deduce. When all the code does with the field
+is read it once, or write it once, a plain field or a pair of
+functions is clearer.
 
 ## The move
 
-Both catalogue pages are short. *Encapsulate Variable*: create a
-function that reads the field, create one that writes it, replace every
-read with a call to the reader and every write with a call to the
-writer, and test [[2](#ref-2)]. The precondition is that the readers and writers
-are the only way in and out — nothing may reach the field directly — and
-the payoff is that the class owns its representation. *Remove Setting
-Method*: once the field can be initialised and never needs to be
-reassigned, delete the setter and initialise at construction [[3](#ref-3)]. Read
-the two together and they are the OO route to what the lens packages:
-reads through a named getter, writes through a named setter, and no
-bare `field = ...` anywhere. Herbert's dissertation on Scala
-refactoring points at the same target from the tooling side: a
-refactoring that turns a mutable field into a pure accessor pair has to
-move the *writes*, and that is the whole analysis [[11](#ref-11)].
+Fowler's mechanics are short. *Encapsulate Variable*: create a
+function that reads the field, create one that writes it, replace
+every read with a call to the reader and every write with a call to
+the writer, and test [[2](#ref-2)]; the precondition is that nothing reaches the
+field directly. *Remove Setting Method*: once the field can be
+initialised and never needs to be reassigned, delete the setter and
+initialise at construction [[3](#ref-3)]. Read together they are the OO route to
+what the lens packages: reads through a named getter, writes through a
+named setter, and no bare `field = ...` anywhere. Stocker's Scala
+refactoring catalogue has the same move — turning a mutable field into
+a pure accessor pair moves the *writes*, and that is the whole
+analysis [[10](#ref-10)].
 
 In the functional reading the move is mechanical. Make the record
-immutable. Define `get` as the record's field accessor and `set` as a
-function returning a copy with the field replaced; package them as a
-lens value. Replace reads with `get`, writes with `set`, read-modify-
-write with `modify`. Where a field sits inside other records, compose
-the lenses along the path. The OO precondition — no direct access — is
-replaced by a type: the only way to reach the field is through the
-lens, and the type checker enforces it. The trickier part is what the
-OO ladder leaves implicit. `set` must leave every other field alone, so
-a lens is not just any `(get, set)` pair; it is one that satisfies the
-three laws, and those laws are precisely what a property test can check
-[[4](#ref-4)].
+immutable. Define `get` as the field accessor and `set` as a function
+returning a copy with the field replaced; package them as a lens
+value. Replace reads with `get`, writes with `set`, read-modify-write
+with `modify`. Where a field sits inside other records, compose the
+lenses along the path; where it sits under a branch of a sum, compose
+a prism first; where the field is one of many, compose a traversal.
+The OO precondition — no direct access — is replaced by a type: the
+only way to reach the field is through the optic, and the type
+checker enforces it. In practice the optic for a field or branch is
+often *auto-derivable* from the type — a library macro or generator
+(`eo`'s `lens`/`prism`, Monocle's optics, `lens`'s Template Haskell)
+writes the "how to reach" for you, and you keep the "what to do"
+[[7](#ref-7)], [[11](#ref-11)].
 
 ## The functional reading
 
-In a referentially transparent language a record field is a *focus*: a
-value that indexes into a structure. A lens is a focus with a reader
-and a writer, and the two directions share one equation. `get` selects
-the focus; `set` replaces it; `modify f` is `set` after `get` after
-`f`. Nested records compose: the composite focus `outer . inner`
-selects `inner` inside `outer`, so a deep update becomes one path
-instead of a copy chain. What makes this a *refactoring* rather than a
-rewrite is that the three lens laws are equations between programs —
-`get (set v s) = v`, `set (get s) s = s`, `set v₂ (set v₁ s) =
-set v₂ s` — and they are exactly the conditions under which replacing
-field access with `get`/`set` preserves behaviour [[4](#ref-4)], [[5](#ref-5)].
-
-Foster, Greenwald, Moore, Pierce and Schmitt defined *well-behaved
-lenses* and proved a large catalog of combinators (composition, map,
-and recursion among them) that compose them while preserving those
-laws; their GetPut and PutGet are the first two equations above, and
-PutPut (the third) distinguishes the very well-behaved class [[4](#ref-4)].
-O'Connor showed that lenses are exactly the coalgebras for the costate
-comonad — the categorical shape of "a structure with a distinguished
-hole" — which is why `get`/`set` pairs and the functor-based encodings
-coincide [[6](#ref-6)]. Gibbons and Johnson give the equational proof of
-that correspondence [[7](#ref-7)]. Van Laarhoven's representation made the
-encoding practical: a lens as a polymorphic function
-`(a -> f a) -> (s -> f s)` for all *functor* `f`, which composes with
-ordinary function composition and is what Kmett's *lens* library and
-Pickering, Gibbons and Wu's *profunctor optics* generalise [[8](#ref-8)], [[9](#ref-9)], [[10](#ref-10)].
-On the OO side the same idea appears as a many-to-one refactoring
-in Stocker's later Scala tooling [[11](#ref-11)].
-
-Concretely, the reader never needs most of that. A lens is a `get` and
-a `set`, and a `modify` defined from them; if the field is nested, the
-lenses compose. The laws are the contract, and the contract is checked,
-not hoped.
+An optic is a value that knows how to reach a *focus* inside a source
+and how to rebuild the source around a new focus. The families differ
+in how many foci they address: a lens reaches exactly one field of a
+product, a prism one branch of a sum, a traversal every element of a
+container. They share one shape — see, modify, rebuild — which is what
+makes them *compose*: `prism .andThen lens` says "that branch, then
+that field", and `each .andThen prism .andThen lens` says "every
+element, that branch, that field". The rewrite itself is a pure
+function on the focus: how you get there is a value, what you do there
+is a function, and the two are independent. This is the optics view of
+the same ladder Fowler climbs — the corridor of accessor methods
+becomes a composable value, and the precondition becomes a type.
+
+The theoretical backbone is the same one that made lenses lawful,
+not just convenient. Foster, Greenwald, Moore, Pierce and Schmitt
+defined the well-behaved lens families and proved their combinators —
+composition, map, recursion — preserve the laws, which is where
+"lawful by construction" comes from [[4](#ref-4)]. O'Connor, and then Gibbons
+and Johnson, gave the categorical reading — lenses are the coalgebras
+for the store comonad — which is why the different encodings coincide
+[[5](#ref-5)], [[6](#ref-6)]. Van Laarhoven's representation made the encoding
+practical as a functor-polymorphic function, which is what Kmett's
+*lens* library builds on [[7](#ref-7)], [[8](#ref-8)]; Pickering, Gibbons and Wu's
+*profunctor optics* shows the same idea scales to prisms and
+traversals [[9](#ref-9)]. The [eo library](https://eo.constructive.dev) is our
+own working treatment: optics derived from the type with one
+`.andThen` surface, and a [cookbook](https://eo.constructive.dev/cookbook)
+of runnable recipes organised by the three jobs optics do best —
+navigating structures, decoupling modules, and threading effects. The
+three examples below follow its "contingent fields", "whole trees"
+and "arbitrary structure" recipes.
 
 ## To and from
 
 <figure class="rf-figure">
 {% include_relative replace-mutable-fields-with-lenses/diagrams/koan.svg %}
 <figcaption>The koan. One equation, read in two directions: replace
-(package the reader and pure writer of a field as a lens value) to the
-right, inline (drop the lens, access the field directly) to the left.
-The three lens laws — <em>get</em> (<em>set v s</em>) = <em>v</em>,
-<em>set</em> (<em>get s</em>) <em>s</em> = <em>s</em>, and
-<em>set v&#8322;</em> (<em>set v&#8321; s</em>) = <em>set v&#8322; s</em> —
-are the equation the move is checked against.</figcaption>
+(package the reader and pure writer of a field as an optic value —
+the "how to reach" and the "what to do") to the right, inline (drop
+the optic, access the field directly) to the left. The move is
+lawful by construction: the optic families are derived from the types
+and compose, and the libraries ship solvers that check the ones you
+write by hand.</figcaption>
 </figure>
 
 The catalogue lists each refactoring in both directions because the two
 moves are one equation read left to right and right to left. Replace a
 field with a lens: define `get` and `set` for the field, replace every
 read with `get`, every write with `set` or `modify`, and where the
-field is nested compose the lenses. Inline a lens: replace `get`, `set`
-and `modify` at their use sites with direct access, and delete the
-lens. The lens laws say both directions are behaviour-preserving:
-`get (set v s) = v` is the forward equation, `set (get s) s = s` the
-backward one, and `set v₂ (set v₁ s) = set v₂ s` says writing twice is
-writing the last value once [[4](#ref-4)].
-
-The directions serve different ends. Replace is for containment, so the
-writes to a field are reachable only through a pure function and any
-invariant the writer holds is visible at the one place it is held; for
-composition, because a lens along a path reaches nested records without
-repeating them; and for reuse, because a lens is a value that can be
-passed to a function that reads and writes through it. Inline is for
-simplicity, because a field that is never composed or updated is
-clearer as a field; and for removing a seam, because a lens whose
-callers couple to its mechanics rather than its meaning adds a hop, not
-a guarantee. Both directions are checked by the same property: for all
-generated inputs, the before-program and the after-program agree on the
-entry point.
+field is nested compose the lenses. Inline a lens: replace `get`,
+`set` and `modify` at their use sites with direct access, and delete
+the optic. Both directions are checked by the same property: for all
+generated inputs, the before-program and the after-program agree on
+the entry point.
 
 ## Three examples
 
 Each example is the same program twice, `Before` and `After`, in Scala 3
-and in Haskell. The entry point keeps its name and its type, the lens is
-the only difference, and a hedgehog property generates inputs and demands
-that both versions agree on every one of them. The sources below are
-included verbatim from the files the tests run against.
-
-### 1 · Account balance: the field becomes a lens
-
-A single mutable field — the balance — is read and written by
-`withdraw`. The Before version spells the update out with a copy; the
-After version packages the field's `get` and pure `set` as one
-`Lens[Account, Int]` and routes the update through `modify`. The second
-property checks the three lens laws, which are the equation that makes
-the move a refactoring.
+and in Haskell, using a tiny self-contained optic encoding — a lens, a
+prism, a traversal, and the compositions between them — so the sources
+run with no dependencies. The entry point keeps its name and its type,
+the optic is the only difference, and a hedgehog property generates
+inputs and demands that both versions agree on every one of them. The
+three are eo's "navigate structures" recipes, in increasing depth of
+nesting.
+
+### 1 · A single node: prism and lens composed
+
+A variable's name in one node of an expression tree. The Before
+version is a hand-written match that rebuilds the hit branch and lets
+every other shape pass. The After version is one composed optic —
+`prism .andThen lens`: the prism decides whether the value is a `Var`
+(the hit), the lens edits the `name` inside it, and every miss passes
+through untouched. The *how* and the *what* are separate values; the
+second property checks that the hit is uppercased and every miss
+passes through.
 
 <figure class="rf-figure">
-{% include_relative replace-mutable-fields-with-lenses/01-account-balance/diagram.svg %}
+{% include_relative replace-mutable-fields-with-lenses/01-rename-var/diagram.svg %}
 </figure>
 
 <div class="rf-pair">
 <div><h4>Before · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Before.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/Before.scala %}{% endhighlight %}
 </div>
 <div><h4>Before · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Before.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/Before.hs %}{% endhighlight %}
 </div>
 </div>
 
 <div class="rf-pair">
 <div><h4>After · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/After.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/After.scala %}{% endhighlight %}
 </div>
 <div><h4>After · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/After.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/After.hs %}{% endhighlight %}
 </div>
 </div>
 
-Note what did *not* change: `withdraw` still returns a new account, the
-bonus field is untouched, and `modify` is a function of the lens we
-could pass elsewhere. The property compares result *values* — both
-sides return their own record type, so the test reads `.balance` and
-`.bonus` off each result.
-
 <details class="rf-spec">
-<summary>The property: <code>Before.withdraw == After.withdraw</code> on generated accounts, and the three lens laws</summary>
+<summary>The property: <code>Before.upperVarName == After.upperVarName</code> on generated trees, and the hit/miss behaviour</summary>
 <div class="rf-pair">
 <div><h4>Spec · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Spec.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/Spec.scala %}{% endhighlight %}
 </div>
 <div><h4>Spec · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-account-balance/Spec.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/01-rename-var/Spec.hs %}{% endhighlight %}
 </div>
 </div>
 </details>
 
-### 2 · Game and player: the composed path
+### 2 · Every node of a tree: the same optic, deeper nesting
 
-The player sits inside a game, and moving it means a copy-update chain
-that touches both records at every call. The After version composes
-`player . x` and `player . y` into paths and moves through them; the
-nested write is one step, not two. This is the composition property
-that made lenses famous: `compose` on lenses is exactly function
-composition read backwards, and the second property re-checks the lens
-laws for the composed path.
+Now the same edit is applied at *every* node of the tree — the nesting
+is what makes the hand-written version hurt. The Before version is a
+recursive walk that rebuilds a hit by hand at each level of the
+recursion; add a level to the tree and the rebuild appears again. The
+After version reuses the *same* `varName` optic from example 1 inside
+a bottom-up `everywhere` walk: "how to reach a variable name" is
+written once, and the walk only decides *where* it applies. This is
+eo's "visit across whole trees" recipe — one derivation and one
+`.andThen`, rather than a rewrite.
 
 <figure class="rf-figure">
-{% include_relative replace-mutable-fields-with-lenses/02-player-position/diagram.svg %}
+{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg %}
 </figure>
 
 <div class="rf-pair">
 <div><h4>Before · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Before.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/Before.scala %}{% endhighlight %}
 </div>
 <div><h4>Before · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Before.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/Before.hs %}{% endhighlight %}
 </div>
 </div>
 
 <div class="rf-pair">
 <div><h4>After · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/After.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/After.scala %}{% endhighlight %}
 </div>
 <div><h4>After · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/After.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/After.hs %}{% endhighlight %}
 </div>
 </div>
 
-Two notes. `compose` is a few lines because the whole encoding is a few
-lines — `Lens` is just a `get` and a `set`, and `modify` is defined
-from them; a library like Kmett's or Monocle supplies the same
-combinators with more machinery behind them [[8](#ref-8)], [[11](#ref-11)]. And the
-property again compares result values, so it reads `.level`, `.player.x`
-and `.player.y` off each result rather than asserting record equality
-across two types.
-
 <details class="rf-spec">
-<summary>The property: <code>Before.moveX/moveY == After.moveX/moveY</code> on generated games, and the composed lens obeys the laws</summary>
+<summary>The property: <code>Before.renameAll == After.renameAll</code> on generated trees, and every name is uppercased afterwards</summary>
 <div class="rf-pair">
 <div><h4>Spec · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Spec.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala %}{% endhighlight %}
 </div>
 <div><h4>Spec · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-player-position/Spec.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/02-rename-tree/Spec.hs %}{% endhighlight %}
 </div>
 </div>
 </details>
 
-### 3 · File tree: the lens inside the recursion
+### 3 · A sparse walk over a list: traversal, prism and lens
 
-The tree's `size` field is updated in the same recursive pass that
-walks the children. The Before version writes it directly in the
-`copy`; the After version routes the write through a lens and leaves
-the recursion alone. This is the inverse picture from example 2: here
-the lens is *not* composed — there is one record type and one field —
-and the reason to use it is that the write is a named, checked step of
-the traversal rather than an anonymous copy. The second property checks
-the lens laws on generated nodes.
+A batch of results, some succeeded and some failed; bump only the
+successes. The Before version is a `map` carrying the branch test and
+the rebuild in the same step. The After version is one composed optic
+— `each .andThen prism .andThen lens`: the traversal reaches every
+element, the prism selects the succeeded branch, the lens edits its
+value, and every failed element passes through untouched. This is eo's
+[cookbook recipe "visit through arbitrary structure"](https://eo.constructive.dev/cookbook#visit-through-arbitrary-structure),
+which notes that this sparse walk is the shape a hand-rolled loop gets
+wrong — the container and the branch test fight over who owns the
+loop; composed optics keep the two apart.
 
 <figure class="rf-figure">
-{% include_relative replace-mutable-fields-with-lenses/03-file-tree/diagram.svg %}
+{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/diagram.svg %}
 </figure>
 
 <div class="rf-pair">
 <div><h4>Before · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Before.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/Before.scala %}{% endhighlight %}
 </div>
 <div><h4>Before · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Before.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/Before.hs %}{% endhighlight %}
 </div>
 </div>
 
 <div class="rf-pair">
 <div><h4>After · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/After.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/After.scala %}{% endhighlight %}
 </div>
 <div><h4>After · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/After.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/After.hs %}{% endhighlight %}
 </div>
 </div>
 
-A design choice is worth stating: example 3 uses one *total* lens whose
-focus is a single field, not a lens over "all files in the tree". Every
-node has a `size`, so the lens is total, the property can test it on any
-node, and the recursion is unchanged. "All the files" is a traversal,
-not a lens — a different abstraction with its own laws — and the page
-stays within the lens equation.
-
 <details class="rf-spec">
-<summary>The property: <code>Before.bumpSizes == After.bumpSizes</code> on generated trees, and the size lens obeys the laws</summary>
+<summary>The property: <code>Before.bumpSucceeded == After.bumpSucceeded</code> on generated batches, and only successes are bumped</summary>
 <div class="rf-pair">
 <div><h4>Spec · Scala</h4>
-{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Spec.scala %}{% endhighlight %}
+{% highlight scala %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala %}{% endhighlight %}
 </div>
 <div><h4>Spec · Haskell</h4>
-{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-file-tree/Spec.hs %}{% endhighlight %}
+{% highlight haskell %}{% include_relative replace-mutable-fields-with-lenses/03-bump-oks/Spec.hs %}{% endhighlight %}
 </div>
 </div>
 </details>
 
 ## Pitfalls
 
-The equation has hypotheses, and each is one of the constructive
-criteria. Where a hypothesis fails, replacing a field with a lens
-changes the program. In a language with referential transparency the OO
-precondition does not become easier to satisfy; it disappears, and the
-move becomes an equation. The structures that make that true are
-gathered in the footnote at the end of this section.
-
-- **Partial lenses.** A lens whose `get` is not defined on part of the
-  source type — reading a field out of a sum type where one branch does
-  not carry it — must `error`/`sys.error` on that region, and the laws
-  can only be checked where the lens is defined. Totality is exactly
-  the condition that makes a lens a lens everywhere; prefer a record
-  shape where every value has the field, or use a prism/traversal for
-  the partial case.
-- **Laziness and evaluation count.** A lens's `set` is lazy in the new
-  value in Haskell — `set l (f s) s'` does not force `f s` unless the
-  result needs it — and `modify f = set l . f . get l` can force `f`
-  earlier than a direct field write would. Where the program is lazy
-  about an untouched field (a bonus never read, an id never shown),
-  `undefined` in that field is a probe: before and after must both
-  tolerate it. In Scala a `def` recomputes and a `val` shares; a lens
-  stored as a `val` builds its functions once.
-- **Strictness.** A `modify` reads the focus, applies a function and
-  writes it back; if the focus is bottom, the read is forced and the
-  result differs from a direct write that never looked. Totality, no
-  `undefined` and no partial functions, is exactly the condition under
-  which this cannot arise. Example 1 probes it with `undefined` in the
-  untouched field.
-- **Composition direction.** `compose outer inner` focuses `inner`
-  *inside* `outer`; the reader writes `inner` after `outer`, and
-  getting the order backwards is a type error, not a runtime bug. Two
-  lenses with the same source do not compose at all — there is no
-  single focus — which is what stops the "compose a pair" mistake from
-  even compiling.
-- **The laws as a contract.** A `(get, set)` pair is a lens only when
-  the three laws hold; a pair that violates PutPut is a lens in name
-  only. Any consumer of a lens — including the ones in examples 2 and 3
-  — relies on them, so the property that checks them is not decoration.
-
-In each case the fix is the same: restore the hypothesis, by keeping
-the lens total, by using a `val` where sharing matters, and by testing
-the laws; or admit that this is not a refactoring and test it as a
-change.
-
-<details class="rf-spec">
-<summary>The functional reading</summary>
-<div markdown="1">
-
-A lens is a focus with a reader and a writer. In a referentially
-transparent language a record `s` with field `a` gives a lens whose
-`get` is the field accessor and whose `set` is the copy-update; the two
-are one value because the field is a projection, not a location. Nested
-records compose because a projection of a projection is a projection:
-`compose outer inner` selects `inner` inside `outer`, and the
-read-modify-write `modify` is `set` after `get` after `f`.
-
-This is not a new idea dressed up. Foster, Greenwald, Moore, Pierce and
-Schmitt introduced the *very well-behaved lens* laws (GetPut, PutGet,
-PutPut) and proved that their combinators — composition, map, recursion
-— preserve them, which made it possible to assemble large bidirectional
-transformations from small, verified lenses [[4](#ref-4)]. O'Connor showed
-lenses are the coalgebras for the costate comonad, the categorical
-shape of "a structure with one hole", and conjectured the equivalence
-of the store and functor encodings [[6](#ref-6)]; Gibbons and Johnson proved
-the correspondence [[7](#ref-7)]. Van Laarhoven's representation, a lens as a
-polymorphic function `(a -> f a) -> (s -> f s)` for every functor `f`,
-is what the *lens* library builds on [[8](#ref-8)], [[9](#ref-9)]; Pickering, Gibbons and
-Wu's *profunctor optics* shows the same idea scales to prisms and
-traversals by generalising the arrow [[10](#ref-10)]. Monocle gives Scala the
-same library treatment [[12](#ref-12)].
-
-That is the point. With referential transparency the OO precondition —
-no direct writes — does not become easier to satisfy; it disappears,
-because the writer is a pure function and the type checker enforces the
-corridor. Replacing a field with a lens stops being something you hope
-preserved behaviour and becomes an equation you wrote down.
-
-</div>
-</details>
+The real pitfalls of this move are the ones that come from carrying
+machinery that does not earn its keep, or from rebuilding more than
+the focus.
+
+- **Accidental complexity.** An optic is worth its indirection when
+  the path composes or varies; a lens for a leaf field that only one
+  caller reads and one writes is a detour — a plain field says the
+  same thing. The same for a traversal where a plain `map` with an
+  explicit match would do: if the container and the branch never
+  change, the two-in-one loop is clearer. This is the inverse side of
+  the equation; it is also the most common way the move goes wrong.
+- **Rebuilding more than the focus.** When you write an optic by
+  hand, the writer must rebuild only what was matched or selected. A
+  prism's `review` that reconstructs a value with the wrong fields,
+  or a `set` that touches a neighbouring field, silently changes the
+  program — the composition is only as good as the instances you
+  compose, which is why the law-solvers in Verification matter.
+- **Laziness and evaluation count.** `modify` reads the focus,
+  applies a function and writes it back. In Haskell the setter is
+  lazy in the new value, and rewriting one element of a traversal
+  must not force the others; in Scala a `def` recomputes and a `val`
+  shares, so where a lens is stored and how it is applied changes how
+  often its functions run.
+- **Choosing the wrong family.** A lens addresses exactly one field,
+  a prism one branch, a traversal many. "Focus a pair of fields" or
+  "edit a field that may be absent" are different families (an affine
+  traversal, a prism), and composing optics whose foci do not line up
+  is a type error, not a runtime bug — the types reject the onesided
+  composition, so the mistake shows up at compile time rather than in
+  production.
+
+In each case the fix is the same: choose the smallest optic that says
+the path, derive it from the type when you can, and check the ones you
+write by hand.
 
 ## Verification
 
@@ -433,18 +369,23 @@ states every entry this way, in Scala and in Haskell, with hedgehog on
 both sides [[14](#ref-14)]. Hedgehog is used because its shrinking is integrated
 into the generator, so a shrunk counterexample obeys the same invariants
 as a generated one and the minimal failing input it reports is a real
-input of the program, not an artefact of a separate shrinker. The lens
-laws are second properties — the equation the move is checked against,
-stated directly.
+input of the program, not an artefact of a separate shrinker.
 
 A property is only worth having if it can fail, so each spec above was
-mutation-checked: change `After` so it is no longer equivalent — flip a
-sign, swap a boundary, drop a case — confirm the property reports and
-shrinks a counterexample, then restore `After`. A property that does
-not fail under mutation is testing the generator, not the refactoring.
-The lens examples are especially well protected: the laws are stated
-for the *lens itself*, so a setter that drops the other fields fails
-the laws before it ever reaches the equality property.
+mutation-checked: change `After` so it is no longer equivalent — a sign
+flip, a wrong target — confirm the property reports and shrinks a
+counterexample, then restore `After`. A property that does not fail
+under mutation is testing the generator, not the refactoring.
+
+The optics themselves need no per-example law properties, because they
+are lawful by construction — but the libraries ship *law-solvers* for
+the instances you do write by hand, so you do not have to re-derive
+the rules. [eo](https://eo.constructive.dev) ships `cats-eo-laws` with
+`FooTests`/`FooLaws` for every optic family, Monocle ships
+`monocle-law` with `LensLaws` and `PrismLaws` [[11](#ref-11)], and for Haskell
+`genvalidity-hspec-optics` provides `lensSpec` and `prismSpec`
+one-liners [[12](#ref-12)]. The property checks the refactoring; the solvers
+check the optics you wrote to do it.
 
 To run everything on this page yourself, from a checkout of
 [the site repository](https://github.com/Constructive-Programming/website):
@@ -459,18 +400,18 @@ with hedgehog installed or Docker, and ends with `all properties passed`.
 ## References
 
 <ol>
-<li id="ref-1">Martin Fowler. <em>Refactoring: Improving the Design of Existing Code</em>. Addison-Wesley, 1999. Chapter on self-encapsulation and the <em>Encapsulate Field</em> catalogue entry. <a href="https://martinfowler.com/books/refactoring.html">https://martinfowler.com/books/refactoring.html</a></li>
-<li id="ref-2">Martin Fowler. <em>Encapsulate Variable</em> (formerly <em>Encapsulate Field</em>). Refactoring.com, online edition. <a href="https://refactoring.com/catalog/encapsulateField.html">https://refactoring.com/catalog/encapsulateField.html</a></li>
+<li id="ref-1">Martin Fowler. <em>Refactoring: Improving the Design of Existing Code</em>. Addison-Wesley, 1999. <a href="https://martinfowler.com/books/refactoring.html">https://martinfowler.com/books/refactoring.html</a></li>
+<li id="ref-2">Martin Fowler. <em>Encapsulate Variable</em> (formerly <em>Encapsulate Field</em>, before that <em>Self-Encapsulate Field</em>). Refactoring.com, online edition. <a href="https://refactoring.com/catalog/encapsulateField.html">https://refactoring.com/catalog/encapsulateField.html</a></li>
 <li id="ref-3">Martin Fowler. <em>Remove Setting Method</em>. Refactoring.com, online edition. <a href="https://refactoring.com/catalog/removeSettingMethod.html">https://refactoring.com/catalog/removeSettingMethod.html</a></li>
-<li id="ref-4">J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce and Alan Schmitt. &ldquo;Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem&rdquo;. <em>ACM Transactions on Programming Languages and Systems</em> 29(3):17, 2007 (also POPL 2005). <a href="https://doi.org/10.1145/1232420.1232424">https://doi.org/10.1145/1232420.1232424</a></li>
-<li id="ref-5">Edward Kmett and contributors. <em>lens: Lenses, Folds and Traversals</em>. The library documentation states the three lens laws (get-put, put-get, put-put) that a lens must satisfy. <a href="https://hackage.haskell.org/package/lens">https://hackage.haskell.org/package/lens</a></li>
-<li id="ref-6">Russell O&rsquo;Connor. &ldquo;Functor is to Lens as Applicative is to Biplate: Introducing Multiplate&rdquo;. In <em>Proceedings of the ACM SIGPLAN Workshop on Generic Programming (WGP 2011)</em>, pp. 25&ndash;36. <a href="https://arxiv.org/abs/1103.2841">https://arxiv.org/abs/1103.2841</a> (also the costate-comonad characterisation, arXiv version)</li>
-<li id="ref-7">Jeremy Gibbons and Michael Johnson. &ldquo;Relating Algebraic and Coalgebraic Descriptions of Lenses&rdquo;. <em>Electronic Communications of the EASST</em> 49:1&ndash;16, 2012 (Workshop on Bidirectional Transformations 2012). <a href="https://doi.org/10.14279/tuj.eceasst.49.726">https://doi.org/10.14279/tuj.eceasst.49.726</a></li>
-<li id="ref-8">Twan van Laarhoven. &ldquo;Talk on Lenses&rdquo;. Slides, Radboud University Nijmegen, 17 May 2011. Introduced the functor-based (van Laarhoven) representation. <a href="https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk">https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk</a></li>
-<li id="ref-9">Edward Kmett. <em>Control.Lens</em>. Hackage package documentation for the <em>lens</em> library. <a href="https://hackage.haskell.org/package/lens/docs/Control-Lens.html">https://hackage.haskell.org/package/lens/docs/Control-Lens.html</a></li>
-<li id="ref-10">Matthew Pickering, Jeremy Gibbons and Nicolas Wu. &ldquo;Profunctor Optics: Modular Data Accessors&rdquo;. <em>The Art, Science, and Engineering of Programming</em> 1(2):7, 2017. <a href="https://doi.org/10.22152/programming-journal.org/2017/1/7">https://doi.org/10.22152/programming-journal.org/2017/1/7</a></li>
-<li id="ref-11">Mirko Stocker. <em>Scala Refactoring</em>. Master&rsquo;s thesis, HSR Hochschule f&uuml;r Technik Rapperswil, 2010. Catalogues pure-function accessor refactorings including field encapsulation. <a href="https://eprints.ost.ch/id/eprint/286/">https://eprints.ost.ch/id/eprint/286/</a></li>
-<li id="ref-12">Julien Truffaut and contributors. <em>Monocle: Optics Library for Scala</em>. <a href="https://www.optics.dev/Monocle/">https://www.optics.dev/Monocle/</a></li>
+<li id="ref-4">J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce and Alan Schmitt. &ldquo;Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem&rdquo;. <em>ACM Transactions on Programming Languages and Systems</em> 29(3):17, 2007. <a href="https://doi.org/10.1145/1232420.1232424">https://doi.org/10.1145/1232420.1232424</a></li>
+<li id="ref-5">Russell O&rsquo;Connor. &ldquo;Functor is to Lens as Applicative is to Biplate: Introducing Multiplate&rdquo;. In <em>Proceedings of the ACM SIGPLAN Workshop on Generic Programming (WGP 2011)</em>, pp. 25&ndash;36. <a href="https://arxiv.org/abs/1103.2841">https://arxiv.org/abs/1103.2841</a></li>
+<li id="ref-6">Jeremy Gibbons and Michael Johnson. &ldquo;Relating Algebraic and Coalgebraic Descriptions of Lenses&rdquo;. <em>Electronic Communications of the EASST</em> 49:1&ndash;16, 2012 (Workshop on Bidirectional Transformations 2012). <a href="https://doi.org/10.14279/tuj.eceasst.49.726">https://doi.org/10.14279/tuj.eceasst.49.726</a></li>
+<li id="ref-7">Twan van Laarhoven. &ldquo;Talk on Lenses&rdquo;. Slides, Radboud University Nijmegen, 17 May 2011. <a href="https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk">https://www.twanvl.nl/blog/news/2011-05-19-lenses-talk</a></li>
+<li id="ref-8">Edward Kmett. <em>lens: Lenses, Folds and Traversals</em>, and <em>Control.Lens</em> documentation. <a href="https://hackage.haskell.org/package/lens">https://hackage.haskell.org/package/lens</a></li>
+<li id="ref-9">Matthew Pickering, Jeremy Gibbons and Nicolas Wu. &ldquo;Profunctor Optics: Modular Data Accessors&rdquo;. <em>The Art, Science, and Engineering of Programming</em> 1(2):7, 2017. <a href="https://doi.org/10.22152/programming-journal.org/2017/1/7">https://doi.org/10.22152/programming-journal.org/2017/1/7</a></li>
+<li id="ref-10">Mirko Stocker. <em>Scala Refactoring</em>. Master&rsquo;s thesis, HSR Hochschule f&uuml;r Technik Rapperswil, 2010. <a href="https://eprints.ost.ch/id/eprint/286/">https://eprints.ost.ch/id/eprint/286/</a></li>
+<li id="ref-11">Julien Truffaut and contributors. <em>Monocle: Optics Library for Scala</em> (including <code>monocle-law</code>). <a href="https://www.optics.dev/Monocle/">https://www.optics.dev/Monocle/</a></li>
+<li id="ref-12">Constructive Programming. <em>eo: optics library and cookbook for Scala 3</em>. <a href="https://eo.constructive.dev">https://eo.constructive.dev</a> (<a href="https://eo.constructive.dev/cookbook">cookbook</a>)</li>
 <li id="ref-13">Koen Claessen and John Hughes. &ldquo;QuickCheck: a lightweight tool for random testing of Haskell programs&rdquo;. In <em>Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2000)</em>, pp. 268&ndash;279. <a href="https://doi.org/10.1145/351240.351266">https://doi.org/10.1145/351240.351266</a></li>
 <li id="ref-14">Jacob Stanley and contributors. <em>Hedgehog: release with confidence, state-of-the-art property testing</em>. <a href="https://github.com/hedgehogqa/haskell-hedgehog">https://github.com/hedgehogqa/haskell-hedgehog</a> and <a href="https://github.com/hedgehogqa/scala-hedgehog">https://github.com/hedgehogqa/scala-hedgehog</a></li>
 </ol>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
deleted file mode 100644
index 57e1357..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.hs
+++ /dev/null
@@ -1,17 +0,0 @@
--- Same, with a lens on the balance: the getter and the pure setter
--- packed as one value.
-module After where
-
-data Account = Account { balance :: Int, bonus :: Int }
-  deriving (Eq, Show)
-
-data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
-
-modify :: Lens s a -> (a -> a) -> s -> s
-modify l f s = set l (f (get l s)) s
-
-balanceLens :: Lens Account Int
-balanceLens = Lens { get = balance, set = \b a -> a { balance = b } }
-
-withdraw :: Account -> Int -> Account
-withdraw a amount = modify balanceLens (subtract amount) a
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
deleted file mode 100644
index a96d327..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/After.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-// Same, with a lens on the balance: the getter and the pure setter
-// packed as one value.
-object After:
-  case class Account(balance: Int, bonus: Int)
-
-  case class Lens[S, A](get: S => A, set: A => S => S):
-    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
-
-  val balance: Lens[Account, Int] =
-    Lens[Account, Int](_.balance, b => a => a.copy(balance = b))
-
-  def withdraw(a: Account, amount: Int): Account =
-    balance.modify(_ - amount)(a)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
deleted file mode 100644
index ecac13b..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.hs
+++ /dev/null
@@ -1,7 +0,0 @@
--- Withdraw from an account: the balance changes, the bonus does not.
-module Before where
-
-data Account = Account { balance :: Int, bonus :: Int }
-
-withdraw :: Account -> Int -> Account
-withdraw a amount = a { balance = balance a - amount }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
deleted file mode 100644
index 7cb97d7..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Before.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-// Withdraw from an account: the balance changes, the bonus does not.
-object Before:
-  case class Account(balance: Int, bonus: Int)
-
-  def withdraw(a: Account, amount: Int): Account =
-    a.copy(balance = a.balance - amount)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
deleted file mode 100644
index e55a959..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.hs
+++ /dev/null
@@ -1,45 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-module Main where
-
-import Control.Monad (unless)
-import System.Exit (exitFailure)
-import Hedgehog
-import qualified Hedgehog.Gen as Gen
-import qualified Hedgehog.Range as Range
-import qualified Before
-import qualified After
-
-genInt :: Gen Int
-genInt = Gen.int (Range.linear (-30) 30)
-
-prop_agrees :: Property
-prop_agrees = property $ do
-  b  <- forAll genInt
-  bn <- forAll genInt
-  am <- forAll genInt
-  let before = Before.withdraw (Before.Account b bn) am
-      after  = After.withdraw (After.Account b bn) am
-  (Before.balance before, Before.bonus before)
-    === (After.balance after, After.bonus after)
-
--- A lens has to satisfy the three equations; they are exactly what
--- makes replacing a field with a get/set pair a refactoring.
-prop_laws :: Property
-prop_laws = property $ do
-  b  <- forAll genInt
-  bn <- forAll genInt
-  v1 <- forAll genInt
-  v2 <- forAll genInt
-  let l = After.balanceLens
-      a = After.Account b bn
-  After.set l (After.get l a) a === a
-  After.get l (After.set l v1 a) === v1
-  After.set l v2 (After.set l v1 a) === After.set l v2 a
-
-main :: IO ()
-main = do
-  ok <- checkParallel $ Group "Props"
-    [ ("withdraw: Before == After", prop_agrees)
-    , ("balance lens obeys get-put, put-get, put-put", prop_laws)
-    ]
-  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
deleted file mode 100644
index 44f4344..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/Spec.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-//> using scala 3.3.4
-//> using dep qa.hedgehog::hedgehog-core:0.14.0
-//> using dep qa.hedgehog::hedgehog-runner:0.14.0
-import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
-
-object Props extends Properties:
-  def tests: List[Test] = List(
-    property("withdraw: Before == After", agrees),
-    property("the balance lens obeys get-put, put-get, put-put", laws),
-  )
-
-  // Raw values, so the same input feeds both Account types.
-  val genInt: Gen[Int] = Gen.int(Range.linear(-30, 30))
-
-  def agrees: Property =
-    for
-      b  <- genInt.forAll
-      bn <- genInt.forAll
-      am <- genInt.forAll
-    yield
-      val before = Before.withdraw(Before.Account(b, bn), am)
-      val after  = After.withdraw(After.Account(b, bn), am)
-      (before.balance, before.bonus) ==== (after.balance, after.bonus)
-
-  def laws: Property =
-    for
-      b  <- genInt.forAll
-      bn <- genInt.forAll
-      v1 <- genInt.forAll
-      v2 <- genInt.forAll
-    yield
-      val a = After.Account(b, bn)
-      val l = After.balance
-      l.get(l.set(v1)(a)) ==== v1 and
-        l.set(l.get(a))(a) ==== a and
-        l.set(v2)(l.set(v1)(a)) ==== l.set(v2)(a)
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
deleted file mode 100644
index 3c855bd..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-account-balance/diagram.svg
+++ /dev/null
@@ -1,46 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 196" role="img" aria-labelledby="d1-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
-  <title id="d1-title">Replacing the balance field with a lens in the withdraw program. Before: withdraw(Account(balance, bonus), amount) reads balance with a.balance and writes it with a.copy(balance = a.balance - amount); the dotted region is the field access and copy spell-out. After: withdraw is balance.modify(_ - amount)(a), where balanceLens = Lens(get = _.balance, set = b => a => a.copy(balance = b)).</title>
-  <g fill="currentColor" font-size="12" opacity=".6">
-    <text x="16" y="26">before</text>
-    <text x="428" y="26">after</text>
-  </g>
-  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
-    <rect x="16" y="36" width="388" height="148" rx="4"/>
-    <rect x="428" y="36" width="336" height="92" rx="4"/>
-    <rect x="428" y="150" width="336" height="34" rx="4"/>
-  </g>
-  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
-    <rect x="44" y="84" width="336" height="66" rx="3"/>
-  </g>
-  <g fill="currentColor" font-size="12">
-    <text x="28" y="58">withdraw(a: Account, amount) =</text>
-    <text x="40" y="76">a.copy(balance = a.balance - amount)</text>
-    <text x="52" y="98">read: a.balance</text>
-    <text x="52" y="116">write: a.copy(balance = ...)</text>
-    <text x="52" y="134">every call site spells out the</text>
-    <text x="52" y="148">field update by hand</text>
-    <text x="440" y="58">withdraw(a, amount) =</text>
-    <text x="452" y="76">balanceLens.modify(_ - amount)(a)</text>
-    <text x="440" y="100">balanceLens =</text>
-    <text x="452" y="120">Lens(get = _.balance,</text>
-    <text x="452" y="136">     set = ...)</text>
-  </g>
-  <g fill="currentColor" font-size="12" text-anchor="middle" opacity=".85">
-    <text x="212" y="168">field access + copy spell-out</text>
-    <text x="596" y="172">get and set packed as one value</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1">
-    <circle cx="386" cy="112" r="7.5"/>
-    <circle cx="428" cy="156" r="7.5"/>
-  </g>
-  <g fill="currentColor" font-size="12" text-anchor="middle">
-    <text x="386" y="116">1</text>
-    <text x="428" y="160">1</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1.2">
-    <path d="M386 132 V144"/>
-  </g>
-  <g fill="currentColor">
-    <path d="M382.5 144 L386 152 L389.5 144 Z"/>
-  </g>
-</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
new file mode 100644
index 0000000..9051ef1
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
@@ -0,0 +1,58 @@
+-- Same, as one composed optic: the prism matches the Var branch,
+-- the lens edits its name, every other shape passes through.
+module After where
+
+import Data.Char (toUpper)
+
+data Var   = Var   { vName :: String, vRef :: Int }
+  deriving (Eq, Show)
+data Expr  = EVar Var | EApp Expr Expr | ELam String Expr
+  deriving (Eq, Show)
+
+data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
+
+modifyL :: Lens s a -> (a -> a) -> s -> s
+modifyL l f s = set l (s, f (view l s))
+
+data Prism s a = Prism
+  { preview :: s -> Maybe a
+  , review  :: a -> s
+  }
+
+modifyP :: Prism s a -> (a -> a) -> s -> s
+modifyP p f s = case preview p s of
+  Nothing -> s
+  Just a  -> review p (f a)
+
+-- A prism followed by a lens: hit -> edit the field;
+-- miss -> pass through.
+data PartialLens s a = PartialLens
+  { plPreview :: s -> Maybe a
+  , plModify  :: (a -> a) -> s -> s
+  }
+
+composeO :: Prism s m -> Lens m a -> PartialLens s a
+composeO p l = PartialLens
+  { plPreview = \s -> view l <$> preview p s
+  , plModify  = \f s -> case preview p s of
+      Nothing -> s
+      Just m  -> review p (modifyL l f m)
+  }
+
+over :: PartialLens s a -> (a -> a) -> s -> s
+over pl = plModify pl
+
+varP :: Prism Expr Var
+varP = Prism
+  { preview = \e -> case e of EVar v -> Just v; _ -> Nothing
+  , review  = EVar
+  }
+
+nameL :: Lens Var String
+nameL = Lens { view = vName, set = \(v, n) -> v { vName = n } }
+
+varName :: PartialLens Expr String
+varName = composeO varP nameL
+
+upperVarName :: Expr -> Expr
+upperVarName = over varName (map toUpper)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
new file mode 100644
index 0000000..227f22e
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
@@ -0,0 +1,45 @@
+// Same, as one composed optic: the prism matches the Var branch,
+// the lens edits its name, every other shape passes through.
+object After:
+  case class Var(name: String, ref: Int)
+  enum Expr:
+    case EVar(v: Var)
+    case EApp(f: Expr, x: Expr)
+    case ELam(bind: String, body: Expr)
+
+  import Expr.*
+
+  case class Lens[S, A](view: S => A, set: (S, A) => S):
+    def modify(f: A => A): S => S = s => set(s, f(view(s)))
+
+  case class Prism[S, A](preview: S => Option[A], review: A => S):
+    def modify(f: A => A): S => S =
+      s => preview(s).map(a => review(f(a))).getOrElse(s)
+  // A prism followed by a lens: hit → edit the field;
+  // miss → pass through.
+  case class PartialLens[S, A](preview: S => Option[A],
+                               modify: (A => A) => S => S)
+
+  def compose[S, M, A](p: Prism[S, M],
+                     l: Lens[M, A]): PartialLens[S, A] =
+    PartialLens(
+      preview = s => p.preview(s).map(l.view),
+      modify  = f => s => p.preview(s) match
+        case Some(m) => p.review(l.modify(f)(m))
+        case None    => s,
+    )
+
+  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
+    pl.modify(f)
+
+  val varP: Prism[Expr, Var] =
+    Prism[Expr, Var](
+      { case EVar(v) => Some(v); case _ => None },
+      EVar(_),
+    )
+  val nameL: Lens[Var, String] =
+    Lens[Var, String](_.name, (v, n) => v.copy(name = n))
+
+  val varName: PartialLens[Expr, String] = compose(varP, nameL)
+
+  def upperVarName(e: Expr): Expr = over(varName, _.toUpperCase)(e)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.hs
new file mode 100644
index 0000000..d3870b7
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.hs
@@ -0,0 +1,14 @@
+-- Uppercase the variable of one Var node: a hand-written match
+-- that rebuilds the hit branch and lets every other shape pass.
+module Before where
+
+import Data.Char (toUpper)
+
+data Var   = Var   { vName :: String, vRef :: Int }
+  deriving (Eq, Show)
+data Expr  = EVar Var | EApp Expr Expr | ELam String Expr
+  deriving (Eq, Show)
+
+upperVarName :: Expr -> Expr
+upperVarName (EVar v) = EVar v { vName = map toUpper (vName v) }
+upperVarName e        = e
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.scala
new file mode 100644
index 0000000..e590fce
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Before.scala
@@ -0,0 +1,14 @@
+// Uppercase the variable of one Var node: a hand-written match
+// that rebuilds the hit branch and lets every other shape pass.
+object Before:
+  case class Var(name: String, ref: Int)
+  enum Expr:
+    case EVar(v: Var)
+    case EApp(f: Expr, x: Expr)
+    case ELam(bind: String, body: Expr)
+
+  import Expr.*
+
+  def upperVarName(e: Expr): Expr = e match
+    case EVar(v) => EVar(v.copy(name = v.name.toUpperCase))
+    case other   => other
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.hs
new file mode 100644
index 0000000..e2c0dfa
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Data.Char (toUpper)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+-- A neutral tree, so one generated input feeds both Expr types.
+data T = TVar String Int | TApp T T | TLam String T
+  deriving (Eq, Show)
+
+genName :: Gen String
+genName = Gen.string (Range.linear 0 4) Gen.alpha
+
+genT :: Int -> Gen T
+genT 0 = TVar <$> genName <*> Gen.int (Range.linear (-10) 10)
+genT depth = Gen.choice
+  [ TVar <$> genName <*> Gen.int (Range.linear (-10) 10)
+  , TApp <$> genT (depth - 1) <*> genT (depth - 1)
+  , TLam <$> genName <*> genT (depth - 1)
+  ]
+
+toBefore :: T -> Before.Expr
+toBefore (TVar n r) = Before.EVar (Before.Var n r)
+toBefore (TApp f x) = Before.EApp (toBefore f) (toBefore x)
+toBefore (TLam b e) = Before.ELam b (toBefore e)
+
+fromBefore :: Before.Expr -> T
+fromBefore (Before.EVar v)  = TVar (Before.vName v) (Before.vRef v)
+fromBefore (Before.EApp f x) = TApp (fromBefore f) (fromBefore x)
+fromBefore (Before.ELam b e) = TLam b (fromBefore e)
+
+toAfter :: T -> After.Expr
+toAfter (TVar n r) = After.EVar (After.Var n r)
+toAfter (TApp f x) = After.EApp (toAfter f) (toAfter x)
+toAfter (TLam b e) = After.ELam b (toAfter e)
+
+fromAfter :: After.Expr -> T
+fromAfter (After.EVar v)   = TVar (After.vName v) (After.vRef v)
+fromAfter (After.EApp f x) = TApp (fromAfter f) (fromAfter x)
+fromAfter (After.ELam b e) = TLam b (fromAfter e)
+
+prop_agrees :: Property
+prop_agrees = property $ do
+  t <- forAll (genT 4)
+  fromBefore (Before.upperVarName (toBefore t))
+    === fromAfter (After.upperVarName (toAfter t))
+
+noVars :: T -> Bool
+noVars (TVar _ _) = False
+noVars (TApp f x) = noVars f && noVars x
+noVars (TLam _ e) = noVars e
+
+prop_hit_and_miss :: Property
+prop_hit_and_miss = property $ do
+  n <- forAll genName
+  t <- forAll (genT 3)
+  After.upperVarName (After.EVar (After.Var n 0))
+    === After.EVar (After.Var (map toUpper n) 0)
+  if noVars t
+    then fromAfter (After.upperVarName (toAfter t)) === t
+    else success
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("upperVarName: Before == After", prop_agrees)
+    , ("the hit is uppercased, misses pass through", prop_hit_and_miss)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
new file mode 100644
index 0000000..7f90a4d
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
@@ -0,0 +1,85 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("upperVarName: Before == After", agrees),
+    property("the hit is uppercased, misses pass through", hitAndMiss),
+  )
+
+  // A neutral tree, so one generated input feeds both Expr types.
+  enum T:
+    case TVar(name: String, ref: Int)
+    case TApp(f: T, x: T)
+    case TLam(bind: String, body: T)
+
+  val genName: Gen[String] =
+    Gen.alpha.list(Range.linear(0, 4)).map(_.mkString)
+  def genT(depth: Int): Gen[T] =
+    val leaf =
+      for n <- genName; r <- Gen.int(Range.linear(-10, 10))
+      yield T.TVar(n, r)
+    if depth == 0 then leaf
+    else
+      Gen.choice1(
+        leaf,
+        for
+          f <- genT(depth - 1)
+          x <- genT(depth - 1)
+        yield T.TApp(f, x),
+        for b <- genName; body <- genT(depth - 1) yield T.TLam(b, body),
+      )
+
+  def toBefore(t: T): Before.Expr = t match
+    case T.TVar(n, r)   => Before.Expr.EVar(Before.Var(n, r))
+    case T.TApp(f, x)   => Before.Expr.EApp(toBefore(f), toBefore(x))
+    case T.TLam(b, e)   => Before.Expr.ELam(b, toBefore(e))
+  def fromBefore(e: Before.Expr): T = e match
+    case Before.Expr.EVar(v)      => T.TVar(v.name, v.ref)
+    case Before.Expr.EApp(f, x)  =>
+      T.TApp(fromBefore(f), fromBefore(x))
+    case Before.Expr.ELam(b, e)   => T.TLam(b, fromBefore(e))
+  def toAfter(t: T): After.Expr = t match
+    case T.TVar(n, r)   => After.Expr.EVar(After.Var(n, r))
+    case T.TApp(f, x)   => After.Expr.EApp(toAfter(f), toAfter(x))
+    case T.TLam(b, e)   => After.Expr.ELam(b, toAfter(e))
+  def fromAfter(e: After.Expr): T = e match
+    case After.Expr.EVar(v)     => T.TVar(v.name, v.ref)
+    case After.Expr.EApp(f, x)  => T.TApp(fromAfter(f), fromAfter(x))
+    case After.Expr.ELam(b, e)  => T.TLam(b, fromAfter(e))
+
+  def agrees: Property =
+    for t <- genT(4).forAll
+    yield
+      fromBefore(Before.upperVarName(toBefore(t)))
+        ==== fromAfter(After.upperVarName(toAfter(t)))
+
+  def hitAndMiss: Property =
+    for
+      n <- genName.forAll
+      t <- genT(3).forAll
+    yield
+      val hit = After.upperVarName(After.Expr.EVar(After.Var(n, 0)))
+        ==== After.Expr.EVar(After.Var(n.toUpperCase, 0))
+      val miss =
+        if tNoVars(t) then
+          fromAfter(After.upperVarName(toAfter(t))) ==== t
+        else Result.success
+      hit and miss
+
+  def tNoVars(t: T): Boolean = t match
+    case T.TVar(_, _)   => false
+    case T.TApp(f, x)   => tNoVars(f) && tNoVars(x)
+    case T.TLam(_, b)   => tNoVars(b)
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/diagram.svg
new file mode 100644
index 0000000..d501ace
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/diagram.svg
@@ -0,0 +1,41 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 200" role="img" aria-labelledby="d1-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d1-title">Replacing a hand-written match with a composed prism and lens. Before: upperVarName(e) matches Var(n, r), rebuilds it, and passes every other shape through; the dotted region is the match and rebuild. After: varName = prism(varP).andThen(lens(nameL)) — the prism decides whether the value is a Var, the lens edits its name, and one over(varName, upper) applies the rewrite; the miss passes through untouched.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="128" rx="4"/>
+    <rect x="428" y="36" width="336" height="128" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="62" width="332" height="34" rx="3"/>
+    <rect x="44" y="112" width="332" height="26" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="50">upperVarName(e) = e match</text>
+    <text x="40" y="70">case Var(n, r) =&gt; Var(n.toUpper, r)</text>
+    <text x="40" y="88">case other =&gt; other</text>
+    <text x="52" y="108">match + rebuild</text>
+    <text x="52" y="126">pass-through</text>
+    <text x="440" y="50">varName = varP .andThen nameL</text>
+    <text x="452" y="70">over(varName, _.toUpperCase):</text>
+    <text x="464" y="88">prism decides the hit (Var)</text>
+    <text x="464" y="106">lens edits the name</text>
+    <text x="464" y="124">miss passes through</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="132" r="7.5"/>
+    <circle cx="428" cy="132" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="136">1</text>
+    <text x="428" y="136">1</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M406 132 H414"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M414 128.5 L422 132 L414 135.5 Z"/>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
deleted file mode 100644
index 8469200..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.hs
+++ /dev/null
@@ -1,40 +0,0 @@
--- Same, with a composed path: player . x and player . y reach the
--- nested field in one step, no copy chain.
-module After where
-
-data Player = Player { pid :: String, px :: Int, py :: Int }
-  deriving (Eq, Show)
-data Game   = Game   { level :: Int, gplayer :: Player }
-  deriving (Eq, Show)
-
-data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
-
-modify :: Lens s a -> (a -> a) -> s -> s
-modify l f s = set l (f (get l s)) s
-
-compose :: Lens s m -> Lens m a -> Lens s a
-compose outer inner = Lens
-  { get = get inner . get outer
-  , set = \a s -> set outer (set inner a (get outer s)) s
-  }
-
-player :: Lens Game Player
-player = Lens { get = gplayer, set = \p g -> g { gplayer = p } }
-
-x :: Lens Player Int
-x = Lens { get = px, set = \v p -> p { px = v } }
-
-y :: Lens Player Int
-y = Lens { get = py, set = \v p -> p { py = v } }
-
-playerX :: Lens Game Int
-playerX = compose player x
-
-playerY :: Lens Game Int
-playerY = compose player y
-
-moveX :: Game -> Int -> Game
-moveX g dx = modify playerX (+ dx) g
-
-moveY :: Game -> Int -> Game
-moveY g dy = modify playerY (+ dy) g
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
deleted file mode 100644
index 7350171..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/After.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-// Same, with a composed path: player . x and player . y reach the
-// nested field in one step, no copy chain.
-object After:
-  case class Player(id: String, x: Int, y: Int)
-  case class Game(level: Int, player: Player)
-
-  case class Lens[S, A](get: S => A, set: A => S => S):
-    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
-
-  def compose[S, M, A](outer: Lens[S, M],
-                       inner: Lens[M, A]): Lens[S, A] =
-    Lens[S, A](s => inner.get(outer.get(s)),
-      a => s => outer.set(inner.set(a)(outer.get(s)))(s))
-
-  val player: Lens[Game, Player] =
-    Lens[Game, Player](_.player, p => g => g.copy(player = p))
-
-  val x: Lens[Player, Int] =
-    Lens[Player, Int](_.x, v => p => p.copy(x = v))
-  val y: Lens[Player, Int] =
-    Lens[Player, Int](_.y, v => p => p.copy(y = v))
-
-  val playerX: Lens[Game, Int] = compose(player, x)
-  val playerY: Lens[Game, Int] = compose(player, y)
-
-  def moveX(g: Game, dx: Int): Game = playerX.modify(_ + dx)(g)
-  def moveY(g: Game, dy: Int): Game = playerY.modify(_ + dy)(g)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
deleted file mode 100644
index 8061f77..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.hs
+++ /dev/null
@@ -1,12 +0,0 @@
--- Move the player inside a game: the nested copy-update touches
--- both records at every move.
-module Before where
-
-data Player = Player { pid :: String, px :: Int, py :: Int }
-data Game   = Game   { level :: Int, gplayer :: Player }
-
-moveX :: Game -> Int -> Game
-moveX g dx = g { gplayer = (gplayer g) { px = px (gplayer g) + dx } }
-
-moveY :: Game -> Int -> Game
-moveY g dy = g { gplayer = (gplayer g) { py = py (gplayer g) + dy } }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
deleted file mode 100644
index 3f905eb..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Before.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-// Move the player inside a game: the nested copy-update touches
-// both records at every move.
-object Before:
-  case class Player(id: String, x: Int, y: Int)
-  case class Game(level: Int, player: Player)
-
-  def moveX(g: Game, dx: Int): Game =
-    g.copy(player = g.player.copy(x = g.player.x + dx))
-
-  def moveY(g: Game, dy: Int): Game =
-    g.copy(player = g.player.copy(y = g.player.y + dy))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
deleted file mode 100644
index ab8feb0..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-module Main where
-
-import Control.Monad (unless)
-import System.Exit (exitFailure)
-import Hedgehog
-import qualified Hedgehog.Gen as Gen
-import qualified Hedgehog.Range as Range
-import qualified Before
-import qualified After
-
-genInt :: Gen Int
-genInt = Gen.int (Range.linear (-30) 30)
-
-genId :: Gen String
-genId = ("p" <>) . show <$> Gen.int (Range.linear 0 9)
-
-prop_agrees :: Property
-prop_agrees = property $ do
-  id <- forAll genId
-  lv <- forAll genInt
-  px <- forAll genInt
-  py <- forAll genInt
-  dx <- forAll genInt
-  dy <- forAll genInt
-  let bg = Before.Game lv (Before.Player id px py)
-      ag = After.Game lv (After.Player id px py)
-      b1 = Before.moveX bg dx
-      b2 = Before.moveY bg dy
-      a1 = After.moveX ag dx
-      a2 = After.moveY ag dy
-  (Before.level b1, Before.px (Before.gplayer b1),
-   Before.py (Before.gplayer b1))
-    === (After.level a1, After.px (After.gplayer a1),
-         After.py (After.gplayer a1))
-  (Before.level b2, Before.px (Before.gplayer b2),
-   Before.py (Before.gplayer b2))
-    === (After.level a2, After.px (After.gplayer a2),
-         After.py (After.gplayer a2))
-
--- The composed path is still a lens: get and set through player . x
--- satisfy the three equations.
-prop_laws :: Property
-prop_laws = property $ do
-  id <- forAll genId
-  lv <- forAll genInt
-  px <- forAll genInt
-  py <- forAll genInt
-  v1 <- forAll genInt
-  v2 <- forAll genInt
-  let l = After.playerX
-      g = After.Game lv (After.Player id px py)
-  After.set l (After.get l g) g === g
-  After.get l (After.set l v1 g) === v1
-  After.set l v2 (After.set l v1 g) === After.set l v2 g
-
-main :: IO ()
-main = do
-  ok <- checkParallel $ Group "Props"
-    [ ("moveX/moveY: Before == After", prop_agrees)
-    , ("composed path lens player.x obeys the laws", prop_laws)
-    ]
-  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
deleted file mode 100644
index 3dcb8d9..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/Spec.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-//> using scala 3.3.4
-//> using dep qa.hedgehog::hedgehog-core:0.14.0
-//> using dep qa.hedgehog::hedgehog-runner:0.14.0
-import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
-
-object Props extends Properties:
-  def tests: List[Test] = List(
-    property("moveX: Before == After", agreesX),
-    property("moveY: Before == After", agreesY),
-    property("the composed path lens player.x obeys the laws", laws),
-  )
-
-  // Raw values, so the same input feeds both Game types.
-  val genInt: Gen[Int] = Gen.int(Range.linear(-30, 30))
-  val genId: Gen[String] =
-    for n <- Gen.int(Range.linear(0, 9)) yield "p" + n.toString
-
-  def agreesX: Property =
-    for
-      id <- genId.forAll
-      lv <- genInt.forAll
-      px <- genInt.forAll
-      py <- genInt.forAll
-      dx <- genInt.forAll
-    yield
-      val b =
-        Before.moveX(Before.Game(lv, Before.Player(id, px, py)), dx)
-      val a = After.moveX(After.Game(lv, After.Player(id, px, py)), dx)
-      (b.level, b.player.id, b.player.x, b.player.y)
-        ==== (a.level, a.player.id, a.player.x, a.player.y)
-
-  def agreesY: Property =
-    for
-      id <- genId.forAll
-      lv <- genInt.forAll
-      px <- genInt.forAll
-      py <- genInt.forAll
-      dy <- genInt.forAll
-    yield
-      val b =
-        Before.moveY(Before.Game(lv, Before.Player(id, px, py)), dy)
-      val a = After.moveY(After.Game(lv, After.Player(id, px, py)), dy)
-      (b.level, b.player.id, b.player.x, b.player.y)
-        ==== (a.level, a.player.id, a.player.x, a.player.y)
-
-  def laws: Property =
-    for
-      id <- genId.forAll
-      lv <- genInt.forAll
-      px <- genInt.forAll
-      py <- genInt.forAll
-      v1 <- genInt.forAll
-      v2 <- genInt.forAll
-    yield
-      val g  = After.Game(lv, After.Player(id, px, py))
-      val l  = After.playerX
-      l.get(l.set(v1)(g)) ==== v1 and
-        l.set(l.get(g))(g) ==== g and
-        l.set(v2)(l.set(v1)(g)) ==== l.set(v2)(g)
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
deleted file mode 100644
index dae6b92..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-player-position/diagram.svg
+++ /dev/null
@@ -1,41 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 200" role="img" aria-labelledby="d2-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
-  <title id="d2-title">Replacing nested copy-updates with a composed lens path. Before: moveX(g, dx) writes g.copy(player = g.player.copy(x = g.player.x + dx)) — the copy chain touches level, player and x. After: playerX = compose player x is one lens, and moveX(g, dx) = playerX.modify(_ + dx)(g); playerX reads g.player.x and writes the nested record in one step.</title>
-  <g fill="currentColor" font-size="12" opacity=".6">
-    <text x="16" y="26">before</text>
-    <text x="428" y="26">after</text>
-  </g>
-  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
-    <rect x="16" y="36" width="388" height="128" rx="4"/>
-    <rect x="428" y="36" width="336" height="128" rx="4"/>
-  </g>
-  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
-    <rect x="44" y="66" width="332" height="58" rx="3"/>
-  </g>
-  <g fill="currentColor" font-size="12">
-    <text x="28" y="58">moveX(g, dx) =</text>
-    <text x="40" y="76">g.copy(player =</text>
-    <text x="52" y="94">g.player.copy(x = g.player.x + dx))</text>
-    <text x="52" y="118">copy chain: level</text>
-    <text x="52" y="134">then player then x</text>
-    <text x="440" y="58">playerX = compose player x</text>
-    <text x="452" y="76">moveX(g, dx) =</text>
-    <text x="464" y="94">playerX.modify(_ + dx)(g)</text>
-    <text x="452" y="118">one lens reach:</text>
-    <text x="452" y="134">reads g.player.x,</text>
-    <text x="452" y="150">writes the whole path</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1">
-    <circle cx="386" cy="94" r="7.5"/>
-    <circle cx="428" cy="94" r="7.5"/>
-  </g>
-  <g fill="currentColor" font-size="12" text-anchor="middle">
-    <text x="386" y="98">1</text>
-    <text x="428" y="98">1</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1.2">
-    <path d="M406 94 H414"/>
-  </g>
-  <g fill="currentColor">
-    <path d="M414 90.5 L422 94 L414 97.5 Z"/>
-  </g>
-</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
new file mode 100644
index 0000000..2662157
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
@@ -0,0 +1,58 @@
+-- Same, with the single varName optic applied at every node of the
+-- tree: how to reach the name is defined once, and the walk only
+-- decides where it applies.
+module After where
+
+import Data.Char (toUpper)
+
+data Var  = Var  { vName :: String, vRef :: Int }
+  deriving (Eq, Show)
+data Expr = EVar Var | EApp Expr Expr | ELam String Expr
+  deriving (Eq, Show)
+
+data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
+
+modifyL :: Lens s a -> (a -> a) -> s -> s
+modifyL l f s = set l (s, f (view l s))
+
+data Prism s a = Prism
+  { preview :: s -> Maybe a
+  , review  :: a -> s
+  }
+
+data PartialLens s a = PartialLens
+  { plPreview :: s -> Maybe a
+  , plModify  :: (a -> a) -> s -> s
+  }
+
+composeO :: Prism s m -> Lens m a -> PartialLens s a
+composeO p l = PartialLens
+  { plPreview = \s -> view l <$> preview p s
+  , plModify  = \f s -> case preview p s of
+      Nothing -> s
+      Just m  -> review p (modifyL l f m)
+  }
+
+over :: PartialLens s a -> (a -> a) -> s -> s
+over pl = plModify pl
+
+varP :: Prism Expr Var
+varP = Prism
+  { preview = \e -> case e of EVar v -> Just v; _ -> Nothing
+  , review  = EVar
+  }
+
+nameL :: Lens Var String
+nameL = Lens { view = vName, set = \(v, n) -> v { vName = n } }
+
+varName :: PartialLens Expr String
+varName = composeO varP nameL
+
+-- Bottom-up: apply the rewrite at every node, descending first.
+everywhere :: (Expr -> Expr) -> Expr -> Expr
+everywhere f e@(EVar _)   = f e
+everywhere f (EApp a b)   = f (EApp (everywhere f a) (everywhere f b))
+everywhere f (ELam b bd)  = f (ELam b (everywhere f bd))
+
+renameAll :: Expr -> Expr
+renameAll = everywhere (over varName (map toUpper))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
new file mode 100644
index 0000000..02755a9
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
@@ -0,0 +1,49 @@
+// Same, with the single varName optic applied at every node of the
+// tree: how to reach the name is defined once, and the walk only
+// decides where it applies.
+object After:
+  case class Var(name: String, ref: Int)
+  enum Expr:
+    case EVar(v: Var)
+    case EApp(f: Expr, x: Expr)
+    case ELam(bind: String, body: Expr)
+
+  import Expr.*
+
+  case class Lens[S, A](view: S => A, set: (S, A) => S):
+    def modify(f: A => A): S => S = s => set(s, f(view(s)))
+  case class Prism[S, A](preview: S => Option[A], review: A => S):
+    def modify(f: A => A): S => S =
+      s => preview(s).map(a => review(f(a))).getOrElse(s)
+  case class PartialLens[S, A](preview: S => Option[A],
+                               modify: (A => A) => S => S)
+
+  def compose[S, M, A](p: Prism[S, M],
+                       l: Lens[M, A]): PartialLens[S, A] =
+    PartialLens(
+      preview = s => p.preview(s).map(l.view),
+      modify  = f => s => p.preview(s) match
+        case Some(m) => p.review(l.modify(f)(m))
+        case None    => s,
+    )
+
+  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
+    pl.modify(f)
+
+  val varP: Prism[Expr, Var] =
+    Prism[Expr, Var](
+      { case EVar(v) => Some(v); case _ => None },
+      EVar(_),
+    )
+  val nameL: Lens[Var, String] =
+    Lens[Var, String](_.name, (v, n) => v.copy(name = n))
+  val varName: PartialLens[Expr, String] = compose(varP, nameL)
+
+  // Bottom-up: apply the rewrite at every node, descending first.
+  def everywhere(f: Expr => Expr)(e: Expr): Expr = e match
+    case EVar(_)     => f(e)
+    case EApp(a, b)  => f(EApp(everywhere(f)(a), everywhere(f)(b)))
+    case ELam(b, bd) => f(ELam(b, everywhere(f)(bd)))
+
+  def renameAll(e: Expr): Expr =
+    everywhere(over(varName, _.toUpperCase))(e)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.hs
new file mode 100644
index 0000000..a8fa0fa
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.hs
@@ -0,0 +1,15 @@
+-- Uppercase the variable of every Var node: a recursive walk that
+-- rebuilds each hit by hand.
+module Before where
+
+import Data.Char (toUpper)
+
+data Var  = Var  { vName :: String, vRef :: Int }
+  deriving (Eq, Show)
+data Expr = EVar Var | EApp Expr Expr | ELam String Expr
+  deriving (Eq, Show)
+
+renameAll :: Expr -> Expr
+renameAll (EVar v)     = EVar v { vName = map toUpper (vName v) }
+renameAll (EApp f x)   = EApp (renameAll f) (renameAll x)
+renameAll (ELam b bd)  = ELam b (renameAll bd)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.scala
new file mode 100644
index 0000000..f7ea6c0
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Before.scala
@@ -0,0 +1,15 @@
+// Uppercase the variable of every Var node: a recursive walk that
+// rebuilds each hit by hand.
+object Before:
+  case class Var(name: String, ref: Int)
+  enum Expr:
+    case EVar(v: Var)
+    case EApp(f: Expr, x: Expr)
+    case ELam(bind: String, body: Expr)
+
+  import Expr.*
+
+  def renameAll(e: Expr): Expr = e match
+    case EVar(v)     => EVar(v.copy(name = v.name.toUpperCase))
+    case EApp(f, x)  => EApp(renameAll(f), renameAll(x))
+    case ELam(b, bd) => ELam(b, renameAll(bd))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.hs
new file mode 100644
index 0000000..96092da
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Data.Char (isUpper)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+-- A neutral tree, so one generated input feeds both Expr types.
+data T = TVar String Int | TApp T T | TLam String T
+  deriving (Eq, Show)
+
+genName :: Gen String
+genName = Gen.string (Range.linear 0 4) Gen.alpha
+
+genT :: Int -> Gen T
+genT depth =
+  let leaf = TVar <$> genName <*> Gen.int (Range.linear (-10) 10)
+  in if depth == 0 then leaf
+     else Gen.choice
+       [ leaf
+       , TApp <$> genT (depth - 1) <*> genT (depth - 1)
+       , TLam <$> genName <*> genT (depth - 1)
+       ]
+
+toBefore :: T -> Before.Expr
+toBefore (TVar n r) = Before.EVar (Before.Var n r)
+toBefore (TApp f x) = Before.EApp (toBefore f) (toBefore x)
+toBefore (TLam b e) = Before.ELam b (toBefore e)
+
+fromBefore :: Before.Expr -> T
+fromBefore (Before.EVar v)  = TVar (Before.vName v) (Before.vRef v)
+fromBefore (Before.EApp f x) = TApp (fromBefore f) (fromBefore x)
+fromBefore (Before.ELam b e) = TLam b (fromBefore e)
+
+toAfter :: T -> After.Expr
+toAfter (TVar n r) = After.EVar (After.Var n r)
+toAfter (TApp f x) = After.EApp (toAfter f) (toAfter x)
+toAfter (TLam b e) = After.ELam b (toAfter e)
+
+fromAfter :: After.Expr -> T
+fromAfter (After.EVar v)  = TVar (After.vName v) (After.vRef v)
+fromAfter (After.EApp f x) = TApp (fromAfter f) (fromAfter x)
+fromAfter (After.ELam b e) = TLam b (fromAfter e)
+
+prop_agrees :: Property
+prop_agrees = property $ do
+  t <- forAll (genT 4)
+  fromBefore (Before.renameAll (toBefore t))
+    === fromAfter (After.renameAll (toAfter t))
+
+allNamesUpper :: T -> Bool
+allNamesUpper (TVar n _) = all isUpper n
+allNamesUpper (TApp f x) = allNamesUpper f && allNamesUpper x
+allNamesUpper (TLam _ b) = allNamesUpper b
+
+refsUnchanged :: T -> T -> Bool
+refsUnchanged (TVar _ r1) (TVar _ r2) = r1 == r2
+refsUnchanged (TApp f1 x1) (TApp f2 x2) =
+  refsUnchanged f1 f2 && refsUnchanged x1 x2
+refsUnchanged (TLam _ b1) (TLam _ b2) = refsUnchanged b1 b2
+refsUnchanged _ _ = False
+
+prop_all_upper :: Property
+prop_all_upper = property $ do
+  t <- forAll (genT 4)
+  let renamed = fromAfter (After.renameAll (toAfter t))
+  allNamesUpper renamed === True
+  refsUnchanged renamed t === True
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("renameAll: Before == After", prop_agrees)
+    , ("every Var name is uppercased, refs unchanged", prop_all_upper)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
new file mode 100644
index 0000000..aa11809
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
@@ -0,0 +1,83 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("renameAll: Before == After", agrees),
+    property("every Var name is uppercased after the walk", allUpper),
+  )
+
+  // A neutral tree, so one generated input feeds both Expr types.
+  enum T:
+    case TVar(name: String, ref: Int)
+    case TApp(f: T, x: T)
+    case TLam(bind: String, body: T)
+
+  val genName: Gen[String] =
+    Gen.alpha.list(Range.linear(0, 4)).map(_.mkString)
+  def genT(depth: Int): Gen[T] =
+    val leaf =
+      for n <- genName; r <- Gen.int(Range.linear(-10, 10))
+      yield T.TVar(n, r)
+    if depth == 0 then leaf
+    else
+      Gen.choice1(
+        leaf,
+        for
+          f <- genT(depth - 1)
+          x <- genT(depth - 1)
+        yield T.TApp(f, x),
+        for b <- genName; body <- genT(depth - 1) yield T.TLam(b, body),
+      )
+
+  def toBefore(t: T): Before.Expr = t match
+    case T.TVar(n, r) => Before.Expr.EVar(Before.Var(n, r))
+    case T.TApp(f, x) => Before.Expr.EApp(toBefore(f), toBefore(x))
+    case T.TLam(b, e) => Before.Expr.ELam(b, toBefore(e))
+  def fromBefore(e: Before.Expr): T = e match
+    case Before.Expr.EVar(v)     => T.TVar(v.name, v.ref)
+    case Before.Expr.EApp(f, x)  => T.TApp(fromBefore(f), fromBefore(x))
+    case Before.Expr.ELam(b, e)  => T.TLam(b, fromBefore(e))
+  def toAfter(t: T): After.Expr = t match
+    case T.TVar(n, r) => After.Expr.EVar(After.Var(n, r))
+    case T.TApp(f, x) => After.Expr.EApp(toAfter(f), toAfter(x))
+    case T.TLam(b, e) => After.Expr.ELam(b, toAfter(e))
+  def fromAfter(e: After.Expr): T = e match
+    case After.Expr.EVar(v)     => T.TVar(v.name, v.ref)
+    case After.Expr.EApp(f, x)  => T.TApp(fromAfter(f), fromAfter(x))
+    case After.Expr.ELam(b, e)  => T.TLam(b, fromAfter(e))
+
+  def agrees: Property =
+    for t <- genT(4).forAll
+    yield
+      fromBefore(Before.renameAll(toBefore(t)))
+        ==== fromAfter(After.renameAll(toAfter(t)))
+
+  def allUpper: Property =
+    for t <- genT(4).forAll
+    yield
+      val renamed = fromAfter(After.renameAll(toAfter(t)))
+      (allNamesUpper(renamed) && refsUnchanged(renamed, t)) ==== true
+
+  def allNamesUpper(t: T): Boolean = t match
+    case T.TVar(n, _)   => n == n.toUpperCase
+    case T.TApp(f, x)   => allNamesUpper(f) && allNamesUpper(x)
+    case T.TLam(_, b)   => allNamesUpper(b)
+  def refsUnchanged(a: T, b: T): Boolean = (a, b) match
+    case (T.TVar(_, r1), T.TVar(_, r2)) => r1 == r2
+    case (T.TApp(f1, x1), T.TApp(f2, x2)) =>
+      refsUnchanged(f1, f2) && refsUnchanged(x1, x2)
+    case (T.TLam(_, b1), T.TLam(_, b2)) => refsUnchanged(b1, b2)
+    case _ => false
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg
new file mode 100644
index 0000000..196eeb9
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg
@@ -0,0 +1,46 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 216" role="img" aria-labelledby="d2-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d2-title">Replacing a recursive match with one optic reused at every node. Before: renameAll recurses over the tree and matches+rebuilds Var at each node by hand. After: everywhere(over(varName, upper)) — the same varName optic from example 1 applied at every node, bottom-up; the walk decides where, the optic decides how.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="136" rx="4"/>
+    <rect x="428" y="36" width="336" height="136" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="104" width="176" height="24" rx="3"/>
+    <rect x="210" y="128" width="176" height="24" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="56">renameAll(e) =</text>
+    <text x="40" y="72">e match</text>
+    <text x="52" y="88">EVar(v) =&gt; EVar(v.copy(name = upper))</text>
+    <text x="52" y="104">EApp(f, x) =&gt; EApp(renameAll(f),</text>
+    <text x="64" y="120">renameAll(x))</text>
+    <text x="52" y="134">ELam(b, bd) =&gt; ELam(b, renameAll(bd))</text>
+    <text x="52" y="156">the rebuild appears at</text>
+    <text x="52" y="170">every depth</text>
+    <text x="440" y="56">everywhere(over(varName, upper))</text>
+    <text x="452" y="72">walk decides where:</text>
+    <text x="464" y="88">every node, bottom-up</text>
+    <text x="452" y="108">varName decides how:</text>
+    <text x="464" y="124">prism then lens, from ex. 1</text>
+    <text x="452" y="148">one optic, reused</text>
+    <text x="452" y="164">at every depth</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1">
+    <circle cx="386" cy="166" r="7.5"/>
+    <circle cx="428" cy="166" r="7.5"/>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle">
+    <text x="386" y="170">1</text>
+    <text x="428" y="170">1</text>
+  </g>
+  <g fill="none" stroke="currentColor" stroke-width="1.2">
+    <path d="M406 166 H414"/>
+  </g>
+  <g fill="currentColor">
+    <path d="M414 162.5 L422 166 L414 169.5 Z"/>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
new file mode 100644
index 0000000..74e470b
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
@@ -0,0 +1,61 @@
+-- Same, with a small traversal composed with a prism and a lens:
+-- reach every element, match the succeeded branch, edit its value.
+module After where
+
+import Data.Maybe (listToMaybe)
+
+data Ok     = Ok     { okValue :: Int }
+  deriving (Eq, Show)
+data Result = Succeeded Ok | Failed String
+  deriving (Eq, Show)
+
+data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
+
+modifyL :: Lens s a -> (a -> a) -> s -> s
+modifyL l f s = set l (s, f (view l s))
+
+data Prism s a = Prism
+  { preview :: s -> Maybe a
+  , review  :: a -> s
+  }
+
+data PartialLens s a = PartialLens
+  { plPreview :: s -> Maybe a
+  , plModify  :: (a -> a) -> s -> s
+  }
+
+composeO :: Prism s m -> Lens m a -> PartialLens s a
+composeO p l = PartialLens
+  { plPreview = \s -> view l <$> preview p s
+  , plModify  = \f s -> case preview p s of
+      Nothing -> s
+      Just m  -> review p (modifyL l f m)
+  }
+
+-- Traversal: reach every element, and within it apply the
+-- partial lens (hits edit, misses pass through).
+each :: PartialLens s a -> PartialLens [s] a
+each pl = PartialLens
+  (\xs -> listToMaybe xs >>= plPreview pl)
+  (\g xs -> map (plModify pl g) xs)
+
+over :: PartialLens s a -> (a -> a) -> s -> s
+over pl = plModify pl
+
+succeededP :: Prism Result Ok
+succeededP = Prism
+  { preview = \r -> case r of Succeeded ok -> Just ok; _ -> Nothing
+  , review  = Succeeded
+  }
+
+valueL :: Lens Ok Int
+valueL = Lens { view = okValue, set = \(ok, v) -> ok { okValue = v } }
+
+okVal :: PartialLens Result Int
+okVal = composeO succeededP valueL
+
+eachSucceeded :: PartialLens [Result] Int
+eachSucceeded = each okVal
+
+bumpSucceeded :: [Result] -> [Result]
+bumpSucceeded = over eachSucceeded (+ 1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
new file mode 100644
index 0000000..5f3281c
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
@@ -0,0 +1,51 @@
+// Same, with a small traversal composed with a prism and a lens:
+// reach every element, match the succeeded branch, edit its value.
+object After:
+  case class Ok(value: Int)
+  enum Result:
+    case Succeeded(v: Ok)
+    case Failed(msg: String)
+
+  import Result.*
+
+  case class Lens[S, A](view: S => A, set: (S, A) => S):
+    def modify(f: A => A): S => S = s => set(s, f(view(s)))
+  case class Prism[S, A](preview: S => Option[A], review: A => S):
+    def modify(f: A => A): S => S =
+      s => preview(s).map(a => review(f(a))).getOrElse(s)
+  case class PartialLens[S, A](preview: S => Option[A],
+                               modify: (A => A) => S => S)
+
+  def compose[S, M, A](p: Prism[S, M],
+                       l: Lens[M, A]): PartialLens[S, A] =
+    PartialLens(
+      preview = s => p.preview(s).map(l.view),
+      modify  = f => s => p.preview(s) match
+        case Some(m) => p.review(l.modify(f)(m))
+        case None    => s,
+    )
+  // Traversal: reach every element, and within it apply the
+  // partial lens (hits edit, misses pass through).
+  def each[S, A](pl: PartialLens[S, A]): PartialLens[List[S], A] =
+    PartialLens(
+      preview = _.headOption.flatMap(pl.preview),
+      modify  = f => _.map(pl.modify(f)),
+    )
+
+  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
+    pl.modify(f)
+
+  val succeededP: Prism[Result, Ok] =
+    Prism[Result, Ok](
+      { case Succeeded(v) => Some(v); case _ => None },
+      Succeeded(_),
+    )
+  val valueL: Lens[Ok, Int] =
+    Lens[Ok, Int](_.value, (ok, v) => ok.copy(value = v))
+  val okValue: PartialLens[Result, Int] = compose(succeededP, valueL)
+
+  val eachSucceeded: PartialLens[List[Result], Int] =
+    each(okValue)
+
+  def bumpSucceeded(xs: List[Result]): List[Result] =
+    over(eachSucceeded, _ + 1)(xs)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.hs
new file mode 100644
index 0000000..082926d
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.hs
@@ -0,0 +1,14 @@
+-- Bump only the successes of a batch: a hand-written map carrying
+-- the branch test and the rebuild in the same step.
+module Before where
+
+data Ok     = Ok     { okValue :: Int }
+  deriving (Eq, Show)
+data Result = Succeeded Ok | Failed String
+  deriving (Eq, Show)
+
+bumpSucceeded :: [Result] -> [Result]
+bumpSucceeded = map step
+  where
+    step (Succeeded ok) = Succeeded ok { okValue = okValue ok + 1 }
+    step f@(Failed _)   = f
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.scala
new file mode 100644
index 0000000..b5bf0d3
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Before.scala
@@ -0,0 +1,15 @@
+// Bump only the successes of a batch: a hand-written map carrying
+// the branch test and the rebuild in the same step.
+object Before:
+  case class Ok(value: Int)
+  enum Result:
+    case Succeeded(v: Ok)
+    case Failed(msg: String)
+
+  import Result.*
+
+  def bumpSucceeded(xs: List[Result]): List[Result] =
+    xs.map {
+      case Succeeded(ok) => Succeeded(ok.copy(value = ok.value + 1))
+      case f @ Failed(_) => f
+    }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.hs
new file mode 100644
index 0000000..c64f6d4
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import Control.Monad (unless)
+import System.Exit (exitFailure)
+import Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import qualified Before
+import qualified After
+
+-- A neutral list element, so one generated input feeds both types.
+data R = Succeeded Int | Failed String
+  deriving (Eq, Show)
+
+genValue :: Gen Int
+genValue = Gen.int (Range.linear (-100) 100)
+
+genMsg :: Gen String
+genMsg = Gen.string (Range.linear 0 6) Gen.alpha
+
+genR :: Gen R
+genR = Gen.choice
+  [ Succeeded <$> genValue
+  , Failed <$> genMsg
+  ]
+
+toBefore :: R -> Before.Result
+toBefore (Succeeded v) = Before.Succeeded (Before.Ok v)
+toBefore (Failed m)    = Before.Failed m
+
+fromBefore :: Before.Result -> R
+fromBefore (Before.Succeeded ok) = Succeeded (Before.okValue ok)
+fromBefore (Before.Failed m)     = Failed m
+
+toAfter :: R -> After.Result
+toAfter (Succeeded v) = After.Succeeded (After.Ok v)
+toAfter (Failed m)    = After.Failed m
+
+fromAfter :: After.Result -> R
+fromAfter (After.Succeeded ok) = Succeeded (After.okValue ok)
+fromAfter (After.Failed m)     = Failed m
+
+prop_agrees :: Property
+prop_agrees = property $ do
+  xs <- forAll (Gen.list (Range.linear 0 10) genR)
+  map fromBefore (Before.bumpSucceeded (map toBefore xs))
+    === map fromAfter (After.bumpSucceeded (map toAfter xs))
+
+prop_only_succeeded :: Property
+prop_only_succeeded = property $ do
+  xs <- forAll (Gen.list (Range.linear 0 10) genR)
+  let bumped = map fromAfter (After.bumpSucceeded (map toAfter xs))
+  and (zipWith check bumped xs) === True
+  where
+    check (Succeeded v1) (Succeeded v0) = v1 == v0 + 1
+    check (Failed m1)    (Failed m0)    = m1 == m0
+    check _ _                           = False
+
+main :: IO ()
+main = do
+  ok <- checkParallel $ Group "Props"
+    [ ("bumpSucceeded: Before == After", prop_agrees)
+    , ("only successes bumped, messages pass through",
+      prop_only_succeeded)
+    ]
+  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
new file mode 100644
index 0000000..6400727
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
@@ -0,0 +1,65 @@
+//> using scala 3.3.4
+//> using dep qa.hedgehog::hedgehog-core:0.14.0
+//> using dep qa.hedgehog::hedgehog-runner:0.14.0
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object Props extends Properties:
+  def tests: List[Test] = List(
+    property("bumpSucceeded: Before == After", agrees),
+    property("only successes are bumped, messages pass through",
+      onlySucceeded),
+  )
+
+  // A neutral list, so one generated input feeds both Result types.
+  enum R:
+    case Succeeded(value: Int)
+    case Failed(msg: String)
+
+  val genValue: Gen[Int] = Gen.int(Range.linear(-100, 100))
+  val genMsg: Gen[String] =
+    Gen.alpha.list(Range.linear(0, 6)).map(_.mkString)
+  def genR: Gen[R] =
+    Gen.choice1(
+      genValue.map(R.Succeeded(_)),
+      genMsg.map(R.Failed(_)),
+    )
+
+  def toBefore(r: R): Before.Result = r match
+    case R.Succeeded(v) => Before.Result.Succeeded(Before.Ok(v))
+    case R.Failed(m)    => Before.Result.Failed(m)
+  def fromBefore(r: Before.Result): R = r match
+    case Before.Result.Succeeded(ok) => R.Succeeded(ok.value)
+    case Before.Result.Failed(m)     => R.Failed(m)
+  def toAfter(r: R): After.Result = r match
+    case R.Succeeded(v) => After.Result.Succeeded(After.Ok(v))
+    case R.Failed(m)    => After.Result.Failed(m)
+  def fromAfter(r: After.Result): R = r match
+    case After.Result.Succeeded(ok) => R.Succeeded(ok.value)
+    case After.Result.Failed(m)     => R.Failed(m)
+
+  def agrees: Property =
+    for xs <- genR.list(Range.linear(0, 10)).forAll
+    yield
+      Before.bumpSucceeded(xs.map(toBefore)).map(fromBefore)
+        ==== After.bumpSucceeded(xs.map(toAfter)).map(fromAfter)
+
+  def onlySucceeded: Property =
+    for xs <- genR.list(Range.linear(0, 10)).forAll
+    yield
+      val bumped =
+        After.bumpSucceeded(xs.map(toAfter)).map(fromAfter)
+      bumped.zip(xs).forall {
+        case (R.Succeeded(v1), R.Succeeded(v0)) => v1 == v0 + 1
+        case (R.Failed(m1), R.Failed(m0))       => m1 == m0
+        case _                                  => false
+      } ==== true
+
+@main def spec(): Unit =
+  val results = Props.tests.map { t =>
+    val r = Property.check(t.withConfig(PropertyConfig.default),
+      t.result, Seed.fromTime())
+    println(Test.renderReport(
+      "Props", t, r, ansiCodesSupported = false))
+    r.status
+  }
+  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/diagram.svg
new file mode 100644
index 0000000..217a73f
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/diagram.svg
@@ -0,0 +1,32 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 216" role="img" aria-labelledby="d3-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
+  <title id="d3-title">Replacing a map-with-match with a composed traversal, prism and lens. Before: bumpSucceeded maps with a branch test and rebuild in the same step. After: each .andThen succeeded .andThen value — the traversal reaches every element, the prism selects the succeeded branch, the lens edits its value; failures pass through untouched.</title>
+  <g fill="currentColor" font-size="12" opacity=".6">
+    <text x="16" y="26">before</text>
+    <text x="428" y="26">after</text>
+  </g>
+  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
+    <rect x="16" y="36" width="388" height="136" rx="4"/>
+    <rect x="428" y="36" width="336" height="136" rx="4"/>
+  </g>
+  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
+    <rect x="44" y="100" width="332" height="26" rx="3"/>
+  </g>
+  <g fill="currentColor" font-size="12">
+    <text x="28" y="56">bumpSucceeded(xs) =</text>
+    <text x="40" y="72">xs.map { case Succeeded(ok) =&gt;</text>
+    <text x="52" y="88">Succeeded(ok.copy(value = ok.value + 1))</text>
+    <text x="52" y="104">case f @ Failed(_) =&gt; f }</text>
+    <text x="52" y="126">branch test and rebuild</text>
+    <text x="52" y="140">in the same step</text>
+    <text x="440" y="56">each .andThen succeeded</text>
+    <text x="452" y="72">.andThen value</text>
+    <text x="440" y="92">every element,</text>
+    <text x="452" y="108">succeeded branch,</text>
+    <text x="452" y="124">edit its value</text>
+    <text x="440" y="144">failures pass through</text>
+  </g>
+  <g fill="currentColor" font-size="12" text-anchor="middle" opacity=".8">
+    <text x="220" y="166">traversal over the list</text>
+    <text x="596" y="166">composed optic</text>
+  </g>
+</svg>
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
deleted file mode 100644
index fccc9f3..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.hs
+++ /dev/null
@@ -1,19 +0,0 @@
--- Same, with a lens on the size field: the write goes through the
--- lens; the recursion over children is unchanged.
-module After where
-
-data Node = Node { name :: String, size :: Int, children :: [Node] }
-  deriving (Eq, Show)
-
-data Lens s a = Lens { get :: s -> a, set :: a -> s -> s }
-
-modify :: Lens s a -> (a -> a) -> s -> s
-modify l f s = set l (f (get l s)) s
-
-sizeLens :: Lens Node Int
-sizeLens = Lens { get = size, set = \v n -> n { size = v } }
-
-bumpSizes :: Node -> Int -> Node
-bumpSizes n by =
-  modify sizeLens (+ by)
-    (n { children = map (`bumpSizes` by) (children n) })
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
deleted file mode 100644
index 8d5de15..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/After.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-// Same, with a lens on the size field: the write goes through the
-// lens; the recursion over children is unchanged.
-object After:
-  case class Node(name: String, size: Int, children: List[Node])
-
-  case class Lens[S, A](get: S => A, set: A => S => S):
-    def modify(f: A => A): S => S = s => set(f(get(s)))(s)
-
-  val size: Lens[Node, Int] =
-    Lens[Node, Int](_.size, v => n => n.copy(size = v))
-
-  def bumpSizes(n: Node, by: Int): Node =
-    size.modify(_ + by)(
-      n.copy(children = n.children.map(bumpSizes(_, by))))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
deleted file mode 100644
index 8db5c56..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.hs
+++ /dev/null
@@ -1,11 +0,0 @@
--- Grow the size of every node of a file tree by the same amount.
-module Before where
-
-data Node = Node { name :: String, size :: Int, children :: [Node] }
-  deriving (Eq, Show)
-
-bumpSizes :: Node -> Int -> Node
-bumpSizes n by =
-  n { size = size n + by
-    , children = map (`bumpSizes` by) (children n)
-    }
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
deleted file mode 100644
index bb46c12..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Before.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-// Grow the size of every node of a file tree by the same amount.
-object Before:
-  case class Node(name: String, size: Int, children: List[Node])
-
-  def bumpSizes(n: Node, by: Int): Node =
-    n.copy(
-      size = n.size + by,
-      children = n.children.map(bumpSizes(_, by)))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
deleted file mode 100644
index 51bc397..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.hs
+++ /dev/null
@@ -1,56 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-module Main where
-
-import Control.Monad (unless)
-import System.Exit (exitFailure)
-import Hedgehog
-import qualified Hedgehog.Gen as Gen
-import qualified Hedgehog.Range as Range
-import qualified Before
-import qualified After
-
-genName :: Gen String
-genName = ("n" <>) . show <$> Gen.int (Range.linear 0 9)
-
-genSize :: Gen Int
-genSize = Gen.int (Range.linear (-20) 20)
-
-genNode :: Int -> Gen Before.Node
-genNode depth =
-  let leaf = Before.Node <$> genName <*> genSize <*> pure []
-  in if depth == 0 then leaf
-     else Gen.choice
-       [ leaf
-       , Before.Node <$> genName <*> genSize
-           <*> Gen.list (Range.linear 0 3) (genNode (depth - 1))
-       ]
-
-toAfter :: Before.Node -> After.Node
-toAfter (Before.Node n s cs) = After.Node n s (map toAfter cs)
-
--- toAfter maps a whole tree faithfully, so After's result can be
--- compared with the converted Before result.
-prop_agrees :: Property
-prop_agrees = property $ do
-  n  <- forAll (genNode 3)
-  by <- forAll genSize
-  After.bumpSizes (toAfter n) by === toAfter (Before.bumpSizes n by)
-
-prop_laws :: Property
-prop_laws = property $ do
-  n  <- forAll (genNode 1)
-  v1 <- forAll genSize
-  v2 <- forAll genSize
-  let l   = After.sizeLens
-      m   = toAfter n
-  After.get l (After.set l v1 m) === v1
-  After.set l (After.get l m) m === m
-  After.set l v2 (After.set l v1 m) === After.set l v2 m
-
-main :: IO ()
-main = do
-  ok <- checkParallel $ Group "Props"
-    [ ("bumpSizes: Before == After", prop_agrees)
-    , ("size lens obeys the laws on generated nodes", prop_laws)
-    ]
-  unless ok exitFailure
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
deleted file mode 100644
index 0093363..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/Spec.scala
+++ /dev/null
@@ -1,68 +0,0 @@
-//> using scala 3.3.4
-//> using dep qa.hedgehog::hedgehog-core:0.14.0
-//> using dep qa.hedgehog::hedgehog-runner:0.14.0
-import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
-
-object Props extends Properties:
-  def tests: List[Test] = List(
-    property("bumpSizes: Before == After", agrees),
-    property("the size lens obeys get-put, put-get, put-put", laws),
-  )
-
-  val genName: Gen[String] =
-    for n <- Gen.int(Range.linear(0, 9)) yield "n" + n.toString
-  val genSize: Gen[Int] = Gen.int(Range.linear(-20, 20))
-
-  def genNode(depth: Int): Gen[Before.Node] =
-    val leaf =
-      for n <- genName; s <- genSize yield Before.Node(n, s, Nil)
-    if depth == 0 then leaf
-    else
-      Gen.choice1(
-        leaf,
-        for
-          n  <- genName
-          s  <- genSize
-          cs <- genNode(depth - 1).list(Range.linear(0, 3))
-        yield Before.Node(n, s, cs)
-        ,
-      )
-
-  def toAfter(n: Before.Node): After.Node = n match
-    case Before.Node(nm, s, cs) => After.Node(nm, s, cs.map(toAfter))
-
-  def same(b: Before.Node, a: After.Node): Boolean = (b, a) match
-    case (Before.Node(n1, s1, c1), After.Node(n2, s2, c2)) =>
-      n1 == n2 && s1 == s2 && c1.size == c2.size &&
-        c1.zip(c2).forall((x, y) => same(x, y))
-
-  def agrees: Property =
-    for
-      n  <- genNode(3).forAll
-      by <- genSize.forAll
-    yield
-      val b = Before.bumpSizes(n, by)
-      val a = After.bumpSizes(toAfter(n), by)
-      same(b, a) ==== true
-
-  def laws: Property =
-    for
-      n  <- genNode(1).forAll
-      v1 <- genSize.forAll
-      v2 <- genSize.forAll
-    yield
-      val l = After.size
-      val m = toAfter(n)
-      l.get(l.set(v1)(m)) ==== v1 and
-        l.set(l.get(m))(m) ==== m and
-        l.set(v2)(l.set(v1)(m)) ==== l.set(v2)(m)
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg b/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg
deleted file mode 100644
index cbff7fb..0000000
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-file-tree/diagram.svg
+++ /dev/null
@@ -1,40 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 780 200" role="img" aria-labelledby="d3-title" style="width:100%;height:auto;font-family:inherit;font-variant-ligatures:none;font-feature-settings:'calt' 0">
-  <title id="d3-title">Replacing a direct field write with a lens inside a recursive traversal. Before: bumpSizes(n, by) writes n.copy(size = n.size + by) then recurses over children. After: bumpSizes uses sizeLens.modify(_ + by)(n) to write the size and recurses over children unchanged; the recursion and the write are two independent steps and the write goes through the lens.</title>
-  <g fill="currentColor" font-size="12" opacity=".6">
-    <text x="16" y="26">before</text>
-    <text x="428" y="26">after</text>
-  </g>
-  <g fill="rgba(128,128,128,.07)" stroke="currentColor" stroke-width="1">
-    <rect x="16" y="36" width="388" height="128" rx="4"/>
-    <rect x="428" y="36" width="336" height="128" rx="4"/>
-  </g>
-  <g fill="rgba(128,128,128,.12)" stroke="currentColor" stroke-width="1" stroke-dasharray="4 3">
-    <rect x="44" y="76" width="332" height="34" rx="3"/>
-  </g>
-  <g fill="currentColor" font-size="12">
-    <text x="28" y="58">bumpSizes(n: Node, by) =</text>
-    <text x="40" y="76">n.copy(</text>
-    <text x="52" y="94">size = n.size + by,</text>
-    <text x="52" y="112">children = children.map(bumpSizes(_, by)))</text>
-    <text x="52" y="140">field write spelled out</text>
-    <text x="440" y="58">bumpSizes(n: Node, by) =</text>
-    <text x="452" y="76">sizeLens.modify(_ + by)(</text>
-    <text x="464" y="94">n.copy(children = children.map(bumpSizes(_, by))))</text>
-    <text x="452" y="140">write through the lens,</text>
-    <text x="452" y="158">recursion unchanged</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1">
-    <circle cx="386" cy="118" r="7.5"/>
-    <circle cx="428" cy="118" r="7.5"/>
-  </g>
-  <g fill="currentColor" font-size="12" text-anchor="middle">
-    <text x="386" y="122">1</text>
-    <text x="428" y="122">1</text>
-  </g>
-  <g fill="none" stroke="currentColor" stroke-width="1.2">
-    <path d="M406 118 H414"/>
-  </g>
-  <g fill="currentColor">
-    <path d="M414 114.5 L422 118 L414 121.5 Z"/>
-  </g>
-</svg>

From b59bde961b937c50e2912cc6d00292dbe2f5f20d Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 22:13:35 +0200
Subject: [PATCH 3/6] LESSONS: record the optics review round for entry 02

---
 .claude/skills/refactoring-entry/LESSONS.md | 22 +++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
index 53d07b1..036400c 100644
--- a/.claude/skills/refactoring-entry/LESSONS.md
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -102,3 +102,25 @@ brief.md or workflow.js and deleted here. Keep the calibration table current.
 - **Workflow-runner gap.** This environment has no Claude Code `Workflow` batch runner; executed the
   workflow phases directly (research → citation verify → examples → mutate/probes → diagrams). Recorded
   findings here so the skill's workflow prompt matches when the runner is available.
+
+## 2026-09-26 — 02 Replace mutable fields with lenses (post-PR review rework)
+
+- **Reviewer (kryptt) asked for the optics framing, not the lens framing.** The entry should teach
+  *optics* (lens · prism · traversal) and the "how to reach vs what to do" separation, mention that
+  optics are lawful *by construction* (not per-example law properties in the page), reuse the eo
+  cookbook recipes, and justify the inverse by decoupling not paying for itself (no cross-domain
+  boundaries). Law-solvers (cats-eo-laws, monocle-law, genvalidity-hspec-optics) belong in
+  Verification, not as hand-written law properties.
+- **Rule.** Example trios should escalate *nesting* (single node → every tree node → sparse walk over a
+  list) so the composed optic's value is visible; the setter-optic encoding (`(a -> a) -> (s -> s)`)
+  is compact but reads cryptic next to same-shaped Lens/Prism data types — prefer explicit
+  `Lens`/`Prism`/`Traversal` cases with `compose` (prism .andThen lens, each .andThen prism .andThen
+  lens) for the page.
+- **Rule (spec comparison).** Keep comparing via projected tuples/`from*` converters (Before/After
+  have distinct record types), and add a *purpose* second property (hit/miss, only-X-changed) rather
+  than also the lens laws — laws are by construction, the purpose property is the page's real check.
+- **Generators.** `Gen.unicode` yields control chars (`\NUL`) that `toUpper` leaves alone; for
+  "all names uppercased" style invariants use `Gen.alpha` (ASCII letters) or exclude non-letter
+  inputs explicitly. `Gen.list/Gen.string` argument order differs between Scala and Haskell hedgehog.
+- **Time.** Rework cost ≈ 1h (examples+specs+diagrams+page). The eo cookbook itself is the source of
+  truth for optics recipes; reference it with anchors.

From b91c8992fa577f57a406d7fc20bd921952eba092 Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 22:34:25 +0200
Subject: [PATCH 4/6] Hide shared example setup; make the skill agent-agnostic
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Move the optic building blocks (Lens/Prism/PartialLens/each) and the
  hedgehog spec runner out of the examples into pages/.../shared/,
  compiled by run.sh (scala-cli sources + runghc -i) but never shown on
  the page. Each Before/After/Spec is now the move itself; the page
  notes the shared setup is hidden.
- SKILL.md/brief.md: fold in the rule (shared setup is accidental
  complexity if shown; hide it in non-published shared/), and generalize
  the skill for any agent — the workflow is described as phases
  (research · examples · review · diagrams), with the Claude Workflow
  script as one optional orchestrator and the gh step generalized.
- LESSONS.md: record the round.
---
 .claude/skills/refactoring-entry/LESSONS.md   | 15 +++++
 .claude/skills/refactoring-entry/SKILL.md     | 59 ++++++++++---------
 .claude/skills/refactoring-entry/brief.md     |  4 +-
 .../replace-mutable-fields-with-lenses.md     | 15 ++---
 .../01-rename-var/After.hs                    | 34 +----------
 .../01-rename-var/After.scala                 | 26 +-------
 .../01-rename-var/Spec.scala                  | 11 +---
 .../02-rename-tree/After.hs                   | 37 ++----------
 .../02-rename-tree/After.scala                | 22 +------
 .../02-rename-tree/Spec.scala                 | 11 +---
 .../03-bump-oks/After.hs                      | 35 +----------
 .../03-bump-oks/After.scala                   | 34 ++---------
 .../03-bump-oks/Spec.scala                    | 11 +---
 .../replace-mutable-fields-with-lenses/run.sh | 10 +++-
 .../shared/Optics.hs                          | 39 ++++++++++++
 .../shared/Optics.scala                       | 32 ++++++++++
 .../shared/SpecRunner.scala                   | 15 +++++
 17 files changed, 170 insertions(+), 240 deletions(-)
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
 create mode 100644 pages/refactorings/replace-mutable-fields-with-lenses/shared/SpecRunner.scala

diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
index 036400c..0951032 100644
--- a/.claude/skills/refactoring-entry/LESSONS.md
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -124,3 +124,18 @@ brief.md or workflow.js and deleted here. Keep the calibration table current.
   inputs explicitly. `Gen.list/Gen.string` argument order differs between Scala and Haskell hedgehog.
 - **Time.** Rework cost ≈ 1h (examples+specs+diagrams+page). The eo cookbook itself is the source of
   truth for optics recipes; reference it with anchors.
+
+## 2026-09-26 — 02 shared/ setup must not appear on the page (post-PR review round 2)
+
+- **Rule (blocking).** Setup shared between examples is *accidental complexity* if shown. A lens
+  entry redefining `Lens`/`Prism`/`PartialLens` in every `After` buries the motivation in the
+  definition of the tool. Move shared machinery to `pages/refactorings/<slug>/shared/` — compiled
+  by `run.sh` (`scala-cli run "$d" --main-class spec "$SHARED"`, `runghc -i"$SHARED"`), never
+  `include_relative`'d. Executed in 02: `shared/Optics.scala|.hs` and `shared/SpecRunner.scala`;
+  the page says the shared files are hidden, each example is the move itself.
+  → folded into SKILL.md §3 and brief.md.
+- **Skill must be agent-agnostic.** It lived in `.claude/skills/` and assumed the Claude Code
+  `Workflow(...)` runner. Rewrote §2 (the workflow) to describe the phases generically — research ·
+  examples · review · diagrams — with the Claude `workflow.js`/`journal.jsonl` as one optional
+  orchestrator, and generalized the `gh`/ship steps. The `Workflow` script stays but nothing else
+  assumes Claude.
diff --git a/.claude/skills/refactoring-entry/SKILL.md b/.claude/skills/refactoring-entry/SKILL.md
index a5f3bbe..450fbf4 100644
--- a/.claude/skills/refactoring-entry/SKILL.md
+++ b/.claude/skills/refactoring-entry/SKILL.md
@@ -26,34 +26,30 @@ the steps below and the `workflow.js` prompts; if you find one that has not, fol
 1. Branch from `master`: `refactoring/<slug>`.
 2. Pick the entry: the first item in `_data/refactorings.yml` without a `slug`, unless the user
    names one. Add `slug: <slug>` to it (that is what links it on the index page).
-3. Toolchain check (the workflow agents assume these work):
+3. Toolchain check (the agents assume these work):
    - `scala-cli --version` (hedgehog `qa.hedgehog::hedgehog-core:0.14.0` + `hedgehog-runner:0.14.0`).
    - `docker image inspect cp-hedgehog` — if missing, `sh pages/refactorings/extract-method/run.sh`
-     builds it (about 2.5 minutes). GHC is not installed on the host; nix is read-only.
+     builds it (about 2.5 minutes). GHC is not installed here; nix is read-only.
 4. Write the brief to the scratchpad: copy `brief.md` from this directory, fill the `<...>` fields.
-   The workflow agents read the brief, not this file.
-
-## 2. Run the workflow (research ∥ examples → verify loop → diagrams)
-
-```
-Workflow({
-  scriptPath: ".claude/skills/refactoring-entry/workflow.js",
-  args: {
-    slug: "<slug>", name: "<Name>", number: <n>, total: 35,
-    brief: "<abs path to brief.md>", scratch: "<abs scratchpad dir>",
-    repo: "<abs repo root>",
-    seeds: ["<paper or tool that anchors the OO side>", "<the FP-side paper>", ...],
-    examples: ["<example 1 idea>", "<example 2 idea>", "<example 3 idea>"]
-  }
-})
-```
-
-- The script runs two tracks in parallel: **research → per-citation skeptics → fix-up**, and
-  **examples → reviewer (mutation + adversarial probes) → fix, up to 3 rounds → diagrams**.
-- If an agent dies (session limit, API error), relaunch with `resumeFromRunId`; finished agents replay
-  from cache. Read `journal.jsonl` before assuming a result is empty.
-- While it runs: write `pages/refactorings/<slug>.md` from the extract-method page (next step), and
-  build the site in a scratch copy with stub SVGs to catch Liquid errors early.
+   The agents that build the entry read the brief, not this file.
+
+## 2. Run the workflow (research ∥ examples → review → diagrams)
+
+This skill describes a *workflow*, not a Claude-specific runner. The phases below are mandatory;
+how you parallelise them depends on your agent runtime:
+
+- **Research** — with verified citations (one skeptic pass per reference), and
+- **Examples** — build + run the 3 Before/After/Spec pairs in both languages, then
+- **Review** — mutation-check + adversarial probes; fix, up to 3 rounds, then
+- **Diagrams** — inline SVG koan + one per example.
+
+If your runtime provides a batch/orchestration runner (e.g. `workflow.js` in this directory is a
+Claude Code `Workflow` script that runs both tracks in parallel and resumes crashed agents from
+`journal.jsonl`), use it with `slug/name/number/total/brief/scratch/repo/seeds/examples` args — but
+any agent can run the phases itself in order (research → citation checks → examples → review →
+diagrams), which is exactly what `workflow.js` does under the hood. While research runs, write
+`pages/refactorings/<slug>.md` from the extract-method page (next step) and build the site in a
+scratch copy with stub SVGs to catch Liquid errors early.
 
 ## 3. Assemble the page
 
@@ -82,9 +78,17 @@ Rules that came from review, keep them:
   markdown inside raw block HTML, and IALs on numbered items break the list).
 - Source lines ≤ 72 characters or the pane scrolls horizontally on a 1280px screen.
 - No `{{` `}}` `{%` `%}` in any included source (Liquid runs before highlighting).
-- Copy `run.sh` from extract-method unchanged into the new sources directory.
+- Copy `run.sh` from extract-method unchanged into the new sources directory (then adjust it only
+  if the entry has a real reason to, e.g. a `shared/` module — see next bullet).
 - Add the new sources directory to `exclude:` in `_config.yml` (sources are included via
   `include_relative`, not published as static files).
+- **Setup shared across examples lives in `shared/` and is never shown on the page.** If the entry
+  needs shared machinery (an optic library, a hedgehog spec runner, a common data type), put it in
+  `pages/refactorings/<slug>/shared/` and have `run.sh` compile it (`scala-cli run "$d" … "$SHARED"`
+  for Scala, `-i"$SHARED"` for Haskell) — but do NOT `include_relative` it. Each Example
+  `Before/After/Spec` on the page is then the *move itself*, with a one-line note in the page that
+  the shared setup is hidden. The reviewer considers inline setup (e.g. redefining a Lens type in
+  every After) accidental complexity that buries the motivation.
 - Do not claim totality or purity the code does not have (e.g. `Int` `div` overflow).
 
 ## 4. Verify before the PR
@@ -100,7 +104,8 @@ Rules that came from review, keep them:
 ## 5. Ship
 
 Commit sources + page + data + config on the branch; push (SSH remote works; if `gh auth status`
-fails ask the user to run `! gh auth login -h github.com -p ssh -w`); open the PR with the
+fails ask the user to run `! gh auth login -h github.com -p ssh -w` — or use whichever GitHub
+tool your environment provides); open the PR with the
 reviewer's mutation table and probe summary in the body. The PR preview URL is
 `https://www.constructive.dev/pr-preview/pr-<N>/refactorings/<slug>/`.
 
diff --git a/.claude/skills/refactoring-entry/brief.md b/.claude/skills/refactoring-entry/brief.md
index cb78550..3440ea0 100644
--- a/.claude/skills/refactoring-entry/brief.md
+++ b/.claude/skills/refactoring-entry/brief.md
@@ -38,7 +38,9 @@ when it does not apply.
 
 ## Code layout (examples agent writes these; reviewer runs them)
 pages/refactorings/<slug>/
-  run.sh                      # copied unchanged from extract-method; runs every NN-*/ dir in both languages
+  run.sh                      # copied from extract-method; runs every NN-*/ dir in both languages
+  shared/                     # shared setup (optics, spec runner, common types) — compiled in,
+                              # NEVER included on the page; each example is then the move itself
   NN-<ex>/Before.scala        # object Before { ... }   the pre-refactoring program
   NN-<ex>/After.scala         # object After  { ... }   the refactored version (same public entry point signature)
   NN-<ex>/Spec.scala          # hedgehog property: forAll generated inputs, Before.f(x) ==== After.f(x). `@main def spec()`.
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses.md b/pages/refactorings/replace-mutable-fields-with-lenses.md
index ca7da9b..b4246cc 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses.md
+++ b/pages/refactorings/replace-mutable-fields-with-lenses.md
@@ -175,13 +175,14 @@ the entry point.
 ## Three examples
 
 Each example is the same program twice, `Before` and `After`, in Scala 3
-and in Haskell, using a tiny self-contained optic encoding — a lens, a
-prism, a traversal, and the compositions between them — so the sources
-run with no dependencies. The entry point keeps its name and its type,
-the optic is the only difference, and a hedgehog property generates
-inputs and demands that both versions agree on every one of them. The
-three are eo's "navigate structures" recipes, in increasing depth of
-nesting.
+and in Haskell. The optic building blocks — a lens, a prism, a
+traversal, and the compositions between them — and the hedgehog spec
+runner live in the entry's `shared/` directory: compiled by `run.sh`,
+never shown on the page, so each example is the move itself. The entry
+point keeps its name and its type, the optic is the only difference,
+and a hedgehog property verifies that both versions agree on every
+generated input. The three are eo's "navigate structures" recipes, in
+increasing depth of nesting.
 
 ### 1 · A single node: prism and lens composed
 
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
index 9051ef1..f6aa34c 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.hs
@@ -3,45 +3,13 @@
 module After where
 
 import Data.Char (toUpper)
+import Optics (Lens(..), Prism(..), PartialLens(..), composeO, over)
 
 data Var   = Var   { vName :: String, vRef :: Int }
   deriving (Eq, Show)
 data Expr  = EVar Var | EApp Expr Expr | ELam String Expr
   deriving (Eq, Show)
 
-data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
-
-modifyL :: Lens s a -> (a -> a) -> s -> s
-modifyL l f s = set l (s, f (view l s))
-
-data Prism s a = Prism
-  { preview :: s -> Maybe a
-  , review  :: a -> s
-  }
-
-modifyP :: Prism s a -> (a -> a) -> s -> s
-modifyP p f s = case preview p s of
-  Nothing -> s
-  Just a  -> review p (f a)
-
--- A prism followed by a lens: hit -> edit the field;
--- miss -> pass through.
-data PartialLens s a = PartialLens
-  { plPreview :: s -> Maybe a
-  , plModify  :: (a -> a) -> s -> s
-  }
-
-composeO :: Prism s m -> Lens m a -> PartialLens s a
-composeO p l = PartialLens
-  { plPreview = \s -> view l <$> preview p s
-  , plModify  = \f s -> case preview p s of
-      Nothing -> s
-      Just m  -> review p (modifyL l f m)
-  }
-
-over :: PartialLens s a -> (a -> a) -> s -> s
-over pl = plModify pl
-
 varP :: Prism Expr Var
 varP = Prism
   { preview = \e -> case e of EVar v -> Just v; _ -> Nothing
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
index 227f22e..ec14d6d 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/After.scala
@@ -1,6 +1,8 @@
 // Same, as one composed optic: the prism matches the Var branch,
 // the lens edits its name, every other shape passes through.
 object After:
+  import Optics.*
+
   case class Var(name: String, ref: Int)
   enum Expr:
     case EVar(v: Var)
@@ -9,29 +11,6 @@ object After:
 
   import Expr.*
 
-  case class Lens[S, A](view: S => A, set: (S, A) => S):
-    def modify(f: A => A): S => S = s => set(s, f(view(s)))
-
-  case class Prism[S, A](preview: S => Option[A], review: A => S):
-    def modify(f: A => A): S => S =
-      s => preview(s).map(a => review(f(a))).getOrElse(s)
-  // A prism followed by a lens: hit → edit the field;
-  // miss → pass through.
-  case class PartialLens[S, A](preview: S => Option[A],
-                               modify: (A => A) => S => S)
-
-  def compose[S, M, A](p: Prism[S, M],
-                     l: Lens[M, A]): PartialLens[S, A] =
-    PartialLens(
-      preview = s => p.preview(s).map(l.view),
-      modify  = f => s => p.preview(s) match
-        case Some(m) => p.review(l.modify(f)(m))
-        case None    => s,
-    )
-
-  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
-    pl.modify(f)
-
   val varP: Prism[Expr, Var] =
     Prism[Expr, Var](
       { case EVar(v) => Some(v); case _ => None },
@@ -39,7 +18,6 @@ object After:
     )
   val nameL: Lens[Var, String] =
     Lens[Var, String](_.name, (v, n) => v.copy(name = n))
-
   val varName: PartialLens[Expr, String] = compose(varP, nameL)
 
   def upperVarName(e: Expr): Expr = over(varName, _.toUpperCase)(e)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
index 7f90a4d..849a47a 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/01-rename-var/Spec.scala
@@ -73,13 +73,4 @@ object Props extends Properties:
     case T.TVar(_, _)   => false
     case T.TApp(f, x)   => tNoVars(f) && tNoVars(x)
     case T.TLam(_, b)   => tNoVars(b)
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
+@main def spec(): Unit = SpecRunner.run(Props.tests)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
index 2662157..be151a2 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
@@ -1,41 +1,16 @@
--- Same, with the single varName optic applied at every node of the
+-- Same, with the same varName optic applied at every node of the
 -- tree: how to reach the name is defined once, and the walk only
 -- decides where it applies.
 module After where
 
 import Data.Char (toUpper)
+import Optics (Lens(..), Prism(..), PartialLens(..), composeO, over)
 
-data Var  = Var  { vName :: String, vRef :: Int }
+data Var = Var { vName :: String, vRef :: Int }
   deriving (Eq, Show)
 data Expr = EVar Var | EApp Expr Expr | ELam String Expr
   deriving (Eq, Show)
 
-data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
-
-modifyL :: Lens s a -> (a -> a) -> s -> s
-modifyL l f s = set l (s, f (view l s))
-
-data Prism s a = Prism
-  { preview :: s -> Maybe a
-  , review  :: a -> s
-  }
-
-data PartialLens s a = PartialLens
-  { plPreview :: s -> Maybe a
-  , plModify  :: (a -> a) -> s -> s
-  }
-
-composeO :: Prism s m -> Lens m a -> PartialLens s a
-composeO p l = PartialLens
-  { plPreview = \s -> view l <$> preview p s
-  , plModify  = \f s -> case preview p s of
-      Nothing -> s
-      Just m  -> review p (modifyL l f m)
-  }
-
-over :: PartialLens s a -> (a -> a) -> s -> s
-over pl = plModify pl
-
 varP :: Prism Expr Var
 varP = Prism
   { preview = \e -> case e of EVar v -> Just v; _ -> Nothing
@@ -50,9 +25,9 @@ varName = composeO varP nameL
 
 -- Bottom-up: apply the rewrite at every node, descending first.
 everywhere :: (Expr -> Expr) -> Expr -> Expr
-everywhere f e@(EVar _)   = f e
-everywhere f (EApp a b)   = f (EApp (everywhere f a) (everywhere f b))
-everywhere f (ELam b bd)  = f (ELam b (everywhere f bd))
+everywhere f e@(EVar _)    = f e
+everywhere f (EApp a b)    = f (EApp (everywhere f a) (everywhere f b))
+everywhere f (ELam b bd)   = f (ELam b (everywhere f bd))
 
 renameAll :: Expr -> Expr
 renameAll = everywhere (over varName (map toUpper))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
index 02755a9..1938ca0 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
@@ -2,6 +2,8 @@
 // tree: how to reach the name is defined once, and the walk only
 // decides where it applies.
 object After:
+  import Optics.*
+
   case class Var(name: String, ref: Int)
   enum Expr:
     case EVar(v: Var)
@@ -10,26 +12,6 @@ object After:
 
   import Expr.*
 
-  case class Lens[S, A](view: S => A, set: (S, A) => S):
-    def modify(f: A => A): S => S = s => set(s, f(view(s)))
-  case class Prism[S, A](preview: S => Option[A], review: A => S):
-    def modify(f: A => A): S => S =
-      s => preview(s).map(a => review(f(a))).getOrElse(s)
-  case class PartialLens[S, A](preview: S => Option[A],
-                               modify: (A => A) => S => S)
-
-  def compose[S, M, A](p: Prism[S, M],
-                       l: Lens[M, A]): PartialLens[S, A] =
-    PartialLens(
-      preview = s => p.preview(s).map(l.view),
-      modify  = f => s => p.preview(s) match
-        case Some(m) => p.review(l.modify(f)(m))
-        case None    => s,
-    )
-
-  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
-    pl.modify(f)
-
   val varP: Prism[Expr, Var] =
     Prism[Expr, Var](
       { case EVar(v) => Some(v); case _ => None },
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
index aa11809..feccdac 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/Spec.scala
@@ -71,13 +71,4 @@ object Props extends Properties:
       refsUnchanged(f1, f2) && refsUnchanged(x1, x2)
     case (T.TLam(_, b1), T.TLam(_, b2)) => refsUnchanged(b1, b2)
     case _ => false
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
+@main def spec(): Unit = SpecRunner.run(Props.tests)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
index 74e470b..a0517d4 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.hs
@@ -2,46 +2,13 @@
 -- reach every element, match the succeeded branch, edit its value.
 module After where
 
-import Data.Maybe (listToMaybe)
+import Optics (Lens(..), Prism(..), PartialLens(..), composeO, each, over)
 
 data Ok     = Ok     { okValue :: Int }
   deriving (Eq, Show)
 data Result = Succeeded Ok | Failed String
   deriving (Eq, Show)
 
-data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
-
-modifyL :: Lens s a -> (a -> a) -> s -> s
-modifyL l f s = set l (s, f (view l s))
-
-data Prism s a = Prism
-  { preview :: s -> Maybe a
-  , review  :: a -> s
-  }
-
-data PartialLens s a = PartialLens
-  { plPreview :: s -> Maybe a
-  , plModify  :: (a -> a) -> s -> s
-  }
-
-composeO :: Prism s m -> Lens m a -> PartialLens s a
-composeO p l = PartialLens
-  { plPreview = \s -> view l <$> preview p s
-  , plModify  = \f s -> case preview p s of
-      Nothing -> s
-      Just m  -> review p (modifyL l f m)
-  }
-
--- Traversal: reach every element, and within it apply the
--- partial lens (hits edit, misses pass through).
-each :: PartialLens s a -> PartialLens [s] a
-each pl = PartialLens
-  (\xs -> listToMaybe xs >>= plPreview pl)
-  (\g xs -> map (plModify pl g) xs)
-
-over :: PartialLens s a -> (a -> a) -> s -> s
-over pl = plModify pl
-
 succeededP :: Prism Result Ok
 succeededP = Prism
   { preview = \r -> case r of Succeeded ok -> Just ok; _ -> Nothing
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
index 5f3281c..1159d9b 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/After.scala
@@ -1,6 +1,8 @@
 // Same, with a small traversal composed with a prism and a lens:
 // reach every element, match the succeeded branch, edit its value.
 object After:
+  import Optics.*
+
   case class Ok(value: Int)
   enum Result:
     case Succeeded(v: Ok)
@@ -8,33 +10,6 @@ object After:
 
   import Result.*
 
-  case class Lens[S, A](view: S => A, set: (S, A) => S):
-    def modify(f: A => A): S => S = s => set(s, f(view(s)))
-  case class Prism[S, A](preview: S => Option[A], review: A => S):
-    def modify(f: A => A): S => S =
-      s => preview(s).map(a => review(f(a))).getOrElse(s)
-  case class PartialLens[S, A](preview: S => Option[A],
-                               modify: (A => A) => S => S)
-
-  def compose[S, M, A](p: Prism[S, M],
-                       l: Lens[M, A]): PartialLens[S, A] =
-    PartialLens(
-      preview = s => p.preview(s).map(l.view),
-      modify  = f => s => p.preview(s) match
-        case Some(m) => p.review(l.modify(f)(m))
-        case None    => s,
-    )
-  // Traversal: reach every element, and within it apply the
-  // partial lens (hits edit, misses pass through).
-  def each[S, A](pl: PartialLens[S, A]): PartialLens[List[S], A] =
-    PartialLens(
-      preview = _.headOption.flatMap(pl.preview),
-      modify  = f => _.map(pl.modify(f)),
-    )
-
-  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
-    pl.modify(f)
-
   val succeededP: Prism[Result, Ok] =
     Prism[Result, Ok](
       { case Succeeded(v) => Some(v); case _ => None },
@@ -42,10 +17,9 @@ object After:
     )
   val valueL: Lens[Ok, Int] =
     Lens[Ok, Int](_.value, (ok, v) => ok.copy(value = v))
-  val okValue: PartialLens[Result, Int] = compose(succeededP, valueL)
+  val okVal: PartialLens[Result, Int] = compose(succeededP, valueL)
 
-  val eachSucceeded: PartialLens[List[Result], Int] =
-    each(okValue)
+  val eachSucceeded: PartialLens[List[Result], Int] = each(okVal)
 
   def bumpSucceeded(xs: List[Result]): List[Result] =
     over(eachSucceeded, _ + 1)(xs)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
index 6400727..7b6e323 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/03-bump-oks/Spec.scala
@@ -53,13 +53,4 @@ object Props extends Properties:
         case (R.Failed(m1), R.Failed(m0))       => m1 == m0
         case _                                  => false
       } ==== true
-
-@main def spec(): Unit =
-  val results = Props.tests.map { t =>
-    val r = Property.check(t.withConfig(PropertyConfig.default),
-      t.result, Seed.fromTime())
-    println(Test.renderReport(
-      "Props", t, r, ansiCodesSupported = false))
-    r.status
-  }
-  if !results.forall(_ == Status.ok) then sys.exit(1)
+@main def spec(): Unit = SpecRunner.run(Props.tests)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/run.sh b/pages/refactorings/replace-mutable-fields-with-lenses/run.sh
index 7b8cb88..39d133a 100755
--- a/pages/refactorings/replace-mutable-fields-with-lenses/run.sh
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/run.sh
@@ -2,23 +2,27 @@
 # Runs every hedgehog property for this refactoring, in both languages.
 # Each NN-*/ directory holds Before + After + Spec in Scala 3 and Haskell;
 # Spec generates inputs and asserts Before and After agree on all of them.
+# The shared/ directory (Scala object Optics, Haskell module Optics) holds
+# the optic building blocks; it is compiled in, never shown on the page.
 #
 # Needs: scala-cli (https://scala-cli.virtuslab.org) and either ghc with
 # hedgehog on the package path, or docker (the image is built on first use).
 set -eu
 cd "$(dirname "$0")"
+SHARED="$(pwd)/shared"
 
 if command -v ghc >/dev/null 2>&1 && ghc-pkg list hedgehog 2>/dev/null | grep -q hedgehog; then
-  hs() { runghc -i"$1" "$1/Spec.hs"; }
+  hs() { runghc -i"$1" -i"$SHARED" "$1/Spec.hs"; }
 else
   docker image inspect cp-hedgehog >/dev/null 2>&1 || \
     printf 'FROM haskell:9.8-slim\nRUN cabal update && cabal install --lib hedgehog\n' | docker build -t cp-hedgehog -
-  hs() { docker run --rm -v "$PWD:/w" -w /w cp-hedgehog runghc -i"$1" "$1/Spec.hs"; }
+  hs() { docker run --rm -v "$PWD:/w" -v "$SHARED:/shared" -w /w cp-hedgehog runghc -i"$1" -i/shared "$1/Spec.hs"; }
 fi
 
 for d in [0-9][0-9]-*/; do
   d=${d%/}
-  echo "== $d (scala)";   scala-cli run "$d" --main-class spec
+  echo "== $d (scala)"
+  scala-cli run "$d" --main-class spec "$SHARED"
   echo "== $d (haskell)"; hs "$d"
 done
 echo "all properties passed"
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
new file mode 100644
index 0000000..2c859ef
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
@@ -0,0 +1,39 @@
+-- Shared optic building blocks for the examples on this page: a Lens,
+-- a Prism, a composed PartialLens, and a traversal `each`. Compiled by
+-- run.sh but not shown on the page, so each example is the move itself.
+module Optics (Lens(..), Prism(..), PartialLens(..), composeO, each, over, modify) where
+
+import Data.Maybe (listToMaybe)
+
+data Lens s a = Lens { view :: s -> a, set :: (s, a) -> s }
+
+modify :: Lens s a -> (a -> a) -> s -> s
+modify l f s = set l (s, f (view l s))
+
+data Prism s a = Prism
+  { preview :: s -> Maybe a
+  , review  :: a -> s
+  }
+
+-- A prism followed by a lens: hit -> edit the field; miss -> pass through.
+data PartialLens s a = PartialLens
+  { plPreview :: s -> Maybe a
+  , plModify  :: (a -> a) -> s -> s
+  }
+
+composeO :: Prism s m -> Lens m a -> PartialLens s a
+composeO p l = PartialLens
+  ( \s -> view l <$> preview p s
+  ) ( \f s -> case preview p s of
+        Nothing -> s
+        Just m  -> review p (modify l f m)
+  )
+
+-- A traversal: reach every element, apply the partial lens to each.
+each :: PartialLens s a -> PartialLens [s] a
+each pl = PartialLens
+  (\xs -> listToMaybe xs >>= plPreview pl)
+  (\f xs -> map (plModify pl f) xs)
+
+over :: PartialLens s a -> (a -> a) -> s -> s
+over pl = plModify pl
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
new file mode 100644
index 0000000..3373fc6
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
@@ -0,0 +1,32 @@
+// Shared optic building blocks for the examples on this page: a Lens,
+// a Prism, a composed PartialLens, and a traversal `each`. Compiled by
+// run.sh but not shown on the page, so each example is the move itself.
+object Optics:
+  case class Lens[S, A](view: S => A, set: (S, A) => S):
+    def modify(f: A => A): S => S = s => set(s, f(view(s)))
+
+  case class Prism[S, A](preview: S => Option[A], review: A => S):
+    def modify(f: A => A): S => S =
+      s => preview(s).map(a => review(f(a))).getOrElse(s)
+
+  // A prism followed by a lens: hit -> edit the field; miss -> pass through.
+  case class PartialLens[S, A](preview: S => Option[A],
+                               modify: (A => A) => S => S)
+
+  def compose[S, M, A](p: Prism[S, M], l: Lens[M, A]): PartialLens[S, A] =
+    PartialLens(
+      preview = s => p.preview(s).map(l.view),
+      modify  = f => s => p.preview(s) match
+        case Some(m) => p.review(l.modify(f)(m))
+        case None    => s,
+    )
+
+  // A traversal: reach every element, apply the partial lens to each.
+  def each[S, A](pl: PartialLens[S, A]): PartialLens[List[S], A] =
+    PartialLens(
+      preview = _.headOption.flatMap(pl.preview),
+      modify  = f => _.map(pl.modify(f)),
+    )
+
+  def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
+    pl.modify(f)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/shared/SpecRunner.scala b/pages/refactorings/replace-mutable-fields-with-lenses/shared/SpecRunner.scala
new file mode 100644
index 0000000..8aeb4f8
--- /dev/null
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/shared/SpecRunner.scala
@@ -0,0 +1,15 @@
+// Shared runner body for every example's hedgehog suite. Each example
+// ends with `@main def spec(): Unit = SpecRunner.run(Props.tests)`;
+// this file holds the boilerplate so the page does not show it.
+import hedgehog.*, hedgehog.core.*, hedgehog.runner.*
+
+object SpecRunner:
+  def run(tests: List[Test]): Unit =
+    val results = tests.map { t =>
+      val r = Property.check(t.withConfig(PropertyConfig.default),
+        t.result, Seed.fromTime())
+      println(Test.renderReport(
+        "Props", t, r, ansiCodesSupported = false))
+      r.status
+    }
+    if !results.forall(_ == Status.ok) then sys.exit(1)

From 9251bf172292a8f975046cdf974e57a51ff6d90e Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 22:54:57 +0200
Subject: [PATCH 5/6] Use Plated for the whole-tree walk; rework Motivation
 smell

- shared/Optics (Scala + Haskell) gains a Plated class/instance with
  descend + everywhere; example 2 declares its Plated[Expr] instance
  and lets everywhere do the walk instead of a hand-written recursion.
- Motivation: the smell is multiple long methods doing too much, with
  reach-the-value complexity mixed into the change code.
- Page example-2 prose updated to say the walk comes from Plated (eo's
  visit-across-whole-trees recipe).
---
 .claude/skills/refactoring-entry/LESSONS.md   |  6 +++++
 .../replace-mutable-fields-with-lenses.md     | 26 +++++++++++--------
 .../02-rename-tree/After.hs                   | 21 ++++++++-------
 .../02-rename-tree/After.scala                | 19 +++++++-------
 .../shared/Optics.hs                          | 12 ++++++++-
 .../shared/Optics.scala                       | 10 +++++++
 6 files changed, 62 insertions(+), 32 deletions(-)

diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
index 0951032..0190371 100644
--- a/.claude/skills/refactoring-entry/LESSONS.md
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -139,3 +139,9 @@ brief.md or workflow.js and deleted here. Keep the calibration table current.
   examples · review · diagrams — with the Claude `workflow.js`/`journal.jsonl` as one optional
   orchestrator, and generalized the `gh`/ship steps. The `Workflow` script stays but nothing else
   assumes Claude.
+- **Rule (blocking).** Do not hand-write the recursion in an "across a whole tree" example. A
+  hand-defined `everywhere` in the example's After buries the point (the optic is reused, not the
+  walk). Add `Plated`/`everywhere` to `shared/` (a `trait`/`class` with a `descend` instance per
+  type; `everywhere f s = descend (everywhere f) (f s)`) and declare the type's `Plated` instance
+  in the example — the walk comes from the library, the example only says which fields recurse.
+  Mention eo's "visit across whole trees" recipe. → folded into brief.md's lens-example guidance.
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses.md b/pages/refactorings/replace-mutable-fields-with-lenses.md
index b4246cc..e10025d 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses.md
+++ b/pages/refactorings/replace-mutable-fields-with-lenses.md
@@ -58,14 +58,15 @@ effects — each recipe runnable against the library.
 ## Motivation
 
 Reach for the lens when access to a field needs to be *decoupled from
-its manipulation*. The smell is repetition of field handling: an
-object-with-accessors whose setters are one-liners nothing intercepts,
-a copy-update chain that grows a level for every record you descend,
-or an update that must be re-derived by hand each time a field moves.
-The optics version of the corridor is a *value*, so it can be passed
+its manipulation*. The smell is multiple long methods that do too
+much — the complexity of reaching the values is mixed up with the
+code for the changes you want to make, and each operation re-derives
+its own path. A lens separates the two: how you get to a value and
+what you do once you have it stop being one entangled method. The
+optics version of the corridor is a *value*, so it can be passed
 around, stored, and composed into paths that reach several levels
 down without ever repeating the intermediate records; and a function
-that needs "every `Instant` in whatever you hand me" can ask for the
+that needs "every `Instant` in whatever you hand me" can call the
 optic instead of the type. When the invariant itself matters — a
 balance that must never go negative, a size that must bracket its
 children — the pure writer makes the transition a value the type
@@ -235,11 +236,14 @@ Now the same edit is applied at *every* node of the tree — the nesting
 is what makes the hand-written version hurt. The Before version is a
 recursive walk that rebuilds a hit by hand at each level of the
 recursion; add a level to the tree and the rebuild appears again. The
-After version reuses the *same* `varName` optic from example 1 inside
-a bottom-up `everywhere` walk: "how to reach a variable name" is
-written once, and the walk only decides *where* it applies. This is
-eo's "visit across whole trees" recipe — one derivation and one
-`.andThen`, rather than a rewrite.
+The After version reuses the *same* `varName` optic from example 1,
+and the walk comes from `Plated` — the recursion of the type as a
+value, declared once (which fields are the sub-terms) and reused
+`everywhere`. The lens says "how to reach a variable name"; the
+`Plated` instance says "where the tree recurses"; and the walk applies
+the optic at every node. This is eo's "visit across whole trees"
+recipe — one `Plated` instance and one `everywhere`, rather than a
+hand-written recursive rebuild.
 
 <figure class="rf-figure">
 {% include_relative replace-mutable-fields-with-lenses/02-rename-tree/diagram.svg %}
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
index be151a2..eda071a 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.hs
@@ -1,16 +1,23 @@
--- Same, with the same varName optic applied at every node of the
--- tree: how to reach the name is defined once, and the walk only
--- decides where it applies.
+-- Same, with the same varName optic applied at every node: the walk
+-- comes from Plated (which fields recurse), not from the example.
 module After where
 
 import Data.Char (toUpper)
-import Optics (Lens(..), Prism(..), PartialLens(..), composeO, over)
+import Optics
+  ( Lens(..), Prism(..), PartialLens(..), Plated(..)
+  , composeO, over, everywhere
+  )
 
 data Var = Var { vName :: String, vRef :: Int }
   deriving (Eq, Show)
 data Expr = EVar Var | EApp Expr Expr | ELam String Expr
   deriving (Eq, Show)
 
+instance Plated Expr where
+  descend f (EApp a b)   = EApp (f a) (f b)
+  descend f (ELam b bd)  = ELam b (f bd)
+  descend _ e            = e
+
 varP :: Prism Expr Var
 varP = Prism
   { preview = \e -> case e of EVar v -> Just v; _ -> Nothing
@@ -23,11 +30,5 @@ nameL = Lens { view = vName, set = \(v, n) -> v { vName = n } }
 varName :: PartialLens Expr String
 varName = composeO varP nameL
 
--- Bottom-up: apply the rewrite at every node, descending first.
-everywhere :: (Expr -> Expr) -> Expr -> Expr
-everywhere f e@(EVar _)    = f e
-everywhere f (EApp a b)    = f (EApp (everywhere f a) (everywhere f b))
-everywhere f (ELam b bd)   = f (ELam b (everywhere f bd))
-
 renameAll :: Expr -> Expr
 renameAll = everywhere (over varName (map toUpper))
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
index 1938ca0..89ac098 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/02-rename-tree/After.scala
@@ -1,6 +1,5 @@
-// Same, with the single varName optic applied at every node of the
-// tree: how to reach the name is defined once, and the walk only
-// decides where it applies.
+// Same, with the single varName optic applied at every node: the walk
+// comes from Plated (which fields recurse), not from the example.
 object After:
   import Optics.*
 
@@ -12,6 +11,12 @@ object After:
 
   import Expr.*
 
+  given Plated[Expr] with
+    def descend(f: Expr => Expr)(e: Expr): Expr = e match
+      case EApp(a, b)  => EApp(f(a), f(b))
+      case ELam(b, bd) => ELam(b, f(bd))
+      case e           => e
+
   val varP: Prism[Expr, Var] =
     Prism[Expr, Var](
       { case EVar(v) => Some(v); case _ => None },
@@ -21,11 +26,5 @@ object After:
     Lens[Var, String](_.name, (v, n) => v.copy(name = n))
   val varName: PartialLens[Expr, String] = compose(varP, nameL)
 
-  // Bottom-up: apply the rewrite at every node, descending first.
-  def everywhere(f: Expr => Expr)(e: Expr): Expr = e match
-    case EVar(_)     => f(e)
-    case EApp(a, b)  => f(EApp(everywhere(f)(a), everywhere(f)(b)))
-    case ELam(b, bd) => f(ELam(b, everywhere(f)(bd)))
-
   def renameAll(e: Expr): Expr =
-    everywhere(over(varName, _.toUpperCase))(e)
+    summon[Plated[Expr]].everywhere(over(varName, _.toUpperCase))(e)
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
index 2c859ef..809409f 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.hs
@@ -1,7 +1,7 @@
 -- Shared optic building blocks for the examples on this page: a Lens,
 -- a Prism, a composed PartialLens, and a traversal `each`. Compiled by
 -- run.sh but not shown on the page, so each example is the move itself.
-module Optics (Lens(..), Prism(..), PartialLens(..), composeO, each, over, modify) where
+module Optics (Lens(..), Prism(..), PartialLens(..), Plated(..), everywhere, composeO, each, over, modify) where
 
 import Data.Maybe (listToMaybe)
 
@@ -37,3 +37,13 @@ each pl = PartialLens
 
 over :: PartialLens s a -> (a -> a) -> s -> s
 over pl = plModify pl
+
+-- Plated: the recursion of a recursive type, as a value. An instance
+-- says which fields are the sub-terms (the "plate"); `everywhere`
+-- then applies a rewrite at every node, bottom-up.
+class Plated s where
+  descend :: (s -> s) -> s -> s
+
+everywhere :: Plated s => (s -> s) -> s -> s
+everywhere f s = descend (everywhere f) (f s)
+
diff --git a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
index 3373fc6..14084d9 100644
--- a/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
+++ b/pages/refactorings/replace-mutable-fields-with-lenses/shared/Optics.scala
@@ -30,3 +30,13 @@ object Optics:
 
   def over[S, A](pl: PartialLens[S, A], f: A => A): S => S =
     pl.modify(f)
+
+  // Plated: the recursion of a recursive type, as a value. An instance
+  // says which fields are the sub-terms (the "plate"); `everywhere`
+  // then applies a rewrite at every node, bottom-up, without the type
+  // knowing how to walk itself.
+  trait Plated[S]:
+    def descend(f: S => S)(s: S): S
+    def everywhere(f: S => S): S => S =
+      s => descend(everywhere(f))(f(s))
+

From eef854f80499f0cc6f646522acb1c1ff29346a21 Mon Sep 17 00:00:00 2001
From: Rodolfo Hansen <rhansen@kitsd.com>
Date: Thu, 3 Sep 2026 23:26:31 +0200
Subject: [PATCH 6/6] Refactoring skill: rule is 'never hand-write intermediate
 helpers'
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Generalize the Plated lesson from 'don't hand-write the recursion' to
'never hand-write intermediate helper methods in an example' (like the
hand-defined everywhere). Folded into SKILL.md §3 and brief.md — the
helper belongs in shared/ or a library; the example declares only the
instance (which fields recurse).
---
 .claude/skills/refactoring-entry/LESSONS.md | 15 +++++++++------
 .claude/skills/refactoring-entry/SKILL.md   |  8 ++++++++
 .claude/skills/refactoring-entry/brief.md   |  7 ++++++-
 3 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/.claude/skills/refactoring-entry/LESSONS.md b/.claude/skills/refactoring-entry/LESSONS.md
index 0190371..68c4200 100644
--- a/.claude/skills/refactoring-entry/LESSONS.md
+++ b/.claude/skills/refactoring-entry/LESSONS.md
@@ -139,9 +139,12 @@ brief.md or workflow.js and deleted here. Keep the calibration table current.
   examples · review · diagrams — with the Claude `workflow.js`/`journal.jsonl` as one optional
   orchestrator, and generalized the `gh`/ship steps. The `Workflow` script stays but nothing else
   assumes Claude.
-- **Rule (blocking).** Do not hand-write the recursion in an "across a whole tree" example. A
-  hand-defined `everywhere` in the example's After buries the point (the optic is reused, not the
-  walk). Add `Plated`/`everywhere` to `shared/` (a `trait`/`class` with a `descend` instance per
-  type; `everywhere f s = descend (everywhere f) (f s)`) and declare the type's `Plated` instance
-  in the example — the walk comes from the library, the example only says which fields recurse.
-  Mention eo's "visit across whole trees" recipe. → folded into brief.md's lens-example guidance.
+- **Rule (blocking).** Do not hand-write intermediate helper methods in an example — like the
+  hand-defined `everywhere` that used to sit in an "across a whole tree" example's After and
+  buries the point (the optic is the reusable bit, not the walk). If the example needs shared
+  walk machinery, add `Plated`/`everywhere` to `shared/` (a `trait`/`class` with a `descend`
+  instance per type; `everywhere f s = descend (everywhere f) (f s)`) and declare the type's
+  `Plated` instance in the example — the walk comes from the library, the example only says
+  which fields recurse. Same for any helper (a fold over the tree, a traversal builder): it
+  belongs in `shared/` or a library, not re-derived in the example.
+  → folded into SKILL.md §3 and brief.md ("Never hand-write helpers").
diff --git a/.claude/skills/refactoring-entry/SKILL.md b/.claude/skills/refactoring-entry/SKILL.md
index 450fbf4..f325fe5 100644
--- a/.claude/skills/refactoring-entry/SKILL.md
+++ b/.claude/skills/refactoring-entry/SKILL.md
@@ -89,6 +89,14 @@ Rules that came from review, keep them:
   `Before/After/Spec` on the page is then the *move itself*, with a one-line note in the page that
   the shared setup is hidden. The reviewer considers inline setup (e.g. redefining a Lens type in
   every After) accidental complexity that buries the motivation.
+- **Never hand-write intermediate helpers in an example.** If the example needs a walk over a
+  recursive type, a fold, or a traversal builder, do not define it in the example's `After` —
+  add it to `shared/` (e.g. a `Plated` class with `descend`/`everywhere`, as in eo's "visit
+  across whole trees" recipe) or use a library, and have the example declare only the instance
+  (`which fields recurse`). A hand-rolled `everywhere` in an example buries the motivation: the
+  optic is the reusable thing, not the helper. This is the same rule as the `shared/` bullet
+  above — shared machinery stays off the page — extended to any intermediate helper the
+  example needs.
 - Do not claim totality or purity the code does not have (e.g. `Int` `div` overflow).
 
 ## 4. Verify before the PR
diff --git a/.claude/skills/refactoring-entry/brief.md b/.claude/skills/refactoring-entry/brief.md
index 3440ea0..61c8a9b 100644
--- a/.claude/skills/refactoring-entry/brief.md
+++ b/.claude/skills/refactoring-entry/brief.md
@@ -51,7 +51,12 @@ pages/refactorings/<slug>/
   * every file self-contained, readable, SHORT (Before/After 8–25 lines each); lines ≤ 72 characters;
   * NO `{{`, `}}`, `{%`, `%}` sequences anywhere (Liquid would eat them);
   * one-line comment at the top of Before/After saying what the program does; no essay comments;
-  * the Scala and Haskell Befores must be parallel (same shape: if Scala has an inline lambda, so does Haskell).
+  * the Scala and Haskell Befores must be parallel (same shape: if Scala has an inline lambda, so does Haskell);
+  * **never hand-write intermediate helpers in an example** — if the example needs a walk over a
+    recursive type, a fold, or a traversal builder, put it in `shared/` (e.g. a `Plated`
+    class with `descend`/`everywhere`, as in eo's "visit across whole trees" recipe) or use a
+    library, and declare only the type's instance in the example (`which fields recurse`). A
+    hand-rolled helper in an example buries the move under the tool.
 - Scala: Scala 3.3.x, directives at the top of Spec.scala only:
     //> using scala 3.3.4
     //> using dep qa.hedgehog::hedgehog-core:0.14.0