Here is what I think is most interesting about zippers:

  1. take any algebraic data type and convert it to an algebraic equation
  2. take the (partial) derivative of that equation over any (type) variables
  3. convert that result back to a data type

You now have the zipper (without the focus) for the original data type

11:52

for example d/da. List a produces (List a)^2 i.e. a pair of lists -- put the focus in and now you have the list zipper:data ListZipper a = ListZipper [a] a [a]

--

Note: This article assumes some introductory Haskell knowledge.

Introduction

Just as algebra is fundamental to the whole of mathematics, algebraic data types (ADTs) are fundamental to many common functional programming languages. They’re the primitives upon which all of our richer data structures are built, including everything from sets, maps, and queues, to bloom filters and neural networks.

Algebraic data types and mathematical algebra have some similar looking operations. In fact, it’s common in type theory to use the algebraic notation to define algebraic data types, rather than the Haskell-style data type declarations:

Untitled

In this essay, we’ll explore this coincidence and what that means for us as programmers. We’ll follow the path all the way to calculus.

Counting inhabitants

As a first foray into the equivalence of algebraic data types and the algebra most of us are more familiar with, we’ll start with simple arithmetic. Specifically, we’ll start by counting the number of inhabitants (values) of a given type. Looking back at the examples:

Untitled

Algebraic manipulations