Zipper

see functional programming

resource The Zipper (Gérard Huet, 1997) --- ../references/The_Zipper.pdf --- https://www.researchgate.net/publication/220676535_The_Zipper

resource The Derivative of a Regular Type is its Type of One-Hole Contexts (Conor McBride, 2001) --- ../references/diff.pdf --- http://strictlypositive.org/diff.pdf. ($3.2 'Examples of Derivatives' has a typo in the reduction of \(\partial_x\ \mathbf{list}\ x\): on the third line the weakening shouldn't extend under \(\times z\). $3.5 'Subterms and Derivatives' has a typo in Theorem (subtree): there should be a \(t\) on the right-hand side of \(u \leq_{\mu x{.}F}\))

definition the derivative of a type is its type of one-hole contexts: the derivative \(\partial_xT\) of \(T\) with respect to \(x\) is the type of terms that look like terms of \(T\) but have one hole somewhere an \(x\) would normally go

and in particular we can always write a function \(\partial_xT \times x \to T\) that plugs \(\partial_xT\)'s hole using an \(x\). the construction is in Figure 5.

examples

• \(\partial_x(x + x) = \mathbf 2\)---whether the hole is in \(\mathrm{inl}\) or \(\mathrm{inr}\)
• \(\partial_x(x \times x) = \mathbf 2 \times x\)---whether the hole is in \(\mathrm{fst}\) or \(\mathrm{snd}\) along with the other component
• \(\partial_x(\mu y.\ \mathbf 1 + x \times y) = \partial_x\ \mathbf{list}\ x = \mathbf{list}\ x \times \mathbf{list}\ x\)---the prefix and suffix
• \(\partial_x(\mu y.\ x + y \times y) = \partial_x\ \mathbf{tree}\ x = \mathbf{list}\ (\mathbf 2 \times \mathbf{tree}\ x)\)---the path from the root equipped with the subtrees we pass by

definition the zipper for a recursive type is the derivative of the free ‹monad over its base ‹functor at zero, what's the problem?

proof (refer to the differentiation rules in Figure 4)

the derivative of Free f a with respect to a is:

\[ \begin{align} &\partial_a(\mathbf{free}_x\ F\ a) \qquad \text{\(x\) is free in \(F\)} \\ =\ &\partial_a(\mu x.\ a + \underline F_a) \\ =\ &\mu z.\ \underline{\partial_a(a + \underline F_a)|x{=}(\mathbf{free}_x\ F\ a)}_z + \underline{\partial_x(a + \underline F_a)|x{=}(\mathbf{free}_x\ F\ a)}_z \times z \\ =\ &\mu z.\ \underline{(\mathbf 1 + \mathbf 0)|x{=}(\mathbf{free}_x\ F\ a)}_z + \underline{(\mathbf 0 + \partial_x \underline F_a)|x{=}(\mathbf{free}_x\ F\ a)}_z \times z \\ =\ &\mu z.\ \mathbf 1 + \underline{\partial_x \underline F_a|x{=}(\mathbf{free}_x\ F\ a)}_z \times z \\ =\ &\mathbf{list}\ \partial_x \underline F_a|x{=}(\mathbf{free}_x\ F\ a) \\ \end{align} \]

taking the derivative at a ~ Void:

\[ \begin{align} &\partial_a(\mathbf{free}_x\ F\ a)|a{=}\mathbf 0 \\ =\ &\big(\mathbf{list}\ \partial_x \underline F_a|x{=}(\mathbf{free}_x\ F\ a)\big)|a{=}\mathbf 0 \\ =\ &\mathbf{list}\ \partial_x F|x{=}(\mu x.\ \mathbf 0 + F) \\ =\ &\mathbf{list}\ \partial_x F|x{=}\mu x{.}F \\ =\ &\mathbf{sub}\ \mu x{.}F \qquad \text{the zipper for \(\mu x{.}F\)} \\ \end{align} \]

so the zipper for Fix f is the derivative of Free f a with respect to a at a ~ Void. this makes sense: the free ‹monad over f is a Fix f but with holes a, so differentiating with respect to a distinguishes one of the holes, and setting a ~ Void plugs all other holes. the result is a Fix f but with a single hole of type Fix f---that's a zipper.

and in particular we can always write a function \(\mathbf{sub}\ \mu x{.}F \times \mu x{.}F \to \mu x{.}F\) that plugs \(\mathbf{sub}\ \mu x{.}F\)'s hole using a \(\mu x{.}F\). the construction is in $3.4 'Subtrees in Recursive Regular Types'.

---

--- ../references/Semantic Domain_ Five (and a Half) Derivatives in Language Theory.pdf --- https://semantic-domain.blogspot.com/2021/02/five-and-half-derivatives-in-language.html