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

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?

Transcript

1. DRTTOHC T h e D e r i v a t i v e o f a R e g u l a r T y p e i s i t s T y p e o f O n e - H o l e C o n t e x t s - C o n o r M c B r i d e
2. Who Am I? • Resident Haskellion-chained- to-the-rocks-of-Javascript on the New York Times interactive news desk • Not the guy that makes the cool maps • PourOver, Fashion Fingerprint, World Cup, MOD • Failed analytic philosopher (the space of reasons was too crowded and too empty)
3. 5 2 5 , 6 0 0 s i g m a s Reasons of Love - The “algebra” behind “algebraic data types” - The types-as-values epiphany - Unlocking the metaprogrammatic promise of dependent types (or at least a sufficiently robust type system) - Bernstein’s “CS connections” criterium
4. A g o n y = > E c s t a s y How I Read It - Does he really mean that kinda derivative? - McBride learned to diff erentiate as a child? - How does associativity work in this symbolism? - What’s a fixed point again?
5. A g o n y = > E c s t a s y How I Read It - Side-eff ects of readership - Algebraic data types - Fixed points - Zippers - Remembering all the calculus I never learned, frittering my days away in a humanities major
6. Types and Fixed Points
7. Y o u d o w n w i t h g a d t s ? Types & Algebra - Taxonomy of algebraic types: - Empty (0): _|_, Unit(1): Lf - Basic type: Int - Product (Int,String): Int × String - Sum (A or B): Nothing + Just Int - Definitions/parametric types … - Recursive types …
8. P a r a m e t r i c p l a y g r o u n d Definitions in types - F|x = S - Define the type variable x in F to be S - List x = [] + (x × List x) - List x | x=Int - List Int = [] + (Int × List Int)
9. What does this mean? µx.F
10. The Fixed Point • The fixed point of a function f(x) is the x such that f(x) = x. • f (fix f) = fix f • Type constructors are just functions • Imagine a type constructor with a variable in it: • Z + S x • How do we make that the Nat type (Z | S Nat) • By substituting the whole constructor for x • Nat = Z + S Nat fixed point of Z + Sx
11. Mr. Fix-It • µx.F can be read as “the fixed point of F over x” • Nat -> µx.1 + x • F x = 1 + x • Nat = Fix F • Fix F = F (Fix F) • Fix F = 1 + Fix F • Nat = 1 + Nat No let/name binding needed
12. W h o ’ s g o t t i m e f o r t h a t ? Or … • µx.F can be read as “the recursive type F, in which we substitute F for x recursively” • Probably easier to think of it this way • Nat -> µy . 1 + y • IntList -> µy . 1 + (Int × y) • IntBtree -> µy . 1 + (Int × y × y)
13. Zippers and Holes
14. “ L i k e V e l c r o f o r t r e e s ” Why Zippers - If our trees are immutable, how can we get fast access to children and parents. - Just turn it “inside-out like a returned glove”! - Filesystems, mazes, Xmonad!
16. 1 2 3 4 5 B 1 (B 2 (B 4 Lf Lf, B 5 Lf Lf),(B 3 Lf Lf)) BT = Lf + B Int (BT, BT)
17. 1 3 2 4 5 , ( ) Split at focus?
18. 1 3 Happy path! Ctx (B 4 Lf Lf) (B 5 Lf Lf) [(Left, 1, B 3 Lf Lf)] 4 5 , , ( ) Ctx LeftChild RightChild [PathSteps]
19. Zip it up Ctx (B 4 Lf Lf) (B 5 Lf Lf) [(Left, 1, B 3 Lf Lf)] (2) Ctx (B 2 (B 4 Lf Lf, B 5 Lf Lf)) (B 3 Lf Lf) [] (1)
20. Zip it down Ctx (B 4 Lf Lf) (B 5 Lf Lf) [(Left, 1, B 3 Lf Lf)] (2) Ctx Lf Lf [(Left, 1, B 3 Lf Lf),(Right, 2, B 4 Lf Lf)] (5)
21. [ 2 B 4 Lf Lf 5 Ctx (Left, 1, B 3 Lf Lf)] B ( Lf Lf) ( ) ( ) [ 2 In motion! B 4 Lf Lf 5 Ctx (Left, 1, B 3 Lf Lf)] B ( Lf Lf) ( ) (Right, , )] ( )
22. Wherefore Holes? • Given some type T that contains x’s of type X, we are looking for the type that describes a T with a specific x removed • One-hole contexts are always contexts with respect to some interior type • A zipper is the one-hole context of a binary tree of x’s (a binary tree with a hole at a specific x) AND the value that was removed
23. Time to Derive
24. A l i t t l e b i t o f c o n t e x t Leibnizian Childhood Pair Triple (1,2) (1,2,3) Int × Int Int × Int × Int Int2 Int3 (L|R,Int) (L|M|R,Int,Int) 2 × Int 3 × Int2 Context: (L,2) Context: (M,1,3)
25. Wait … Pair Type: Int2 Context: 2 × Int Triple Type: Int3 Context: 3 × Int2 That looks like the power rule to me!
26. BIG IDEA: To find the type of a context of type T with a hole in place of some x, take the partial derivative of T with respect to x CTXx (T) = ∂x T
27. OTHER IDEA: Think of finding partial derivatives (wrt x) as answering the question “How can we find x’s in T’s”
28. Simple Derivatives - (Empty) ∂x 0 = 0 - An empty instance is its own (empty) context - ∂x x = 1 - A single value has a singleton context - Int -> Unit - ∂x y = 0 - We find no x’s in a y - ∂x (S + T) = ∂x S + ∂x T - The context of a sum is the sum of contexts - Lef t Int + Right Int -> 1 + 1
29. Products Rule! - ∂x (S × T) = (∂x S × T) + (S × ∂x T) - The derivative of a product type follows the product rule. - Intuitive explanation: either 1) we find the container for x in S and record T or 2) we find the container for x in T and record S - Consider we are looking for an Int context of the type Int × String (Int, String). - ∂Int Int = 1, ∂Int String = 0 - Applying the product rule: 1 × String + Int × 0 - Otherwise known as String - The context of an Int in (Int,String) is simply the string. The hole has to be the only Int.
30. T h e C h a i n ( r u l e ) G a n g Harder Derivatives - Definitions (F | y=S) are a problem because a context for x could be hiding in S. You can’t just take the par tial derivative of F. - So just apply the multivariable chain rule !! … Wait, what? - ∂x (F|y=S) = (∂x F|y=S) + (∂y F|y=S)×∂x S - Let’s all agree no one want s to see the derivation of this ^
31. T h e C h a i n ( r u l e ) G a n g Harder Derivatives - ∂x (F|y=S) = (∂x F|y=S) + (∂y F|y=S)×∂x S - Intuitively: If you’re looking for x’s in a F where y=S, either 1) your x is at the top level of F and you don’t care what’s inside y=S or 2) your x is inside a y, so you have to record which y and then find the context inside of that - Foo y -> (String, y) | y=Int - Find an Int context - (∂Int (String×y)|y=S) + (∂y (String×y)|y=Int)×∂Int Int - 0 + ( String ) × 1 - The context is String just as expected
32. BREATHER
33. Recursive Derivs • ∂x (µx.F) = ∂x (F|x=µx.F) • Expand the derivative of a recursive type into the derivative of a definition • ∂x F|x=µx.F + ∂y F|x=µx.F × ∂x (µx.F) • Either your x is at the top level or you have to go a level deeper and find it there • Isomorphic to [∂y F|x=µx.F] × ∂x F|x=µx.F • A list of steps until you get to your hole’s level and then its context at that level But this is what we needed in the first place!
34. Recursive Derivs • ∂x (µx.F) = ∂x (F|x=µx.F) • Expand the derivative of a recursive type into the derivative of a definition • ∂x F|x=µx.F + ∂y F|x=µx.F × ∂x (µx.F) • Either your x is at the top level or you have to go a level deeper and find it there • Isomorphic to [∂y F|x=µx.F] × ∂x F|x=µx.F • A list of steps until you get to your hole’s level and then its context at that level Encode sum with list (f actor by ∂x F)?
35. Recursive Derivs • [∂y F|x=µx.F] × ∂x F|x=µx.F • A list of steps until you get to your hole’s level and then it s context at that level • Wait, where have we seen that before … (zip)
36. Let’s Test • What’s the one-hole context of a list? List x = 1 + (x × List) List x = µy. 1 + (x × y) ∂y (µy. 1 + (x × y)) = ∂y (1 + (x × y) | y = List x) = [∂y (1 + x × y)] × ∂x (1 + x × y) = [x] × (y | y = List x) = (List x) × (List x) ! • The context of a List is t wo list s? • Yup. Prefix and suffix • [1,(2),3,4] -> ([1],[3,4])
37. List Context [1,2,3,4,5] ! [1,2,3,(),5] ! ([1,2,3],[5])
38. Let’s Test • What’s the one-hole context of a binary tree Btree x = Leaf + (x, Btree x, Btree x) Btree x = µy. 1 + (x × y2) ∂y (µy. 1 + (x × y2)) = ∂y (1 + (x × y2) | y = Btree x) = [∂y (1 + (x × y2))] × ∂x (1 + (x × y2)) = [2xy | y = Btree x] × (y2 | y = Btree x) = [2x ×(Btree x)] × (Btree x)2 = [(2,x,Btree x)],(Btree x),(Btree x) ! • The context of a binary tree is list of steps, a lef t child, and a right child
39. Does the BIG IDEA make sense? • In Calculus, a derivative describes a relationship between instantaneous rates of change • dx/dt is a context/ is contextual • Leibnizian omniscience (Actual Newton-Leibniz f anart) http://ejweir.deviantart.com/
40. Why Should You Care? • You probably won’t be asked to implement a zipper structure at work on Monday … or ever. • DRTTOHC demonstrates the value/ promise of transformations between kinds of types • Metaprogramming! Write functions on containers, get functions on contexts for free. (If you can write the type signature, the function should be trivial … right? RIGHT?)
41. But How!? • A language in which types are *just* values that you can operate on normally • You write a `context` function that transforms types into the one-hole context type. • If you can write type-generic functions you can automatically transform functions on a type T to function on that T’s context • Idris example
42. “…one only has to open one’s old school textbooks almost at random and ask ‘what does this mean for datatypes?’”