Elliott Replaces Neural Net Backpropagation Tapes With Category Theory
Microsoft Research
Automatic differentiation requires no computational graphs, execution tapes, or mutable state because derivatives are linear transformations that compilers can synthesize directly from functional code.
Conal Elliott formulates automatic differentiation (AD) using category theory, defining derivatives uniformly as linear transformations rather than fragmented scalars, vectors, covectors, or Jacobian matrices. (3:20)
Reverse-mode AD is derived purely as the general AD category instantiated with continuation-passing style (CPS) or transposed linear maps, eliminating the need for tapes, computational graphs, partial derivatives, or mutable state. (75:13)
Using Joachim Lambek's 1980 equivalence between typed lambda calculus and Cartesian closed categories, standard functional code compiles directly via a GHC plugin into categorical AD representations without modifying source programs. (29:57)
The dichotomy between symbolic and automatic differentiation is rejected as artificial, characterizing AD as symbolic differentiation executed correctly and compositionally by a compiler. (49:08)
Detailed notes
## Background
Published on YouTube by Microsoft Research on July 26, 2018, this technical talk features researcher Conal Elliott presenting a radically simplified approach to automatic differentiation (AD). The presentation outlines a generalized, purely functional AD algorithm derived directly from categorical specifications, demonstrating that reverse-mode AD can be executed without the operational overhead of computational graphs, execution tapes, variables, or mutation.
## TL;DR
Elliott re-examines the foundations of calculus and automatic differentiation by unifying derivatives as linear transformations within Cartesian and Co-Cartesian categories rather than ad-hoc containers or computational graphs. By redefining differentiation to return a pair consisting of the primal result and a derivative linear map, he achieves compositionality where derivatives compose naturally via linear map composition. He shows that the traditional divide between forward-mode and reverse-mode AD is simply a matter of associativity in composing linear transformations, with reverse-mode AD naturally emerging from continuation-passing style and dual categories. Finally, he explains how an AD-agnostic compiler plugin translating typed lambda calculus into categorical combinators can generate correct-by-construction, highly parallelizable differentiation routines directly from standard functional code.
## Atmosphere & style
The presentation carries the measured, intellectually rigorous atmosphere of a distinguished computer science research seminar, grounded by Elliott's quiet conviction and dry wit. While addressing dense categorical proofs and lambda calculus transformations, Elliott conveys palpable frustration with the complex, stateful machinery of mainstream machine learning frameworks, famously confessing that conventional reverse-mode literature makes him want to weep. The talk unfolds as an illuminating conceptual rescue mission, peeling back decades of accidental engineering complexity to reveal the pristine, inevitable mathematical elegance underneath.
## Bulletin
- [03:20](https://www.youtube.com/watch?v=ne99laPUxN4&t=200s) Conal Elliott formulates automatic differentiation (AD) using category theory, defining derivatives uniformly as linear transformations rather than fragmented scalars, vectors, covectors, or Jacobian matrices.
- [01:15:13](https://www.youtube.com/watch?v=ne99laPUxN4&t=4513s) Reverse-mode AD is derived purely as the general AD category instantiated with continuation-passing style (CPS) or transposed linear maps, eliminating the need for tapes, computational graphs, partial derivatives, or mutable state.
- [29:57](https://www.youtube.com/watch?v=ne99laPUxN4&t=1797s) Using Joachim Lambek's 1980 equivalence between typed lambda calculus and Cartesian closed categories, standard functional code compiles directly via a GHC plugin into categorical AD representations without modifying source programs.
- [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) The dichotomy between symbolic and automatic differentiation is rejected as artificial, characterizing AD as symbolic differentiation executed correctly and compositionally by a compiler.
## Key takeaways
- [01:42](https://www.youtube.com/watch?v=ne99laPUxN4&t=102s) Traditional calculus relies on fragmented representations (scalars, vectors, covectors, Jacobians) across dimensions, whereas Michael Spivak's coordinate-free definition unifies derivatives as linear transformations.
- [09:25](https://www.youtube.com/watch?v=ne99laPUxN4&t=565s) The classical chain rule is non-compositional on its own; pairing the primal function value with the derivative linear map restores compositional modularity across sequential pipelines.
- [10:50](https://www.youtube.com/watch?v=ne99laPUxN4&t=650s) Linear functions serve as their own derivative linear transformations everywhere, providing exact local linear approximations without extra computation.
- [07:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=448s) Parallel composition (fork) models independent semantic fan-out without data dependencies, separating structural branching from sequential composition.
- [18:51](https://www.youtube.com/watch?v=ne99laPUxN4&t=1131s) Differentiable functions can be formalized via a Cartesian functor specification that preserves categorical structure across identity, composition, projections, and pairing.
- [29:57](https://www.youtube.com/watch?v=ne99laPUxN4&t=1797s) Lambek's theorem proves typed lambda calculus corresponds to Cartesian closed categories, allowing GHC Core to compile directly into categorical combinators.
- [39:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=2358s) Computational graphs in reverse-mode AD literature are post-hoc visualizations rather than necessary operational mechanisms for computing derivatives.
- [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) Automatic differentiation is symbolic differentiation performed correctly by a compiler, avoiding expression bloat through compiler let-bindings and subexpression sharing.
- [55:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=3318s) Parameterizing derivative types over arbitrary Cartesian and co-Cartesian categories generalizes AD beyond hardcoded function implementations.
- [01:02:33](https://www.youtube.com/watch?v=ne99laPUxN4&t=3753s) Representing linear maps as opaque functions incurs prohibitive basis-sampling costs for high-dimensional domains, motivating structural matrix representations via scale, fork, and join.
- [01:08:27](https://www.youtube.com/watch?v=ne99laPUxN4&t=4107s) Matrix composition associativity directly maps parenthesization choices to execution modes: right-association corresponds to forward-mode AD, while left-association yields reverse-mode AD.
- [01:12:41](https://www.youtube.com/watch?v=ne99laPUxN4&t=4361s) Continuation-passing style (CPS) structurally enforces left-association and prevents intermediate quadratic matrix materialization in reverse-mode AD.
- [01:17:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=4672s) Linear duality manifests concretely as matrix transposition, converting continuation consumers into reverse-mode linear maps.
- [01:21:16](https://www.youtube.com/watch?v=ne99laPUxN4&t=4876s) Conventional dual-number implementations exhibit type flaws by allowing primal outputs to depend on derivative inputs, an error prevented by explicit linear-map signatures.
- [01:23:54](https://www.youtube.com/watch?v=ne99laPUxN4&t=5034s) Categorical AD decouples the chain rule from primitive derivative definitions, avoiding redundant rules embedded within mathematical primitives.
- [01:29:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=5362s) Categorical compilation techniques originally designed to synthesize dynamically reconfigurable FPGA hardware transfer directly to automatic differentiation.
Daan Leijen opens the seminar by welcoming Conal Elliott back to Microsoft Research, describing him as a former MSR colleague and good friend. Elliott worked in the graphics group at MSR from 1994 until 2002 and is currently a Distinguished Scientist at Target. Leijen recalls being deeply inspired as a student by Elliott’s pioneering work on functional reactive animation, praising his distinctive gift for conceptual simplification: where computer animation was traditionally encumbered with matrices, frame rates, and timers, Elliott exposed its essence simply as functions over continuous time. Leijen notes that machine learning and automatic differentiation have become similarly bogged down in complex mechanisms, expressing confidence that Elliott’s new work will strip away that complexity to uncover their true essence.
```mermaid
flowchart LR
accTitle: Evolution of Elliott's Core Research Approach
accDescr: Diagram showing how Elliott applies semantic simplification to graphics and now to differentiation.
subgraph Graphics["Functional Reactive Animation (1990s)"]
G_Old["Complex machinery:<br/>Matrices, frames, timers"] -->|Distill essence| G_New["Animation = Functions of continuous time"]
end
subgraph AD["Automatic Differentiation (Present)"]
AD_Old["Complex machinery:<br/>Graphs, tapes, partial derivatives"] -->|Distill essence| AD_New["AD = Linear transformations & composition"]
end
```
Elliott takes the stage, noting that this is his first return to MSR to deliver a talk since his departure in 2002. Turning directly to the topic, he poses the fundamental question: what is a derivative? He stresses that unless this foundational question is answered rigorously and cleanly, it is impossible to construct an illuminating theory of automatic differentiation: “If we don't know what this means what's kind of hopeless to have any clean rigorous illuminating story about automatic differentiation.”
[01:42](https://www.youtube.com/watch?v=ne99laPUxN4&t=102s) The Confusion of Traditional Calculus Notions
Elliott recounts how conventional mathematics curricula incrementally introduce conflicting, patchwork definitions of the derivative:
- In elementary single-variable calculus (Calculus I), the derivative of a function at a point is taught as a single scalar number—the ratio expressing the rate of output growth relative to input growth.
- Moving to multivariable settings, when a function produces a higher-dimensional output, the derivative suddenly becomes a vector.
- Conversely, if the function consumes a higher-dimensional input and produces a scalar, the derivative becomes a different kind of vector—a covector. Elliott emphasizes that confusing vectors with covectors is rampant and produces severe conceptual errors and software bugs: “These two are often not distinguish which leads to all kinds of confusions and bugs in software but they're really importantly different. They look alike but they mean radically different things though, vector co-vector.”
- When both domain and codomain are multivariable, the derivative shifts into a matrix of partial derivatives (the Jacobian matrix).
- When considering higher-order derivatives (derivatives of derivatives), one is forced into higher-dimensional tensors.
Each ad-hoc representation introduces its own customized version of the chain rule. Elliott argues that this proliferation of representations yields a fractured, incomplete conceptual framework that ultimately fails calculus students, computer scientists, and software engineers alike.
[03:20](https://www.youtube.com/watch?v=ne99laPUxN4&t=200s) The Unified Definition: Derivatives as Linear Transformations
To escape this fragmentation, Elliott asserts that there is a single, beautiful, unifying formulation: the derivative of a function at a point is simply a linear transformation. He introduces the differentiator operator $D$ using Haskell-like type signature notation, encouraging the audience to interrupt with questions at any point.
$$\mathcal{D}:: (a \to b) \to (a \to (a \multimap b))$$
Here, $\mathcal{D}$ maps an arbitrary function from $a$ to $b$ to a function that, given an evaluation point in $a$, returns a linear transformation from $a$ to $b$ (denoted by Elliott as $a \multimap b$).
```mermaid
flowchart TD
accTitle: Unified Semantic View vs Concrete Representations
accDescr: Shows the abstract definition of derivative mapping down to multiple concrete representations.
Abstract["Abstract Derivative: D f a:: a ⊸ b<br/>(Linear Transformation)"]
The general mathematical definition of the derivative is formulated in terms of a local linear approximation: perturbing the input of function $f$ at point $a$ by a small displacement $\epsilon$ yields the base value $f(a)$ plus the linear map $\mathcal{D}(f)(a)$ applied to $\epsilon$, with the error vanishing superlinearly as $\epsilon \to 0$. Elliott notes that this coordinate-free definition holds across arbitrary dimensions and requires only that the domain and codomain are vector spaces equipped with suitable limit structures. He credits this insight to Michael Spivak’s classic 1965 text *Calculus on Manifolds*, calling it “a beautiful little gem of a book” that cuts straight to the core of differentiation.
Under this perspective, the various forms of multiplication found across calculus textbooks—scalar multiplication, dot products, outer products, and matrix products—are simply concrete representations of a single abstract operation: the composition of linear maps. The universal chain rule is therefore cleanly stated using standard function composition ($\circ$):
In response to an audience question asking whether matrices are merely concrete ways to represent these linear functions, Elliott agrees wholeheartedly: “Yes, exactly. So, abstractly we have a linear transformation from a to b, concretely, it might have a matrix that represents the linear transformation.” He points out that standard linear algebra software libraries treat matrices as raw containers, leading to runtime shape mismatch bugs because their type systems fail to track input and output spaces. Typing derivatives as linear transformations guarantees composition correctness at compile time. Moreover, decoupling the abstract essence from matrix representations opens the door to superior representations, as Elliott observes: “the matrix representation actually turned out to be a bad idea even though it's just about universally adopted.”
[07:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=448s) Sequential vs. Parallel Composition and the Non-Compositionality of the Chain Rule
Elliott explains that sequential composition ($\circ$) is only one mode of combining computations. The second fundamental pattern is parallel composition, which he defines via the pairing combinator `fork`:
$$\text{fork}(f, g)(a) = (f(a), g(a))$$
Where $f:: a \to c$ and $g:: a \to d$, the function $\text{fork}(f, g):: a \to (c, d)$ distributes a shared input $a$ to both functions without introducing data dependencies between them. Elliott clarifies that parallel here refers to semantic independence rather than operational concurrency: “Logically, this is parallel. When I say parallel, I don't mean operationally, I don't mean that runs in parallel... I mean semantically, there's no data dependencies. Where sequential composition is all about data dependencies, parallel composition is free of them.” While conventional automatic differentiation literature routinely claims that differentiation is “all about the chain rule,” the chain rule accounts solely for sequential composition, forcing systems to handle fan-out and parallel branching through ad-hoc, clumsy mechanisms.
Returning to the sequential chain rule, Elliott identifies a serious structural flaw when attempting to turn it into an efficient, compositional implementation. An algorithm is compositional if the transformed result of a compound expression can be computed purely from the transformed results of its immediate subcomponents: “whatever operation on performing, like differentiation of a composition, I form by taking the derivative of each of the two functions and then somehow combining them. All right? Well, the chain rule doesn't work that way. The chain rule isn't compositional”. To evaluate $\mathcal{D}(g \circ f)(a)$, the chain rule requires $\mathcal{D}(g)$ to be evaluated at $f(a)$ rather than $a$. Because the derivative of $g$ requires the intermediate primal value $f(a)$, computing the derivative in isolation from the original function violates strict compositional structure—a tension that lies at the core of why traditional AD algorithms struggle with complexity.
[09:25](https://www.youtube.com/watch?v=ne99laPUxN4&t=565s) The Compositional Fix: Preserving the Original Value
Conal Elliott addresses a fundamental obstacle in making differentiation compositional. When calculating the derivative of a composite function $g \circ f$, the chain rule demands not only the derivatives of $f$ and $g$, but also the evaluation of $f$ itself at the input argument. In a naive implementation that computes only the derivative, this need for the intermediate value makes compositional reasoning and implementation clumsy.
Elliott provides an elegant fix: instead of computing just the derivative mapping, the differentiated function is redefined to take an input $a$ and produce both the original result $b$ and the derivative. As Elliott explains, “This enhanced specification is compositional because when you write out the implications of it, computing the function and its derivative for $f$ and $g$ involves just $f$ and $g$ and its derivatives.” An audience member asks for clarification about the output type: “So you mean the $b$ on the right side is the same as the $b$ computed above the function?” Elliott confirms this directly: “Yes. Exactly. So all we're doing... says that this enhanced derivative of $f$ is $f$ itself and the derivative of $f$. That's all just don't forget $f$, that's all this is saying.” He points out that this essential adjustment is ubiquitous across all automatic differentiation implementations precisely because it is required to achieve modular, compositional behavior.
```mermaid
flowchart LR
accTitle: Compositional Differentiation Pair
accDescr: Shows the enhanced derivative mapping an input to both its evaluation and its linear derivative.
subgraph EnhancedDerivative["D a b"]
direction TB
In["Input: a"] --> F["f(a): b"]
In --> Df["D f(a): a ⊸ b"]
end
```
[10:50](https://www.youtube.com/watch?v=ne99laPUxN4&t=650s) Derivatives as Linear Maps and Approximations
Elliott explores a core insight from the perspective of calculus on manifolds: the derivative of any linear function is that linear function itself, everywhere. While this property might initially sound counterintuitive, it follows naturally from the geometric and analytical meaning of derivatives. Differentiation fundamentally constructs local linear approximations. At the point of tangency, the linear approximation is perfectly accurate; as one moves away, it becomes increasingly inaccurate, requiring higher-order terms like second derivatives (quadratic approximations) for greater fidelity.
Because a linear function is already linear, it serves as its own exact local approximation. As Elliott states: “So, when I say the derivative of a linear function is itself everywhere, all I'm saying is that linear functions are their own perfect linear approximations.” He notes that mathematicians and programmers already rely on this fact implicitly:
- The scalar derivative of $f(x) = x$ is commonly described as $1$, which in the language of linear transformations represents the identity map (multiplying by $1$).
- Similarly, the derivative of $f(x) = 2x$ is the linear transformation that multiplies by $2$.
- For non-scalar multidimensional domains, the derivative of the identity function is represented by the identity matrix (ones on the diagonal, zeros elsewhere).
- Projection functions, such as taking the first or second element of a pair, are also linear functions and therefore serve as their own derivatives everywhere.
[13:06](https://www.youtube.com/watch?v=ne99laPUxN4&t=786s) Stripping Away the Accidental Baggage of Reverse Mode
Elliott asserts that the core foundation of automatic differentiation is already complete. By starting with primitive operations (addition, multiplication, sine, cosine) whose derivatives are known analytically, and combining them with linear primitives alongside sequential and parallel composition, automatic differentiation emerges naturally.
He contrasts this principled foundation with the prevailing literature on reverse-mode automatic differentiation (RAD) and backpropagation in machine learning, which he views as needlessly complex and weighed down by historical baggage. Because backpropagation was invented in the 1950s and 1960s and later rediscovered by the machine learning community without a background in crisp mathematical specifications, it became entangled with ad-hoc operational machinery. Elliott argues that once one discards the “historical accidental baggage, graphs, and variables, and layers, and things like that, the essence really is just what I've shown you, and we can now put these pieces together into automatic differentiation, and then we're done.”
[14:15](https://www.youtube.com/watch?v=ne99laPUxN4&t=855s) Categorical Foundations: Categories and Cartesian Categories
To organize these operational building blocks cleanly, Elliott turns to basic category theory, reassuring the audience that no advanced categorical background is necessary. He defines a category as an algebraic structure over "function-like things" (morphisms) that have a domain and codomain, governed by two operations:
1. **Identity:** Mapping an object to itself.
2. **Composition:** Taking an arrow from $b$ to $c$ and an arrow from $a$ to $b$, producing an arrow from $a$ to $c$.
These operations satisfy standard algebraic laws: composition must be associative, and the identity morphism must serve as both the left and right identity for composition.
Elliott then introduces a *Cartesian category*, which enriches a standard category with a formal notion of products (pairs). A Cartesian category includes three characteristic operations:
- **Extract Left (`exl`):** Projects the first element from a pair.
- **Extract Right (`exr`):** Projects the second element from a pair.
- **Fork (`△`):** Takes two morphisms sharing the same domain and combines them into an arrow that produces a pair in its codomain.
These structures form standard categorical interfaces that originated in 1950s algebra. Applying them to automatic differentiation allows one to treat differentiable functions—computations that evaluate a value along with its derivative—as first-class arrows within an algebraic interface rather than ordinary computable functions.
[17:23](https://www.youtube.com/watch?v=ne99laPUxN4&t=1043s) Formalizing the Differentiable Function Specification
Elliott translates these mathematical concepts into a Haskell formulation. He introduces an abstract type wrapper, `D a b`, representing a differentiable function from `a` to `b`:
$$\mathcal{D}\ a\ b \cong a \to (b \times (a \multimap b))$$
Here, a differentiable computation is represented concretely as a function taking an argument of type $a$ and returning a pair containing the output value $b$ and a linear map representing the derivative $(a \multimap b)$.
He defines the specification morphism $\hat{D}$ (written `d hat`), which takes an ordinary mathematical function $f: a \to b$ and lifts it into the category of differentiable functions `D a b` by packaging $f$ alongside its derivative $\mathcal{D} f$. Elliott takes care to stress an important theoretical distinction: “I want to emphasize here, the specification is not computable. So, given an arbitrary computable function, even if it's continuous, even if it's differentiable in a mathematical sense, it's not computable to construct its derivative.” The goal of the work is not to mechanically differentiate arbitrary closed-box functions, but rather to begin from an elegant, non-computable mathematical specification and systematically derive a correct-by-construction, computable algorithm.
[18:51](https://www.youtube.com/watch?v=ne99laPUxN4&t=1131s) The Specification: Homomorphisms over Category and Cartesian Structure
Conal Elliott opens by outlining the overarching strategy: taking a specification that is non-computable, simple, and compelling, and calculating from it an implementation that is both efficiently computable and automatable. The goal is automatic differentiation (AD), organized around standard categorical interfaces in Haskell—specifically `Category`, `Cartesian` (representing products), and additional classes for elementary operations like sine and cosine.
The formal specification demands that the non-computable differentiation operator $\hat{\mathcal{D}}$ preserve category and Cartesian structure. This requirement collapses cleanly into five core equations: two from the `Category` interface (identity and composition) and three from the `Cartesian` interface (left extraction/projection, right extraction/projection, and product fork). In each case, $\hat{\mathcal{D}}$ applied to an operation in the category of smooth functions yields the corresponding operation in the target category of differentiable functions, which compute a primal value paired with its derivative. Elliott emphasizes how much conceptual clarity this provides: “That any intuition you form about what does it mean when I'm composing these two things is captured precisely and elegantly by these five requirements.”
An audience member asks whether this means $\hat{\mathcal{D}}$ is a functor. Elliott agrees, clarifying that it is a Cartesian functor, or more broadly, a homomorphism over the algebraic structure. It maps each piece of vocabulary—identity, composition, left/right projection, and fork—directly across categories, distributing over that structure compositionally.
```mermaid
flowchart LR
accTitle: Cartesian Functor Mapping
accDescr: Diagram showing the differentiation functor mapping category and Cartesian operations to differentiable operations.
subgraph Source["Smooth Functions (Cartesian Category)"]
direction TB
id1["id"]
comp1["g ∘ f"]
fork1["f △ g (fork)"]
proj1["exl / exr"]
end
subgraph Target["Differentiable Functions (Target Category)"]
direction TB
id2["id_D"]
comp2["g_D ∘_D f_D"]
fork2["f_D △_D g_D"]
proj2["exl_D / exr_D"]
end
Source -->|"D̂ (Cartesian Functor)"| Target
```
[22:03](https://www.youtube.com/watch?v=ne99laPUxN4&t=1323s) Deriving the Implementation: Chain Rule, Fork, and Leibniz Rule
Elliott explains that once these five equations are laid out, finding the implementation becomes an exercise in elementary algebra, fully detailed in his paper *The Simple Essence of Automatic Differentiation*. The derivation relies on three standard pillars: the chain rule, the fork rule, and the fact that linear functions serve as their own derivatives everywhere, alongside basic calculus rules for arithmetic operations.
Operationally, the derived code weaves primal evaluation and derivative calculation together. For a linear function $f$, its differentiable counterpart takes $a$ to $(f(a), f)$ (or $f \mathbin{\triangle} \text{const } f$). For composition $g \circ f$ evaluated at $a$:
1. $f(a)$ evaluates to a pair of output value $b$ and derivative $f'$.
2. $g(b)$ evaluates to output value $c$ and derivative $g'$.
3. The primal result is $c$, while the derivative is the composition of the linear maps $g' \circ f'$, exactly reproducing the chain rule.
For the fork operation, Elliott notes that the derivatives and values are computed with zero data dependencies between them, making them completely independent and inherently parallelizable. Negation, addition, identity, and projections are linear, so their derivatives are trivial. Multiplication, however, is non-linear; differentiating it at a point $(a, b)$ produces a linear map that accepts perturbations $(\Delta a, \Delta b)$ and outputs $b \cdot \Delta a + a \cdot \Delta b$, which is the classical Leibniz product rule.
An audience member asks about how linear maps are represented. Elliott notes that while they can simply be viewed as functions that happen to be linear, there are multiple representations—both traditional matrix forms and non-traditional structures—that will form the central story of the lecture. Another audience question asks whether parametricity and type theory (such as linear types or the "lollipop") might uniquely force these implementations as free theorems. Elliott acknowledges the elegance of the idea while remaining cautious: “There's something that's to me very compelling and inevitable about this development, and that may be a clue that there's actually a free theorem.” However, because the constructions require vector space or module structures rather than unconstrained polymorphism, classical parametricity theorems do not immediately apply out of the box.
- Deriving composition automatically inlines and composes primal evaluations alongside linear derivative maps.
- Fork operations exhibit no mutual data dependencies, allowing parallel evaluation of both components and their derivatives.
- Linear operations require no specialized derivative storage because their derivatives are constant and equal to the functions themselves.
- Non-linear multiplication synthesizes the Leibniz rule directly from the specification.
[28:07](https://www.youtube.com/watch?v=ne99laPUxN4&t=1687s) Running Examples: Squaring and Magnitude Squared
To examine the performance characteristics of this naive AD algorithm and show how it can be systematically improved, Elliott introduces small running examples written in Haskell.
The first example is scalar squaring:
$$\text{sqr } a = a \times a$$
Elliott clarifies the Haskell type signature `Num a => a -> a`, joking about the common functional programming pun where the type variable and the value variable share the name `a`. While `a` could be floating-point numbers, doubles, complex numbers, or higher-dimensional structures, it is easiest to think of it concretely as a real number.
The second example is the magnitude squared function on pairs:
$$\text{magSqr } (a, b) = a^2 + b^2$$
Operating on products of type $a \times a$, this function computes the sum of the squares of the components. Elliott begins breaking down how the derived AD machinery handles these compositions to illustrate the operational mechanics and computational trade-offs that arise in practice.
[29:13](https://www.youtube.com/watch?v=ne99laPUxN4&t=1753s) Motivating Examples across Scalar and Non-Scalar Domains
To ground the formal development, Elliott presents three simple functions of varying complexity. The first is squaring a number—a purely scalar function ($x \mapsto x^2$). The second takes a pair $(a, b)$, squares each component, and adds them together ($a^2 + b^2$, or the squared magnitude). The third takes a pair $(x, y)$, forms their product $z = x \cdot y$, and computes both the sine and cosine of $z$.
These specific examples are deliberately chosen because they expose the boundaries between scalar and non-scalar structures in different ways. Squaring is entirely scalar; magnitude squared has a non-scalar domain (a pair) mapping to a scalar codomain; and the sine/cosine product function has both a non-scalar domain and a non-scalar codomain. These programs can initially be written down as ordinary, simple, purely functional programs, but the core strategy is to rewrite them into categorical vocabulary.
[29:57](https://www.youtube.com/watch?v=ne99laPUxN4&t=1797s) Logic, Category Theory, and Joachim Lambek's 1980 Result
Moving from pure functional expressions to categorical combinators represents an important conceptual leap. Elliott emphasizes that there is a deep foundational connection uniting logic, category theory, and computation: “at the heart of a computation, reason in the foundation of mathematics are all the same thing.” In mainstream imperative languages such as C#, Java, or untyped languages like JavaScript, this mathematical core is completely obscured by syntactic noise and incidental complexity. In contrast, an elegant and mathematically pure formal system like the typed lambda calculus makes the correspondence direct and visible. Haskell, as Elliott notes, is essentially typed lambda calculus with syntactic sugar.
Elliott traces this insight back to a 1980 result by mathematician Joachim Lambek. While programmers naturally assume that lambda terms denote computable functions, Lambek showed that computable functions represent merely one possible interpretation. The models of typed lambda calculus are precisely the Cartesian closed categories (CCCs):
1. **Category:** Equipped with identity and associative composition.
2. **Cartesian:** Equipped with binary products, including left and right projections (`exl`, `exr`) and the pairing/fork operation (`△`).
3. **Closed:** Equipped with first-class functions (exponentials).
Any mathematical structure that provides these operations and obeys the category laws forms a consistent model of the typed lambda calculus. Rather than forcing the programmer to write in an austere categorical language, an AD-agnostic compiler plugin can automatically translate standard typed lambda calculus into categorical vocabulary. Once translated, instead of interpreting the terms as ordinary computable functions, the compiler interprets them in an alternative category—specifically, the category of differentiable functions.
```mermaid
flowchart LR
accTitle: Translation of Lambda Calculus to Categorical Models
accDescr: Pipeline showing typed lambda calculus compiled to Cartesian Closed Categories and mapped to distinct interpretations.
subgraph FrontEnd["Source Language"]
A["Haskell Code<br/>(Typed Lambda Calculus)"]
end
subgraph Transformation["Compiler Level"]
B["Compiler Translation<br/>(Cartesian Closed Category)"]
end
A -->|"automatic translation"| B
B -.-> C
B --> D
B -.-> E
```
---
[33:30](https://www.youtube.com/watch?v=ne99laPUxN4&t=2010s) Compiling Combinators: Squaring, Sum of Squares, and Sine/Cosine
An audience member asks about modular boundaries, observing that in the categorical translation of the magnitude squared function, squaring was inlined rather than referenced by name: “do you need to do that in Haskell log transformation and break modular boundaries or?” Elliott answers that this inlining is purely an artifact of where his prototype compiler implementation currently stands: “There's nothing, yes. So, at some step, this would look like multiplication composed... it will be square composed with exl, and that would be square composed with the exl. That'll be more readable and more modular, yes. Just not quite there yet.”
Elliott then steps through how these functions look when expressed purely in point-free categorical combinators:
- **Squaring ($x^2$):** Take the identity combinator and fork it with itself (`id △ id`). Given a value $a$, this duplicates it to $(a, a)$. Composing that duplication with multiplication yields squaring: `mul ∘ (id △ id)`.
- **Magnitude squared ($a^2 + b^2$):** Take the input pair, project the left element with `exl`, and duplicate it (`exl △ exl`), then multiply; do the same with the right projection (`exr △ exr`) in parallel; finally, compose with `add` to sum the two squared branches. Because composition reads right-to-left, data flows into projections, through multiplications in parallel, and into addition.
- **Cosine-Sine Product ($z = x \cdot y \implies (\cos z, \sin z)$):** Take the input pair, multiply them together to form $z$, and fork the cosine and sine functions in parallel: `(cos △ sin) ∘ mul`.
Because the derivative of each basic operation (`mul`, `add`, `fork`, `compose`) was already established in the categorical framework, evaluating these categorical expressions in the differentiable category yields an implementation that computes exact derivatives alongside normal values.
---
[35:43](https://www.youtube.com/watch?v=ne99laPUxN4&t=2143s) Why Automatic Differentiation Has Nothing to Do with Graphs
Elliott presents a visual graph of the magnitude-squared function to show how the categorical combinators map to execution flow—illustrating how the left and right projections feed into parallel multiplication nodes whose outputs feed directly into an addition node. In this demonstration, he points out that three distinct categories are operating simultaneously:
1. The standard semantic category of ordinary mathematical or computable functions.
2. A syntactic category that manipulates abstract syntax trees to pretty-print expressions.
3. A category that constructs a visualization graph.
4. The target category of differentiable functions.
This leads Elliott to a central, emphatic critique of conventional machine learning orthodoxy. In machine learning, particularly regarding reverse-mode AD and backpropagation, differentiation is almost universally framed in terms of computational graphs and tapes. Elliott rejects this premise entirely: “automatic differentiation is almost always talked about in terms of graphs, especially in Machine Learning, especially in reverse mode. I think that's always a mistake. Okay, because differentiation has nothing to do with graphs... differentiation is about functions, there's no graphs there.”
Elliott explains that any compositional API where outputs plug into inputs can trivially be represented as a graph—just as elementary arithmetic can be drawn as a dataflow graph of addition and multiplication nodes. But arithmetic itself is not about graphs; it is about numbers and operations governed by an algebraic domain and a type system. While a compiler author or a graph theorist may use graphs as an internal implementation artifact, equating differentiation itself with graphs obscures the mathematics. Dispensing with graphs, tapes, and mutable state is precisely what differentiates his approach from mainstream AD frameworks.
[39:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=2358s) Graphs as Visualizations vs. Graphs as Computation
Conal Elliott addresses a potential misunderstanding regarding the graphical diagrams displayed in his slides. While audiences might suspect he is doing something akin to graph-based frameworks like TensorFlow, he firmly disabuses them of that notion:
> “Even when I show you the result of automatic differentiation as a graph, the graph came second, not first.”
He insists that the graphs are strictly an after-the-fact visualization technique to communicate computational structure to human eyes, not an internal mechanism used to compute derivatives.
To demonstrate, Elliott walks through the simple squaring function, showing both its categorical representation and its computational graph. When the expression is interpreted inside the category of differentiable functions and reinterpreted into a visual diagram, it emits two distinct parts. The first output is the evaluation of the primal function: taking an input $a$ and returning $a \times a = a^2$. The second output is a linear function—represented on the diagram as a small green box taking an input and returning an output. Elliott labels the perturbation input $da$ (a small delta). The linear map computes $a \times da \times 2$, yielding $2a \cdot da$.
Elliott stresses a conceptual correction about the nature of derivatives: people conventionally say "the derivative of $a^2$ is $2a$," but strictly speaking, it is the linear map that takes $da$ to $2a \cdot da$. Saying the derivative is $2a$ is merely shorthand for "multiplication by $2a$."
```mermaid
flowchart LR
accTitle: Squaring Function Derivative Map
accDescr: Dataflow graph showing primal value computation alongside the derivative linear function.
subgraph Primal["Primal Computation"]
A["Input: a"] --> Square["a * a"] --> Out1["Result: a^2"]
end
subgraph Tangent["Derivative (Linear Function)"]
DA["Input: da"]
A -.-> Scale["* 2a"]
DA --> Scale --> Out2["Result: 2a * da"]
end
```
[41:19](https://www.youtube.com/watch?v=ne99laPUxN4&t=2479s) Sum of Squares and the Simplicity of Categorical AD
Moving to a slightly richer example, Elliott examines the sum of two squares, $(a, b) \mapsto a^2 + b^2$. Interpreting this categorical expression yields the original primal computation—computing $a^2$, $b^2$, and adding them together—alongside the combined derivative map. For a moment, Elliott stumbles over his own diagram while tracing the wires:
> “Yes, so never mind when I say, yes this is correct my brain was incorrect.”
Tracing the diagram carefully, he confirms that the linear map receives the tangent pair $(da, db)$, calculates $2a \cdot da$ and $2b \cdot db$, and sums them to produce the derivative result.
An audience member chimes in to confirm the underlying mechanics: there is no mysterious trickery occurring; one simply defines derivatives for primitive building blocks (like multiplication or addition) and composes them sequentially and in parallel. Elliott wholeheartedly agrees, reiterating:
> “I want to emphasize the simplicity of what's going on here particularly in contrast to the complexity of what goes on in the literature about automatic differentiation, particularly what's called reverse mode, which is the mode that's needed for machine learning and other uses of high dimensional optimization problems.”
- Primitives require known derivatives, and composition structures (sequential and parallel) handle the rest.
- The categorical foundation bypasses the standard algorithmic machinery (ad-hoc stateful graphs, tapes, mutation) typical in reverse-mode literature.
[43:24](https://www.youtube.com/watch?v=ne99laPUxN4&t=2604s) Audience Q&A: Sum Types, Discontinuities, and Church Encodings
An audience member asks how this categorical approach handles sum types (disjoint unions) and discontinuities. Elliott acknowledges that the question touches on several angles, but notes that the most fundamental issue is mathematical:
> “...the first and most fundamental question is differentiation even meaningful, because once you once you have some types, you no longer can have purely continuous functions, well, you can but none of them are interesting, right? They would have to always be the left or the right disjunct of the sum.”
Elliott remarks that while he has pondered sum types, he does not yet know the definitive categorical answer. The dialogue turns to encoding sums. An audience member suggests Church encodings. Elliott notes that while pairs and sum types can be encoded as higher-order functions (using universal quantification and rank-2 types, which correspond categorically to cones), it remains an open question whether differentiability carries through cleanly:
- Sum types inherently introduce branching and non-differentiable or trivially constant transitions between disjoint components.
- Encoding products or sums via Church encodings requires universal quantification (rank-2 polymorphism).
- An audience member points out that Church encoding is essentially an instance of continuations, which Elliott confirms will appear later in the presentation.
Elliott emphasizes why he favors this perspective: starting from backpropagation as presented in standard machine learning papers leaves one "without a prayer" of proving correctness or understanding core invariants. Re-grounding the problem in the language of category theory strips away unnecessary complexity and enables rigorous re-examination of features like continuations and Church encodings.
[46:43](https://www.youtube.com/watch?v=ne99laPUxN4&t=2803s) The True Objective: Compiling Mathematical Representations
An audience member tries to clarify Elliott's high-level objective: is the goal to take an arithmetical circuit and differentiate it? Elliott sharpens the distinction:
> “Repeat the question, is it my goal here to take a description of mathematical function, and generate code that computes its derivative correctly and efficiently, is that the question, right? The answer is yes. That's exactly my goal.”
Elliott explains a key nuance: one cannot differentiate an arbitrary mathematical function in the abstract because mathematical functions themselves are not directly computable entities. Instead, one differentiates a *representation* of a function. While popular tools choose computational graphs as their starting representation, Elliott considers that a poor choice compared to standard lambda calculus, which can be cleanly translated into categorical expressions completely independently of differentiation.
Another audience member brings up symbolic differentiation, wondering how it differs from Elliott's goal since numeric Fortran programs also tackle differentiation. Elliott points out that standard AD literature often draws a flawed three-way taxonomy:
1. **Numerical approximation / Secant method / Method of finite differences:** Approximating slopes by evaluating nearby points and drawing a line, which Elliott flatly dismisses: *"Okay, well it's incorrect."*
2. **Symbolic differentiation:** Manipulating algebraic formula expressions directly.
3. **Automatic differentiation:** Often categorized simply as "numeric."
Elliott contends that pigeonholing automatic differentiation as purely "numeric" is misleading. Depending on how one views it, AD has numeric aspects, but viewed from another lens, it is inherently symbolic, rendering standard historical distinctions imprecise.
[49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) Demystifying Symbolic vs. Automatic Differentiation
An audience member remarks that the approach seems entirely symbolic because it manipulates symbols. Conal agrees that the statement is factually true, but points out that it is fundamentally misleading: in a compiler, *everything* being done is symbolic. At runtime, one could conversely say everything is numeric (represented by bits), but neither characterization is particularly clarifying.
```mermaid
flowchart TD
accTitle: Three Approaches to Differentiation
accDescr: Comparison of Numerical, Classical Symbolic, and Automatic Differentiation via a Compiler.
subgraph Approaches["Approaches to Differentiation"]
N["1. Numerical Approximation<br>(Secant / finite differences)"]
S["2. Classical Symbolic<br>(AST expression rewrite)"]
AD["3. Automatic Differentiation<br>(Chain rule on primitives)"]
end
N -->|"Drawback"| N_Issue["Inaccurate & terrible performance"]
S -->|"Drawback"| S_Issue["Commonly done poorly;<br>exponential bloat without sharing"]
AD -->|"Conal's Perspective"| CompilerAD["Symbolic differentiation<br>performed well by a compiler"]
```
Conal reviews the standard textbook taxonomy that categorizes differentiation into three distinct methods:
1. **Numerical approximation** (the secant method or method of finite differences), which computes derivatives incorrectly and suffers from terrible accuracy and performance.
2. **Symbolic differentiation**, which mimics high school calculus by explicitly manipulating algebraic syntax trees (e.g., matching on $\sin(u)$ to yield $\cos(u) \, du$).
3. **Automatic differentiation (AD)**, which applies the chain rule systematically to programmatic primitives.
Conal challenges this tripartite distinction, asserting that the conventional boundary between symbolic and automatic differentiation is an artificial dichotomy. As he puts it:
> “What I'm really saying is this, automatic differentiation is symbolic differentiation performed by a compiler.”
Literature often treats symbolic differentiation as fatally flawed due to performance problems. Conal counters that symbolic differentiation *done badly* has all kinds of problems, but that is simply the consequence of poor engineering rather than an inherent flaw of symbolic methods: “All right? So, don't do it badly.” By embedding differentiation into the compiler pipeline, one effectively tricks the compiler into doing symbolic differentiation. Compilers naturally work symbolically and excel at preserving performance and eliminating redundancies. When an audience member suggests symbolic differentiation can fail on unsupported expressions while this approach guarantees success within its vocabulary, Conal notes that both paradigms face the exact same limitation: if an expression falls outside the recognized mathematical vocabulary, differentiation cannot proceed.
[52:36](https://www.youtube.com/watch?v=ne99laPUxN4&t=3156s) Sharing Computation Between Primal and Derivative
Conal presents a third concrete code example: computing the sine and cosine of a product ($\sin(x \cdot y)$ and $\cos(x \cdot y)$), displaying both the undifferentiated source and its differentiated version. Even in this small example, a major feature is visible: extensive computation sharing between the regular value (often called the *primal*) and the derivative.
He recalls an essential design choice introduced earlier in the talk: the textbook chain rule on derivatives alone is not compositional because evaluating the derivative of $g \circ f$ at $x$ requires the value of $f(x)$ itself. Conal resolved this by pairing each function with its derivative:
This pairing does more than restore category-theoretic compositionality—it unlocks computational efficiency. In practice, a mathematical function and its derivative share substantial intermediate work. Augmenting the function to return both primal and derivative in a unified specification makes that shared computation easy to reuse:
> “By putting them both into one specification, it makes it possible to optimize and share computation.”
Addressing the common complaint that symbolic differentiation causes an exponential explosion in work—either during compilation to optimize away redundant trees or at runtime to evaluate them—Conal emphasizes that this is avoided naturally. Compilers handle sharing as part of their fundamental job.
When an audience member points out that compilers transform syntax trees into directed acyclic graphs (DAGs) using `let`-bindings, Conal cautions against thinking in terms of graphs altogether:
> “When you say let, that's not the remark wants to turn tree into a diag, what I would say is stop thinking about graphs, okay.... Just don't create the problem in the first place, don't think about trees and graphs because differentiation has nothing to do with trees and graphs.”
Working with trees compositionally is straightforward, but naive trees duplicate shared subexpressions exponentially; trying to explicitly manipulate graphs to refactor trees adds immense, unnecessary complexity. By relying on simple categorical primitives and letting compiler bindings handle common subexpressions, graph manipulation disappears from the calculus entirely.
[55:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=3318s) Generalizing Derivatives via Cartesian Categories
Conal turns back to the Haskell implementation derived earlier by solving the five structural-preservation equations for $\hat{\mathcal{D}}$. Driven originally by an aesthetic desire to write clean code, he noticed a striking pattern in the operations defining differentiable functions:
| Operation on $D$ | Operation on Primal Functions | Operation on Derivative Parts |
|:--- |:--- |:--- |
| **Identity** (`id`) | Identity function (`id`) | Identity linear map (`id`) |
| **Composition** (`(.)`) | Function composition (`(.)`) | Linear map composition (`(.)`) |
| **Left Projection** (`exl`) | Function `exl` | Linear map `exl` |
| **Right Projection** (`exr`) | Function `exr` | Linear map `exr` |
| **Fork / Pair** (`(&&&)`) | Function `(&&&)` | Linear map `(&&&)` |
The definition of differentiable operations relies on virtually nothing specific to concrete linear maps. It requires only that linear maps support identity, composition, projections, and pairing, and that they satisfy the standard Cartesian category laws. Conal reflects on how this visual symmetry uncovered a deeper mathematical truth:
> “So, this observation and writing the code purely aesthetic motivations, it led to I think a deep and very powerful insight, which is that, automatic differentiation not only can be expressed elegantly, but much much more generally than the original specification.”
Because every operation on differentiable functions maps directly to an identical operation on the derivative representation, the derivative type can be parameterized:
- In the earlier derivation, the representation type was hardcoded to linear maps (`LinearMap`).
- In the generalized formulation, $D_k$ is parameterized over an arbitrary Cartesian category $k$.
- Any mathematical representation that forms a Cartesian category can stand in for the derivative.
The derived implementation remains identical in structure. The only minor modification is explicitly distinguishing operations on functions from operations on the generalized derivative category $k$ (e.g., distinguishing between function identity and category identity), and handling linear primitives like negation (`negate`) and addition (`add`) through their generalized linear versions.
[58:53](https://www.youtube.com/watch?v=ne99laPUxN4&t=3533s) Refactoring Multiplication: Scaling and Joining
Conal Elliott examines the derivative of multiplication, noting that his earlier expression was written strictly in terms of functions rather than in the vocabulary of an arbitrary Cartesian category. Multiplication itself is not a linear operation, but bilinear; however, when one argument is fixed, the operation becomes linear. Elliott identifies two core computational patterns at play: scaling an input, and decomposing a pair of inputs to compute intermediate results and add them together.
To formalize these patterns in a way that generalizes beyond ordinary functions, he introduces two operations: `scale` and `join`. Scaling by $u$ is the linear function that multiplies its argument by $u$. The `join` operation serves as the exact dual to `fork`. While `fork` takes two arrows sharing the same domain and pairs up their results, `join` takes two arrows sharing the same codomain, applies each to one component of an incoming pair, and sums their outputs. Using this newly introduced vocabulary, the derivative of multiplication simplifies to $\lambda (a, b) \to \text{scale}(b) \mathbin{\triangledown} \text{scale}(a)$ (joining scale by $b$ with scale by $a$, corresponding to $b \cdot da + a \cdot db$).
> “So, multiplication isn't linear. That's what's called bi-linear. But when you provide one argument to multiplication, the result is linear.” — Conal Elliott
```mermaid
flowchart LR
accTitle: Cartesian Fork versus Co-Cartesian Join
accDescr: Visualizing fork combining two arrows with the same domain and join combining two arrows with the same codomain.
subgraph ForkSubgraph["Fork (Cartesian)"]
direction LR
InA["a"] -->|"f"| OutB["b"]
InA -->|"g"| OutC["c"]
end
subgraph JoinSubgraph["Join (Co-Cartesian)"]
direction LR
InPair["(a, b)"] -->|"f on a, g on b"| Add["+"]
Add --> OutShared["c"]
end
```
[01:01:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=3668s) Co-Cartesian Categories and Additive Linear Maps
Elliott presents the formal categorical structure that mirrors Cartesian categories: the co-Cartesian category. Where a Cartesian category provides two projections or extractors along with the pairing operation `fork`, a co-Cartesian category provides the duals: two injections (`inl` and `inr`) and the combining operation `join`. For additive linear maps represented as functions, the injections introduce zero values (injecting from the left pads a zero on the right, and vice versa), while `join` parcels out arguments and adds the results.
This formulation yields a clean, elegant vocabulary for defining linear transformations as regular functions equipped with an additive context. All involved types must support addition and scaling, wrapping standard functions in an explicit categorical abstraction. While this representation using functions is mathematically concise and works smoothly for theoretical calculations, Elliott notes that it exposes severe practical shortcomings when applied to real-world computational workloads.
> “So, instead of having two projections or extractors, we have two injections. Left and right. Instead of taking two arrows with the same domain, we take two with same co-domain.” — Conal Elliott
[01:02:33](https://www.youtube.com/watch?v=ne99laPUxN4&t=3753s) The Cost of Representing Linear Maps as Functions
The central limitation of representing linear maps as functions appears when an algorithm must extract an explicit data representation, such as a vector or matrix, from the linear map. In computer graphics, for instance, lighting and shading require the normal vector at a surface point, which is derived from the cross product of partial derivatives. Because the cross product requires concrete vectors rather than opaque functions, the underlying linear map must be converted into data.
The standard way to extract a matrix or vector from a linear function is to sample it across a standard basis, such as feeding the columns of an identity matrix (one-hot vectors) through the function to accumulate the Jacobian. However, this becomes prohibitively expensive when the domain is high-dimensional. In machine learning and deep optimization problems, input dimensions routinely reach millions. Sampling a million-dimensional domain requires a million forward passes, producing quadratic work:
- **Computer Graphics Shading:** Computing surface normals via cross products requires converting the differential linear map into explicit tangent vectors.
- **Deep Learning Optimization:** Gradient descent needs a concrete gradient vector to determine the direction of input adjustments toward an optimum.
- **Domain vs. Codomain Asymmetry:** Optimization objective functions typically have a scalar (one-dimensional) codomain and a massive (million-dimensional) domain.
- **Sampling Bottleneck:** Because function sampling cost scales with the dimension of the *domain*, extracting gradient vectors via basis passes is completely unviable.
> “If we're doing optimization problems, particularly if we have high dimensional domains, we would not want to use functions or representation because it's just too expensive to extract representation.” — Conal Elliott
[01:06:04](https://www.youtube.com/watch?v=ne99laPUxN4&t=3964s) Matrices as Compositions of Scale, Fork, and Join
To eliminate the catastrophic cost of sampling functions across high-dimensional bases, Elliott explains why standard practice abandons pure functions in favor of matrix representations. Conceptually, a matrix can be viewed structurally as a "structure of structures" indexed by the domain and codomain types. By defining operations for applying a matrix to a vector and solving the corresponding preservation equations algebraically, standard matrix multiplication arises naturally as a consequence.
Elliott highlights a structural perspective on matrices built entirely from the three operations already introduced:
1. **$1 \times 1$ Matrices:** Represented purely as primitive `scale` operations.
2. **Vertical Juxtaposition:** Stacking matrices that share the same width corresponds directly to `fork` (sharing a domain).
3. **Horizontal Juxtaposition:** Placing matrices side-by-side that share the same height corresponds directly to `join` (sharing a codomain).
Under this lens, type constraints naturally enforce dimensionality requirements: matrices can only be stacked vertically if their domains align, and horizontally if their codomains align. Using matrices directly guarantees that data representations are maintained without expensive sampling steps, setting the stage for evaluating reverse-mode derivative representations.
> “If you think about matrices, every matrix is either a one by one, which means it's scaling, or it's a horizontal or vertical juxtaposition of matrices. That's not how I was taught to think about matrices but I think is a very nice way.” — Conal Elliott
[01:08:27](https://www.youtube.com/watch?v=ne99laPUxN4&t=4107s) Matrix Associativity and Compile-Time Optimization
Elliott raises a fundamental question: if linear compositions are implemented via matrix multiplication, why is matrix multiplication associative? Rather than plodding through a tedious, algebraic coordinate proof, he argues that associativity holds by construction: “Matrix multiplication is associative because function composition is associative and matrix multiplication correctly implements function composition, when the functions are linear.” Viewing matrix multiplication as the solution to implementing composition of linear maps means its associativity naturally flows from the original problem definition.
```mermaid
flowchart LR
accTitle: "Matrix Multiplications and Tree Re-Association"
accDescr: "Shows how static type dimensions allow the compiler to re-associate matrix products for efficiency."
subgraph UserLevel ["Programmer Representation"]
Source["Modular Composition<br/>(Clarity-focused)"]
end
However, associativity introduces a major operational challenge: different parenthesizations yield radically divergent computational performance. Elliott insists this burden should never fall on the programmer, who must focus strictly on clarity and modularity. In a statically typed language, vector dimensions are encoded within the types themselves, giving the compiler access to all necessary dimensions ahead of time. Because multiplication cost depends entirely on matrix dimensions rather than runtime values, the compiler can perform optimal parenthesization at compile time—using dynamic programming ($O(n^3)$) or faster $O(n \log n)$ algorithms—completely avoiding runtime overhead.
- Right-associating the composition chain corresponds to forward-mode automatic differentiation.
- Left-associating the composition chain corresponds to reverse-mode automatic differentiation.
- For high-dimensional input domains and low-dimensional codomains (typical in machine learning loss functions where inputs number in the millions), reverse-mode AD is overwhelmingly more efficient.
[01:12:41](https://www.youtube.com/watch?v=ne99laPUxN4&t=4361s) Continuation-Passing Style and Reverse-Mode AD
Assuming the ultimate codomain is one-dimensional (or very low-dimensional), Elliott notes that complete left-association is universally recognized in machine learning as the optimal strategy, matching backpropagation. To guarantee automatic left-association regardless of how an expression was written, he adopts a continuation-passing style (CPS) representation. A morphism from $a$ to $b$ is represented indirectly as a transformer: given a consumer of $b$, produce a consumer of $a$. Formally, an arrow $f \colon a \to b$ is interpreted as a function that composes with $f$ on the right and accepts a consumer of the result on the left.
Elliott stresses a dramatic, often overlooked computational advantage of this CPS transformation: in high-dimensional settings, computing explicit intermediate derivative matrices produces enormous, quadratically large representations. These intermediate representations are frequently sparse—often identity matrices or even pure zero matrices. Composing directly with incoming continuations bypasses explicit matrix allocation altogether, collapsing vast operations into tiny, efficient computations.
```mermaid
flowchart LR
accTitle: "Continuation Category Transformation"
accDescr: "Mapping a linear map into a continuation category consumer."
- Transforming linear maps into a continuation category guarantees full left-association of compositions by design.
- Computation begins simply by supplying the identity continuation at the outer boundary.
- Zero matrices represent the maximum sparsity case, while identity matrices have a non-zero density proportional to the square root of the total elements.
- Bypassing the construction of sparse intermediate matrices prevents enormous quantities of wasted compute.
[01:15:13](https://www.youtube.com/watch?v=ne99laPUxN4&t=4513s) The Continuation Category and Reverse-Mode Without Tears
When an audience member reminds him that only fifteen minutes remain and that time must be reserved for questions, Elliott reassures the room that the punchline is imminent. He introduces the formal continuation category, parameterized over an underlying category (such as linear maps or matrices) and an ultimate codomain result type $r$. Setting up an algebraic functor equation requiring the continuation constructor to preserve structure across the standard category laws yields the concrete implementation of reverse-mode automatic differentiation.
Elliott contrasts this pure categorical result with standard computer science treatments: “Literature talks about graphs and talks about mutations, partial derivatives, none of that is necessary.” Instead, reverse-mode AD emerges purely as the general AD category instantiated with continuation-transformed matrices. Remarking on the simplicity of the construction, Elliott quips, “Every time I read a paper on reverse-mode AD, I want to cry,” citing that visceral reaction as the motivation for his paper's quest to make reverse AD clean, declarative, and elegant. He transitions to the final trick needed to obtain classical backpropagation: specializing linear transformations from an $n$-dimensional vector space into its base one-dimensional scalar field.
[01:17:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=4672s) Duality, Continuation Representations, and Transposition
Conal Elliott delves into the duality properties of linear algebra to construct reverse-mode automatic differentiation. When the codomain of a linear map is the underlying scalar field itself, a linear function from a vector space $U$ to that scalar field is known as a dual vector. In linear algebra, this duality manifests concretely as matrix transposition. When vector space $U$ is finite-dimensional, the space of all linear maps from $U$ to the scalar field is isomorphic to $U$ itself. Every such linear map can be expressed simply as the dot product with a fixed vector, waiting for its second argument.
This observation serves as the foundation for the continuation representation. Starting with linear maps from $A$ to $B$, applying the continuation transformation produces functions mapping consumers of $B$ to consumers of $A$ (linear consumers). Because linear consumers of $B$ and $A$ to the scalar field $S$ are isomorphic to $B$ and $A$ directly, this continuation form can be simplified into functions mapping from $B$ back to $A$. Elliott states that a simple specification relating continuations to duals allows the formulation of an algebra problem with five equations. Solving these equations yields the complete implementation of a dual category:
```mermaid
flowchart LR
accTitle: Dual Category Mappings
accDescr: Mapping between standard categorical operations and their dual counterparts under reverse-mode AD.
subgraph Primal["Primal Operations"]
id1["Identity"]
comp1["Composition (g ∘ f)"]
ex1["Extractors (exl, exr)"]
inj1["Injectors (inl, inr)"]
f1["Fork (△)"]
j1["Join (▽)"]
sc1["Scale (s)"]
end
subgraph Dual["Dual Counterparts"]
id2["Identity"]
comp2["Flipped Composition (f ∘ g)"]
inj2["Injectors"]
ex2["Extractors"]
j2["Join"]
f2["Fork"]
sc2["Scale (s)"]
end
id1 <--> id2
comp1 <--> comp2
ex1 <--> inj2
inj1 <--> ex2
f1 <--> j2
j1 <--> f2
sc1 <--> sc2
```
In this dual category, identity maps to identity, composition maps to flipped composition, extractors become injectors, injectors become extractors, fork becomes join, join becomes fork, and scaling is dual to itself. Interpreting fork, join, and scale as primitive matrix-building operations reveals that this dual construction is precisely matrix transposition. Elliott delivers the core takeaway for reverse-mode automatic differentiation: “So, here's backpropagation. So, no mutations, no variables, no graphs, no partial derivatives. It's just the general AD where we use the dual of additive functions, and no matrix compositions here.”
- Finite-dimensional linear maps from $U$ to scalars are isomorphic to $U$ via dot products.
- Reverse-mode AD is realized as generalized AD instantiated with the dual category of linear/additive functions.
- The construction eliminates graphs, tapes, variables, partial derivatives, and matrix-matrix multiplications.
[01:20:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=4822s) Why Scaling is Its Own Dual
An audience member asks why the dual of scaling is scaling itself rather than its reciprocal: “Why was the dual of scale to scale?” Elliott clarifies that duality is fundamentally different from inversion; inversion would indeed require dividing by the scalar, but duality behaves differently. Another audience member chimes in, suggesting that it makes sense when thinking of transposition.
Elliott acknowledges this perspective, noting that if one views a scalar multiplication as a 1×1 matrix, taking its transpose simply yields the matrix itself. However, Elliott expresses dissatisfaction with relying on matrix transposition as the primary conceptual foundation:
> “Transposition is about duality, not duality is about transposition.”
Elliott argues that explaining the behavior via 1×1 matrices leaves unaddressed why transposition was used in the first place or what it truly represents in linear algebra. The deeper motivation comes directly from duality and the continuation representations; matrix transposition is merely a concrete downstream consequence of duality, not its underlying cause.
[01:21:16](https://www.youtube.com/watch?v=ne99laPUxN4&t=4876s) Dual Numbers and the Flaws of Standard Forward-Mode AD
A participant asks how Elliott's categorical framework relates to the familiar formulation of automatic differentiation over commutative rings of dual numbers over $\mathbb{R}$, suggesting that Elliott's fork operation seems equivalent to appending a dual component to a function. Elliott agrees that dual numbers represent pairs containing a value and its derivative, which mirrors his original derivative type pairing a value with a linear map. Dual numbers provide a convenient way to implement forward-mode AD using operator overloading in traditional programming languages. However, Elliott points out two significant problems with the conventional dual numbers approach:
1. **Lack of generality:** Restricting representations to pairs of scalars limits the formulation strictly to scalar-to-scalar functions, preventing a unified treatment of higher-dimensional spaces.
2. **A semantic and type-theoretic flaw:** Standard forward-mode AD functions map from dual numbers to dual numbers ($(\mathbb{R} \times \mathbb{R}) \to (\mathbb{R} \times \mathbb{R})$). This type allows the output value to depend on the input derivative, an operation that is mathematically nonsensical in differentiation.
> “If you look at forward-mode, usually is you end up taking functions from dual numbers to dual numbers. A value and derivative to a new value and derivative. But that transformation of a number to derivative to a number derivative, only some of them are sensible. Because the value out cannot depend on the derivative in, and yet the types of it can. So that to me is a fundamental flaw in this whole idea of dual numbers and the whole way that forward-mode AD [is done].”
Elliott explains that standard implementations are only correct because programmers manually exercise extreme caution not to let output values depend on input perturbations. By contrast, refactoring the type signature so that a single value input yields a pair containing the output value and a linear map from delta-in to delta-out ($\Delta_{\text{in}} \to \Delta_{\text{out}}$) guarantees by construction that the primal value output can never depend on the input perturbation. Elliott shares that he only realized this flaw after trying to implement forward-mode differentiation himself and analyzing how the two modes formally relate.
[01:23:54](https://www.youtube.com/watch?v=ne99laPUxN4&t=5034s) Decoupling the Chain Rule from Differentiation Axioms
An audience member directs Elliott back to earlier slides showing Cartesian category axioms and the implementation of the differentiation functor $\hat{\mathcal{D}}$, asking from which categorical axiom the Leibniz rule (product rule) is derived. Elliott clarifies that the Leibniz rule belongs to the numeric category rather than the base Cartesian category.
Elliott laments how differential calculus, symbolic differentiation, and automatic differentiation are conventionally taught and practiced. Standard calculus textbooks state rules such as $\frac{d}{dx}(\sin u) = \cos u \cdot u'$ or $(uv)' = u'v + v'u$. In all of these standard presentations, the chain rule is baked into every individual differentiation rule. Elliott argues that combining rules in this manner introduces unnecessary complexity:
> “Every one of those rules has the chain rule embedded in it. Every one of those rules is the chain rule plus another rule. So, by using this categorical approach we said no, the derivative of sine is cosine, plus we have the chain rule. So, we don't need to have these kind of complicated rules, every one of which has the chain rule embedded in it.”
By isolating primitive mathematical operations (such as declaring the derivative of $\sin$ to simply be $\cos$) and handling function composition purely through the categorical chain rule, the entire system becomes strictly orthogonal and clean.
[01:25:39](https://www.youtube.com/watch?v=ne99laPUxN4&t=5139s) Hardware Compilation and Dynamically Reconfigurable FPGAs
When asked whether these theoretical insights have been applied to optimize circuits, Elliott explains that hardware compilation was the original motivation for his entire line of research. He describes a GHC (Glasgow Haskell Compiler) plugin he created. The plugin intercepts GHC's internal typed lambda calculus representation (Core), converts ordinary Haskell code into an abstract categorical representation, and instantiates that representation over chosen categories, such as differentiable functions or hardware circuits. Optimization is handled via generic rewrite rules written in GHC's rewrite-rule sublanguage, meaning optimizations apply uniformly across all categorical targets.
Elliott explains that the motivation originated during his time working at a hardware startup developing dynamically reconfigurable computing devices:
- Traditional FPGAs are reconfigured infrequently (e.g., “like once a year”).
- The hardware Elliott worked on could reconfigure itself at runtime at full operational clock speed: 2 billion times per second (2 GHz).
- Dynamic reconfiguration enables massive runtime optimizations.
- The company's business model initially focused on high-throughput packet processing for networking routers, such as real-time deep-packet inspection for network viruses.
- Moving to runtime-reconfigurable hardware allowed them to emulate complex three-dimensional circuit layouts, which are far more compact and efficient than static two-dimensional silicon circuits.
[01:27:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=5272s) Dynamic Reconfigurability and the Spacetime FPGA Architecture
Conal Elliott concludes by revealing the origin story behind his categorical compiler framework. The motivation did not start with automatic differentiation at all, but rather with an ambitious hardware engineering challenge: making three-dimensional field-programmable gate arrays (FPGAs). Three-dimensional circuits are inherently far more efficient than two-dimensional ones because the dominant cost in computation—both in power dissipation and time latency—stems from moving electrons across physical distances. In three dimensions, physical interconnect paths can be substantially shorter than in a flat plane. However, fabricating true physical 3D silicon chips is extraordinarily difficult.
Elliott recounts meeting Steve Teig, the visionary founder behind the architecture, and being immediately captivated by Teig's breakthrough concept. Rather than physically stacking silicon layers, Teig realized that the third dimension could be created dynamically over time through ultra-fast reconfiguration, creating an architecture dubbed "Spacetime." This architecture drew directly upon Hermann Minkowski’s mathematical formulation of spacetime used in relativity. With billions of operations occurring simultaneously, the hardware was designed to perform massively parallel computation on an unprecedented scale.
Because standard imperative programming languages carry an inescapable sequential bias, programming such a device required a paradigm shift. Purely functional programming, free from mutable state and forced execution ordering, offered an ideal solution. Elliott took on the challenge of compiling a pure functional language directly onto this dynamically reconfigurable hardware. As he explains Teig's core insight and his own fascination with it:
> “He realized that I can implement a three-dimensional FPGA by implementing one dimension in time instead of space.”
- Three-dimensional circuit geometry dramatically reduces electron travel distance, slashing energy consumption and propagation delay relative to two-dimensional planar chips.
- Dynamic reconfigurability realizes the third spatial dimension virtually by cycling through configurations across time steps, grounded in Minkowski's spacetime geometry.
- Sequential programming languages inherently fight massively parallel architectures that target billions of concurrent operations per second, whereas purely functional languages avoid sequential bias naturally.
---
[01:29:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=5362s) Compiling Functional Code to Hardware and the Epiphany for Automatic Differentiation
To bridge high-level functional code and massively parallel silicon, Elliott leveraged a foundational insight from 1980 establishing the equivalence between typed lambda calculus and Cartesian closed categories. Because Haskell compiles down in the Glasgow Haskell Compiler (GHC) to GHC Core—a tiny, robust dialect of typed lambda calculus—Elliott realized he could build a compiler plugin that translates that lambda calculus directly into categorical operations. Instead of instantiating the category with standard computable functions, the compiler targets a category of circuits, enabling the direct synthesis of graph representations and Verilog hardware descriptions.
During the development of this hardware-synthesis pipeline, Elliott had an unexpected realization. Having worked on automatic differentiation years earlier, he saw that the exact same categorical abstraction was not merely an idiosyncratic trick for compiling circuits, but rather an exceptionally clean, rigorous foundation for computing derivatives. By varying the target category from hardware circuits to dual spaces and linear maps, the framework elegantly derives both forward-mode and reverse-mode automatic differentiation without the messy state, graph tapes, or mutation found in conventional machine-learning frameworks. Elliott brings the lecture to a close on this unifying note before opening the floor to discussions.
> “Then, I remembered, wow, this 1980 result that says the typed lambda calculus is equivalent to this vocabulary, and Haskell is equivalent to the typed lambda calculus.”
```mermaid
flowchart LR
accTitle: Categorical Compilation Pipeline
accDescr: Flow diagram showing how Haskell source code is transformed via GHC Core into categorical primitives and reinterpreted as hardware circuits or automatic differentiation.
- The compiler converts GHC Core's typed lambda calculus into category-theoretic combinators based on well-established categorical semantics.
- By changing the semantic interpretation of the categorical vocabulary, the same compiler pipeline generates massively parallel FPGA hardware circuits or computes automatic differentiation.
- The categorical foundation eliminates the need for tapes, computational graphs, and mutable state in automatic differentiation, delivering correct-by-construction derivatives directly from source code.
- Conal Elliott concludes the talk with a brief wrap-up, offering to stay and answer questions offline.
## Notable quotes
> [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) What I'm really saying is this, automatic differentiation is symbolic differentiation performed by a compiler. — Conal Elliott
> [01:08:27](https://www.youtube.com/watch?v=ne99laPUxN4&t=4107s) Matrix multiplication is associative because function composition is associative and matrix multiplication correctly implements function composition, when the functions are linear. — Conal Elliott
> [01:20:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=4822s) Transposition is about duality, not duality is about transposition. — Conal Elliott
> [10:50](https://www.youtube.com/watch?v=ne99laPUxN4&t=650s) So, when I say the derivative of a linear function is itself everywhere, all I'm saying is that linear functions are their own perfect linear approximations. — Conal Elliott
## Mentioned
Conal Elliott, Daan Leijen, Microsoft Research, Target, Michael Spivak, Calculus on Manifolds, Haskell, Joachim Lambek, The Simple Essence of Automatic Differentiation, TensorFlow, Fortran, Glasgow Haskell Compiler (GHC), GHC Core, Verilog, Steve Teig, Hermann Minkowski, Cartesian closed categories
## Video description
Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Commonly used RAD algorithms such as backpropagation, however, are complex and stateful, hindering deep understanding, improvement, and parallel execution. This paper develops a simple, generalized AD algorithm calculated from a simple, natural specification. The general algorithm is then specialized by varying the representation of derivatives. In particular, applying well-known constructions to a naive representation yields two RAD algorithms that are far simpler than previously known. In contrast to commonly used RAD implementations, the algorithms defined here involve no graphs, tapes, variables, partial derivatives, or mutation. They are inherently parallel-friendly, correct by construction, and usable directly from an existing programming language with no need for new data types or programming style, thanks to use of an AD-agnostic compiler plugin.
See more at https://www.microsoft.com/en-us/research/video/the-simple-essence-of-automatic-differentiation/
## Background
本讲座由微软研究院（Microsoft Research）于 2018 年 7 月 26 日在 YouTube 平台发布，演讲者为知名计算机科学家 Conal Elliott。视频简介指出，反向模式自动微分（RAD）虽是深度学习和大规模优化的核心，但现存算法（如反向传播）复杂且具有状态性，而本报告提出了一种从简洁规范推导出的广义自动微分算法，无需图、磁带、可变状态或偏导数即可原生支持并行并保证构造正确性。
## TL;DR
Conal Elliott 在演讲中彻底解构了传统微积分与机器学习中对导数的拼凑理解，回归流形微积分的本质——将导数统一视作线性变换。通过将导数计算与原函数值绑定以恢复组合性，他利用范畴论与笛卡尔闭范畴（CCC）的结构保全性质，将一个直观但不可计算的数学规范严密推导为可执行的高效算法。进一步地，通过引入延续传递风格（CPS）与对偶范畴，他证明了深度学习中被奉为圭臬的反向传播算法，本质上不过是该通用框架在可加函数对偶范畴下的自然特例，从而彻底剥除了计算图、磁带和内存突变等历史包袱。
## Atmosphere & style
整场讲座兼具学术思辨的严密与反叛教条的锋芒，Conal Elliott 操着沉稳而幽默的语调，以一种举重若轻的姿态带领听众层层拨开深度学习文献的迷雾。现场互动极具学术交锋感，听众频繁插话追问理论细节，而 Conal 总是能以更底层的数学公理与哲学思辨给予透彻回应。演讲从纯粹数学美学出发，中途直击工业界计算图思维的狭隘，最终出人意料地收束于 2 GHz 动态重构时空 FPGA 硬件的工程渊源，带给观众一种豁然开朗、直击事物本质的智力震撼。
## Bulletin
- [01:42](https://www.youtube.com/watch?v=ne99laPUxN4&t=102s) Conal Elliott 提出导数的本质并非标量、矩阵或张量，而是不同向量空间之间的线性变换，所有特定维度的微分规则与乘法本质上都是线性映射的复合。
- [09:25](https://www.youtube.com/watch?v=ne99laPUxN4&t=565s) 传统链式法则因依赖原函数求值而缺乏组合性；通过在微分算子中同时返回原值与导数线性映射，求导被形式化为保持范畴与笛卡尔结构的严谨代数函子。
- [01:15:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=4528s) 通过引入延续传递风格（CPS）与线性代数对偶性，反向模式自动微分（RAD / Backpropagation）无需图、磁带、突变变量或偏导数即可被严谨推导与实现。
- [01:25:39](https://www.youtube.com/watch?v=ne99laPUxN4&t=5139s) 该算法源于将 Haskell 纯函数式程序通过 GHC Core 插件直接编译到 2 GHz 动态重构时空 FPGA 电路时的理论副产物。
## Key takeaways
- [01:42](https://www.youtube.com/watch?v=ne99laPUxN4&t=102s) 传统微积分教学将导数割裂为数字、向量、协向量、雅可比矩阵与张量，实际上导数的统一定义是定义域切空间到陪域切空间的局部线性变换。
- [07:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=448s) 链式法则的本质是线性变换的复合，但纯导数计算本身不具备组合性（Non-compositional），因为复合求导依赖前驱函数在输入点处的原始求值结果。
- [09:25](https://www.youtube.com/watch?v=ne99laPUxN4&t=565s) 将求导签名扩充为同时产生原函数值与导数线性映射（$a \to (b, a \multimap b)$），可以彻底闭环数据依赖并恢复严格的代数组合性。
- [10:50](https://www.youtube.com/watch?v=ne99laPUxN4&t=650s) 线性函数的导数在任意点处均为其自身，标量导数 1 的数学本质是恒等线性映射，多维中的单位矩阵也是恒等函数的具体表示。
- [18:51](https://www.youtube.com/watch?v=ne99laPUxN4&t=1131s) 自动微分算法可严格形式化为从函数范畴到可微函数范畴的笛卡尔函子，只需满足保持恒等、复合、左投影、右投影与分叉等 5 个代数方程即可求解实现。
- [31:40](https://www.youtube.com/watch?v=ne99laPUxN4&t=1900s) 基于 1980 年 Joachim Lambek 确立的理论，类型化 Lambda 演算与笛卡尔闭范畴（CCC）等价，使得纯函数式程序能够被编译器自动重写为范畴组合子表达。
- [36:01](https://www.youtube.com/watch?v=ne99laPUxN4&t=2161s) Elliott 尖锐批判了深度学习领域将自动微分与计算图、有状态磁带绑定的教条，指出微分关乎函数而非图论，图只是可视化结果而非计算手段。
- [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) 在编译器视角下，自动微分本质上是由编译器执行的高效符号微分，借助编译期的公共子表达式消除与局部绑定即可彻底避免传统符号求导的表达式爆炸。
- [55:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=3318s) 推导出的自动微分结构完全参数化于底层的笛卡尔范畴，线性映射的数值表示可以被任意满足范畴公理的具体结构平滑替代。
- [01:02:33](https://www.youtube.com/watch?v=ne99laPUxN4&t=3753s) 用黑盒函数表示线性映射在高维优化中存在严重基底采样灾难（需 $n$ 次前向传播）；而矩阵可通过 scale（$1 \times 1$）、fork（垂直堆叠）与 join（水平拼接）代数化重构。
- [01:08:27](https://www.youtube.com/watch?v=ne99laPUxN4&t=4107s) 矩阵乘法的结合律源自函数复合的结合律，矩阵向右结合对应前向模式自动微分，向左结合对应反向模式自动微分，最优结合策略可在编译期基于类型维度静态推导。
- [01:12:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=4348s) 引入延续传递风格（CPS）可将计算强制重结合为完全向左的形式，同时能在计算中自动跳过高维中间稀疏矩阵的显式构造。
- [01:17:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=4672s) 反向传播算法的数学本质是通用自动微分特化在可加函数的对偶范畴上，复合反转、分叉与合并对偶、提取与注入对偶，完全规避了传统反向传播的繁冗机制。
- [01:21:16](https://www.youtube.com/watch?v=ne99laPUxN4&t=4876s) 传统前向模式 AD 中对偶数类型 $(x, \Delta x) \to (y, \Delta y)$ 存在允许输出依赖微分扰动的类型漏洞，而范畴化模型从静态类型上杜绝了这一非因果依赖。
- [01:27:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=5272s) 整套范畴论自动微分框架源于将 Haskell 编译到基于闵可夫斯基时空架构的 2 GHz 动态可重构 FPGA 电路编译器项目的理论延伸与迁移。
## Detailed walkthrough
### [00:04](https://www.youtube.com/watch?v=ne99laPUxN4&t=4s) 开场介绍：从函数式响应动画到自动微分的本质
微软研究院的 Daan Leijen 主持了本场演讲，并向观众隆重介绍了演讲者 Conal Elliott。Conal 曾于 1994 年至 2002 年在微软研究院图形学组（Graphics Group）工作，目前是 Target 的杰出科学家（Distinguished Scientist）。Daan 回忆道，自己在读博士时就深受 Conal 早期工作的启发，尤其是关于函数式响应式动画（Functional Reactive Animation, FRAN）的研究。Daan 指出：“Conal 的拿手好戏就是把极其复杂的事物抽丝剥茧——在那个年代，动画总是充斥着矩阵、帧序列和定时器，而他用一种优美的方式重构了这一切，将动画的本质概括为时间的函数。”Daan 认为，Conal 在本次关于自动微分（Automatic Differentiation, AD）与机器学习的工作中再次施展了同样的本领：当下的领域充斥着各种让人眼花缭乱的复杂概念，遮蔽了事物的本质，而本次演讲旨在拨开迷雾，厘清核心。
Conal Elliott 接过话筒，幽默地表示自 2002 年离开微软研究院后，这是他第一次回到这里做技术报告。他首先明确了主题：自动微分大致来说就是自动计算导数的技术。既然要讲自动微分，最核心的起点就必须回答一个根本问题：究竟什么是导数？Conal 强调：“如果我们不知道导数意味着什么，那么想要对自动微分给出一个清晰、严谨且富有洞察力的解释，就是痴人说梦。”
### [01:42](https://www.youtube.com/watch?v=ne99laPUxN4&t=102s) 传统微积分教学的拼凑概念 vs 统一定义
Conal 带领听众回顾了标准微积分教学中的演进路径。对于大多数人（包括 Conal 自己在高中的微积分课程）来说，最初学到的导数概念是一个标量数字（Number），表示在某一点处函数输出随输入变化的增长比率（斜率）。然而随着学习深入，这个定义开始不断打补丁：
- 当函数的输出变为多维时，导数不再是标量，而变成了向量（Vector）；
- 当函数的输入变为多维而输出为标量时，导数变成了另一种向量（即余向量/协向量 Co-vector）。这两种向量在传统计算中常被混为一谈，导致了软件中大量的混淆与 Bug，但它们在数学意义上截然不同；
- 当函数的定义域和值域同时是高维空间时，导数变成了由偏导数构成的雅可比矩阵（Jacobian Matrix）；
- 如果进一步考虑二阶及更高阶的导数（导数的导数），维度将进一步攀升，演变为高维张量（Tensor）。
更糟糕的是，每出现一种新的导数表示形式，教材就会引入一套专属的链式法则（Chain Rule）。Conal 直言，这种四处缝补、零散割裂的教学体系，对于微积分初学者、计算机科学家以及软件工程师而言都是一场灾难。为此必须推倒重来，寻找一个大一统的本质视角。Conal 提出：“不要再说函数的导数是一个数字、一个向量、一个协向量、一个矩阵或某种高维怪兽；这里有一个普适、优美且统一的说法——导数就是一个线性变换（Linear Transformation）。”这才是关于导数的真正全局视角。
```mermaid
flowchart TD
accTitle: 传统导数表象与统一定义对比
accDescr: 对比传统微积分中碎片化的导数表现形式与Spivak提出的统一定义——线性变换。
subgraph Frag["碎片化的传统表示（各自定义与特定规则）"]
S["标量数字 (Scalar)"]
V["向量 (Vector)"]
CV["协向量 (Co-vector)"]
M["雅可比矩阵 (Jacobian Matrix)"]
T["高维张量 (Higher-order Tensor)"]
end
subgraph Unified["数学本质与统一抽象"]
LT["线性变换 (Linear Transformation)<br/>D(f)(a): a ⊸ b"]
end
Frag -.->|"本质均为不同空间上的"| Unified
```
### [04:00](https://www.youtube.com/watch?v=ne99laPUxN4&t=240s) 严谨表述：导数作为线性变换与复合的链式法则
Conal 引入了带有 Haskell 风格的类型签名与数学记号来严格形式化微分算子 $D$：
- 若原始函数为 $f: a \to b$；
- 那么微分操作 $D$ 的类型为 $(a \to b) \to (a \to (a \multimap b))$，即它接受一个函数，返回一个新函数，该函数接收输入点 $a$，并产生一个从输入切空间到输出切空间的线性变换（记为 $a \multimap b$）。
导数的通用严格定义来自于微积分分析中的局部线性逼近：当输入在点 $a$ 处扰动 $\epsilon$ 时，$f(a + \epsilon) \approx f(a) + D(f)(a)(\epsilon)$，当 $\epsilon \to 0$ 时二者的误差是高于一阶的无穷小。该定义适用于任意维度的向量空间乃至无穷维空间（只需存在极限）。Conal 提到，这个优雅的视角是他本科时在 Michael Spivak 1965 年的名著《流形上的微积分》（*Calculus on Manifolds*）中学到的，他盛赞该书是一部直击微分本质的经典之作。
既然导数的本质是线性变换，那么所谓标量乘法、点积（Dot Product）、外积（Outer Product）以及矩阵乘法（Matrix Multiplication），本质上全都是同一种操作在特定表示下的体现：**线性映射的复合（Composition of Linear Maps）**。通用的链式法则只有唯一一条：复合函数的导数等于各自导数线性变换的复合：
$$D(g \circ f)(a) = D(g)(f(a)) \circ D(f)(a)$$
现场听众提问澄清：通常我们得到的或者用来实现线性映射的是矩阵等具体表示？Conal 给予了肯定回答，并进一步强调了类型安全与抽象的威力。如果仅停留在矩阵层面，线性代数库中充满着非类型安全的操作（例如必须手动保证左矩阵的列数等于右矩阵的行数）；但若在类型系统级别将导数建模为线性变换，编译器的类型系统就会自动静态保证维度的正确性。更关键的是：“通过对导数进行抽象讨论（这也是本讲座的核心），我们可以打破常规，探索全新的表示形式，而不是死守矩阵表示——因为矩阵表示虽然被普遍采用，但事实证明它其实是个糟糕的主意。”
- 导数类型签名：$D: (a \to b) \to (a \to (a \multimap b))$
- 线性逼近定义：$f(a + \epsilon) = f(a) + D(f)(a)(\epsilon) + o(\epsilon)$
- 统一条目：所有特定维度的导数形式与乘积法则，均是线性变换及其复合的具体表示。
### [07:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=448s) 两种复合：串行链式法则的非组合性问题
除了用于串行串联的顺序复合（Sequential Composition，即函数嵌套 $g \circ f$），Conal 指出了另一种在程序与数学中同等关键的形式：并行复合（Parallel Composition，或称为分叉 Fork）。
- 顺序复合要求前者的输出类型匹配后者的输入类型，其核心在于数据依赖（Data Dependencies）；
- 并行复合则接受相同的输入 $a$，同时供给给两个不同函数 $f: a \to c$ 与 $g: a \to d$，生成一对结果：
$$(f \bigtriangleup g)(a) = (f(a), g(a))$$
Conal 特别澄清，这里的“并行”是指语义层面的无数据依赖（Semantic parallelism），并非局限于运行时的物理并行执行（尽管它天生利于并行硬件执行）。传统的自动微分或符号微分文献常宣称“一切全关乎链式法则”，Conal 纠正了这一误区：链式法则只管得了顺序复合，处理并行复合时往往极其笨拙，而将串行复合与并行复合统一纳入框架，能带来巨大的简洁性与推导能力。
最后，Conal 回到顺序复合的链式法则并指出一个对算法实现极为不利的致命弱点：**链式法则本身不是组合式的（Non-compositional）**。在计算机科学中，如果一个操作是组合式的，意味着计算复合结构的结果只需要直接递归调用子结构的操作并予以合并。然而观察链式法则公式：
$$D(g \circ f)(a) = D(g)(f(a)) \circ D(f)(a)$$
计算 $g$ 的导数不仅需要 $g$ 本身，还必须依赖 $f$ 在 $a$ 处的原始求值结果 $f(a)$。这意味着微分算子无法单纯通过组合 $D(g)$ 与 $D(f)$ 完成，必须将求值与求导纠缠在一起。这一结构性矛盾正是后续重新推导自动微分算法的关键伏笔。
### [09:25](https://www.youtube.com/watch?v=ne99laPUxN4&t=565s) 链式法则的组合性修复：保留原函数值
如果仅计算函数的导数，复合函数求导时会遇到严重的结构性障碍。Conal Elliott 指出，在对复合函数 $g \circ f$ 求导时，根据微积分链式法则，结果不仅涉及 $f$ 和 $g$ 的导数，还必须用到 $f$ 本身在输入点处的输出值。这种对“原函数值”的额外依赖，导致单纯求导的运算在代数推理与程序实现上无法做到优雅的组合（compositional）。
```mermaid
flowchart LR
accTitle: Compositional Differentiation Pipeline
accDescr: 增强型导数规范在输入 a 后同时产生函数值 b 与线性导数映射，使得复合求导具备组合性。
subgraph D_f["增强型求导 D(f)"]
InA["输入 a"] --> F_eval["求值 f(a)"]
InA --> D_eval["求导 D(f)(a)"]
F_eval --> OutB["输出值 b"]
D_eval --> LinMap["线性映射 (a -> b)"]
end
subgraph D_g["增强型求导 D(g)"]
OutB --> G_eval["求值 g(b)"]
OutB --> G_eval_D["求导 D(g)(b)"]
G_eval --> OutC["输出值 c"]
G_eval_D --> LinMapG["线性映射 (b -> c)"]
end
LinMap --> Chain["线性组合 (Compose)"]
LinMapG --> Chain
Chain --> OutLin["最终导数 (a -> c)"]
```
Conal Elliott 提出了一个极为简洁的修复方案：不要仅仅计算导数，而是让求导运算在输入参数 $a$ 时，同时返回原函数计算出的值 $b$ 以及对应的导数。现场听众随即追问确认：“你的意思是右侧的 $b$ 与上面那个函数算出来的 $b$ 是同一个吗？”Conal Elliott 明确证实了这一点。只要利用叉积操作符（fork operator）将原函数与导函数绑定在一起，复合求导的输入与输出依赖就完全闭环了。Conal Elliott 总结道：“This one fix makes differentiation compositional, and automatic differentiation does this.”（正是这一项修正让微分具备了组合性，所有的自动微分也正是这么做的。）
### [10:50](https://www.youtube.com/watch?v=ne99laPUxN4&t=650s) 线性函数的局部逼近与自身导数
从流形上的微积分（calculus on manifolds）以及将导数视为线性映射的角度审视，会得出一个极其优美的数学结论：**线性函数的导数在任何点都是其自身**。Conal Elliott 解释说，这听起来可能有点反直觉，但从本质上讲，一阶微分的核心就在于“局部线性逼近”。切线在切点处是完全精确的线性逼近，随着远离切点误差会逐渐增大；而高阶导数（如结合一阶与二阶导数）给出的则是二次逼近。由于微分追求的就是线性逼近，而线性函数自身就是自身完美的线性逼近，因此其导数自然就是该函数本身。
人们在日常计算中其实早已不自觉地运用了这一规律，只是习惯了标量视角。例如微积分中 $x$ 对 $x$ 的导数是 $1$，$2x$ 对 $x$ 的导数是 $2$。标量求导得出的“$1$”，其数学本质并非孤立的数字 $1$，而是“乘以 $1$ 的线性变换”，也就是恒等函数（identity function）。在多维空间中，这一导数则体现为对角线上全为 $1$、其余全为 $0$ 的单位矩阵（identity matrix），单位矩阵正是恒等函数的一种具体表示。同理，提取数据对（pair）中第一个或第二个元素的投影函数也是线性函数，它们的导数同样处处是它们自身。因此，对任意线性函数 $f$，在点 $a$ 处的增强求导结果就是对 $(f(a), f)$ 的直接打包。
### [13:06](https://www.youtube.com/watch?v=ne99laPUxN4&t=786s) 剥除历史包袱：反向模式自动微分的本质
掌握了基元操作（加法、乘法、正弦、余弦等）的已知导数，再加上线性函数的特性，剩下的工作就只有串联复合与并联组合。Conal Elliott 强调，自动微分的全貌实际上已经展现在眼前。然而在机器学习和主流文献中，尤其是被广泛使用的反向模式自动微分（Reverse-mode AD / RAD），往往被描述得异常复杂。
Conal Elliott 剖析了这种复杂性的根源：反向模式最初在 20 世纪 50 或 60 年代被提出，后来被机器学习领域以“反向传播”（backpropagation）的名义重新发明。但该领域的再发现缺乏严密、清晰的数学规范与推导传统，从而积累了大量历史遗留的偶然包袱（accidental baggage）——诸如显式的计算图、磁带（tapes）、有状态变量以及人工层（layers）。如果彻底剥除这些历史包袱，自动微分的核心概念其实非常纯粹：
- 基础微积分中的简单基元算子及其导数映射；
- 线性函数的自反性；
- 串行与并行组合规则。
### [14:15](https://www.youtube.com/watch?v=ne99laPUxN4&t=855s) 抽象代数结构：范畴与笛卡尔范畴接口
为了将上述纯粹的数学思想在代码中进行优雅的封装，Conal Elliott 引入了源自 20 世纪 50 年代代数学的范畴论（Category Theory）工具，并向在座听众保证无需具备深厚的范畴论背景。范畴的核心在于提供了一套泛化函数概念的抽象接口：
1. **对象与态射**：类似函数的结构，具有定义域（domain）与陪域（codomain）；
2. **基本操作**：包含恒等映射（identity）以及能将 $a \to b$ 与 $b \to c$ 串接为 $a \to c$ 的复合操作（composition）；
3. **代数公理**：满足复合的结合律，以及恒等映射作为左右单位元。
进一步地，针对需要处理数据对（pairs/products）的场景，接口被特化为**笛卡尔范畴**（Cartesian category）。它引入了三个关键操作：提取左侧元素（extract left）、提取右侧元素（extract right）以及将两个共享相同定义域的态射合流为一个输出为数据对的叉积操作（fork）。在自动微分中，由于要处理的并不是普通意义上的函数，而是“不仅计算原值还能计算导数的函数”，将这套通用的代数接口实例化到可微函数类型上便水到渠成。
### [17:23](https://www.youtube.com/watch?v=ne99laPUxN4&t=1043s) 可微函数类型 D 与规范的非可计算性
在具体实现层面，Conal Elliott 展示了对应的 Haskell 类型定义与增强规范。定义一个抽象包装类型 `D a b`，用来表示从类型 $a$ 到 $b$ 的可微函数。它的底层结构就是一个函数：接收输入 $a$，返回输出值 $b$ 与一个代表导数的线性映射（linear map from $a$ to $b$）所组成的对：
```haskell
-- 可微函数的抽象类型表示
newtype D a b = D (a -> (b, a:-* b))
-- 增强型求导规范（非直接可计算）
dHat:: (a -> b) -> D a b
dHat f = D (\a -> (f a, derivative f a))
```
在展示该规范（`dHat`）时，Conal Elliott 抛出了一个深刻的计算理论论断：“I want to emphasize here, the specification is not computable.”（我在这里想强调的是，这个规范是不可计算的。）对于给定的任意可计算函数，即使在数学意义上处处连续且处处可微，要在算法层面上构造出它的导数在一般情况下是不可计算的（non-computable）。整个研究最引人入胜之处，正是从这样一个极度简洁但不可计算的数学公理规范出发，通过一系列严密的推导与程序代数变换，最终计算出一个极其简单、完全可执行且完全并行的自动微分算法。
### [18:51](https://www.youtube.com/watch?v=ne99laPUxN4&t=1131s) 自动微分的范畴论规范：从不可计算到可高效执行
Conal Elliott 阐明了整个研究的核心方法论：将一个极其简单直观但“不可计算”的规范，直接转换为一个不仅计算效率极高、而且可以完全自动化的实现。为了实现自动微分（Automatic Differentiation, AD），代码被组织为若干抽象类型类的实例（如范畴 `Category`、笛卡尔范畴 `Cartesian`，以及包含正弦、余弦等基础运算的运算类）。
```mermaid
flowchart LR
accTitle: Specification to Executable Implementation Pipeline
accDescr: Pipeline showing the specification defined as a Cartesian functor transformed into a computable and automatable AD implementation.
subgraph Spec["范畴论规范"]
S1["D̂: 不可计算的语义定义"]
S2["保持范畴与笛卡尔结构<br/>（5 个结构代数方程）"]
S1 --> S2
end
subgraph Transformation["代数推导与内联"]
T1["利用链式法则、Fork 法则与线性性质代数求解"]
end
subgraph Impl["可执行实现"]
I1["可微分函数范畴 (D)"]
I2["高效且完全可自动化执行"]
I1 --> I2
end
Spec --> Transformation --> Impl
```
这个规范的核心命题在于：不可计算的导数语义映射函数 $\hat{\mathcal{D}}$ 严格保持了范畴结构（Category Structure）与笛卡尔结构（Cartesian Structure）。这体现在五个极其对称的方程上（两个来自范畴接口，三个来自笛卡尔接口）：
1. **恒等映射保持**：$\hat{\mathcal{D}}(\text{id}) = \text{id}$
2. **复合运算保持**：$\hat{\mathcal{D}}(g \circ f) = \hat{\mathcal{D}}(g) \circ \hat{\mathcal{D}}(f)$
3. **左投影保持**：$\hat{\mathcal{D}}(\text{exl}) = \text{exl}$
4. **右投影保持**：$\hat{\mathcal{D}}(\text{exr}) = \text{exr}$
5. **分叉算子保持**：$\hat{\mathcal{D}}(f \mathbin{\triangledown} g) = \hat{\mathcal{D}}(f) \mathbin{\triangledown} \hat{\mathcal{D}}(g)$
在方程右侧，所有的运算均作用在可微分函数范畴 $\mathcal{D}$ 上，例如右侧的 $\text{id}$ 是既能计算函数原值又能计算导数的“可微分恒等函数”。现场有听众立刻敏锐地指出：“所以 $\hat{\mathcal{D}}$ 是一个函子（functor）？”Conal 赞同并解释道：“是的，它是一个笛卡尔函子（Cartesian functor）。”更广泛地讲，它是定义在这些结构词汇（恒等、复合、提取、分叉）上的同态（homomorphism），表明导数计算能够沿着程序的代数结构完美分配。Conal 强调这种形式的优美性：
> “任何关于‘当我复合这两样东西时到底意味着什么’的直觉，都被这五个要求精确而优雅地捕捉了下来。”
### [22:03](https://www.youtube.com/watch?v=ne99laPUxN4&t=1323s) 代数求解方程：推导运算实现与乘法的莱布尼茨法则
将这五个规范方程作为代数问题进行求解，其具体推导过程载于论文《The Simple Essence of Automatic Differentiation》中。求解过程自然利用了链式法则（Chain Rule）、分叉法则（Fork Rule）以及线性函数自身处处即为导数的线性性质，再配合加法、取反等基本微分算子，便可导出具体的操作性实现。
在复合运算的实现中，函数值与导数是同步计算的：对输入 $a$，计算 $f(a)$ 得到中间值 $b$ 及其导数 $f'$；接着将 $b$ 传入 $g$，得到最终结果 $c$ 及其导数 $g'$。最终的导数由两个局部导数复合而成，这在本质上就是链式法则的程序内联体现。对于分叉运算（Fork），两路计算之间由于没有数据依赖，它们的导数和原值完全是独立并行计算后再进行合并。
```mermaid
flowchart TD
accTitle: Differentiable Composition and Product Rule
accDescr: Operational dataflow for composing differentiable functions and evaluating the Leibniz product rule for multiplication.
subgraph Composition["可微分复合运算: (g ∘ f)(a)"]
A["输入 a"] --> F["计算 f(a)"]
F -->|"中间值 b"| G["计算 g(b)"]
F -->|"局部导数 df"| Comp["导数复合: dg ∘ df (链式法则)"]
G -->|"局部导数 dg"| Comp
G -->|"最终结果 c"| Out["输出 (c, 导数)"]
Comp --> Out
end
subgraph MultRule["乘法 (非线性) 的导数: d(a * b)"]
InP["输入增量: (Δa, Δb)"] --> L["线性映射: b * Δa + a * Δb"]
L -->|"莱布尼茨乘积法则"| DOut["乘法微分结果"]
end
```
对于基础算子，取反（negation）与加法（addition）由于属于线性映射，其导数形式非常简单；而乘法（multiplication）是非线性的，因此需要特殊处理。在点 $(a, b)$ 处的乘法运算，除了产生原值积外，其微分是一个线性映射（linear map）：该线性映射接收扰动增量 $(\Delta a, \Delta b)$，并返回 $b \cdot \Delta a + a \cdot \Delta b$。Conal 指出，这正是微积分中的莱布尼茨法则（Leibniz rule）。
- **线性算子的通用微分**：若 $f$ 为线性函数，其可微分形式在输入 $a$ 处直接返回原值 $f(a)$，其导数部分恒为常量 $f$ 本身。
- **无数据依赖的分叉（Fork）**：由于分叉结构中子分支之间相互独立，其值与导数可解耦并行计算，具备天然的并行友好性。
- **乘法的微积分基础**：乘法在 $(a, b)$ 处的微分映射严格服从莱布尼茨法则，在 $\Delta a$ 和 $\Delta b$ 上保持线性。
### [24:57](https://www.youtube.com/watch?v=ne99laPUxN4&t=1497s) 线性映射的本质与自由定理（Free Theorems）的猜想
当有听众对乘法导数的定义和具体表示提出疑问时，Conal 剖析了“线性映射”的核心概念。线性映射最朴素的理解就是“恰好满足线性性质的函数”；因此在点 $(a, b)$ 处的导数本身就是一个接收 $(\Delta a, \Delta b)$ 的线性函数。关于如何表示线性映射，既存在常规表示（如矩阵），也有后续将详细探讨的非常规高效表示。
听众进一步追问，给出的这些满足规范方程的实例是否具有唯一性？在强类型的纯函数式编程中，特别是在参数多态（parametric polymorphism）的背景下，是否能仅凭类型签名推导出唯一的实现？Conal 解释道，参数化性质（parametricity）是一个非常深刻的理论性质，虽然这里的函数并非完全自由的多态（它们依赖于向量空间或模的代数结构，需要满足线性代数约束），但这并不排除存在某些受限条件下的“自由定理”（free theorems）。
> “整个推导过程对我而言有一种极其引人入胜的必然性，这也许正是一个线索，暗示着其背后确实隐藏着某种自由定理。”
Conal 坦言，这套推导在直觉上如此自然和不可避免，或许意味着背后的数学结构远比大家想象的要本质和简单。
### [28:07](https://www.youtube.com/watch?v=ne99laPUxN4&t=1687s) Haskell 示例：从平方到向量模长平方
Conal 切换到三个具体的 Haskell 运行示例，以此作为基准来评估这套朴素算法的性能表现，并为后续的性能优化做铺垫：
1. **平方函数 (`square`)**：
其定义为输入 $a$ 计算 $a \times a$，类型为 `Num a => a -> a`。Conal 幽默地解释了 Haskell 程序员常玩的一个双关把戏（pun）——将类型变量名和值变量名取成完全相同的符号 `a`，在概念上大家可以直接将其看作实数 $\mathbb{R}$。
2. **模长平方函数 (`magSqr`)**：
处理数对（pair）$a \times a$ 的输入，定义为分量平方之和（即 $x^2 + y^2$）。
这些极简的代码示例不仅展示了高级类型抽象在具体数学函数上的自然落地，同时也为后续讨论反向模式自动微分（Reverse-mode AD）的性能瓶颈与表示变换埋下了伏笔。
### [29:13](https://www.youtube.com/watch?v=ne99laPUxN4&t=1753s) 三个典型函数的标量与非标量维度结构
Conal Elliott 首先回顾了用于演示的三个示例函数。第一个最简单的平方函数（纯标量函数）；第二个是稍不平凡的示例：输入数对 $(a, b)$，分别计算 $a^2$ 与 $b^2$ 并相加（即模长平方函数）；第三个则是给定 $x$ 与 $y$，首先计算乘积 $z = x \times y$，接着同时计算并返回 $z$ 的余弦和正弦值 $(\cos z, \sin z)$。
Elliott 解释了挑选这三个例子的深意：它们以极其直观的方式覆盖了“标量”与“非标量”在定义域和陪域上的不同组合情况。第一个例子是纯标量输入输出；第二个例子的定义域是非标量的（输入二元组），陪域是标量；而第三个例子的定义域与陪域同时是非标量的。通过这三组对照，能够清晰展现微分机制在处理不同代数结构时的普适性。
- 纯标量函数：$\mathbb{R} \to \mathbb{R}$（如平方函数）
- 非标量定义域函数：$\mathbb{R} \times \mathbb{R} \to \mathbb{R}$（如数对平方和）
- 双非标量函数：$\mathbb{R} \times \mathbb{R} \to \mathbb{R} \times \mathbb{R}$（如二元积的余弦与正弦对）
---
### [29:48](https://www.youtube.com/watch?v=ne99laPUxN4&t=1788s) 范畴论与类型化 Lambda 演算的深刻统一
接下来是至关重要的大跨步：将普通的纯函数式程序重写为范畴词汇（Categorical Vocabulary）。Elliott 强调，在数学基础领域存在着一种极深的内在联系，它将范畴论、逻辑学（涵盖各种逻辑分支）以及计算理论紧密联结在一起。“At the heart of computation, reason in the foundation of mathematics are all the same thing.”（计算的核心、数学基础中的推理，本质上全都是同一回事。）
然而在主流命令式编程语言（如 C#、Java、甚至没有静态类型的 JavaScript）中，这种数学本质被层层噪声严重掩盖。唯有在优雅、纯粹且严格的类型化 Lambda 演算（Typed Lambda Calculus）中，这种对应关系才最为通透和显露。Haskell 归根结底就是包裹了语法糖的类型化 Lambda 演算。
```mermaid
flowchart LR
accTitle: 三位一体对应关系
accDescr: 逻辑、范畴论与计算之间的等价对应关系
subgraph Trinity["数学与计算的统一体系"]
L["逻辑学<br/>(Logics)"] --- C["计算理论 / 类型化演算<br/>(Computation / Typed Lambda)"]
C --- K["范畴论 / 笛卡尔闭范畴<br/>(Category Theory / CCC)"]
K --- L
end
```
---
### [31:40](https://www.youtube.com/watch?v=ne99laPUxN4&t=1900s) Joachim Lambek (1980) 成果与笛卡尔闭范畴（CCC）
Elliott 搬出了数学家 Joachim Lambek 在 1980 年做出的里程碑式结论：类型化 Lambda 演算不仅有“可计算函数”这一种程序员习以为常的解释模型，实际上存在着无数种与之相容的语义模型。只要一个数学模型满足笛卡尔闭范畴（Cartesian Closed Category, CCC）的公理结构，它就是类型化 Lambda 演算的一个完备且一致的解释：
- **范畴（Category）**：包含恒等态射（Identity）与态射复合（Composition）。
- **笛卡尔（Cartesian）**：拥有左/右投影（First / Second Projections, $\mathrm{exl} / \mathrm{exr}$）以及分叉配对操作（Fork / $\triangle$）。
- **闭（Closed）**：具备一等公民函数（First-class functions / 指数对象 / 柯里化与求值）。
这意味着纯函数式代码可以被编译器自动重写为纯范畴组合子词汇，随后赋予其非传统的数学解释。Elliott 强调，在他们的框架中，编译器自动完成这一降阶翻译，进而将其解释为“可微函数”（Differentiable Functions），这就是整套方案的核心底牌。
---
### [33:30](https://www.youtube.com/watch?v=ne99laPUxN4&t=2010s) 编译器内联与范畴表达式的直观构造
现场有听众提问：在将 Haskell 转换为范畴论形式时，幻灯片上的平方函数似乎被内联了，这种转换是否必须破坏原有的模块化边界？Elliott 澄清道，这绝非什么深层理论限制，纯粹是当前原型实现阶段的局限性。在未来更成熟的形式中，平方函数完全可以表达为独立的模块化态射，形式上写作与投影复合的形式（例如 $\mathrm{sq} \circ \mathrm{exl}$），从而保持代码的整洁与抽象。
Elliott 细致剖析了各个函数如何用范畴操作符搭建：
1. **平方函数（Square）**：利用恒等函数与自身的 Fork（$\mathrm{id} \triangle \mathrm{id}$）将输入值 $a$ 复制为 $(a, a)$，再与乘法态射复合（即乘法应用在复制值上）。
2. **模长平方函数（Sum of Squares）**：从二元组中通过左投影提取 $x$ 并复制平方（$x^2$），通过右投影提取 $y$ 并复制平方（$y^2$），两者以分叉组合并行执行，最终结果复合至加法态射。
3. **乘积的三角函数对**：先执行标量乘法，再并行执行余弦与正弦求值。
```mermaid
flowchart TD
accTitle: 模长平方的范畴计算流程
accDescr: 展示从输入对中分别提取元素、并行平方并求和的数据流图
subgraph Extract["提取与复制"]
IN["输入 (x, y)"] --> EXL["提取左侧: exl"]
IN --> EXR["提取右侧: exr"]
EXL --> DUP1["Fork 复制: (x, x)"]
EXR --> DUP2["Fork 复制: (y, y)"]
end
subgraph Compute["乘法与求和"]
DUP1 --> MUL1["乘法 (*) -> x^2"]
DUP2 --> MUL2["乘法 (*) -> y^2"]
MUL1 --> ADD["加法 (+)"]
MUL2 --> ADD
ADD --> OUT["输出: x^2 + y^2"]
end
```
Elliott 坦言，这套无点（point-free）范畴组合子是机器和数学家做形式化推理的绝佳语言，但让程序员肉手编写则是“一场灾难”。幸运的是，从人类友好的语言到这种严谨数学语言的重写过程完全由编译器自动化代劳。
---
### [36:01](https://www.youtube.com/watch?v=ne99laPUxN4&t=2161s) 语义多态与对“计算图”教条的批判
在展示了模长平方函数的范畴流图之后，Elliott 深入阐述了系统的“语义多态”（Semantic Polymorphism）。同一套范畴表达式，在系统中实际上横跨了多个不同的范畴解释：
- **普通计算范畴**：最平凡的数学函数或可计算函数。
- **语法打印范畴**：将组合与算子变成纯 AST 语法节点，用于美观打印代码。
- **图构建范畴**：将数据依赖关系生成为拓扑图，方便人类直观可视化并行结构。
- **可微范畴（Derivative Category）**：自动微分的实际承载者，执行前向与反向微分语义。
随后，Conal Elliott 抛出了整场演讲中最尖锐的一个论点，直击当时乃至现代机器学习界的核心假设：“Automatic differentiation is almost always talked about in terms of graphs, especially in Machine Learning, especially in reverse mode. I think that's always a mistake.”（自动微分几乎总是被拿来在图的层面上谈论，尤其是在机器学习和反向模式中。我认为这从头到尾都是个错误。）
Elliott 进一步论证道，微分是关于**函数**的数学，图论结构与微分的本质没有半点瓜葛。任何表现力丰富的编程接口或代数系统（包括孩童时期学到的四则运算 API），由于存在输出流向输入的组合关系，都可以被人在外部“具象化为一张图”。编译器后端或图论学者固然习惯从图的角度审视程序，但硬把自动微分的概念与图、磁带（tapes）或者图遍历绑定在一起，完全是概念层面的混淆。彻底摆脱对“图”的执念，正是该工作区别于几乎所有现有自动微分系统（如各类主流深度学习框架）的最根本特质。
### [039:18] 图可视化与平方函数的导数表示
Conal Elliott 首先明确界定了可视化与核心计算之间的界线。他提醒观众，虽然幻灯片中会出现很多图（graphs），但这绝对不意味着他在搞类似于 TensorFlow 之类严重依赖计算图的系统。Elliott 明确指出：“这些图纯粹用于可视化，它们与自动微分本身没有任何关系。即使我以图的形式向你们展示微分结果，那也是图在后、计算在前，这意味着它只是我向你们展示结果的一种手段，而不是计算导数的方法。”
接着，Elliott 给出了一个具体的平方函数求导示例。首先是在范畴语言中表示的简单平方表达式，以及对应计算过程的可视化图。当把该表达式放入可微函数范畴（category of differentiable functions）中进行语义解释，再将得到的内部函数表示转译为图时，结果由两部分组成：第一部分是原函数的输出，即输入 $a$ 经过乘法得到 $a^2$；第二部分则是一个绿色方框表示的线性函数。该线性函数接收一个微小增量（Elliott 记为 $da$，即微小的 $\Delta$），并输出 $a \times da \times 2$。
```mermaid
flowchart LR
accTitle: Differentiable Squaring Function
accDescr: Data flow of squaring function producing both function value and linear derivative map
subgraph Eval ["原函数计算"]
InA["a"] --> Square["a * a"]
Square --> OutVal["a²"]
end
subgraph Deriv ["导数线性映射"]
InDA["da"] --> Mult1["* a"]
Mult1 --> Mult2["* 2"]
Mult2 --> OutDA["2a · da"]
end
```
Elliott 借此澄清了一个常见的数学误区：通常人们习惯脱口而出“$a^2$ 的导数是 $2a$”，但在严格的线性映射视角下并非如此——导数实际上是将 $da$ 映射为 $2a \cdot da$ 的线性函数。“当我们在微积分里说 $a^2$ 的导数是 $2a$ 时，实际含义是‘乘以 $2a$’，因为导数是一个线性映射。”
### [041:19] 平方和示例与组合式求导的本质
Elliott 随后展示了一个更复杂的例子：两个变量的平方和计算 $a^2 + b^2$。在范畴化表达式并经可微函数范畴解释后，系统同样并行计算出两套结果：
1. 原函数的输出：分别计算 $a^2$ 和 $b^2$ 并将二者相加。
2. 线性导数映射：输入扰动向量 $(da, db)$，通过线性组合生成 $2a \cdot da + 2b \cdot db$。
在解释过程中，Elliott 看着图上的连线一度有些困惑，口误说成“$b \times b \times db$，这不对吧”，但随即恍然大悟并笑着修正：“没错！当然完全正确！我的大脑刚才短路了，图是正确的。”输入 $da$ 乘以 $a$ 再乘 2 得到 $2a \cdot da$，另一侧得到 $2b \cdot db$，最终相加即为整体的导数线性映射。
现场听众随即指出，这种设计其实“毫无魔法可言”，只需对像余弦、乘法这样的基元（primitives）定义好导数，剩下的就是各种组合。Elliott 对此深表赞同，并热情回应：“没错，完全没有魔法！我们只需要知道基元的导数，然后对于每一种组合形式——主要是顺序组合与并行组合这两种——知道如何组合这些可微函数，这就齐活了。这就是自动微分的全部内容。”Elliott 强调，这种简洁性与现有文献（特别是深度学习和高维优化领域所需的反向模式反向传播算法）中充斥的复杂性形成了鲜明反差。
### [043:24] 针对和类型（Sum Types）与断点的理论探讨
现场有听众提问：系统如何处理和类型（sum types，即不相交并集/tagged unions），特别是当程序中存在不连续点或条件分支时会发生什么？
Elliott 坦率承认这是一个极其深刻且有趣的问题。从最基础的数学层面来看，一旦引入和类型，函数通常就无法保持纯粹的连续性（除非平凡地永远只走左分支或右分支），因此“求导”这一概念本身的数学定义是否仍然有意义都要打上问号。Elliott 表示：“关于和类型，我思考过很久，我相信这背后应该有一个极其优雅的答案，但我目前还不知道那是什么。”
随后听众与 Elliott 展开了关于 Church 编码与和类型的延伸讨论：
- 和类型与积类型（products/pairs）在纯函数式理论中可以通过带有全称量化（universal quantification / rank-2 types）的函数进行 Church 编码。
- 听众指出 Church 编码在范畴论中对应于锥（cones），并且本质上是一种延续传递风格（continuation）。
- Elliott 指出，如果在引入和类型之前先对积类型做 Church 编码，探究可微性概念在 Church 编码下如何自然延伸，将是一个极具价值的研究方向；如果积类型能走通，和类型也很有希望。
- Elliott 进一步阐述了范畴论抽象的威力：“如果直接从机器学习或 AD 文献中描述的反向传播算法出发，我根本无从下手，我甚至无法理解那个算法到底是什么意思、它是否正确；但当我们把它还原到如此简单、坚实的范畴论地基上时，我们就能重新理性探讨这些边界问题——无论是 Church 编码、和类型，还是性能优化。”
### [046:43] 自动微分、符号微分与数值近似的边界
讨论转向了整个系统的工程与理论目标。听众提问：给定一个算术电路或数学函数的表示，系统的目标是否就是编译出正确且高效计算其导数的代码并进行优化？
Elliott 坚定地回答：“完全正确，这正是我的目标。”不过他随即澄清了一个关键的概念边界：
- 我们不能对“抽象的数学函数本身”进行计算求导，因为数学函数实体本身是不可计算的；我们处理的必须是“数学函数的某种表示（representation）”。
- 业内很多人倾向于使用“计算图（graphs）”作为表示，但 Elliott 认为相比于使用 $\lambda$ 演算并自动转译为范畴表达式，计算图是一个糟糕的选择。而将高级语言表达式自动转译为范畴表达式的步骤，本身是通用的，完全独立于微分机制。
接着有听众将该方案与符号微分（symbolic differentiation）以及传统的 Fortran 数值程序进行对比，指出它们的高层目标似乎是一致的。Elliott 分析了自动微分文献中常见的分类范式：
- 许多论文开篇常说在计算机上求导有三种方式：数值近似（差分法/割线法）、符号微分与自动微分。
- 数值近似通过在邻近的两点连线来估算斜率，但这种方法在数学上是不精确且容易产生数值误差的。
- Elliott 特别批判了简单将差分法归类为“数值（numeric）”的说法：“这种称呼很不妥当，因为自动微分本质上也是数值的。从某种角度看它是数值的，从另一种角度看它又是符号的。如果仅仅把第一种差分法叫做数值方法，而在区分 AD 与符号微分时说‘AD 是数值的，符号微分是符号式的’，这会带来极大的误导。”
### [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) 符号微分与自动微分之辨：编译器的本质视角
在探讨求导实现时，现场听众提出疑问：整套推导看起来完全是在摆弄符号，这难道不就是符号微分（Symbolic Differentiation）吗？Conal Elliott 指出这种观点在业界非常流行，虽然听上去符合事实，但本质上具有误导性。因为在编译器的世界里，所有的操作在编译期都必然是“符号化”的；只有到了运行期，人们才会将其视作数值计算。如果程序在运行期去操作数学表达式的结构，那属于运行期的符号处理；但编译器的核心职责就是对代码的抽象结构进行符号重写。因此，“代码是符号化的”并不能作为区分自动微分与传统符号微分的依据。
Conal Elliott 梳理了三种常见的求导途径：第一种是通过数值逼近（如割线法或有限差分法），这种方法不仅精度存在误差，在计算性能上更是极其低劣；第二种是传统意义上的符号微分，即编写一套程序去模拟高中微积分的规则，把数学表达式的抽象语法树进行规则替换（比如将 $\sin(u)$ 替换为 $\cos(u) \cdot du$）；第三种则是利用链式法则逐层传播的自动微分（Automatic Differentiation, AD）。针对后两者的分歧，Elliott 给出了一个犀利的反传统论断：“在我看来，自动微分就是由编译器执行的符号微分（Automatic differentiation is symbolic differentiation performed by a compiler）。”
文献中往往将二者截然对立，批评传统符号微分存在表达式爆炸等严重缺陷。但 Elliott 强调，所谓的缺陷只是因为以往的符号微分“实现得太烂”（doing things badly），而不是符号微分这一方法本身的过错。编译器本身极其擅长在符号层面做优化、公共子表达式消除与性能保持；通过利用编译器插件去完成求导规则重写，实际上是“哄骗”编译器替我们优雅、高效地完成了符号微分。对于听众提出“传统符号微分可能遇到不可导表达式无法求出”的顾虑，Elliott 解释两者面临相同的边界：一旦超出了系统已知的微分词汇表（Vocabulary），无论符号微分还是自动微分都会束手无策，两者在表达能力的限制上并没有本质不同。
---
### [52:36](https://www.youtube.com/watch?v=ne99laPUxN4&t=3156s) 原始值与导数的共享计算，以及告别“图与树”的思维陷阱
Conal Elliott 通过乘积的复合函数（$\sin$ 与 $\cos$ 的乘积运算）展示了第三个求导示例，重点剖析计算共享（Sharing of Computation）对求导效率的关键作用。在传统的纯导数计算中，链式法则表面上看似不是“复合结构”（not compositional），因为导数公式本身不仅依赖子函数的导数，还依赖子函数在当前输入点的原始计算值（Primal Value）。Conal Elliott 早期的一个核心洞见就是通过“扩充”函数定义——让求导计算同时返回函数的原始值与其导数——从而恢复了严格的范畴复合性（Compositionality）。
这种复合性带来的另一个巨大收获是效率：原始函数与导数之间通常包含大量重合的中间子表达式。将二者合并在同一个范畴规范中计算，使得编译器能够极其自然地识别并共享这些中间计算。传统符号微分之所以广受诟病，正是因为它缺乏计算共享机制，常常导致生成指数级膨胀的代码树，进而迫使系统在编译期或运行期消耗指数级的计算量去化简冗余运算。而在良好构建的编译器中，`let` 绑定与公共子表达式提取（Common Subexpression Elimination）是编译器的基本功，开发者完全无需手动干预即可坐享极致的共享优化。
```mermaid
flowchart TD
accTitle: Primal and Derivative Computation Sharing
accDescr: 展现同时返回原始值与导数如何促成编译器天然的计算共享与复合性
subgraph InputStage["输入与原始计算"]
X["输入 x"] --> P["计算原始值 (Primal) f(x)"]
X --> Shared["共享中间状态 (Shared Exprs)"]
end
subgraph DerivativeStage["导数计算"]
Shared --> D["计算线性导数 D f(x)"]
end
subgraph AugmentedResult["扩充结果对"]
P --> Pair["( f(x), D f(x))"]
D --> Pair
end
```
当听众提到编译器这种行为有助于将“树”（Tree）折叠为有向无环图（DAG）时，Elliott 随即告诫大家不要陷入图论的死胡同。他说：“如果从图的角度去思考，你就会陷入困境，觉得操纵树比操纵图更简单，可某些树又比图呈指数级庞大。”由于树无法表达引用共享，必须通过重复节点来表示相同子项，许多系统便引入复杂的图操作算法去把大树重构成具有更多共享的图，这不仅极其繁重而且容易滋生 bug。Elliott 直截了当地指出大家应该从源头掐断这种思维：“ differentiation has nothing to do with trees and graphs（微分与树或图根本没有半点关系）。”只要站在范畴论的高维代数视角，利用语言本身的局部绑定，完全不需要引入额外的图数据结构。
---
### [55:18](https://www.youtube.com/watch?v=ne99laPUxN4&t=3318s) 提取范畴代数模式：自动微分向任意笛卡尔范畴的推广
当 Elliott 审视通过求解五个同态方程（关于微分函子 $\hat{\mathcal{D}}$ 保结构性质的方程）推导出的 Haskell 代码时，一种强烈的代码美学模式引起了他的注意：
- 可微函数的恒等元（Identity），其导数正好对应于线性映射的恒等元；
- 可微函数的顺序复合（Composition），其导数的组合恰好是线性映射之间的顺序复合；
- 在笛卡尔范畴操作中，左提取元（`exl`）对应线性映射的左提取元，右提取元（`exr`）对应线性映射的右提取元，叉积配对（Fork / `&&&`）也严格对应线性映射的叉积操作。
```haskell
-- 范畴化可微函数的结构同态模式
id = D (id &&& const id)
(D f). (D g) = D (\x -> let (y, g') = g x
(z, f') = f y
in (z, f'. g'))
exl = D (exl &&& const exl)
exr = D (exr &&& const exr)
(D f) &&& (D g) = D (\x -> let (y, f') = f x
(z, g') = g x
in ((y, z), f' &&& g'))
```
这些定义中除了要求线性映射具备恒等元、顺序复合、投影与分叉操作并且满足范畴公理之外，**完全不需要了解线性映射的具体数值内部实现**。Conal Elliott 总结道：“线性映射几乎没有任何需要你提前了解的特殊属性，你唯一需要知道的，就是它们也构成了一个笛卡尔范畴（Linear maps, there's almost nothing you need to know about them. You need to know that they form a Cartesian category also）。”这就意味着，任何具有笛卡尔范畴特性的数学对象或函数式构造，都可以在理论上替代原本具体的“线性映射”，在自动微分体系中充当导数的角色。
基于这一纯粹源自数学审美的发现，Elliott 将最初写死的自动微分算法进行了深度的参数化泛化：
- 将具体的微分类型算子 $D$ 泛化为带有范畴参数的 $D_k$，其中下标 $k$ 可以是任意满足公理的笛卡尔范畴。
- 代码的核心逻辑保持原样，只在类型系统上做出区分：一组操作作用于原函数范畴（普通的变换函数），另一组平行操作则多态地作用于承载导数的范畴 $k$。
- 对于取反（`negate`）与加法（`add`）等本来就具备线性的原子操作，只需提取它们在目标范畴 $k$ 中的线性对应版本即可完成平滑迁移。这种推广为后续推导更高效的反向模式自动微分（RAD）埋下了至关重要的基石。
### [58:53](https://www.youtube.com/watch?v=ne99laPUxN4&t=3533s) 乘法的求导困境与余笛卡尔（Co-Cartesian）词汇的引入
Conal Elliott 首先指出了之前定义中的一个局限：乘法运算显得格外棘手且尴尬。先前写出的乘法导数形式 `\lambda (a, b). \lambda (da, db). b * da + a * db` 严重依赖普通函数的求值机制，其中的线性映射被直接写成了具体的函数闭包，而非适用于任意笛卡尔范畴的抽象箭头。为了摆脱对具体函数的依赖，Elliott 提出了两个核心的代数构建模式：其一是缩放（scaling），其二是将输入对拆分计算后再求和的操作。
乘法本身并非线性映射（它是双线性的，bi-linear），但只要固定其中一个参数，乘法关于另一个参数就变成了纯粹的线性映射。为此，Elliott 引入了两个词汇：
1. `scale u`：表示将输入参数乘以标量 $u$ 的线性映射。
2. `join`：笛卡尔范畴中 `fork`（接收同一个域的输入，将其分配给两个箭头并生成一对输出）的对偶（dual）操作。`join` 接收两个具有相同陪域（co-domain）的映射，接受一个输入对（pair），分别交给这两个映射处理，最后将两个结果相加。
凭借这套新词汇，乘法的导数表达式可以重构成极其紧凑的形式：“`\lambda (a, b). join (scale b) (scale a)`”。之所以 $b$ 在前，是因为微分展开式为 $b \cdot da + a \cdot db$。这一重构并没有凭空增加逻辑，却将原本写死在函数上的运算提升到了适用于更广范畴的“余笛卡尔”（co-Cartesian）词汇体系中。
```mermaid
flowchart LR
accTitle: Fork 与 Join 的对偶关系
accDescr: 对比展示 Fork（接收单一输入复制分发）与 Join（接收配对输入计算求和）的对偶数据流
subgraph ForkStage["Cartesian: fork f g"]
direction LR
InA["输入 x"] --> FA["f"]
InA --> GA["g"]
FA --> OutA1["f(x)"]
GA --> OutA2["g(x)"]
end
subgraph JoinStage["Co-Cartesian: join f g"]
direction LR
InB1["输入 da"] --> FB["f = scale b"]
InB2["输入 db"] --> GB["g = scale a"]
FB --> AddNode["+ (加法求和)"]
GB --> AddNode
AddNode --> OutB["b·da + a·db"]
end
```
- **余笛卡尔操作符族**：对应笛卡尔范畴中的两个投影提取器（left / right projections），余笛卡尔范畴引入了左注入与右注入（injections）。在函数表示下，左注入即在右侧补零，右注入即在左侧补零。
- **可加性上下文**：在线性变换的抽象表示中，所有涉及的类型都具有可加性（additive），底层的求和与合并操作正是在该代数约束下得以成立。
### [01:02:33](https://www.youtube.com/watch?v=ne99laPUxN4&t=3753s) 用函数表示线性映射的致命缺陷：高维基底采样的维度灾难
用普通函数来表示线性映射固然简单优美，但在工程实践中却面临一个严重的现实障碍：很多场景下，我们必须从线性映射中提取出显式的数据表示（如具体向量或矩阵）。Conal Elliott 举了两个典型例子：
1. **计算机图形学中的着色与光照**：在对 3D 表面上的某一点进行光照计算时，需要知道该点的法向量（normal vector），以便与光线或视线方向计算点积。法向量需要通过两个偏导数向量的外积（cross product）求得，这要求导数必须是实实在在的向量数据，而非一个只能调用的黑盒函数。
2. **机器学习与深度学习中的梯度下降**：在优化问题中，算法必须获得具体的梯度向量（gradient vector），以指明沿哪个方向更新参数去搜寻局部极小值。
要从一个已知为线性的黑盒函数中提取出紧凑的向量或雅可比矩阵（Jacobian matrix），唯一的通用做法是将其在标准基底上进行逐一采样（例如使用单位矩阵的各行/各列组成的独热向量 one-hot vectors 分别调用该函数），并将输出汇总成矩阵。Elliott 严厉地指出：在机器学习这类输入维度动辄数百万的领域，这种做法是绝对不可行的。“如果那个函数的定义域是高维的，比如说一百万维——在机器学习中这很常见——那么我就得构造一个一百万乘一百万的单位矩阵，得到一百万个独热向量，逐一灌入这个函数里；这会带来极度昂贵的二次方计算开销。”
在基于梯度的优化问题中，这种代价的不对称性显得尤为荒谬：目标的输出（陪域）往往仅仅是一维的标量标度（即 loss 或目标函数值），而输入的参数空间（定义域）却极其庞大。使用黑盒函数表示导数，导致转换成本完全被庞大的输入维度绑架。Elliott 强调：“如果我们做优化问题，尤其是当定义域是高维时，我们绝不会想用函数来作为表示，因为提取数据表示的代价实在太高了。”
- **采样开销**：对于 $n$ 维输入，采样雅可比矩阵需要对黑盒线性映射运行 $n$ 次前向传播（$n$ passes），每次传入一个独热向量（one-hot vector）。
- **优化任务的维度错配**：陪域维度极低（通常为 1），定义域维度极高（可达 $10^6$ 以上），使得基于输入基底的采样成为算法效率的灾难性瓶颈。
### [01:06:04](https://www.youtube.com/watch?v=ne99laPUxN4&t=3964s) 矩阵的代数解构：作为 Scale、Fork 与 Join 的几何拼接
既然从函数中提取矩阵成本太高，自然的解决方案就是“从一开始就使用矩阵，不要用函数来表示线性映射”。然而，Elliott 并没有采用传统线性代数教课书中的观点，而是提出了一种泛化的结构化视角：将矩阵视为由类型约束的“结构的结构”（a structure of structures），其行结构与列结构分别由陪域与定义域的类型决定。
当定义了矩阵应用于向量的运算，并要求该运算保持代数结构时，就形成了一组包含五个方程的代数问题，而矩阵乘法本身正是这个代数系统的自然解。Elliott 指出，任何矩阵本质上都可以通过先前建立的三个基础构件组合而成：
1. **$1 \times 1$ 矩阵**：本质上就是纯粹的标量缩放（`scale`）。
2. **矩阵的垂直堆叠（Vertical Juxtaposition）**：当两个矩阵宽度相同时，将它们上下堆叠，这在范畴论操作中精确对应于 `fork`（要求定义域相同）。
3. **矩阵的水平拼接（Horizontal Juxtaposition）**：当两个矩阵高度相同时，将它们左右拼接，这在范畴论操作中精确对应于 `join`（要求陪域相同）。
Elliott 评价道：“这不是当年别人教我理解矩阵的方式，但我认为这是一个非常漂亮的方式。”类型系统在此处扮演了严格的几何守护者：类型签名强行保证了只有宽度相同的矩阵才能做垂直堆叠（`fork` 保证相同输入域），只有高度相同的矩阵才能做水平拼接（`join` 保证相同输出陪域）。这使得矩阵的代数操作与范畴论构建完美契合，也为在自动微分系统中彻底替换导数的底层表示铺平了道路。
- **三元核心词汇映射**：
- `scale` $\Leftrightarrow 1 \times 1$ 基础标量运算单元
- `fork` $\Leftrightarrow$ 相同列宽矩阵的垂直拼接（输入复制分发）
- `join` $\Leftrightarrow$ 相同行高矩阵的水平拼接（输出加和合并）
- **类型安全**：矩阵拼接的几何合法性被严格编码在箭头的范畴类型特征之中，避免了维度不匹配的运行时错误。
### [01:08:27](https://www.youtube.com/watch?v=ne99laPUxN4&t=4107s) 矩阵乘法的结合律与结合顺序之谜
当自动微分系统里充斥着大量的矩阵乘法时，一个非常有趣的问题随之浮现：在范畴论中，凡是出现组合（composition）的地方，在线性映射的具象化下都是通过矩阵乘法来实现的。众所周知，矩阵乘法满足结合律，但究竟“为什么”它是结合的？Conal Elliott 指出，很多人会试图去写一长串代数展开式来进行机械证明，但他认为“那是吃力不讨好的笨办法”（"No, that's the hard way."）。从根本上说，矩阵乘法之所以满足结合律，纯粹是因为函数复合（function composition）本身具有结合律，而矩阵乘法在线性函数语义下，不过是对函数复合的正确实现而已。这种思考方式更加直接而本源：矩阵乘法并不是先凭空捏造出来然后再去验证结合律的运算，它最初的动机就是为了解决“如何正确表示并计算由矩阵所代表的线性函数的复合”，因此其结合律自然是由原始动机推导而出的必然属性。
虽然矩阵乘法在代数上是结合的，但运算的不同结合方式却会导致天壤之别（very different performance）的计算性能。如果系统依赖矩阵来表示导数，就必须极其巧妙地选择结合顺序。然而，Conal Elliott 前面展示的核心定义并没有偏向任何特定的线性映射组合方式——代码写成什么结构，系统就忠实地维持什么结构。如果完全指望程序员为了自动微分的效率去把组合顺序写成最优形式，这是极其错误的，因为程序员追求的目标是代码的清晰性与模块化，而“效率与模块化往往是背道而驰的”（“efficiency and modularity are at odds with each other.”）。因此，这项优化重任必须交给编译器，而非程序员。
```mermaid
flowchart LR
accTitle: Matrix Composition Re-association
accDescr: Demonstrating how different matrix association strategies affect computation in forward and reverse AD.
subgraph Input["原始程序表达"]
direction TB
P["程序员编写的组合<br/>(追求清晰性与模块化)"]
end
subgraph Compiler["编译期类型推导优化"]
direction TB
DP["动态规划 / O(n log n) 算法<br/>(仅依赖矩阵维度类型)"]
end
subgraph Strategies["结合策略分类"]
direction TB
FAD["向右结合 (Right-associated)<br/>前向模式 (Forward-mode AD)"]
RAD["向左结合 (Left-associated)<br/>反向模式 (Reverse-mode AD)"]
end
P --> Compiler
Compiler --> FAD
Compiler --> RAD
```
### [01:10:23](https://www.youtube.com/watch?v=ne99laPUxN4&t=4223s) 编译期重结合优化与反向模式的必然性
幸运的是，对于矩阵链乘的优化问题，学术界早有解法。我们可以利用动态规划算法在 $O(n^3)$ 时间内求得计算代价最小的最优结合方案，甚至还有更精妙的算法能在 $O(n \log n)$ 时间内完成。更关键的洞见在于：矩阵乘法的计算开销完全取决于矩阵的“维度”，而与矩阵的具体“数值”无关（除非考虑稀疏矩阵的特定零元素预测）。在强静态类型函数式语言的语境下，矩阵的维度信息本身就是类型系统的一部分。Conal Elliott 强调：“所以，我们可以在编译期而不是运行期完成最优的重结合，这是一个巨大的胜利。”（“So, we can do the optimal re-association at compile time, not at run-time, that's a huge win.”）。
在所有可能的结合方式中，有两种最典型的极端情况：
- **向右结合（Right-association）**：对应于**前向模式自动微分（Forward-mode AD）**。
- **向左结合（Left-association）**：对应于**反向模式自动微分（Reverse-mode AD）**。
对于任何基于梯度的优化任务（如当下的机器学习），反向模式 AD 的计算效率要远远胜出，其优势幅度取决于输入维度的规模——而在现代机器学习中，输入维度通常高达数百万维。Conal Elliott 提出，如果我们假定最终输出的目标类型（终极余域 codomain）是低维的，特别是当它只是一维标量（损失函数标量）时，那么向左结合（即反向模式）几乎就是普适的最优策略。这恰恰就是现代深度学习中反向传播算法（backpropagation）所做的事情。
### [01:12:28](https://www.youtube.com/watch?v=ne99laPUxN4&t=4348s) 延续传递风格（CPS）与稀疏矩阵的计算跳过
为了在不破坏程序员模块化代码的前提下自动获得完全向左结合的性质，Conal Elliott 引入了一种经典的函数式编程技术——**延续传递风格（Continuation Passing Style, CPS）**。其核心理念是：一个从类型 `a` 到 `b` 的映射，可以等价地表示为“如果给我一个消费 `b` 的方法，我就能给你一个消费 `a` 的方法”。这种表示法在信息上是完全无损且同构的双向转换。给定函数 $f$，我们将其解释为一个在其右侧复合 $f$、在其左侧接收针对结果 $b$ 的消费者（即延续 continuation）的结构。只要把这个机制打包进范畴结构中，不论原始代码的语法树是如何嵌套结合的，其内在表示都会被强制拉平成**完全向左结合**的形式，最后只需传入一个恒等延续（identity continuation）即可启动计算。
这种基于延续的抽象带来了巨大的性能红利。当计算高维输入输出函数的导数时，外积或直接雅可比矩阵的尺寸是二次方膨胀的，极耗内存。但实际上，内部生成的中间矩阵往往极其稀疏，甚至频繁出现全零矩阵（最稀疏的情况）或单位矩阵（非零元素数量仅为元素总数开平方的极度稀疏情况）。如果直接物化构造出这些中间矩阵，会产生极大的算力浪费。而通过将它们直接与传入的延续进行复合运算，系统能够彻底规避中间巨型稀疏矩阵的构建过程，直接将其化简为极小规模的计算。
### [01:15:13](https://www.youtube.com/watch?v=ne99laPUxN4&t=4513s) 延续范畴与“告别眼泪”的反向模式自动微分
在讲座剩余约 15 分钟时，会议主持提醒 Conal 注意时间并留出提问环节，Conal 欣然回应称这几张幻灯片正是整个研究的高潮所在（the punchline）。他正式展示了形式化的延续范畴（Continuation Category）：以底层范畴（`~>`）与最终结果类型 `r`（最终的标量余域）为参数，把延续概念打包封装。在这里，延续映射 `cont` 同样必须严格满足范畴态射的五个保结构方程。借助范畴同构解决代数问题后，得到的反向模式自动微分实现精炼得令人屏息。
Conal 对比了现有文献中的繁琐设计并感叹，在传统文献中，反向模式 AD 充斥着计算图、内存可变状态（mutations）、磁带（tapes）和偏导数符号，然而这些实际上全都不需要。反向模式 AD 所需的全部精髓，不过是一个完全通用的延续技巧，而这个技巧在标准函数库中随处可用，根本不应与微分引擎深度耦合。最终的反向模式 AD 范畴，仅仅是将通用的 AD 范畴参数化应用于“矩阵的延续变换版本”而已。Conal Elliott 幽默地总结道：“每次我读关于反向模式自动微分的论文时，我都想哭。所以我想这就是他们给这篇论文起名为《无泪反向模式 AD》的原因。”（“Every time I read a paper on reverse-mode AD, I want to cry. So I think that's how they came up with this title.”）。
- **延续范畴的参数化结构**：矩阵以标量为索引（`Matrices` indexed by scalar），延续范畴则以矩阵类型及终极目标类型 $r$ 为索引。
- **反向传播的本质特例**：在讲座的最后几分钟，Conal 开始揭示通往标准 Backprop 的最后一步蜕变——考虑从百万维向量空间映射到其底层一维标量域（scalar field）的线性变换，这也正是梯度计算的核心场景。
### [01:17:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=4672s) 线性代数对偶性、延续变体与反向传播的本质
当线性映射的目标空间（余定义域）退化为标量场本身时，从向量空间 $u$ 到标量的导数便被称为对偶向量（dual vector）。Conal Elliott 指出，在线性代数中存在着极其优美的对偶性质，人们通常将其具象化为矩阵转置（matrix transposition），但矩阵转置的底层灵魂完全是对偶性。在有限维向量空间中，所有结果落在标量场内的线性映射都与空间 $u$ 本身同构，这类映射的本质就是某个固定向量与第二个参数的内积（dot product）。
当把这种对偶性与延续（continuation）表示法结合时，便迎来了整个理论的高潮：原本从 $a$ 到 $b$ 的线性映射，经过延续变换后，转变为将“$b$ 的线性消费者”映射为“$a$ 的线性消费者”；由于在标量场下这些消费者分别同构于 $b$ 和 $a$ 本身，因此该延续形式可以直接表示为从 $b$ 到 $a$ 的函数。Conal Elliott 通过设定五个代数方程并求解，直接推导出了对偶范畴（dual category）的实现：恒等映射依然是恒等映射，函数复合转变为反转复合（flip composition），提取子（extractors）变成了注入子（injectors），注入子变成了提取子，分叉（fork）转为合并（join），合并转为分叉，而缩放（scale）操作的对偶仍然是缩放本身。Conal Elliott 总结道：“So, here's backpropagation. So, no mutations, no variables, no graphs, no partial derivatives.”（这就是反向传播。没有状态突变，没有变量，没有计算图，也没有偏导数。）它仅仅是通用自动微分在可加函数对偶范畴上的特化，完全避开了繁重的矩阵乘法组合，在计算上极其高效。
```mermaid
flowchart LR
accTitle: 对偶范畴映射对应关系
accDescr: 展示原范畴操作如何对偶转换到反向传播操作
subgraph Primal["原范畴操作 (a -> b)"]
direction TB
P_comp["复合 (g. f)"]
P_ext["提取子 (exl, exr)"]
P_inj["注入子 (inl, inr)"]
P_fork["分叉 (fork / △)"]
P_scale["缩放 (scale s)"]
end
subgraph Dual["对偶范畴 / 反向传播 (b -> a)"]
direction TB
D_comp["反转复合 (f*. g*)"]
D_ext["注入子 (转换为注入)"]
D_inj["提取子 (转换为提取)"]
D_fork["合并 (join / ▽)"]
D_scale["缩放自身 (scale s)"]
end
P_comp ==> D_comp
P_ext ==> D_inj
P_inj ==> D_ext
P_fork ==> D_fork
P_scale ==> D_scale
```
---
### [01:20:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=4822s) 缩放对偶与矩阵转置的哲学辩析
进入现场提问环节后，一位观众首先提出了疑问：“为什么 scale 的对偶还是 scale？”Conal 笑着回应称这确实很有趣，并澄清对偶并非求逆运算（inverse）。观众随之附和，认为这更类似于矩阵转置。Conal 承认，如果从矩阵的角度来看，$1 \times 1$ 矩阵的转置自然是其自身，但他对仅仅给出这种表层解释并不满意。
Conal Elliott 进一步剖析了线性代数教学中的本末倒置问题：“Transposition is about duality, not duality is about transposition.”（转置源于对偶，而不是对偶源于转置。）他强调，直接拿“$1 \times 1$ 矩阵转置不变”作为答案是一种逆向视角，它没有回答最根本的哲学问题：人们最初为什么要在数学中引入矩阵转置？转置在线性映射中到底代表什么意义？事实上，正是对偶性以及函数延续的构造逻辑，才从根本上赋予了矩阵转置数学合理性与现实动机。
- 对偶（Dual）关注的是线性消费者的反向传递，与代数中的乘法逆元（Inverse）完全是不同概念。
- 矩阵的转置操作之所以合理，本质上是对偶范畴中箭头反转与内外积变换在基底坐标下的具象投影。
---
### [01:21:16](https://www.youtube.com/watch?v=ne99laPUxN4&t=4876s) 对偶数陷阱与前向模式 AD 的类型缺陷
另一位观众随后将话题引向了经典自动微分领域，询问该理论与实数上的交换环对偶数（dual numbers over $\mathbb{R}$）之间的对应关系，并猜测讲座中的分叉（fork）操作是否等价于向函数追加一个对偶分量。Conal 确认了两者存在联系，指出前向模式自动微分通常在具有运算符重载的语言中非常易于实现，常见的做法就是将每个数值包装为一对数字：一个表示原值，另一个表示导数。
然而，Conal 话锋一转，严厉批评了主流前向模式自动微分在类型设计上的根本缺陷。常规实现要求函数直接接受对偶数并返回对偶数，即把“输入值与输入导数”转换为“输出值与输出导数”。然而在数学本质上，输出的函数原值绝不可能依赖于输入的微分扰动增量（$\Delta$），但对偶数的类型签名却完全允许甚至暗示了这种荒谬依赖的存在。Conal 犀利地指出，这种方式之所以没有频繁酿成灾难，完全是因为开发者个人编码时小心翼翼，从形式化类型系统的角度看它是不可靠的。若进行正确的代数重构，剥离“输出值对输入导数的依赖”，就会自然导出他所提出的表示法：函数接受一个输入值，产出一个输出值以及一个从输入扰动映射到输出扰动的独立线性函数。
- 传统对偶数类型：$(x, \Delta x) \to (y, \Delta y)$，类型层面未能阻止 $y$ 依赖 $\Delta x$。
- 正确的范畴化表示：$x \to (y, \Delta x \multimap \Delta y)$，从类型结构上严格保证了因果性与导数的线性本质。
---
### [01:23:54](https://www.youtube.com/watch?v=ne99laPUxN4&t=5034s) 链式法则与微积分教学的历史包袱
在探讨范畴公理时，观众询问笛卡尔范畴中关于 $\hat{\mathcal{D}}$ 函子的公理是否蕴含了莱布尼茨乘积法则（Leibniz rule）。Conal 说明这属于数值范畴的范畴，随后展开了对微积分传统教学方法的深刻反思。他认为，无论是在大学微积分课堂、传统的符号微分系统，还是现有的自动微分工具中，都普遍存在一种极具误导性的教学惯性。
他在微积分课程中学到的规则往往形如：“$\sin u$ 的导数是 $\cos u \cdot du$”或者“$uv$ 的导数是 $u'v + uv'$”。Conal 批评指出，这些规则全都把链式法则（Chain rule）生硬地内嵌到了每一个基本函数的导数定义之中，导致每条规则都在做“链式法则加特化规则”的复合计算。而在范畴论的视角下，这两者被干净利落地解耦：$\sin$ 的纯粹导数就是 $\cos$，乘法运算有其独立的导数形式，而复合则是通过统一、通用的链式法则来处理。这种正交性彻底摆脱了传统微积分中臃肿、重复且充满特殊情况的规则定义。
> “Every one of those rules has the Chain rule embedded in it. Every one of those rules is the Chain rule plus another rule.” —— Conal Elliott
---
### [01:25:39](https://www.youtube.com/watch?v=ne99laPUxN4&t=5139s) 硬件编译动机与 2 GHz 动态重构硬件
当观众问及这些数学洞见是否被用于优化电路或在实际编译器中落地时，Conal 兴奋地分享了这项研究的工程渊源。他编写了一个名为 GHC（Glasgow Haskell Compiler）插件的工具，能够在编译阶段截获 Haskell 的内部中间表示——有类型 Lambda 演算 Core，将其转化为纯粹的范畴形式，随后根据具体需求将其例化为任意目标范畴（例如可微函数范畴）。编译器中利用 Haskell 代码及其重写规则子语言（rewrite rules）实现的大量代数重写规则，对所有符合范畴公理的解释器（包括自动微分与硬件电路）均通体适用。
Conal 透露，这项研究最初的灵感其实完全来自于他多年前从事的硬件编译工作。当时他在一家硬件公司任职，任务是将 Haskell 代码直接编译成硬件电路。该公司拥有一种极为先进的动态可重构硬件：它类似于 FPGA，但不同于普通 FPGA 往往数月乃至一年才烧录重构一次，该芯片在运行时以 2 GHz（每秒 20 亿次）的时钟频率动态改变自身的内部逻辑布局。这种极高频的运行时硬件重构带来了巨大的性能收益，例如部署在路由器中实时检测网络数据包是否包含恶意病毒攻击。Conal 指出，在硬件合成领域，三维电路往往比传统的二维平面电路具备更高的效率优势，而基于范畴论的代数抽象恰好为这种高度动态的硬件生成与优化提供了坚不可摧的数学底座。
### [01:27:52](https://www.youtube.com/watch?v=ne99laPUxN4&t=5272s) 从三维时空 FPGA 架构到范畴论编译器的诞生
Conal Elliott 在演讲结尾揭示了这项研究最初的真实动机。三维电路在理论上远比二维电路高效，因为计算中消耗的大部分能量和时间都花在移动电子上；而在三维空间中，电子移动的物理路径要比二维短得多。然而，制造真正的物理三维 FPGA 极为困难。当时，Steve Teig 提出了一个绝妙的洞见：通过动态可重构性（Dynamic Reconfigurability），将其中一个空间维度用“时间”来实现。这种架构被称为“时空”（Space-Time）架构，严格建立在闵可夫斯基（Minkowski）为爱因斯坦狭义相对论所梳理的时空数学框架之上。Conal Elliott 坦言，当他听完这个构想后，几乎在 30 秒内就决定一定要与 Steve Teig 合作。当时抛给 Conal 的核心挑战是：面对这样一台旨在实现每秒万亿次、大规模并行计算的硬件，该如何对其进行编程？任何顺序执行的传统语言都会受到内在顺序偏见的严重制约，而纯函数式语言天然不受顺序执行模型的束缚。Conal 的任务正是将纯函数式程序直接编译到这种三维 FPGA 上。
为了解决纯函数式语言向硬件电路的编译问题，Conal 想到硬件工程师虽然不习惯用范畴论术语描述电路，但范畴论语言完全可以用来形式化地刻画硬件电路。结合 1980 年代确立的经典理论成果——带类型的 Lambda 演算（Typed Lambda Calculus）与笛卡尔闭范畴在语义上等价，而 Haskell 经过 GHC 编译后生成的核心中间表示（GHC Core）正是一种非常小巧的类型化 Lambda 演算，整个编译链路豁然开朗。Conal 设计的编译器插件拦截 GHC Core，将其转换为通用的范畴语言；接着，不再将其例化为常规的可计算函数，而是例化为大规模并行电路范畴（Category of Circuits），再将该范畴表示渲染为图结构，并最终生成 Verilog 硬件描述代码。正是在完成了这一套用于硬件综合的范畴编译器后，曾在自动微分（AD）领域有过研究的 Conal 突然顿悟，意识到这种范畴化方案恰恰也是重构自动微分的绝佳范式，从而催生了本次演讲所展示的全新自动微分算法。演讲至此圆满结束，Conal 随后向听众致谢并在掌声中结束了报告。
关于为何坚决摒弃顺序语言并采用纯函数式语言来驱动这种并行硬件，Conal Elliott 斩钉截铁地总结道：
> “It's not going to be in any sequential language, every sequential language is going to be deeply acknowledged because this is massively parallel, we want to be doing millions of operations simultaneously.”
```mermaid
flowchart LR
accTitle: Haskell到FPGA电路的范畴论编译流程
accDescr: 展示从纯函数式Haskell源码通过GHC Core转换为范畴论表示并最终生成Verilog的流程
subgraph Frontend["语言前端与中间表示"]
Haskell["Haskell 源码"] --> GHC["GHC 编译器"]
GHC --> Core["GHC Core<br/>(类型化 Lambda 演算)"]
end
subgraph Category["范畴化与特化"]
Core --> Cat["范畴语言表达<br/>(Categorical Vocabulary)"]
Cat --> Circuits["电路范畴例化<br/>(Category of Circuits)"]
end
subgraph Backend["硬件后端"]
Circuits --> Graph["电路图表示"]
Graph --> Verilog["Verilog 硬件代码"]
end
```
- **三维计算与物理极限**：计算功耗与延迟的主要物理瓶颈在于电子迁移的距离，三维电路路径极短，因而性能显著优于二维结构。
- **时空换维度**：Steve Teig 提出的核心创新在于利用动态可重构技术，以“时间”维度替换难以物理实现的第三个“空间”维度，打造时空架构 FPGA。
- **理论基石**：该架构深植于闵可夫斯基时空相对论数学，而编译器后端则结合了 1980 年确立的类型化 Lambda 演算与笛卡尔闭范畴的对应定理。
- **研究的副产物**：本场报告探讨的优雅自动微分算法并非孤立发明的产物，而是 Conal 将函数式语言编译到硬件电路这一长期探索过程中，将范畴论工具顺理成章迁移到自动微分领域所带来的突破性成果。
## Notable quotes
> [36:01](https://www.youtube.com/watch?v=ne99laPUxN4&t=2161s) Automatic differentiation is almost always talked about in terms of graphs, especially in Machine Learning, especially in reverse mode. I think that's always a mistake. — Conal Elliott
> [49:08](https://www.youtube.com/watch?v=ne99laPUxN4&t=2948s) 在我看来，自动微分就是由编译器执行的符号微分。 — Conal Elliott
> [00:04](https://www.youtube.com/watch?v=ne99laPUxN4&t=4s) 如果我们不知道导数意味着什么，那么想要对自动微分给出一个清晰、严谨且富有洞察力的解释，就是痴人说梦。 — Conal Elliott
> [01:20:22](https://www.youtube.com/watch?v=ne99laPUxN4&t=4822s) Transposition is about duality, not duality is about transposition. — Conal Elliott
## Mentioned
Conal Elliott, Daan Leijen, Steve Teig, Michael Spivak, Joachim Lambek, Microsoft Research, Target, Calculus on Manifolds, The Simple Essence of Automatic Differentiation, Haskell, GHC, Verilog, FPGA, TensorFlow
## Video description
Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Commonly used RAD algorithms such as backpropagation, however, are complex and stateful, hindering deep understanding, improvement, and parallel execution. This paper develops a simple, generalized AD algorithm calculated from a simple, natural specification. The general algorithm is then specialized by varying the representation of derivatives. In particular, applying well-known constructions to a naive representation yields two RAD algorithms that are far simpler than previously known. In contrast to commonly used RAD implementations, the algorithms defined here involve no graphs, tapes, variables, partial derivatives, or mutation. They are inherently parallel-friendly, correct by construction, and usable directly from an existing programming language with no need for new data types or programming style, thanks to use of an AD-agnostic compiler plugin.
See more at https://www.microsoft.com/en-us/research/video/the-simple-essence-of-automatic-differentiation/
[Source](https://www.youtube.com/watch?v=ne99laPUxN4)
Source quotes
[36:01] Conal Elliott: Automatic differentiation is almost always talked about in terms of graphs, especially in Machine Learning, especially in reverse mode. I think that's always a mistake.
[49:08] Conal Elliott: 在我看来，自动微分就是由编译器执行的符号微分。
[0:04] Conal Elliott: 如果我们不知道导数意味着什么，那么想要对自动微分给出一个清晰、严谨且富有洞察力的解释，就是痴人说梦。
[80:22] Conal Elliott: Transposition is about duality, not duality is about transposition.
Source quotes
[49:08] Conal Elliott: What I'm really saying is this, automatic differentiation is symbolic differentiation performed by a compiler.
[68:27] Conal Elliott: Matrix multiplication is associative because function composition is associative and matrix multiplication correctly implements function composition, when the functions are linear.
[80:22] Conal Elliott: Transposition is about duality, not duality is about transposition.
[10:50] Conal Elliott: So, when I say the derivative of a linear function is itself everywhere, all I'm saying is that linear functions are their own perfect linear approximations.
Original transcript
[0:04] >> I'm Daan and I'm honored
to host today Conal Elliott,
[0:09] former MSR colleague and
a good friend of mine.
[0:13] Conal used to work here at
Microsoft Research until 2002,
[0:18] and now he's a distinguished
scientist at the target.
[0:23] But the way he was here
at Microsoft research,
[0:26] I was so busy students and I
remember being so inspired
[0:29] by his beautiful work on
functional reactive animations,
[0:33] and at that time was really
inspirational to me.
[0:37] One thing that Conal is great at
[0:39] is taking something
really complicated.
[0:41] In that time like animations
you will always have
[0:43] matrixes and frames and timers,
[0:46] and he kind of rephrase
it in a beautiful way
[0:49] about the essence of animations
as functions of time.
[0:52] I think with this work he
applies the same trick again
[0:55] but now in terms of differentiation
and machine learning,
[0:59] it's always about
all these complicated things,
[1:01] and you almost don't
see the essence,
[1:03] and this talk will hopefully
shed some light on it.
[1:05] So, thanks a lot, Conal.
[1:07] >> Thanks, Don. It's
great to be here.
[1:09] Yes, I was at Microsoft Research
[1:11] in the graphics group from
[1:12] '94 to 2002, I had a good time.
[1:16] So, this is my first time
back giving a talk.
[1:19] So, anyway, we're
going to talk about
[1:21] automatic differentiation
which has
[1:25] to do roughly with computing
derivatives automatically.
[1:29] So, a good place to start
[1:30] would be a question,
what's a derivative?
[1:32] All right, this is like
the heart of the matter.
[1:34] If we don't know what this means
[1:35] what's kind of hopeless to have
[1:37] any clean rigorous
illuminating story
[1:40] about automatic differentiation.
[1:42] So, if you had
an education like me,
[1:45] you probably, let's say,
[1:47] I took calculus one in
high school and I learned
[1:49] a derivative of a function
at point is a number,
[1:52] and that number has to do
with the ratio of how fast
[1:55] the output of the
function is growing
[1:56] relative to the
input at that point.
[1:58] Sounds kind of calculus
one perspective.
[2:01] But a little later,
turns out well
[2:02] it might not be a number,
it might be a vector.
[2:04] So, if my function yields
a higher dimensional result,
[2:08] not a scaler, not
just like reals,
[2:10] we can get a vector out.
[2:12] But the function
could instead consume
[2:14] a higher dimensional
result in which case
[2:16] we get a different
kind of vector.
[2:18] These two are often not
[2:20] distinguish which
leads to all kinds of
[2:21] confusions and bugs in
[2:23] software but they're really
importantly different.
[2:25] They look alike but they mean
[2:26] radically different things
though, vector co-vector.
[2:28] Then, a little later,
[2:30] if we have higher-dimensional
domain and co-domain,
[2:32] input and output of function in
[2:33] which case we're
going to have to have
[2:35] a matrix of partial derivatives
[2:37] which is sometimes called
the Jacobian matrix.
[2:40] So, maybe we've arrived at
the fully general story here,
[2:43] a higher dimensional domain
and co-domain but,
[2:46] well, there are
higher derivatives.
[2:48] A higher derivative is
[2:49] a derivative of derivative
that's derivative two.
[2:51] So, higher derivative
is going to be even
[2:53] higher dimensional than two.
[2:54] For instance, so you get
these kind of arbitrarily
[2:56] high dimensional tensors column.
[2:59] So, anyway, and then,
[3:00] we have all these
different notions of
[3:02] derivatives and every
[3:03] one of those notions
has its own chain rule,
[3:05] they're all different
from each other.
[3:07] Of course, when you see
this many variations
[3:09] there probably going to be
other variations as well.
[3:11] So, we get a complicated
incomplete story,
[3:14] and this isn't going to go
well for a calculus student,
[3:17] it's not going to go well for
[3:18] computer scientitists
or software engineers.
[3:20] So, we need a better story.
So, let's start over.
[3:23] Instead of saying that
the derivative of a function is
[3:27] a number of vector co-vector
[3:28] matrix or some kind of
higher-dimensional beast,
[3:30] there's one general
beautiful unifying story
[3:33] which is the derivative is
a linear transformation.
[3:36] That's the general story.
[3:38] So, I'm gonna talk about D.
D is the differentiator.
[3:43] So, differentiation
is a function,
[3:46] I'm going show you some notation.
[3:48] If it's unfamiliar
or you're confused,
[3:50] Pauleen interrupt me and ask
[3:51] questions or about anything else.
[3:53] I enjoy interaction
during the talk,
[3:55] then they'll be time for
questions at the end as well.
[3:57] So, this is a bit
haskell in notation,
[4:00] so this means that D has
this as the following type.
[4:02] So, differentiation consumes
a function from a to b,
[4:06] and it yields a
function from a to
[4:07] linear transformations
from a to b.
[4:10] That's the general
notion of a derivative.
[4:12] All of these other notions are
[4:15] representations of linear maps.
[4:17] All of the chain rules are
[4:19] implementations of
the same thing which is,
[4:23] which I'll show on
the next slide.
[4:25] So, here's the general
definition of a derivative.
[4:29] Which is, we're going to
take a function f at a,
[4:32] and we're going to perturb
the input a little bit,
[4:35] and sample f but we're
also just going to take
[4:37] the result and perturb it
a little bit linearly.
[4:40] That's the D of F, is going to be
[4:41] a linear transformation
D, f, a is.
[4:43] So, we feed Epsilon in to
this linear transformation.
[4:47] So, this is the general
definition of derivative.
[4:49] Works for all dimensions,
[4:50] it works for things other than
[4:52] linear vector kinds of things.
[4:55] It just need to be vector spaces
[4:57] and a little bit
more limits have to exist.
[4:59] So, I learned perspective
as an undergrad
[5:02] from a book called
Calculus on Manifolds,
[5:04] Michael Spivak, 1965.
[5:06] It's a beautiful
little gem of a book.
[5:09] It gets right to the heart
[5:11] of what differentiation is about.
[5:13] Now, as I mentioned there were
[5:16] all these different
representations of derivatives,
[5:17] each of them have
their own chain rule.
[5:19] But really those chain rules
all mean the same thing.
[5:23] They all have some fun
with multiplication,
[5:26] you can multiply two
scalars together,
[5:28] you can multiply two vectors
[5:31] in one sense and you get a
[5:32] dot product in a different sense,
[5:33] you get what's called
the outer products
[5:34] of inner and outer products,
[5:36] or if they're matrices,
you get matrix products.
[5:38] But all of those
notions of products
[5:40] represent the same thing which is
[5:42] composition of linear maps.
[5:44] So, the one unifying
[5:46] general chain rule is
the following: It says,
[5:48] "The derivative of
a composition of two functions,
[5:50] g compose f at a is, well,
[5:53] we're gonna take
the derivative of f at a,
[5:55] and the derivative
of g at f of a,
[5:58] and fa, the derivative
of g at f of a,
[6:02] and I'm going to compose them.
[6:03] So, normally you would see
instead of composition,
[6:05] you'd see some kind of
multiplication here.
[6:07] But a multiplication
is there because
[6:10] it correctly implements
the composition.
[6:14] But the real one single story
is composition. Yes.
[6:17] >> Would you go one bit when
[6:19] you showed the linear function.
[6:22] >> Yes.
[6:22] >> That you're saying like,
[6:24] normally that's what you get
as a or we can implement
[6:28] linear met like a matrix
[6:31] or something representational
that's function.
[6:34] >> Yes, exactly. So, abstractly
[6:36] we have a linear
transformation from a to b,
[6:38] concretely, it might have
[6:39] a matrix that represents
the linear transformation.
[6:43] But the important thing is,
if you think in terms of
[6:45] representations,
is that a matrix?
[6:46] Is that a vector? Is
that this kind of vector
[6:48] or the other kind of
vector and so on?
[6:50] Normally like
linear algebra packages,
[6:52] software libraries will have
[6:54] some matrix package and it has
[6:56] all these unsafe operations,
[6:57] like you multiply two matrices
[6:59] and well, they have to conform,
[7:00] the width of one has to be the
[7:01] same as the height of
the other and so on,
[7:03] and the type systems usually
don't give that to you.
[7:04] But if you say linear
transformations,
[7:06] the type system gives
you the co-domain.
[7:08] You cannot have a
type correct program
[7:10] that tries to multiply
matrices that don't fit.
[7:13] For instance, moreover
by talking about
[7:15] it abstractly and this is
really key to this talk,
[7:18] we can innovate and use
different representations,
[7:20] not a matrix
representation because
[7:21] the matrix representation
actually turned
[7:23] out to be a bad idea even
[7:24] though it's just about
universally adopted.
[7:28] So, this form
[7:30] of competition is
sequential composition.
[7:33] But there's another kind which
is parallel composition.
[7:36] So, if you have two functions and
[7:38] the output of one
[7:40] matches the input
of the other you
[7:41] can sequentially compose them.
[7:42] But there's another form
which is you
[7:43] have two functions and they have
[7:44] the same domain and
have the same input.
[7:46] So, one takes you from a to c,
[7:48] the other takes you from
a to d. You can fuse
[7:50] those functions
together into one that
[7:52] gives you the pair of results.
[7:53] It's a very simple definition,
we call this fork.
[7:56] So, the fork of f and g
when you apply it to a,
[7:59] where you give a to
each of the functions
[8:00] and you pair up the results.
[8:02] So, logically, this is parallel.
[8:04] When I say parallel, I
don't mean operationally,
[8:05] I don't mean that
runs in parallel.
[8:07] It's a good idea for it to run in
[8:08] parallel but that's
a separate issue.
[8:10] I mean semantically, there's
no data dependencies.
[8:12] Where sequential composition is
[8:14] all about data dependencies,
[8:15] parallel composition
is free of them.
[8:17] So, these two forms of
competition are both important.
[8:20] It's something that the
differentiation, especially,
[8:23] automatic or symbolic
differentiation,
[8:25] it's said that these
[8:26] methods are all about
the chain rule.
[8:27] There not all about
the chain rule,
[8:28] the chain rule is only about
sequential composition.
[8:30] They have other
clumsy ways so they
[8:32] typically talk about
parallel composition.
[8:33] But we can talk about
them really elegantly
[8:35] in terms of this one notion,
[8:36] and we got a lot
of mileage out of
[8:38] making these kind of
single general definition.
[8:42] Just go back to sequential
composition, the chain rule,
[8:46] you probably learned in
[8:48] high school except in
this generalized form.
[8:51] So, the problem with
the chain rule,
[8:53] and if we're thinking about
how to implement something.
[8:55] Want to do an
implementation, want to
[8:57] be able to reason about it,
[8:59] wanted to be correct
[9:01] and optimize, all
that kind of thing.
[9:03] Well, it's a huge help
[9:05] for the algorithm to
be compositional.
[9:06] What I mean by composition
[9:08] is whatever operation
on performing,
[9:09] like differentiation
of a composition,
[9:12] I form by taking
the derivative of each of
[9:14] the two functions and then
somehow combining them.
[9:17] All right? Well, the chain rule
doesn't work that way.
[9:20] The chain rule isn't
compositional,
[9:22] and then if you look at
the definition here,
[9:24] the derivative of
a composition is,
[9:25] well, it involves
a derivative of f and g,
[9:28] but it also involves f itself.
[9:32] So, this is going to
be kind of awkward to
[9:36] talk about it in terms of
[9:37] reasoning and implementing
compositionally.
[9:39] But there's a simple fix.
[9:42] The fix is instead of
computing just the derivative,
[9:45] so you get this
function of a to b,
[9:48] and we get back a function from a
[9:49] that not only compute
this derivative
[9:51] but also the original value,
and that's it.
[9:55] This enhanced specification
is compositional
[9:58] because when you write out
the implications of it,
[10:03] computing the function
and its derivative for f
[10:07] and g involves just f and
g and its derivatives.
[10:10] >> So you mean the b
on the right side is
[10:12] the same as the b computed
above the function?
[10:14] >> Exactly.
[10:14] >> The left- hand side?
[10:15] >> Exactly. The left-hand side?
[10:17] >> Both that function.
[10:18] So, taking g and b,
[10:20] is that b the same b?
[10:22] >> Yes.
[10:22] >> Okay.
[10:23] >> Exactly. So all we're doing,
[10:24] and here's the definition
specification,
[10:27] so I'm using this fork operator,
[10:28] I didn't need to do that.
[10:29] So, says that this
enhanced derivative of
[10:31] f is f itself and
[10:33] the derivative of f. That's all
[10:34] just don't forget f,
that's all this is saying.
[10:37] This one fix makes
differentiation compositional,
[10:41] and automatic
differentiation does this.
[10:43] You can find this any
automatic differentiation
[10:47] because you have to to make
it compositional. All right.
[10:50] So, there's one other really
[10:52] lovely result from
this perspective,
[10:55] this calculus on manifolds,
[10:56] or derivatives is linear maps,
[10:57] and that's the following:
The derivative of
[11:01] a linear function is
itself everywhere.
[11:05] So, that's may sound weird.
[11:08] But if you think about what
derivatives really mean,
[11:10] derivatives are all about
linear approximations.
[11:13] So, when you have
the derivative of function
[11:15] at a point, what
you're saying is,
[11:16] well, we know what the value
of the function is.
[11:19] But if we also know
what the first
[11:21] derivative so that like
the tangent at that point,
[11:24] that tangent is linear
[11:26] and it's a local
linear approximation.
[11:29] At that point, it's
exactly correct.
[11:31] As it moves away from the point,
[11:33] it's slightly incorrect
and further you get
[11:34] away it's more and
more incorrect.
[11:36] If you want to get
a closer approximation
[11:39] you could use a first and
second derivative,
[11:41] then you get some kind of
local quadratic approximation.
[11:43] It's going to be a much better
approximation and so on.
[11:45] But for differentiation,
the first derivatives,
[11:48] differentiation is all about
[11:49] making linear approximations.
[11:51] So, when I say the derivative of
[11:53] a linear function is
itself everywhere,
[11:54] all I'm saying is that
linear functions are
[11:56] their own perfect
linear approximations.
[11:58] It's really like nothing,
it's not completely obvious.
[12:02] Now, this is something you
know without knowing it.
[12:05] If you say like
what's the derivative
[12:07] of x with respect to x,
[12:09] you'd say it's one,
[12:11] or 2x with respect to
x, you say it's two.
[12:15] So, but I just told you know
[12:16] the derivative is
the function itself.
[12:18] That's because when we
say the derivative of
[12:20] the function x goes to x is one,
[12:22] it's not one it's
the linear transformation
[12:24] that multiplies by one.
[12:27] Which is the same as
the identity function.
[12:29] So, the derivative of the
identity is the identity,
[12:32] is the general way of saying it.
[12:34] Sometimes it looks like if
[12:35] you have scalar functions
you might say it's one,
[12:37] if you have non-scalar functions
[12:39] you might say it's
the identity matrix.
[12:41] The identity matrix, so the
[12:44] matrix that's one's
on the diagonal,
[12:45] zeros elsewhere, that's just a
[12:46] representation of the
identity function.
[12:49] So, similarly, the
first and second,
[12:52] these are functions
that take a pair
[12:53] and give you the first or
second element.
[12:54] Those are linear also.
So, those functions are
[12:56] their own derivatives
also everywhere.
[12:58] In general, they could
take the derivative
[13:00] of a linear function f at a,
[13:02] you get more f of a and f itself,
[13:03] that's the derivative. All right.
[13:06] So, now I've really shown you
[13:08] automatic differentiation,
it's all here.
[13:11] If you take primitive
operations, addition,
[13:14] multiplication, sine,
cosine and so on,
[13:16] and we know what
their derivatives are.
[13:18] Just look them up
or remember them,
[13:20] or prove them analytically.
[13:22] Then, you start
composing things in
[13:23] parallel and in sequence.
[13:25] Then, we have
all the linear functions
[13:27] which is the easy case.
[13:29] This is all there you start
automatic differentiation.
[13:31] So, if you read the literature
[13:32] especially what's
called reverse mode
[13:34] which is what's used
in Machine Learning,
[13:35] extremely complex.
[13:36] But it's because it has
all this historical baggage.
[13:40] It's because it was invented a
[13:42] long time ago in
the '50s or '60s,
[13:45] and then reinvented by
Machine Learning people,
[13:48] rediscovered in terms of
[13:49] something called
back propagation,
[13:51] but wasn't from
this kind of heritage of
[13:54] crisp mathematical specifications
[13:56] and rigorous development.
[13:59] So, if you get rid of
[14:01] all the kind of
historical accidental baggage,
[14:03] graphs, and variables,
and layers,
[14:06] and things like that, the essence
[14:07] really is just what
I've shown you,
[14:09] and we can now put
these pieces together
[14:10] into automatic differentiation,
and then we're done.
[14:13] Not really because I'm going to
[14:14] show you some improvement.
[14:15] So, what I want to
talk about here now
[14:17] is a nice way to package
up this information.
[14:19] So, I said we have
linear functions
[14:21] and they'll be some primitives,
[14:24] sine, cosine and so on, and
[14:25] then sequential and
parallel composition.
[14:28] Now, those are
the basic building blocks,
[14:31] those building blocks have
[14:32] a mathematical history to them.
[14:35] We can take those operations,
[14:37] you can take that
identity and composition,
[14:40] there's an algebraic notion
is called the category,
[14:42] I don't expecting anybody
to category theory background,
[14:46] it's just the idea of I've got
[14:49] some thing which you can think of
[14:50] the function like thing.
[14:52] I means there's
a domain and co-domain.
[14:54] It doesn't really have
to be a function like
[14:55] thing but you can
think of it that way.
[14:58] So, that's going to
be this guy, so this
[14:59] will be something like functions,
[15:01] and has two things,
identity and composition.
[15:03] In the identity map
something to itself,
[15:04] composition takes
something from b to c
[15:07] and a to a and gives
you an a to c. Okay.
[15:09] So, this is a
generalization of the idea
[15:11] of the identity function and
composition on functions.
[15:14] There are certain laws,
this is algebra,
[15:16] so there's certain
laws which is for here
[15:18] just that the composition
is associative,
[15:21] and the identity is
the right and left
[15:23] identity for
composition. That's all.
[15:25] So, anything that satisfies,
[15:27] it has these kind of operations
[15:28] satisfies the clause
is a category,
[15:30] that's what category means.
[15:32] But now, there are
some additional operations.
[15:35] So, in addition to category,
[15:36] there is this more
specialized notion
[15:39] of a Cartesian category,
[15:41] and all that means is
there's a it has a notion
[15:43] of products of pairs.
[15:45] There are three operations:
One is extract left,
[15:48] other is extract right,
[15:50] that's what it's going
first second before.
[15:52] So, given a pair, you can
get the first element.
[15:55] Given a pair, you can
get second element,
[15:57] and then there's
fork which is two of
[15:59] these funny arrows
with the same domain,
[16:02] and you get another one with
[16:03] that domain but pairs in result.
[16:05] So, I've talked about
[16:06] these operations on functions
and I'm just saying,
[16:08] there's actually a wider context
[16:10] not just mathematical
functions are
[16:11] computable functions as we use
[16:12] in computer science to
software engineering.
[16:16] This will be really important
[16:18] because automatic
differentiation is
[16:20] all about one of these things
[16:22] that's not exactly a function,
[16:24] it's a differentiable function.
[16:25] It's a function that computes
with derivatives as well,
[16:28] Then, there'll be
some other interfaces.
[16:31] So, this is Haskell
[16:33] looking stuff but I
hope you get the idea.
[16:34] It's talking about
two different interfaces.
[16:36] One specializes the other,
[16:38] so that makes additional
restrictions. They have laws.
[16:41] The laws here say things
like if you take two of
[16:44] these arrows, you combine them,
[16:47] and then you follow
new compose with say,
[16:50] extract left, then you
get up the original one.
[16:53] Exactly. I think there is
nothing is surprising at all.
[16:57] So, now I've shown
[17:00] you all the building blocks
of automatic differentiation,
[17:02] and then I've shown
you an interface,
[17:04] which is a common interface not
[17:05] specific to automatic
differentiation.
[17:07] It's one that come out of algebra
[17:09] particularly in the '50s
I think, 1950s that is.
[17:13] Now, I'm just going to put
all the pieces together,
[17:16] and there's a Haskell program
[17:18] if you don't understand
what something means,
[17:20] please interrupt. All right.
[17:23] So, we're going to go
back to our specification
[17:24] and I've tweaked it a little bit.
[17:26] So, I said we're going
to define this type.
[17:28] It's a type of differentiable
functions from a to b.
[17:31] So, that's D a b, and
this is a Haskell.
[17:34] It isn't just says that
one of these guys,
[17:37] differentiable
function from a to b
[17:38] has this representation.
[17:39] It's a function
from a to a pair of
[17:41] b and a linear map from a to b.
[17:42] Jack, what I showed you before,
[17:43] but now I've just made this
[17:45] little D thing here
which is just a wrapper.
[17:47] It's just something that says,
[17:49] the type of this thing is
[17:51] not the underlying
representation,
[17:52] it's just more kind
of abstract notion.
[17:55] Now, here's our specification.
[17:57] So, this d hat,
[17:59] we're going to take
a function from a to
[18:00] b and give you a D from a to b.
[18:03] What does it do? Just
what it did before.
[18:04] It takes fn as its derivative,
[18:06] combines them into one
[18:07] but now we wrap it
up with a D. So,
[18:09] there's just a little bit of
[18:10] this programming
language wrapping.
[18:12] I want to emphasize here,
[18:13] the specification
is not computable.
[18:16] So, given an arbitrary
computable function,
[18:19] even if it's continuous,
[18:21] even if it's differentiable
in a mathematical sense,
[18:23] it's not computable to
construct its derivative.
[18:25] So, that's not a shallow result.
[18:31] So, one of the things that
I really like about this,
[18:34] what I'm sharing with you today,
[18:35] is that we started
with extremely simple,
[18:37] compelling specification.
[18:39] I'm saying we just take the
function and its derivative,
[18:41] mathematical derivative,
not computable derivative.
[18:44] Simple specification, and then,
[18:46] we're going to go through
a process of, well,
[18:49] I'll show you the outline of it,
[18:50] you can read the
paper for details,
[18:51] of transforming the specification
into an implementation.
[18:54] So, we get something
that's not computable,
[18:56] very simple and compelling,
[18:57] we end up with something
that's efficiently computable,
[19:00] and not only that,
but it's automatable.
[19:02] That is the transformation.
[19:05] So, here's the specification.
[19:08] So, what we're going to do is
automatic differentiation.
[19:11] I'm going to organize the code
[19:12] as instances of these classes,
[19:14] category, and Cartesian, and
a few other things for sine,
[19:17] and cosine, and so on.
[19:19] The specification is to say that
[19:21] this not computable
function D hat
[19:23] preserves the category and
[19:27] Cartesian structure.
Here's what I mean.
[19:29] It's just these five equations.
[19:31] Two from the category interface
[19:33] and three from the
Cartesian interface.
[19:35] The Cartesian just
means about products.
[19:37] Category just means about
identity and composition.
[19:39] So, what we're saying
is that this D hat
[19:41] of the identity is the identity.
[19:43] D hat of g compose f is
[19:45] the composition of
D hats of g and
[19:49] f. The left extractor goes
[19:51] to itself in
[19:53] the other category, that's
the important thing.
[19:55] On the right hand side,
we see this id functions,
[19:58] that id is differentiable
function does
[19:59] D. This composition
is on functions,
[20:03] this one is on differentiable
function on D and so on.
[20:06] So, the derivative of the fork
[20:07] is the fork of
the derivative and so on.
[20:08] So, this is extremely
simple specifications
[20:11] of very compelling form.
[20:12] What that means
is, you can really
[20:15] think about
differentiable functions
[20:17] just in terms of
the specification.
[20:20] That any intuition you
[20:22] form about what does it
mean when I'm composing
[20:23] these two things is captured
[20:26] precisely and elegantly by
these five requirements.
[20:30] So, these requirements are
going to be the specification,
[20:32] and then the trick is to derive
[20:35] a correct implementation that's
[20:37] computable to
the actual implementation.
[20:39] That's the game. Yes.
[20:42] >> So, [inaudible] is a functor.
[20:44] >> Yes.
[20:44] >> It's a functor?
[20:45] >> Yes it is a Cartesian functor.
[20:46] >> Okay.
[20:47] >> Yes. So, more generally
it's a homomorphism.
[20:51] So, if we have
these abstract notions,
[20:56] for instance, category
and Cartesian,
[20:58] they have a vocabulary,
[20:59] identity compose, extract
left to right, fork.
[21:02] What we're saying is that D is
[21:04] compositional over that structure
[21:06] or distributes over
that structure.
[21:07] It's a homomorphism
over that structure.
[21:09] It's also called a functor,
Cartesian functor.
[21:17] >> [inaudible] is
this a equals to a,
[21:21] plus a linear a
[21:23] which is your definition of
identity of the merchandise.
[21:26] >> Yes. So, this is
the regular identity function,
[21:29] that's the differentiable
identity function which
[21:32] means it knows how to compute
[21:33] a value and it's derivative.
[21:34] >> Yes.
[21:35] >> Yes, and so, on all
of them are like that.
[21:37] This is the general game,
[21:38] we'll play this game
over and over,
[21:39] so it's it's important to
[21:41] pause and appreciate
what's going on.
[21:44] Simple specification,
very regular,
[21:47] a simple definition of a function
[21:49] and a specification that's
always of this form,
[21:52] that this kind of
simple compelling definition is,
[21:56] that distributes over the
structure or preserves
[21:58] the structure or the functor
in category language.
[22:03] So, if we take these five
equations and we solve them,
[22:08] it's an algebra problem.
[22:10] So, we solve these five
equations we get this result.
[22:14] Now, how to get this real?
[22:16] It's in a paper called
[22:18] The Simple Essence of
Automatic Differentiation.
[22:21] It really just follows
from the chain rule,
[22:26] the fork rule which
I haven't shown you,
[22:29] and the linearity,
[22:33] the property of linear functions
[22:34] that are learned
derivatives everywhere,
[22:35] and then a few special things,
[22:37] we know the derivative of
negation, addition and so on.
[22:40] So, solve those equations
you get this form.
[22:42] I'm just going to show
you what this looks
[22:44] like operationally.
[22:45] So, for instance, this
[22:48] is the one that says if
f is a linear function,
[22:50] the differentiable form D
[22:53] is a function that takes a
and gives you f of a and then
[22:56] a. I could have written
that differently as
[22:59] just f fork constants where
constants is the thing that,
[23:04] whatever argument you give
it, it gives you f back.
[23:07] So, for instance, if you look
at how composition works,
[23:11] there's really two things in
here because the meaning of
[23:15] the specification D hat
is we're going to have
[23:17] the original function and
[23:19] then simultaneously
compute it's derivative,
[23:21] so that's exactly what
we do here.
[23:22] So, we compose
a differentiable versions of
[23:25] g and f. We can
differentiable function at a.
[23:28] Well, what do we do at a?
[23:29] We take f of a and we get
its value b and the derivative.
[23:34] Remember these guys g computes
a function n and its,
[23:38] sorry f and g. Then,
[23:40] we take a and put it into g,
[23:42] and we get c. That's going to be
[23:44] the final result of the function
[23:46] but we also get
a derivative there.
[23:47] Here we are using the
composition to the functions,
[23:50] the result, and then we compose
[23:52] the derivatives, and
this is the chain rule.
[23:54] So, I did it, I just
took the chain rule,
[23:55] the definition, did in-lining,
[23:58] wove the code together,
[24:00] and then fork is quite
[24:02] similar but there are
no data dependencies.
[24:04] So, for the two derivatives and
[24:06] values are computed completely
[24:08] independently, and then combined.
[24:11] Then, for the basic operations,
[24:14] negation and addition are linear,
[24:16] so we can just use
the general linear,
[24:19] so it's identity, so we did
the extract left and right,
[24:21] that's why these
ones were simple.
[24:22] Multiplication is not linear,
[24:24] so there's little more here.
[24:25] So, multiplication is, well we're
[24:27] going to take
multiplication itself than
[24:28] operation but we also
need it's derivative.
[24:32] So, the multiplication function
at the argument a and b,
[24:37] so by multiplying a by b, well,
[24:39] it's going to give
you a linear map,
[24:40] and that linear map is going to
[24:41] take a Delta a and Delta b,
[24:44] and then it's going to scale b by
[24:46] Delta a and a by Delta b,
[24:48] and add them, and this is
what's called the Leibniz rule,
[24:50] rule for products
differentiation.
[24:53] So, that's really, that's
[24:55] it, that's automatic
differentiation.
[24:57] >> When you get
through your team a
[24:59] and b wrong, define this.
[25:02] >> So, think about linear maps,
[25:06] there are different ways to
think about linear maps,
[25:07] so that's kind of the heart
of the star, we'll get to.
[25:10] A simple way to think
about linear maps
[25:11] is they're just functions
that happen to be linear.
[25:14] So, the derivative at
[25:18] a point ab is going to give
[25:19] you a function that is linear.
[25:21] That function is what's a
function from Delta a, Delta b.
[25:24] So, this whole thing
is the linear map.
[25:28] If you look, yes, it's
linear in Da and Db.
[25:31] >> Yes, I am
[25:33] thinking how you would
normally represent this.
[25:36] >> Yes.
[25:37] >> Like they will be
accepted, basically,
[25:40] filling in all the possible
values in there, yes.
[25:46] >> Yes, so there
are different ways
[25:48] to represent linear maps
[25:49] and we're going to
talk about them.
[25:52] There's some kind of
traditional ways and
[25:54] some non-traditional ways
that work really well.
[25:56] >> So, you gave instantiations
[26:01] that satisfy the equations
for the previous line?
[26:06] >> So, what you're
asking about this?
[26:08] >> So, these instances
that satisfy the equation?
[26:11] >> Exactly. So, what
[26:14] was provided here was
these definitions here,
[26:18] these definitions with
organizing essences,
[26:20] they satisfy this specification,
[26:21] they are a solution,to
these equations, yes.
[26:24] >> But if you have
[26:26] polymorphic functions that
somehow distortions are weak.
[26:31] >> Oh, you're asking
about are there
[26:34] some maybe some deep type
[26:35] theoretic or
directional properties.
[26:37] >> Theories to say, okay, there's
[26:38] only one function that's-
[26:40] >> So, the remark is sometimes,
[26:43] if we're in a pure
functional programming in
[26:45] strongly typed, but
more than that,
[26:48] in a parametrically
polymorphically typed the setting,
[26:52] there are certain inferences
you can make that are
[26:55] valid that depend only
on the type information,
[26:58] and this inference is one
of them because these have
[27:01] been automatically determined
just based on the types.
[27:04] I don't know. They are
[27:07] not fully polymorphic because
[27:09] they require vector
space structure,
[27:11] and so, this property is
called parametricity,
[27:14] which a deep property.
[27:15] It's not as evidently applicable,
[27:18] but it doesn't mean
it's not an applicable.
[27:19] >> So, it doesn't
apply to the lollipop?
[27:21] Is that what you're saying?
[27:22] >> It doesn't apply to what?
[27:23] >> The lollipop.
[27:24] >> Oh, yes.
[27:26] Also the Lollipop or
the linear map types
[27:30] that's on a fully general
construction of wires notion of
[27:32] vector spaces or
at least modules,
[27:35] let's call this a generalization.
[27:36] So, sometimes in the presence
[27:40] of these certain
algebraic constraints,
[27:41] they are still interesting
free theorems.
[27:43] I have no idea whether
there are free theorems
[27:46] that you know that relate to
automatic differentiation.
[27:49] Even to the extent that
you're suggesting,
[27:50] which is maybe this whole thing
is a free theorem.
[27:52] That would be very cool,
and I really don't know.
[27:55] There's something
that's to me very
[27:57] compelling and inevitable
about this development,
[28:00] and that may be a clue that
[28:02] there's actually a free theorem.
[28:03] It's maybe easier
in a sense then,
[28:06] then I think it is simpler.
[28:07] All right, now I want to
show you some examples,
[28:10] and then we're going to get into
[28:12] thinking about the
performance characteristics
[28:15] of this simple algorithm,
[28:17] and how we can improve them.
[28:19] So, I started out with
[28:21] these three simple
running examples.
[28:23] This is Haskell code.
[28:24] I'll talk you through it. If I
[28:26] don't explain something that
[28:28] you'd like explained, please ask.
[28:30] So, here is a squaring function.
[28:32] So, we're saying
this squaring function,
[28:34] square of a is a times a,
[28:35] just defining this function.
[28:36] Well, it's type is, it goes
from some type a to a.
[28:40] Sorry, this is
kind of common pun we do in
[28:42] Haskell programming we name
[28:43] the variables in the types
of the same things.
[28:45] That may be a little
confusing, and
[28:47] a just has to be numeric
for this to make sense.
[28:49] So, it could be ints
and floats and doubles
[28:51] and other things complex numbers,
[28:54] and maybe
higher-dimensional things,
[28:55] even functions and so on.
[28:57] All right, but you can just
think of this as being
[28:59] a real number, a here.
[29:01] A little bit more of
[29:02] a sophisticated function,
thus magnitude squared.
[29:05] So, if you have
a pair, a cross a,
[29:08] where this is pairing,
magnitude squared is,
[29:11] it's just that the
sum of the squares of
[29:12] the components. So what do we do?
[29:13] We take the pair a, b and we
[29:15] square a and square b
and add them.
[29:16] This is a little bit
less trivial example,
[29:19] and here's another one, which is
[29:21] the cosine and sine of
a product of two numbers.
[29:24] So, given x, y we're going
to compute the sine and
[29:26] the cosine of z, and what is z?
[29:29] It's the product of x and y.
[29:31] Okay? Now, why B3
examples because they
[29:34] get to scalar versus
[29:35] non scalar in different
interesting ways.
[29:38] This is a purely scalar function.
[29:39] This one takes a non scalar,
has non scalar domain.
[29:42] This one has a non-scalar
domain and codomain,
[29:44] both, okay? All right.
[29:48] Now, we can take these
expressions, this is simple.
[29:53] It's a pure function program,
[29:54] and rewrite them in
categorical vocabulary.
[29:57] Okay, well, this is a big step
[29:58] and it's kind of important step.
[30:01] You may or may not
be familiar with
[30:03] this that there's a deep,
[30:05] deep connection among
foundations of mathematics.
[30:08] Particularly, this approach
to category theory on
[30:10] the one hand of logic,
[30:13] and not just one logic,
but logics in general.
[30:15] So, for one reason,
[30:17] I guess another way to think
of it and computation.
[30:21] Okay? That at the heart
of a computation,
[30:24] reason in the foundation of
[30:25] mathematics are
all the same thing.
[30:27] Okay? But that connection
particularly between
[30:30] computation and
this foundational approach
[30:33] mathematics category theory is,
[30:35] well, it's not so obvious
in mainstream languages.
[30:38] So, if you have
an imperative language like
[30:41] C-sharp or Java or I don't know,
[30:43] JavaScript, or worse,
it doesn't even
[30:45] have static typing,
that kind of thing.
[30:48] Well, this connection
to the essence
[30:51] of mathematics and
category theory in
[30:53] particular is quite obscured.
[30:55] It's there, it's just hard
to see and all the noise.
[30:58] But if you take a very
elegant, pure, simple,
[31:01] rigorous notion of programming,
[31:04] namely the typed Lambda calculus,
[31:06] then there's a very clear
connection between the two.
[31:10] Okay? So, I'm not saying that
only functional programming
[31:13] corresponds to logic
and category theory,
[31:17] I'm just saying that
that in that setting,
[31:19] it's most clearly evident, okay?
[31:21] This functional programming
is equally expressive,
[31:23] do imperative programming
[31:25] object-oriented,
whatever flavor you want.
[31:26] Okay? But this connection is
[31:28] quite simple in this setting of
[31:30] a typed Lambda calculus and this
[31:32] is just the sugar ring of
the typed Lambda calculus.
[31:34] Haskell is just typed
Lambda calculus sugared.
[31:36] That's a little more than that
and it's essentially that.
[31:40] So, there's a, as a result
from 1980 by Joachim Lambek,
[31:47] which says that if you take
the typed Lambda calculus,
[31:51] there are different models of it,
[31:53] there are different
interpretations of it.
[31:54] Okay? So, the one that I'm
used to it because I've been
[31:57] doing computer
programming for a while
[31:58] is computable functions.
[31:59] So, I think this code,
[32:01] Lambda calculus it means
computable functions.
[32:05] But what Lambek
showed in 1980 is,
[32:08] now, that's just
one interpretation.
[32:10] That there are a lot
of interpretations
[32:12] that are consistent
[32:13] with the laws of Lambda calculus,
[32:17] and they're exactly
the inhabitants,
[32:21] they're exactly the models that
[32:23] have a mathematical property
[32:24] namely they are the Cartesian
closed categories.
[32:27] Okay? So, I haven't
said what closed means,
[32:29] closed means you have
first-class functions.
[32:31] Okay? Categories means you
have identity and composition,
[32:33] Cartesian means you have got
[32:34] the first second projections,
[32:36] the left are projections,
and this fork operation.
[32:39] Closed means you have a notion
of first-class functions.
[32:42] Anything that has those,
[32:45] that's it satisfies
those interfaces,
[32:46] and I'm only showing you
two of them look like,
[32:48] and it satisfy the laws,
[32:49] every one of those things is
[32:51] a consistent model of
the typed Lambda calculus.
[32:54] So, the way you can
think of that is,
[32:56] every one of those is
[32:57] a valid sensible interpretation
[32:59] of a purely functional
language like Haskell.
[33:02] Moreover, we know how to
automatically convert
[33:07] the Lambda calculus
into this language.
[33:09] So, that's the idea
[33:11] here is that we're going
to write in Haskell,
[33:14] we're gonna automatically,
so not the programmer,
[33:17] the compiler automatically
translates to this vocabulary.
[33:20] Then, instead of interpreting
[33:22] this vocabulary in
the usual sense,
[33:23] computable functions, I want to
[33:25] interpret in some unusual sense.
[33:26] In our case, it's
the differentiable functions.
[33:29] That's the game.
[33:30] >> If you say all transformation
[33:33] from Haskell to category three,
[33:35] and this is that you're inline
[33:38] the square function in there,
[33:39] do you need to do that in
[33:41] Haskell log transformation and
[33:42] break modular boundaries or?
[33:44] >> No thanks. So, the question
is, well, first of all,
[33:47] it's an observation that home
I translate a square here,
[33:51] but then I didn't
just use square,
[33:53] which I could have now this is
[33:54] purely just where the
implementation is at this point.
[33:57] It's a little awkward
at this point for me
[33:59] to preserve that modularity.
[34:02] But there's nothing.
[34:04] >> There's no deep reason.
[34:05] >> There's nothing, yes.
[34:07] So, at some step, this would
[34:08] look like multiplication
composed.
[34:11] Sorry, it will be square
composed with exl,
[34:14] and that would be square
composed with the exl.
[34:15] That'll be more readable
and more modular, yes.
[34:18] Just not quite there yet.
[34:20] All right, so for squaring,
what do we do is, well,
[34:23] we take the identity function
and itself together,
[34:26] work them together,
that gives you function
[34:28] that you give it a and it
gives you a and itself.
[34:31] Just duplicates, so that's
a duplicating function.
[34:33] Then, compose that
with multiplication.
[34:35] So, you take a value,
duplicate it,
[34:36] and then you take the product of
[34:38] that pair, that squaring.
[34:40] Okay, what do we do here well,
[34:42] we take the left extractor and
[34:44] itself and that gives
us x out of x y,
[34:47] and then we take it fork with
itself we get x x, right?
[34:51] We multiply that so
that's x squared,
[34:53] this is y squared, we do
[34:55] those in parallel and
then we add the result.
[34:57] We see this is composed,
[34:58] so you read from right to left.
[35:01] Cosine sine progress even
simpler you take the product,
[35:04] and then in parallel of
the sine, the cosine and sine.
[35:07] So, what I'm saying is,
[35:10] we already know how to take
[35:11] derivatives if we write our
programs and this vocabulary,
[35:14] and that's what the
previous slideshows.
[35:17] So, if we take these definitions
[35:20] of the operations like add,
[35:22] compose, fork, and so on,
[35:24] and we use those
interpretations here,
[35:27] we'll get versions of
[35:28] these functions that compute
not on the regular values,
[35:30] but their derivatives
exactly, all right.
[35:33] But, this is a terrible language
[35:34] for person to have
to write in, So,
[35:36] one of the language
for a compiler,
[35:38] or mathematician to
reason about but it's
[35:39] a terrible language for
a programmer to write.
[35:41] Okay, so fortunately we have
[35:43] this automatic translation from
[35:45] a kind of human-friendly
language,
[35:48] maybe debatable to mathematically
[35:52] austere and easy to
reason about language.
[35:55] So, now I want to show
you some examples of
[35:58] this interpretation applied
[35:59] for automatic differentiation.
[36:01] So, here again is
the magnitude squared
[36:03] function, sum of the squares,
[36:05] and here's it's
categorical translation,
[36:07] I just mean this is exactly
the same thing but rephrased,
[36:10] and this is automatic, this step.
[36:12] Now, if we interpret,
[36:14] what have we done here?
[36:16] Oh yes, so this isn't
differentiation,
[36:18] this is just the function itself.
[36:20] So, this is what the category
expression looks like,
[36:23] this function we can visualize
in terms of a graph,
[36:27] and this is what it looks like.
[36:29] So, this kind of emphasizes
the parallel nature
[36:31] of fork here and that's
this fork right there.
[36:33] Okay, so what do we got?
[36:35] Here's the extract left,
[36:38] and it's getting fed in,
[36:39] both of them to multiply,
that's this one.
[36:41] Also, the right
extractors get fed
[36:43] into another multiply,
these two in parallel,
[36:46] their results, they take
the same argument and
[36:48] their results get
fed in to addition.
[36:52] So, what do I want to say here?
[36:57] Oh yes, all right now in fact
[37:00] there are three different
categories going on here,
[37:03] okay one category is the one
[37:05] that we just apply unconsciously,
[37:07] at least I do which is just
[37:08] to think that this
means functions,
[37:10] plano-mathematical functions
are computable functions,
[37:12] that's the usual one,
we have in programming.
[37:15] This display here,
this categorical expression,
[37:19] expression in terms of
this funny category language,
[37:21] it's another category itself.
[37:23] So, I have a category
that it then
[37:26] interprets composition as
well in a syntactic way,
[37:29] multiplication makes
all the operations
[37:31] syntactic and then it
pretty prints the result,
[37:34] okay that's just
for my convenience.
[37:36] Another category,
it builds a graph,
[37:40] okay and then I display
that graph here.
[37:43] Then another category
is the derivative one,
[37:46] the differentiable one which
I'm going to show you next.
[37:49] Okay, but important thing
I want to say here is,
[37:54] automatic differentiation
is almost
[37:57] always talked about
in terms of graphs,
[37:59] especially in Machine Learning,
[38:02] especially in reverse mode.
[38:03] I think that's always a mistake.
[38:05] Okay, because differentiation has
[38:08] nothing to do with graphs,
[38:09] unlike differentiation
by differentiation,
[38:11] differentiation is
about functions,
[38:12] there's no graphs there.
[38:15] So, you can think about
any domain of interests,
[38:18] anytime you're doing programming,
and you've got well,
[38:20] there's some compositional thing
[38:22] going on, some algebraic,
[38:23] something rather very expressive,
[38:25] which of course want we want
our APIs to be expressive,
[38:27] it means you use
them multiple times,
[38:29] do you feed the output
of one operation
[38:31] the input of another thing.
[38:32] Every API you can think
of as being about graphs,
[38:37] arithmetic is an API, okay?
[38:39] Addition multiplication and
just like literal numbers
[38:41] is an API that you
learned as a young child,
[38:44] and you can think of it as being
[38:46] about graphs, but it's not.
[38:47] No. Well, unless you're
[38:50] really didn't graph theory
or something like that,
[38:52] it's not about graphs,
[38:54] it's about its domain,
[38:55] that domain has a vocabulary.
[38:57] It hopefully has
a type system that
[38:59] mediates what gets
composed with what.
[39:01] You can think of those things as
[39:03] graphs, but you shouldn't,
[39:04] a compiler writer thinks
about them as graphs.
[39:06] A graph theorist maybe
[39:08] might want to think
about them as graphs,
[39:10] but differentiation has
nothing to do with graphs.
[39:12] So, I want to make
[39:14] that point because it
distinguishes his work
[39:16] from almost all other AD work
[39:18] that I now especially
where is known.
[39:20] But I also want to
say you're going see
[39:22] a lot of graphs and you
might be tempted to
[39:23] think I'm doing something like
[39:24] these systems TensorFlow
or something,
[39:26] that's all hung up
on graphs like no,
[39:27] these graphs are just
about visualization,
[39:29] they have nothing to do with
automatic differentiation.
[39:31] Even when I show you the result
[39:33] of MI differentiation as a graph,
[39:35] the graph came second, not first.
[39:37] Meaning it's a way for me
to show you the result,
[39:41] not a way to compute
the derivative.
[39:43] Okay, so here's an AD example,
[39:45] I'll make a little simpler
this is the squaring function,
[39:47] this is the expression
[39:49] in this category language
and this is a graph that
[39:51] just shows you what
[39:54] the computation looks
like, all right?
[39:56] Now, what I get here is this is
[39:59] the derivative of the
differentiable function version,
[40:02] so if I take this expression
and interpret it in
[40:05] this category
[40:07] of differentiable functions
that I showed you.
[40:09] Then I take
the resulting function
[40:12] on the inside the
representation of it,
[40:14] and I turn it into a graph,
[40:16] I reinterpret it as a graph,
this is the result we get.
[40:21] So, this is the original
function, so that's a,
[40:24] that's a squared, a times a,
[40:27] and that's the first result.
[40:29] The second result is going to be
[40:30] a function that's linear,
[40:32] and the way I'm showing functions
[40:33] here as this little green box,
[40:35] and the input is, in
[40:36] this input and out is the
output of the function.
[40:39] So, what do we have
here? This is a,
[40:40] this is the linear
function that takes,
[40:42] I'm going to call it da, okay
It's just a little Delta.
[40:46] So, we get a times da
times 2, all right.
[40:52] So, this is the linear map
that maps da to 2ada.
[40:56] You're used to thinking of
that as the derivative is 2a,
[40:59] the derivative
a square root is 2a.
[41:01] It's not, it's da times 2a.
[41:05] Okay, that's a linear function,
[41:08] it's a function from da,
that multiplies da by 2a.
[41:12] When we say the derivative of a
[41:13] squared is 2a,
that's what we mean,
[41:15] it means multiply by 2a
because it's linear.
[41:19] Okay, here's one more
sophisticated example,
[41:22] the sum of two squares,
[41:23] okay this is the categorical
[41:25] expression and when we interpret
[41:27] these operations in
[41:28] the differentiable function
category, we get this result.
[41:31] Again, we're going to compute
the original function here,
[41:34] so this is what ab,
[41:35] so that's a squared, b squared,
and we're adding them.
[41:37] That's the first result, and
[41:39] the second one is the derivative.
[41:41] So, it's going to take a da db,
[41:43] and here we get da times b,
[41:47] that's b, that says a
times db, this is what?
[41:52] This is b times b,
[41:55] times db, that's not right.
[42:05] Okay, so we get two,
[42:10] Oh yes! Of course,
that's exactly right.
[42:12] Yes, so never mind when I say,
[42:14] yes this is correct
my brain was incorrect.
[42:17] This is a da times a,
[42:19] doubled, those are two ada,
[42:21] this is 2bdb, we're
going to add them.
[42:24] That's the linear map, right.
[42:28] >> So, there is
no real magic here,
[42:30] right? Find the perimeters.
[42:32] What made you like, cosines
specials include this once,
[42:35] and have so that you
just compose the-
[42:37] >> Exactly.
[42:38] >> The d guys and I said what.
[42:41] >> Exactly.
[42:42] >> Right, Yes, there's
no magic here.
[42:44] >> No.
[42:45] >> Yes.
[42:46] >> Exactly.
[42:46] >> Except for derivatives.
[42:47] >> Yes.
[42:47] >> They used to fit in.
[42:48] >> Yes.
[42:48] >> First of all its composition.
[42:50] >> Yes, so we have to know
derivatives our primitives,
[42:53] and then every composing form,
[42:55] in which there are two main ones,
[42:56] seem much longer
than a parallel.,
[42:58] know how we compose
[43:00] these differentiable
functions, and that's it.
[43:01] That's all there is done
like differentiation.
[43:04] Okay. Yes, thank you,
[43:07] I want to emphasize
the simplicity of
[43:08] what's going on here
particularly in
[43:10] contrast to the complexity
of what goes on in
[43:12] the literature about
automatic differentiation,
[43:14] particularly what's
called reverse mode,
[43:16] which is the mode that's needed
for machine learning and
[43:19] other uses of high dimensional
optimization problems.
[43:24] >> A question.
[43:25] >> Yes.
[43:26] >> How would you deal with sums,
[43:28] and I'm thinking about like
discontinuities and so on.
[43:31] >> Yes, so some types.
[43:33] >> Yes.
[43:33] >> Yes, so the question is,
so I've shown you how to-
[43:35] what- we can deal scalars,
[43:39] and we can deal with products.
[43:40] So, what about when we have
[43:42] sometimes of disjoint unions
that kind of thing.
[43:45] There's a few angles
on the question,
[43:48] but the first and most
fundamental question
[43:50] is differentiation
even meaningful,
[43:52] because once you once
you have some types,
[43:55] you no longer can have
purely continuous functions,
[43:57] well, you can but none of
them are interesting, right?
[43:59] They would have to
always be the left or
[44:00] the right disjunct of
the sum. all right.
[44:03] So, I don't know,
[44:07] I'm going to show you
something that is similar
[44:09] but interestingly
different from sums,
[44:12] but your question yes
it's really about sums.
[44:14] Is something I've thought about,
[44:16] I think it's probably
a really lovely answer,
[44:20] and I don't know what it is.
[44:21] >> I suppose in
some way you can encode
[44:23] some and fit inside
your system what does numbers.
[44:25] >> Yes.
[44:26] >> What does it look like
at the end of the day.
[44:28] >> Yes, so you can
church encode it,
[44:31] though you can represent,
[44:32] so some sometimes is
like disjoint unions,
[44:34] it's either that or
that plus a tag,
[44:36] something that tells
you which it is.
[44:38] So, even when you
add like wo or b,
[44:41] you'll still get to
know which real,
[44:42] the left one or the right one,
[44:44] that's why we call
disjoint union.
[44:47] I forgot what your remark was.
[44:50] >> What the are few- I
mean church encode aside.
[44:52] >> Oh yes, church encode. Yes, so
[44:54] these types can be encoded
in terms of functions,
[44:57] actually even pairs can be
encoded in terms of functions,
[45:00] but actually that's not enough,
[45:01] you need universals as well,
[45:02] universal quantification, yes.
[45:05] What the universal
quantification then n function,
[45:07] then you can get pairs and sums,
[45:09] but I don't know like
if you encode it,
[45:12] even products before we get to
[45:14] sums encode products in that way,
[45:16] what happens to the notion
of differentiability,
[45:18] because they'll
just ride along in
[45:19] a sensible way with
the church encoding,
[45:21] that's a really
interesting question.
[45:22] If the answer is yes,
[45:24] then it will be
encouraging to try
[45:25] the same thing with sums.
[45:26] >> It might get to
the same round of [inaudible].
[45:31] >> Yes, yea, it might.
[45:32] >> Yes, these are
interesting questions.
[45:34] >> The questions is always busy,
[45:37] that the church encoding is
an instance of continuation.
[45:40] >> Yes, okay, and
we'll get into that.
[45:42] >> So, I'm sure we'll
get continuations.
[45:44] >> Yes, we'll get
continuations. All right.
[45:46] >> For church encoding
you need rank two types-
[45:48] >> Yes.
[45:49] >> Which corresponds
to cones in category
[45:52] were they to extend
here in your theories?
[45:54] >> Yes absolutely, yes.
[45:55] What I love about this framework
if you think about
[45:57] automatic differentiation and not
[45:58] just that but a lot of
different problems,
[46:00] a lot of people do, prompts
if we can reexamining
[46:03] in terms of this the language
[46:04] of the seventh category theory.
[46:06] What I led us at the space
locations are so simple.
[46:09] All right?
[46:10] So if I was trying to start
from back propagation,
[46:13] as it's described in
the Machine Learning
[46:15] literature or the AD literate.
[46:16] I wouldn't have a prayer,
[46:19] I don't even understand
what this algorithm,
[46:23] I don't understand its meaning
[46:24] or whether it's correct or not,
[46:26] without introducing
these complications.
[46:29] But, when we get it to
this really simple foundation,
[46:32] then we can revisit
these questions.
[46:33] Yes, what if you do
charge encoding,
[46:34] what if you do sums,
[46:36] what if you aren't happy
with the performance.
[46:40] You get out of here and
you want to reason.
[46:43] >> So, your objective is
you given the circuits,
[46:48] an arithmetical circuit, you
want to differentiate it?
[46:52] >> I'm given a
function on a circuit.
[46:55] >> Okay.
[46:55] >> But there was somebody say.
[46:56] >> You don't want to listen here.
[46:57] >> Okay, yes.
[46:58] >> You're given
the representation
[47:00] of an hypothetical function.
[47:02] >> Yes, you're right.
[47:03] >> Your objective
is to compile it,
[47:06] compile the derivative
and optimize it.
[47:09] >> Yes.
[47:09] >> That's the main goal.
[47:11] >> Yes.
[47:12] >> It's derivative.
[47:13] >> Repeat the question,
it is my goal
[47:16] here to take a description
of mathematical function,
[47:19] and generate code
that computes its
[47:21] derivative correctly
and efficiently,
[47:23] is that the question, right?
[47:25] >> Yes.
[47:25] >> The answer is yes.
[47:27] Yes that's exactly my goal.
[47:28] Now, it is important distinction,
[47:30] we're given a representation
of a mathematical function,
[47:33] given a mathematical function
[47:35] itself, it's not computable.
[47:36] We can't compute
its derivative, but
[47:37] given a representation yes.
[47:38] So, there are different
representations you might choose.
[47:41] A popular one is graphs.
[47:43] What I'm saying is
that's always a bad idea
[47:46] compared with this much
simpler setting of saying,
[47:49] "Well, we're going to take
the Lambda calculus."
[47:50] Moreover, that's
just a starting point,
[47:53] what's really much
more convenient
[47:54] is this categorical expression,
[47:56] of which we can
automatically translate.
[47:58] That step has nothing to
do with differentiation.
[48:00] >> There is also this type
of symbolic differentiation.
[48:03] >> Yes.
[48:03] >> Is it different? I mean I
don't understand variable,
[48:06] the numerical Fortran programs.
[48:09] >> Yes.
[48:09] >> But it seems the high-level
goal seems identical.
[48:14] >> Yes, it is.
[48:16] >> Yes.
[48:16] >> So, if you read
the AD literature,
[48:18] maybe some Machine Learning,
AD literature.
[48:22] A lot of paper start
out by saying there are
[48:24] three different ways to compute
[48:25] derivatives on a computer.
[48:27] One is as they call
numeric or approximation,
[48:30] that there is called the secant
[48:31] method or method of differences,
[48:33] those are all different terms
to the same thing,
[48:35] and it's just you take
a couple of points,
[48:37] hopefully near each other,
[48:39] you draw a line,
[48:40] and you say that's
roughly the derivative.
[48:42] Okay, well it's incorrect.
[48:44] >> Isn't that a miracle to it.
[48:45] >> That's yes, but
[48:47] America's people will call it
[48:49] in America that's not
a good description,
[48:50] because automatic
differentiation in numeric too.
[48:52] If you look at it one
way it's numeric,
[48:55] if you've got another way
it's symbolic.
[48:56] So, just call the first
[48:58] one numeric is
a little misleading.
[49:00] >> Okay.
[49:01] >> Yes, because you can
set difference between AD
[49:03] and automatic and symbolic
differentiations,
[49:05] AD is numeric and
symbolic is symbolic.
[49:08] But that's a funny perspective,
[49:10] I think there's
a quite popular perspective,
[49:11] but I don't think
it's a very good.
[49:12] >> Well.
[49:13] >> Well because-
[49:15] >> Also, seems all symbolic you
[49:16] just working with symbols, right?
[49:19] >> Yes, I think so, it's one of
[49:21] these things that I would
agree with you with
[49:23] except that what you're saying
is true, but misleading.
[49:27] >> Okay.
[49:28] >> In the following sense,
[49:29] so it's made factual but it's
[49:31] not true in the following sense,
[49:34] everything that is done by
a compiler is symbolic.
[49:38] >> Sure.
[49:38] >> Okay, so to talk
[49:40] about something and
say it's symbolic,
[49:41] its not, if you're in a compiler,
everything is symbolic.
[49:44] Once you're doing runtime,
[49:45] you can say everything's numeric.
[49:47] Well, okay if
your program is doing
[49:49] a symbol manipulation like
symbolic differentiation,
[49:52] then okay, it's not
[49:53] a very useful way to think
of it as it's numeric,
[49:55] of course it is because it's
[49:56] using bit and coding of things.
[49:59] But that's not very helpful
perspective, yes exactly.
[50:01] So, everything is symbolic
when done by compiler.
[50:04] Automatic differentiation,
the story is,
[50:10] there are three ways to
compute derivatives,
[50:11] one is incorrectly by
numerical approximation,
[50:16] that's called the
secant method or
[50:17] method of differences, okay?
[50:18] That's very popular, but it's
[50:20] terrible performance-wise
and accuracy-wise.
[50:24] Another is what's called
symbolic differentiation,
[50:27] which is you write code
[50:28] that does what you
did in high school,
[50:30] which is like manipulate
symbols and we'll see
[50:32] that the derivative of
sine u is cosine udu,
[50:35] and so you're writing
something that is manipulating
[50:38] some representations of
mathematical expressions, okay?
[50:41] So, that's typically
called symbolic
[50:43] and there's automatic
differentiation,
[50:44] okay, which is what
I'm showing you,
[50:46] which uses the chain rule and so
[50:48] on.But from my perspective,
[50:50] I don't think that's
a very helpful description.
[50:53] I don't think it's true.
[50:54] >> Because it's higher level,
you're saying it's
[50:56] more mathematical,
that's why numeric.
[50:58] >> What I'm saying is that-.
[51:00] >> It has algebraic rules.
[51:02] >> Yes.
[51:02] >> It was suppose to
organize when you
[51:04] reorganize code in a compiler.
[51:06] >> What I'm really
saying is this,
[51:07] automatic differentiation
is symbolic differentiation
[51:10] performed by a compiler.
[51:11] That's my perspective on
[51:13] the relationship between the two.
[51:14] So you won't find that statement
in the literature,
[51:18] you'll find these two at
[51:19] very different things,
unlike differentiation.
[51:21] Look at one symbolic
[51:22] differentiates
all kinds of problems.
[51:23] I think what is true is
symbolic differentiation
[51:26] done badly has
all kinds of problems,
[51:28] but that's nothing to do with
symbolic differentiation,
[51:29] that has to do with
doing things badly,
[51:31] all right? So, don't do it badly.
[51:33] >> Symbol.
[51:34] >> In the context of a compiler,
[51:36] it's convenient to do it well.
[51:38] So, I'm doing
symbolic differentiation,
[51:41] I'm tricking a
compiler into doing
[51:42] symbolic differentiation.
[51:44] No big deal because
[51:44] compiler does everything
symbolically.
[51:46] I wanted to have
good performance,
[51:48] no big deal because
compilers are good
[51:49] at maintaining performance, okay.
[51:53] >> Can I say that one difference
[51:55] with usually use
symbolic differentiation
[51:59] that may not work, right?
[52:00] You may write expressions that
[52:02] cannot be enabled by the code,
[52:05] in your case I
guarantee that if I
[52:08] write it within this limits
and I print out, it's true.
[52:11] >> Yes.
[52:12] >> So, now [inaudible] yes.
[52:13] >> It's factual and
misleading yes,
[52:15] so if you do
[52:16] things symbolically, you
can run into problems.
[52:18] If you do it, here you
can't run a problem,
[52:19] now that both you can run it
[52:20] the same problems in either
[52:21] setting which is if you try to
[52:22] express something outside of
[52:24] the vocabulary of which
for which we know how to
[52:26] symbolically or automatically
[52:27] differentiate, then we're
going to run the problems.
[52:30] So, maybe in one setting,
[52:31] it's a little more commune
[52:32] to respect your expressiveness,
[52:33] maybe, I don't really
know if it is.
[52:36] Okey-dokey, so here's
the third example,
[52:39] the sine and cosine
of the product, okay?
[52:44] This is the
undifferentiated version,
[52:45] there's a differentiated version.
[52:47] Okay, and what I want to show
here is that there's a lot
[52:50] of sharing of computation
between the regular value,
[52:54] which is sometimes called the
primal and the derivative.
[52:57] Okay, well this is
a small example,
[52:59] so there can't be a whole lot
of sharing because
[53:00] there isn't a whole lot
of computation going on.
[53:02] But this is crucial
[53:03] and I forgot to
mention this at first,
[53:05] this one-step early on in
[53:07] the talk when I said
sequential composition,
[53:10] the chain rule is
not "compositional,
[53:11] " ironically, centered
about competition.
[53:14] I made it compositional by
[53:17] augmenting the function with its
[53:19] derivative instead of just
computing the derivative.
[53:21] That augmentation not only
makes it compositional,
[53:23] it makes it possible
to do computed
[53:24] efficiently and that's because
[53:27] the original definition
of just the derivative
[53:29] uses the derivatives
of functions,
[53:31] and the regular value of
functions and usually there's
[53:34] a lot of shared computation
[53:35] between a function
and its derivative.
[53:36] So, by putting them both
into one specification,
[53:39] it makes it possible to
optimize and share computation.
[53:42] Okay? Not only possible it
is quite easy because I
[53:45] showed you the code
that shares, okay?
[53:49] With some what's called
symbolic differentiation,
[53:51] sharing is a big deal and
[53:53] the main criticism is symbolic
differentiation is that,
[53:57] well you don't get sharing,
[53:58] you end up doing like
exponentially large
[54:00] work to compute or
[54:01] exponentially large
work to optimize
[54:03] away the redundant
work at runtime,
[54:06] so usually do
a huge amount of work at
[54:07] compile time or runtime.
[54:08] All right, that's just
[54:11] because people are used to
[54:12] doing symbolic
differentiation badly,
[54:14] that's all, it's not
[54:16] a problem with the symbolic
approach and as I said,
[54:19] this is symbolic but the
compiler's doing it.
[54:21] I don't even have to
help the compiler
[54:24] be smart about sharing because
[54:25] compiler is smart about sharing,
[54:26] that's a part of their job.
[54:27] >> That really helps to
create tree into a diag.
[54:32] >> Yes, the compilers do that.
[54:33] When you say let, that's not
[54:35] the remark wants to
turn tree into a diag,
[54:36] what I would say is stop
thinking about graphs, okay.
[54:40] So, if you think about graphs,
[54:41] then you're going to run it
this thing like, "Oh my God,
[54:43] it's easier to manipulate trees
[54:45] compositionally than graphs,"
graphs are very awkward,
[54:47] trees are super simple, it's
like the simplest thing.
[54:50] So, oops! But some trees are
[54:52] exponentially larger than
the graphs they represent.
[54:54] In other words, trees
don't have sharing,
[54:56] you have to do duplication
to represent the same thing.
[54:59] So, you could think in
terms of graphs, trees,
[55:04] manipulation of graphs
that refactor big trees
[55:07] into into graphs with
[55:09] more sharing that's a lot
[55:10] of work and it's
really complicated.
[55:11] Just don't create the problem
in the first place,
[55:13] don't think about trees
and graphs because
[55:15] differentiation has nothing
to do with trees and graphs.
[55:18] Okay. So I go back to
[55:22] the Haskell code that
[55:25] is derived by solving
these five equations,
[55:29] the structure preserving nature
[55:32] of the d-hat operation, okay?
[55:34] So, this is the code I
showed you a few slides ago,
[55:37] and I want to note
[55:39] that there is a something
that jumped out at me,
[55:41] when I first was working
on this differentiation.
[55:45] In this category language,
[55:47] I started noticing a pattern,
[55:50] and when I start nosing patterns,
[55:51] I like to write pretty code.
[55:53] So, I tried to pull
[55:55] those patterns outside so could
[55:56] really see what was going on.
[55:57] I noticed the first one that
really caught my eye is
[56:01] the composition of differentiable
functions involves
[56:04] the composition of
derivatives, okay?
[56:07] The identity differentiable
function involves
[56:10] the identity linear map.
[56:14] So, I got the differential
[56:17] identity function involves
the identity linear map,
[56:20] is the derivative everywhere.
[56:24] The composition of
differentiable function
[56:27] involves the composition of
[56:28] the derivatives of linear maps.
[56:30] So, not only that, but
that's all it needed.
[56:33] These definitions use
nothing about linear maps
[56:35] other than that they have
identity and composition,
[56:38] and that they satisfy the laws.
[56:41] So, that was interesting.
[56:43] Then get into Cartesian,
oh, Interesting.
[56:45] The left extractor, involves
[56:48] the left extractor
for the linear map.
[56:50] The right extractor
and the fork involves
[56:52] the fork and that's
all that it used.
[56:55] So, this code is not
only pretty and poetic,
[56:58] which is really how I got to it,
[56:59] but it says something
very powerful,
[57:01] which is that linear maps,
[57:04] there's almost nothing you
need to know about them.
[57:07] You need to know that they form
[57:08] a Cartesian category also.
[57:10] That means that every notion
[57:13] of every function like thing,
[57:15] that has a Cartesian category,
[57:17] and there's a lot of them,
[57:18] can play the role of linear maps.
[57:21] So, this observation and writing
[57:24] the code purely
aesthetic motivations,
[57:26] it led to I think
[57:28] a deep and very powerful
insight, which is that,
[57:29] automatic
differentiation not only
[57:31] can be expressed elegantly,
[57:32] but much much more
[57:34] generally than
the original specification.
[57:39] So, that's the point here.
[57:42] Every one of these operations on
[57:43] differentiable functions
just used as
[57:44] a corresponding operation
on linear maps
[57:46] and therefore, we can generalize,
[57:47] we place the role
of linear maps by
[57:49] arbitrary other thing that
has identity compensation,
[57:55] projections and fork,
and satisfy the laws.
[57:58] So, all I've done from
this slide to this slide,
[58:01] is I've parameterized
this notion.
[58:03] So, D here, it had
linear maps built in.
[58:06] This D, the subscript says,
[58:08] it's going to take a parameter,
[58:11] it's going to take
any old Cartesian category,
[58:13] for instance linear maps,
and use them here.
[58:16] The definitions are unchanged.
[58:19] Well, I made one little change.
[58:21] I'm making a clear distinction
[58:23] between linear D. It takes a
function and its derivative,
[58:27] they're always going
to be the same.
[58:29] Like identity and
identity XL and XL.
[58:32] But one will be on functions
and the other will
[58:34] be on the linear map like thing.
[58:38] So, the code really is unchanged,
[58:40] except for this duplication,
[58:41] just to make
that distinction clear.
[58:45] Well, there's
one awkward thing here,
[58:48] the gate and add are linear.
[58:50] So, we're going to take
just the linear versions
[58:52] of them. So here we are.
[58:53] See, this is the extract left
on functions, this is on,
[58:56] I want to say a linear maps,
[58:57] but it's not just linear maps,
[58:58] It's arbitrary, this notion here.
[59:01] But multiplication,
that's awkward.
[59:02] I don't really have
a way to talk about it.
[59:04] Because originally,
I wrote it this way.
[59:07] But this is functions.
[59:08] So this linear map,
[59:10] this is literally a function.
[59:11] So, it's not a kind of
an arbitrary Cartesian category.
[59:14] Well, so, let's write
this in another way.
[59:17] I'm going to suggest a couple
of pieces of vocabulary.
[59:19] Next, tell you what
they mean on functions
[59:21] and then say we can
generalize them also.
[59:24] Then we get another expression
[59:26] of a derivative of
multiplication.
[59:29] So, there are
two things going on.
[59:30] One is scaling and
[59:32] the other is where we take
a pair and we break it up.
[59:35] We do some computations
and we add the results.
[59:38] Those are the two
patterns that I want.
[59:40] So, one of them is called scale.
[59:41] So, scale of u,
[59:44] is the linear function that
multiplies its argument by u.
[59:48] So, multiplication isn't linear.
[59:51] That's what's called bi-linear.
[59:52] But when you provide
one argument to multiplication,
[59:55] the result is linear.
[59:58] Then there's this operation,
I'm calling it join.
[60:02] So, remember fork, it took
[60:03] two functions or two arrows
of the same domain,
[60:08] and gave us and took
an argument given to both,
[60:11] and then paired up the results.
[60:12] Join is the dual of that.
[60:14] Sorry. Yes, that's right.
[60:17] So, with Join, we have two of
[60:19] these maps with the
same co-domain.
[60:21] The same result and
possibly different arguments.
[60:26] So, we're going to take a pair
[60:27] rather than generating a pair.
[60:28] So, it's just a dual.
[60:29] A reverse of a fork.
What do we do?
[60:33] Well, when you do join f
and g, you get a pair.
[60:36] You parcel out the arguments,
[60:38] give one to f, one to
g, and add the results.
[60:41] So, that I'm calling join.
[60:43] With this vocabulary, we can just
[60:45] refactor this expression
and now we get this form.
[60:47] lambda ab, we're going to join
[60:49] scale by b, with scale by a.
[60:52] So, why is b first? Because
it's b times da, a times db.
[60:57] So, now with this vocabulary,
[61:00] I haven't really made
this anymore general.
[61:01] I've just described
it differently but
[61:03] I've introduced new vocabulary
that does generalize.
[61:08] So, here's a new vocabulary.
[61:10] We have the category in
the Cartesian forms,
[61:13] and now we have
this co-Cartesian.
[61:15] It gives three operations
that are the dual,
[61:17] the reversal of
the Cartesian operations.
[61:20] So, instead of having
two projections or extractors,
[61:23] we have two injections.
[61:24] Left and right. Instead of
[61:27] taking two arrows
with the same domain,
[61:29] we take two with same co-domain.
[61:30] So, this is the new vocabulary.
[61:32] Then one more thing, settings
[61:36] that know how to do
scaling. All right.
[61:40] So now, given this vocabulary,
[61:41] now we can write linear
transformations as functions.
[61:45] So, all I'm doing is I'm
repackaging when I said before.
[61:48] So, this is a little new type.
[61:50] This is just saying, we
can going to represent
[61:52] these additive functions,
[61:53] as just regular old functions,
[61:55] but with the context
of additivity,
[61:57] and the all the types
involve are additive.
[61:59] Now, where that
additivity comes in,
[62:01] I'm omitting from this slide,
but it's in the paper.
[62:04] The interesting new thing here,
[62:06] is that we have
this co-Cartesian operation.
[62:08] So, to inject from the left,
[62:11] we add a zero on the right.
[62:13] To inject on the right,
we add a zero on
[62:14] the left and the join operation
does the addition.
[62:17] Parceling out as an addition,
[62:19] and scaling just
as multiplication.
[62:21] So, with this definitions,
[62:23] now we get back to
where we were before.
[62:25] We have essentially using
[62:26] functions to represent
linear maps,
[62:28] but now we have
this more elegant vocabulary.
[62:33] Now, we can do something
more interesting.
[62:35] Now, we can change
our representation.
[62:37] Instead of using functions
as linear maps to represent
[62:40] linear we can use
other representations.
[62:41] Why would we want to?
[62:42] What's wrong with using
these these functions?
[62:44] It's the simplest way
to do it but has
[62:46] a problem and here's
the main one.
[62:48] It's that sometimes we need to
[62:50] extract a data kind
[62:52] of representation
from the linear map.
[62:54] So, if we get a linear map,
[62:56] it's represented by a function.
[62:57] I might need to do
something like, well,
[62:59] a couple of examples are,
[63:00] one is, if you're doing
computer graphics,
[63:04] and you're doing
a lighting and shading,
[63:06] so you got some 3D model and
[63:07] the light source,
surface properties,
[63:10] and so on, to light
a surface at a point,
[63:13] we need to know
the normal vector.
[63:15] So you got the surface,
[63:16] and you can think of the
tangent plane or normal vector,
[63:19] and we're going to take
a dot product within
[63:21] a normal vector and
the vector between my eye,
[63:23] and that point or the light
and the point, I guess.
[63:26] So, how do we get
the normal vector?
[63:30] Well, we take
the cross product of
[63:32] the two partial derivatives.
[63:35] So for that, we need a data
[63:37] representation, we need vectors.
[63:39] How do we get from a function
that we know is linear,
[63:43] to a compact data representation?
[63:45] A vector for it?
[63:47] Well, there's
a simple way to do it.
[63:48] Which is you take the function,
[63:50] as long as it's linear, you
can sample it on a basis.
[63:53] The results you get
are the vector.
[64:00] So, you take function
or the matrix.
[64:02] Take the function that
if you know is linear,
[64:05] sample it on a basis.
[64:06] What's a basis? For instance,
[64:08] take the identity
matrix, all right?
[64:10] So, the rows or columns
you think about it,
[64:12] the identity matrix,
that forms the basis.
[64:14] So, you apply the function
to each of those vectors.
[64:17] Then you accumulate the results,
[64:19] that is the Jacobian matrix.
[64:20] The data representation.
[64:21] But it's terribly expensive.
[64:24] In some settings, if
the domain of that function,
[64:28] so that's what we're on a basis
of, is high-dimensional,
[64:31] say it's a million and
that's not a typical,
[64:33] that's quite typical
for machine learning.
[64:35] So, it's in the millions.
[64:36] Then I'm going to
make a million by
[64:37] a million identity matrix.
[64:39] I got a million, what's
called one-hot vectors,
[64:41] which is zero everywhere
and a one seller
[64:43] and pump them through
this function.
[64:44] It's extremely expensive
to renew quadratic work.
[64:47] So, this is not
a viable approach.
[64:49] This is why we wouldn't
want to represent.
[64:54] If we're doing
optimization problems,
[64:56] particularly if we have
high dimensional domains,
[64:59] we would not want
to use functions or
[65:00] representation because it's just
[65:03] too expensive to
extract representation.
[65:07] Another motivation besides
computer graphics,
[65:09] is just search, is
[65:11] machine learning, deep
learning in particular.
[65:13] Want to do gradient descent,
what do we do we?
[65:15] We need a gradient vector.
[65:17] Because that's what tells
us in what direction to
[65:20] adjust the input or searching for
[65:22] a local minimum or maximum.
[65:25] So, we could for an n-dimensional
domain make n passes,
[65:29] each on a one-hot vector,
[65:31] very expensive and particularly
[65:33] expensive for gradient-based
optimization,
[65:35] which is like the most
[65:36] valuable application
of these ideas.
[65:39] So, ironically, we have a very
low dimensional co-domain.
[65:43] The result, it's one-dimensional
[65:45] if we're doing optimization.
[65:46] We have a high
function that takes
[65:48] some high dimensional
input and gives
[65:49] you an objective function value.
[65:51] One. Unfortunately, the cost of
[65:54] converting the function
representation depends on
[65:56] the dimension of the domain.
[65:58] Relies on the domain being small.
[65:59] But the domain is large,
the co-domain is small.
[66:01] So, this is a serious problem.
[66:04] So, there's a solution which is
[66:06] use matrices in the first place.
[66:08] Don't use functions to represent
[66:10] linear maps. Just use matrices.
[66:11] That's what everybody
really does. All right?
[66:14] Well, in a nice typesetting,
[66:17] there's lovely and general way
to think about that,
[66:19] which is that something
in the matrixes,
[66:22] like row columns, is
two-dimensional rectangular thing.
[66:24] Think of it as a
structure of structures.
[66:26] It's got a row structure
and a column structure.
[66:28] You know structure of structures
and those structures are
[66:30] dependent on the domain type
and the co-domain type.
[66:33] Okay, so that's
what's going on here.
[66:35] I'm not going to go
into this in detail.
[66:37] But if you define a notion
of a matrix like thing,
[66:41] in a more general setting,
[66:42] and you'd find what it
means to apply one of
[66:44] the matrix to a vector,
[66:46] and also multiply
the matrix by the vector.
[66:49] That gives us
an algebraic problem,
[66:50] two of the same form,
these five equations.
[66:53] Say that this apply
thing preserves structure.
[66:56] We can solve those equations
[66:58] and what comes out
of those equation,
[67:00] those are matrix
multiplication and so on.
[67:01] Matrix multiplication is
[67:02] a solution to an algebra problem.
[67:04] I think I will skip
over this part.
[67:11] This is just about
these three Ps of vocabulary.
[67:15] Scale, fork, and join,
[67:17] that is the vocabulary
of matrices.
[67:19] If you think about matrices,
[67:21] every matrix is
either a one by one,
[67:24] which means it's scaling
[67:26] or it's a horizontal
[67:28] or vertical juxtaposition
of matrices.
[67:31] That's not how I
was taught to think
[67:32] about matrices but I
think is a very nice way.
[67:34] If you have those three
building blocks, one by ones,
[67:36] horizontal juxtaposition
[67:37] of matrices with the same height,
[67:39] vertical juxtaposition of
matrices with the same width.
[67:42] All matrices, those
operations are
[67:45] exactly the scale,
fork, and join.
[67:49] The types guarantee
that when you stack,
[67:53] you can always stack matrices
with the same width.
[67:56] Or if you juxtapose them
[67:57] horizontally, they have
to be the same height,
[67:59] that's in the types.
Where does that come in?
[68:02] Join requires that
the co-domains are the same.
[68:05] Requires the domains
are the same.
[68:07] Now.
[68:11] So, at this point we're
talking about matrices.
[68:16] I would say, we tried functions,
[68:17] it works out very nicely.
[68:19] But, for high-dimensional
domains,
[68:21] it's too expensive to extract
the data representations.
[68:23] So, why don't we use matrices
in the first place.
[68:25] So, we can do that, but now
[68:27] an interesting question arises,
[68:28] which is if a lot of
matrix multiplication happens,
[68:31] everywhere we said composition
[68:33] that gets implemented by
matrix multiplication.
[68:36] Matrix multiplication
is associative.
[68:39] Why is matrix
multiplication associative?
[68:43] It's maybe a funny question,
[68:45] why is it associative?
[68:47] You might say, "Well,
[68:49] here's a proof that
it's associative."
[68:50] But, I want to say,
[68:51] "No, that's the hard way."
[68:53] Matrix multiplication
is associative
[68:55] because function composition is
[68:56] associative and
matrix multiplication
[68:57] correctly implements
function composition,
[69:00] when the functions are linear.
[69:01] That's a much more
direct way to think
[69:03] about compositionality and
about matrix multiplication.
[69:07] Matrix multiplication is
solution of a problem,
[69:09] which is how do you
implement correctly,
[69:12] composition of functions that are
[69:13] represented by
matrices, and then,
[69:15] answer to that or the problem
is matrix multiplication,
[69:17] the associativity follows from
[69:19] the original
motivation for making
[69:20] it the first place,
not after the fact.
[69:24] So, matrix multiplication
is associative,
[69:28] but different ways of
associate give you
[69:31] different performance,
very different performance.
[69:34] So, that means if we're
going to use matrices,
[69:37] we want to be clever
about how to associate.
[69:40] The definitions that
I showed you are not
[69:45] at all biased to how
[69:46] to do the compositions
of linear maps.
[69:49] Whatever composition structure
you give originally,
[69:52] it's going to maintain
that structure.
[69:54] Some of those composition will be
[69:57] efficient and other ways
that you might have,
[70:00] but didn't compose it,
would be a more efficient,
[70:02] more or less efficient, So,
[70:05] what we'd like to do,
though is not rely on
[70:07] the programmer to
write the compositions
[70:09] in a way that's efficient for
[70:10] automatic differentiation
because a program
[70:12] has a different thing
he's trying to achieve
[70:13] which is clarity and modularity.
[70:15] The compiler should then,
[70:17] figure out how to
make it efficient,
[70:19] not the programmer, because
those two are at odds with
[70:20] each other efficiency and
[70:21] modularity are odds
with each other.
[70:23] So, fortunately there's
a simple way to,
[70:27] I don't think it's
simple, Thoughtially,
[70:28] there's a way to
take any composition
[70:31] of matrices and generate
[70:33] the optimal capital re-associate
[70:36] into something that's
computationally optimal.
[70:38] While it's not simple, there
are couple of algorithms.
[70:40] One's the n-cubed algorithm that
[70:42] does dynamic
programming and then,
[70:43] there are these much cleverer,
[70:45] subtler algorithms to
do in log in time.
[70:49] Where does this
smarts going to go?
[70:51] Here's the cool thing,
the cost of
[70:55] matrix multiplication
depends only on
[70:57] the dimensions of
the matrix, not the values.
[70:59] If you want to be really
clever and talk about
[71:01] special matrices
that you in a way,
[71:03] you can predict,
they're going to be
[71:03] zeros and that's not the case.
[71:04] Let's say, you're not talking
about special matrices.
[71:07] So, the optimal composition
[71:10] as multiplication of matrices
[71:12] depends only on the dimensions.
[71:13] Their dimensions depends only on
[71:15] the types in this setting.
[71:18] So, the dimensions as part of
[71:19] the types and that's
compiled time information,
[71:22] because it's a statically
typed language.
[71:23] So, we can do the optimal
[71:25] re-association at compiled time,
[71:26] not at run-time,
that's a huge win.
[71:30] There are two common
associations that are made.
[71:34] If you associate all the
composition to the right,
[71:36] you get what's called
forward mode ND,
[71:38] you associate on the left
what's called reverse mode AD.
[71:43] For any kind of
[71:45] gradient-based optimization and
[71:47] reverse AD is
significantly better.
[71:48] How much better? It depends
on the domain of dimension.
[71:51] For machine learning
these days it's huge,
[71:53] it's several millions.
[71:56] So, how can we do
this optimal reassociation?
[72:00] Well, as I said, there
are these algorithms,
[72:01] but there's
another way, which is,
[72:04] if we know, if we just
assume that the result,
[72:08] that the final codomain,
[72:09] the final result type
is low-dimensional.
[72:11] Particularly if it's
one-dimensional,
[72:13] then I think it's the case
[72:14] and I don't know this for a fact,
[72:15] I think it's the case
that full left association
[72:18] in the large reverse node is
always the best strategy.
[72:21] I'm not sure that's true,
[72:23] I am sure that it corresponds
[72:25] exactly what's in
a machine learning,
[72:26] that's a back propagation does.
[72:28] So, how can we
think about getting
[72:31] this left association
automatically
[72:34] and there's this
nice technique which
[72:36] is related something it's
[72:39] called continuation
passing style.
[72:41] So, the idea is the following:
[72:43] If I have a function
like going from a to b,
[72:45] this can be linear maps
or regular functions,
[72:48] so on, I can represent it
by something that says,
[72:51] "If I know how to consume b,
[72:53] I can give you a way
to consume a."
[72:57] So, these two are
equivalent representations,
[73:01] you can transform either one to
[73:02] the other without
loss of information.
[73:04] So, if I have a direct way
of going from a to b,
[73:06] there is an indirect
representation that says,
[73:08] "If I know what I
wanted to do with b,
[73:11] then I would know what
I wanted to do with a,
[73:13] which is apply this thing
and then consume the b."
[73:16] So, given an a, we're
going to compute
[73:17] the b and then consume it.
[73:19] So, that's the meaning,
given a function f,
[73:22] we kind of interpret
f. So, that's f,
[73:26] we interpret it by as something
that composes with f on
[73:29] the right and some consumer
[73:32] of the resulting b value
on the left.
[73:34] That's a continuations come.
[73:36] If you make this transformation,
[73:39] package it up to the category,
[73:41] then no matter
what composition style
[73:43] you used in the
original expression,
[73:45] it's going to turn into fully
[73:46] left associated and
the representation.
[73:51] You need a way to kick
it off and that's just
[73:53] by supplying the
identity continuation.
[73:56] Then, one point I want to
make is, I think a very,
[74:00] very big performance win
[74:02] here from this
perspective, which is,
[74:04] remember we're going to
be computing derivatives
[74:06] of a function at a point
[74:07] that's input and when f
is higher-dimensional,
[74:11] say in its domain and co-domain,
[74:13] on its input and output,
then that result,
[74:15] is going to be something large,
[74:18] therefore, represented
on matrices is going
[74:20] to be two dimensional,
it's going to be
[74:21] quadratically large.
A lot of times, these
[74:24] internal matrices are
quite sparse, it could be
[74:27] the zero matrix that actually
happens fairly frequently.
[74:30] So, very sparse, sparse
means how many elements,
[74:34] well the density is how many
elements are non-zero.
[74:37] Zero is the sparsest you can get,
[74:39] there's also quite common
is the identity matrix,
[74:41] well that's also extremely
sparse and you think
[74:43] that's the density of
[74:44] the square root of the
number of elements.
[74:47] So, these matrices can be very
[74:49] sparse and then that
[74:51] means that you're wasting
a lot of computation,
[74:53] if instead of just
computing them,
[74:55] we compute them composed
[74:56] with a continuation
that we're getting in,
[74:59] then we can bypass
[75:00] the construction of
the matrices entirely,
[75:03] then we get very
small computations.
[75:05] I'm not sure, but I think this
is probably a very large,
[75:08] when performance wise, it's
also very easy to implement.
[75:13] >> So, Conal, it's
only 15 minutes
[75:15] left. Make room for questioning.
[75:17] >> Yes, absolutely,
yes, thank you.
[75:19] So, this slide and
then a couple of
[75:21] more is the punchline.
[75:23] >> Yes.
[75:25] So, this is a
continuation category.
[75:27] As I say, we've got
[75:28] some underlying category,
totally arrow,
[75:30] and we've got some ultimate
result type r. So,
[75:32] this r is going to be
the ultimate codomain.
[75:34] We're just going to pack it up
[75:36] this notion of continuation,
[75:37] and now we set up
another algebra problem,
[75:40] which is how do we interpret
[75:42] or say a function
here in linear map?
[75:46] In this category, well, we
just do what I said before,
[75:48] it's just we're
going to compose on
[75:50] the right with the function.
[75:51] The left is going to
be the continuation.
[75:53] Now, we say cont has
to preserve structure.
[75:56] Meaning those same
five equations,
[75:58] always the same
five equations it maps.
[75:59] It did compositions to
compositions and so on.
[76:02] When we solve
this algebra problem
[76:04] with the help of
some isomorphism,
[76:06] we get this definition.
[76:08] So, this definition is
[76:10] a reverse-mode
automatic differentiation,
[76:13] this code is reverse-mode.
[76:14] It's much, much simpler
[76:15] than anything I've
seen in literature.
[76:17] Literature talks about graphs
and talks about mutations,
[76:21] partial derivatives, none
of that is necessary.
[76:25] Okay. All that's necessary is
[76:27] this little continuation trick,
[76:28] and that trick is annotated
on my differentiation.
[76:30] It's just something that
would be in a library.
[76:31] You're programming
with this vocabulary,
[76:33] we're going to have a library.
[76:34] It's going to have
continuation and it becomes
[76:35] useful for all kinds of things.
[76:37] So, this is the reverse-mode AD.
[76:42] It's a general AD category
parameterized by
[76:45] a continuation transform
version of matrices.
[76:49] >> Triple M subscripts.
[76:51] >> Yes. So, matrices is
indexed by the scalar.
[76:59] Continuation is indexed by, well,
[77:01] in this case, matrices and
the final result type,
[77:03] and you plug that into
the general AD thing
[77:06] which is no more complicated
than the specialized AD.
[77:08] So, this is a reverse-mode
AD without tears.
[77:11] Every time I read a paper
[77:13] on reverse-mode AD,
I want to cry.
[77:14] So I think that's how they
came up with this title.
[77:17] Okay. All right.
[77:20] Now, this is the final
essential trick.
[77:23] This is what gets backprop.
[77:25] It's a more specialized version
[77:27] of reverse-mode AD that's
a little more efficient.
[77:30] Here's the key idea.
[77:32] If you look at linear
transformations
[77:36] from a vector space
to its scalar field.
[77:39] So this, you might be r the
million and s will be r,
[77:44] so it's the underlying
scalar field.
[77:45] So, in general, you can
[77:46] have linear
transformations between
[77:47] any two vector spaces with
the same scalar field.
[77:50] But if the result of
[77:52] the codomain is the scalar
field itself, then u,
[77:55] derivatives from u to
that, scale to that,
[77:57] that's called a dual vector,
[77:59] and there's this lovely duality
[78:01] property in linear algebra.
[78:03] You will see it in terms
of matrix transposition.
[78:06] Matrix transposition is all about
[78:07] duality. Here's the cool thing.
[78:10] If you're interested in
[78:12] linear maps that result
in the scalar field,
[78:15] they're isomorphic to u itself.
[78:17] If u is finite-dimensional.
[78:21] Every one of these linear maps
[78:23] has a particular form which is
[78:24] the dot product with a vector,
[78:27] and then it's waiting
for its second argument.
[78:31] Now, here's the cool thing.
[78:33] If we use that continuation
representation.
[78:36] So, this is the punch line.
[78:39] We have linear maps from a to b.
[78:41] We use the continuation
transformation
[78:43] and we get b consumer
[78:44] to an a consumer,
linear consumers.
[78:47] But these guys are isomorphic
to b and a itself.
[78:50] So, it represent linear
maps from a to b in
[78:53] this continuation form with s,
[78:56] the scalar field, but we can
[78:58] represent that continuation form
[78:59] by just functions from b to a.
[79:04] Again, there's
a very simple specification
[79:07] that relates the
continuation to the dual.
[79:10] Again, we set up
the algebra problem
[79:15] with five equations
and we solve it.
[79:17] Now, we get this
incredibly lovely form.
[79:20] This gives you the implementation
of a dual category.
[79:26] Now, we can see, wow,
[79:28] the identity is the identity,
[79:29] composition is
the flip composition,
[79:32] the extractors are the injectors,
[79:34] the injectors are the extractors,
[79:36] fork is join and join is fork,
[79:38] and scale is itself.
[79:40] If you think of these operations,
[79:43] fork joining scale as being
matrix building operations,
[79:46] then what we've done
is we've described
[79:47] that to the transposition
of matrices.
[79:50] So, here's backpropagation.
[79:56] So, no mutations,
[79:58] no variables, no graphs,
no partial derivatives.
[80:02] It's just the general AD
[80:05] where we use the dual
of additive functions,
[80:09] and no matrix compositions here.
[80:12] It's extremely efficient.
[80:15] Then, I just have
a bunch of examples,
[80:18] but I think I'll pause
and take questions.
[80:20] If there are questions
about examples,
[80:21] I'll show them and
otherwise it's not.
[80:22] >> Why was the dual
of scale to scale?
[80:24] >> Yes. That's funny.
[80:26] So, the dual is not the inverse.
[80:28] For the inverse, if you want
[80:30] to scale it like the inverse.
[80:31] So, It's really-
[80:33] >> I think of the transpose.
[80:34] >> I can give you
a variety of answers.
[80:37] If you want think about
matrices and you think
[80:39] the transpose are one
by one, you get itself.
[80:42] But I'm not satisfied with
that answer because it
[80:46] leaves the question
of why do you use
[80:48] transposition in the first
place? What does it mean?
[80:51] What does transposition have
to do with linear maps?
[80:54] The duality and
[80:56] the continuations
instructions that I showed
[80:58] you are exactly what
motivates transposition.
[81:01] So, I can say it's because
[81:04] transposition preserves
one by one matrices,
[81:07] but that's a backwards answer
from my perspective.
[81:10] Transposition is about duality,
[81:12] not duality is about
transposition.
[81:16] >> So, I learned about automatic
differentiation through
[81:19] the framework of
the commutative ring
[81:21] of dual numbers over r. Now,
[81:24] I was wondering if you
could relate to my ideas of
[81:26] your work to the language
of dual numbers.
[81:28] It seems to me that your
fork idea of take combining
[81:31] functions derivative is exactly
[81:33] appending a dual component
to a function.
[81:35] >> Yes. So, as I said there,
[81:38] commonly AD is done in
[81:39] two flavors, forward
and reverse-mode.
[81:43] Forward-mode is fairly easy and
[81:46] convenient to express in a lot of
[81:47] programming languages
especially if
[81:48] you have operator overloading.
[81:50] A way to do that is to
everywhere you have numbers,
[81:53] instead use something that's
[81:54] sometimes called dual numbers,
[81:55] which is a pair of a number
and a second number.
[81:58] The second number
represents the derivative.
[82:00] So, it's very much like you
see in my original type by
[82:02] the function that
gives you a pair
[82:03] of number in a linear map.
[82:05] >> Exactly, yes.
[82:06] >> Okay. So, yes,
[82:08] you can explain the
dual number idea
[82:10] in terms of this
categorical form.
[82:12] But of course, if it's
a pair of numbers,
[82:16] then you can only talk about
[82:17] differentiation of
scalar function.
[82:19] All right. So, it's
much, much less general.
[82:22] It's also wrong the way that
forward-mode AD is done.
[82:27] Well, it's correct only
because people are careful.
[82:30] If you look at forward-mode,
[82:33] usually is you end
[82:35] up taking functions from
dual numbers to dual numbers.
[82:37] A value anti-derivative to
a new value anti-derivative.
[82:41] But that transformation of
[82:44] a number to derivative
to a number derivative,
[82:46] the only some of
them are sensible.
[82:48] Because the value out cannot
depend on the derivative in,
[82:54] and yet the types of it can.
[82:57] So that to me is a fundamental
flaw in this whole idea
[83:01] of dual numbers and the whole
way that a forward-mode AD.
[83:04] Meaning you have to be careful
[83:07] that these functions are
dual number to dual numbers.
[83:09] Some of them represent
sensible differentiation,
[83:12] some of them don't.
[83:13] If you refactor it and say, "No,
[83:15] the value out cannot
depend on the Delta in."
[83:19] you get my representation.
[83:21] Which as you take
a single number in,
[83:24] you get out a single number as
[83:26] the value and another function
from a Delta to a Delta.
[83:30] So, if that representation,
[83:31] the number at
the value out cannot
[83:33] depend on the derivative in. Yes.
[83:37] >> Makes sense.
[83:38] >> So, that's something I
didn't appreciate until I asked
[83:41] myself exactly the same
question because I did
[83:42] this forward mode as well,
[83:44] and I wondered, "Do these
two relate to each other?"
[83:46] That's when I
realized, "Oh, this is
[83:47] really unfortunate aspect
of the forward mode."
[83:51] >> Let' see.
[83:54] If there are no other
questions, I'd want more.
[83:55] Could you go back to your slide,
[84:01] see the axioms for a category,
[84:03] in a Cartesian category.
[84:04] Immediately after you say
that your implementation of
[84:09] your D hat factor
satisfies this rise.
[84:14] >> Yes, it does maybe.
[84:16] >> Yes, okay. So, under
the next slide, right?
[84:18] You have your implementation
of D hat, right?
[84:21] >> Yes.
[84:21] >> I was wondering from
[84:23] what axiom on the previous slide
[84:24] does the Leibniz rule come from?
[84:26] >> Oh, that's a different.
[84:27] >> It doesn't. Yes, well,
[84:28] that's the numerical category.
[84:30] >> Yes, exactly.
Exactly. So, it's
[84:33] an unfortunate thing about
[84:34] the way differentiation is
taught in calculus classes,
[84:37] and the way that symbolic
differentiation is done,
[84:40] and now automatic
differentiation is done.
[84:41] There's a really unfortunate
thing which is that,
[84:43] you look at the rules
you learned in,
[84:45] rules I learned anyway
in differential calculus
[84:47] and it said things like,
[84:48] derivative of a sine is cosine,
but it didn't say that.
[84:50] It said that the derivative
of sine u is cosine udu.
[84:53] All right. Your cosine u
is minus sine udu.
[84:58] So, for times
the derivative of u.
[85:01] So, and then multiplications,
[85:04] derivative of u times v
is the derivative of u,
[85:06] the derivative of a product uv
is the derivative of
[85:09] u times v plus the derivative
of v times u. All right.
[85:11] Every one of those rules
[85:13] has the Chain rule
embedded in it.
[85:15] Every one of those rules is
[85:17] the Chain rule plus another rule.
[85:19] So, by using this categorical
approach we said no,
[85:22] the derivative of,
is in same sine,
[85:24] derivative of sine
u is cosine udu,
[85:26] derivative of sine is cosine,
[85:28] plus we have the Chain rule.
[85:30] So, we don't need to have
[85:31] these kind of complicated rules,
[85:33] every one of which has
the Chain rule embedded in it.
[85:39] >> Can you say anything about,
[85:41] did you exploits these insights,
[85:45] better circuits or was
there [inaudible].
[85:48] >> Yes, yes. Yes, yes.
[85:50] So, well, I'll tell you
what I do and you can tell
[85:51] me that if I'm exploiting
or what you don't mind.
[85:54] So, as this plugin I have,
[85:56] it's a plugin in Haskell
Compiler lets call it GFC.
[85:59] >> All right.
[85:59] >> I thought there's a GFC,
it's a Haskell Compiler.
[86:01] I wrote a plugin in
it that transforms
[86:04] the internal
representation which is
[86:06] the type Lambda calculus
called core.
[86:10] Transforms the regular
Haskell code into
[86:13] categorical form and then
[86:15] instantiates it with respect to
[86:16] whatever category you want,
[86:18] for instance,
differentiable functions.
[86:19] There are rewrite rules,
[86:21] most of which are just
specified and just
[86:24] Haskell code and the
rewrite rule sub-language.
[86:26] Those rewrite rules are
true of all categories,
[86:29] if they involve this category
language or Cartesian,
[86:32] if they involve
a Cartesian and so on.
[86:33] So, a lot of optimizations
in there that work for
[86:36] all interpretations, including
differentiable functions.
[86:39] >> Do you have any ideas
that you've been taught?
[86:42] Say, different circuits and
compiled it within Haskell.
[86:47] >> Yes. So, what I actually did.
[86:49] >> I actually tried it
keeping it in circuit but.
[86:51] >> Yes, well, I don't
mind saying circuits.
[86:54] This whole work was was motivated
[86:56] by compounding
Haskell to hardware.
[86:58] That was my job a few years ago.
[86:59] I worked at a hardware
company that had
[87:02] this really cool dynamically
reconfigurable hardware.
[87:07] So, it's like an FPGA
but it reconfigured
[87:09] it two billion times a second
that are like once a year.
[87:12] So, reconfigured as it ran.
[87:14] So ran it to billion
times a second,
[87:17] two gigahertz, and it
[87:18] reconfigured itself
at two gigahertz.
[87:20] There's a huge win from doing
[87:21] this kind of
runtime optimization.
[87:24] So, my job was.
[87:25] >> Do we see all this
addition come in?
[87:27] >> Originally for
things like FPGA
[87:30] it's useful like
running in a router,
[87:34] in checking your packets for
Russian virus or whatever.
[87:37] >> This would be
the reconfiguration.
[87:39] What would require
the reconfiguration
[87:41] to have in circuits?
[87:42] >> Reconfiguration
in this setting
[87:46] three-dimensional
circuits are much
[87:49] more efficient than
two-dimensional circuits,
[87:50] can be, I mean.
[87:51] Pretty much on
circuit can be much
[87:52] more efficient that
two-dimensional circuits.
[87:53] Why? Because most of
the power and time
[87:56] taken up during computation
is moving electrons.
[87:59] They have to move from
one place to another.
[88:02] Pads in three-dimensions
are much,
[88:03] much shorter than
a two-dimension.
[88:04] So, if you can make
a three-dimensional FPGA,
[88:06] you can get much
better performance.
[88:08] But it's really hard to make
a three-dimensional FPGA.
[88:10] So, this fellow, Steve Teigen,
[88:12] has a wonderful idea,
this inside,
[88:13] this man is brilliant
and I knew like
[88:15] 30 seconds I wanted to
work with this man.
[88:18] He realized that I can implement
[88:21] a three-dimensional FPGA by
[88:22] implementing one dimension
in time instead of space.
[88:26] That's the point of
dynamic reconfigurability.
[88:30] So, you get much, much shorter
pathways in space-time,
[88:33] and the architecture was called
[88:34] space-time, and it really,
[88:35] honest to God, is based on
[88:37] Minkowski's mathematics
of relativity.
[88:41] Minkowski used to clean up
the math that Einstein used.
[88:45] So, my job was, initially,
[88:48] it would be FPGA applications
[88:49] but eventually it'll
be all computation.
[88:52] How are we going to
program this thing?
[88:54] It's not going to be in
any sequential language,
[88:55] every sequential language
is going to be deeply
[88:57] acknowledged because this
is massively parallel,
[88:59] we want to be doing
[89:00] millions of operations
simultaneously.
[89:03] Meaning, two billion, million
operations per second.
[89:10] So, it's not going to be
any sequential language.
[89:12] But a purely functional language
[89:14] doesn't have
this sequential bias.
[89:15] So, how do we compile the
purely functional language into
[89:18] a three-dimensional FPGA?
That was my job.
[89:22] I hit on this solution which
[89:24] is I realized one day that you
[89:26] could describe circuits using
[89:28] this language that
I've shown you.
[89:29] This language is a language
[89:31] that can be used to
describe circuits.
[89:33] Hardware engineers don't
do that but you could.
[89:36] Then, I remembered, wow,
this 1980 result that says
[89:39] the type Lambda calculus is
[89:41] equivalent to this vocabulary,
[89:42] and Haskell is equivalent to
the type Lambda calculus.
[89:44] So, if I go from Haskell,
put it through GFC,
[89:46] and go to its internal language,
[89:48] which is a very small
Lambda calculus,
[89:50] I take that internal language and
[89:51] transform it into the
language of categories,
[89:54] and then instead of
instantiating with
[89:55] usual one by all
computable functions,
[89:57] I do the category of circuits
[89:58] of massively parallel circuits.
[90:01] Then, I represent
that in terms of
[90:03] the graphs as a rendering
of that representation,
[90:05] and then I generate Verilog code.
[90:07] Eventually, we were going
to do things that are
[90:09] better than Verilog but
that's where I started.
[90:11] That really was
my original motivation.
[90:13] But then one day I
realized because I'd
[90:15] worked on ADL a while ago,
[90:17] I realized that the categorical
approach is a much,
[90:22] much better way to think
[90:23] about automatic
differentiation, so.
[90:25] All right. I think that's
a good stopping place.
[90:28] >> Yes, thank you.
[90:32] >> I'll be around.
