The Derivative of a Regular Type is its Type of One-Hole Contexts
📜 Abstract
Polymorphic regular types are tree-like datatypes generated by polynomial type expressions over a set of free variables and closed under least fixed point. The ‘equality types’ of Core ML can be expressed in this form. Given such a type expression T with x free, this paper shows a way to represent the one-hole contexts for elements of x within elements of T, together with an operation which will plug an element of x into the hole of such a context. One-hole contexts are given as inhabitants of a regular type ∂xT, computed generically from the syntactic structure of T by a mechanism better known as partial differentiation. The relevant notion of containment is shown to be appropriately characterized in terms of derivatives and plugging in. The technology is then exploited to give the one-hole contexts for sub-elements of recursive types in a manner similar to Huet’s ‘zippers’[Hue97].
✨ Summary
Summary
McBride formalizes the observation that differentiating a regular algebraic datatype with respect to a type variable computes the datatype of its one-hole contexts. For sums and products, the derivative follows the usual rules of elementary calculus; for recursive types, the construction yields finite paths of context frames leading from the root to a selected subterm. The paper also defines a generic plugging operation and proves that derivatives characterize containment, while iterated context construction characterizes subtrees of recursive datatypes. This gives a principled, type-directed account of Huet-style zippers.
The paper’s primary research influence is documented in subsequent work on containers. Derivatives of Containers gives a categorical account of the construction, characterizes differentiation through a universal property, and verifies calculus laws—including the chain rule and rules for initial algebras—within the container framework. (people.cs.nott.ac.uk) The later paper ∂ for Data: Differentiating Data Structures explicitly identifies McBride’s 2001 observation as its starting point and generalizes the analysis using containers, linear maps, and laws for initial algebras and terminal coalgebras. (journals.sagepub.com) Subsequent work on polynomial functors and higher-order structure continues to cite the paper as an early source for the connection between datatype derivatives and one-hole contexts. (drops.dagstuhl.de) The sources located show clear influence on research in functional programming, type theory, containers, and generic traversal; they do not provide evidence of a specific industrial deployment or product adoption.