Erik Hinton on The Derivative of a Regular Type is its Type of One-Hole Contexts

Erik Hinton explains Conor McBride's paper on taking the derivative of algebraic data types to yield one-hole contexts, or zippers.

Meetup: meetup.com/papers-we-love/events/182798272/ Papers are generally loved for one of two reasons. Either the paper is foundational, siring a lineage of important research, or the paper is useful, guiding readers toward clever optimizations, fault-tolerant solutions, and non-intuitive hacks. "The Derivative of a Regular Type is its Type of One-Hole Contexts" is neither. Only a few papers build on McBride's work and the conclusions of the paper, though promising, haven't yet found any real employ. This paper is lovable, fun, and important because it is a radical thought experiment in the limits of abstraction. The paper poses the question: we call data types "algebraic", so can we "do calculus" on them? Surely, the nomenclature is just coincidental? What would it even mean to take the derivative of a data type? The paper stretches algebraic data types to what should be their breaking point and then demonstrates that it's not a breaking point ay all. By considering the paper's set-up and implications, we gain a deeper understanding of types and what they abstract. As it will turn out, you can take the derivative of data type and the result is meaningful. The derivative of an algebraic type is another data type, namely the type that can represent any specific context in the original type, any position in the original structure. This relationship is eerily similar to the relationship of functions to their derivatives (roughly, the contextual rate of change) that we all learned in high school. • No previous knowledge of calculus, algebraic data types, zippers, contexts or anything else is required. This talk will cover: - What is an algebraic data type? - What is a zipper and its sister structure, the one-hole context? - How can we derive a one-hole context from any given type? (How can we represent a specific location in an arbitrarily complex tree, type, etc) - What are the one-hole contexts of common types: the list, the binary tree, the ternary tree, and the rose tree? - Why would anyone care?