Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Tom Smeding, Matthijs Vákár
Abstract
Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent value, dual-numbers reverse-mode AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis used a custom operational semantics for which it is unclear whether it can be implemented efficiently. We take inspiration from their use of linear factoring to optimise dual-numbers reverse-mode AD to an algorithm that has the correct complexity and enjoys an efficient implementation in a standard functional language with support for mutable arrays, such as Haskell. Aside from the linear factoring ingredient, our optimisation steps consist of well-known ideas from the functional programming community. We demonstrate the use of our technique by providing a practical implementation that differentiates most of Haskell98. Where previous work on dual numbers reverse AD has required sequentialisation to construct the reverse pass, we demonstrate that we can apply our technique to task-parallel source programs and generate a task-parallel derivative computation.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext dbbef623-e1a1-40b0-9ba8-6c872ed6eda6Cited by top-tier papers4
- On the Correctness of Automatic Differentiation for Neural Networks with Machine-Representable ParametersWonyeol Lee, Sejun Park, Alex AikenICML 2023 · 6 citations
- Efficient CHADTom Smeding, Matthijs VákárPOPL 2024 · 6 citations
- ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable ProgramsMathieu Huot, Alexander K. Lew, Vikash K. Mansinghka, Sam StatonLICS 2023 · 5 citations
- JAX Autodiff from a Linear Logic PerspectiveGiulia Giusti, Michele PaganiPOPL 2026
Builds on8
- A simple differentiable programming languageMartín Abadi, Gordon D. PlotkinPOPL 2020 · 49 citations
- Automatic differentiation in PCFDamiano Mazza, Michele PaganiPOPL 2021 · 47 citations
- Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiationFaustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis et al.POPL 2022 · 27 citations
- Backpropagation in the simply typed lambda-calculus with linear negationAloïs Brunel, Damiano Mazza, Michele PaganiPOPL 2020 · 24 citations
- Purity of an ST monad: full abstraction by semantically typed back-translationKoen Jacobs, Dominique Devriese, Amin TimanyOOPSLA 2022 · 13 citations
Related papers
- AD for an Array Language with Nested ParallelismRobert Schenck, Ola Rønning, Troels Henriksen, Cosmin E. OanceaSC 2022 · 11 citations
- You Only Linearize Once: Tangents Transpose to GradientsAlexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson et al.POPL 2023 · 13 citations
- Reverse-mode automatic differentiation and optimization of GPU kernels via enzymeWilliam S. Moses, Valentin Churavy, Ludger Paehler, Jan Hückelheim et al.SC 2021 · 50 citations
- Compositional Taylor expansion in cartesian differential categoriesAymeric WalchLICS 2025
- ParDiff: Efficiently Parallelizing Reverse-Mode Automatic Differentiation with Direct IndexingShuhong Huang, Shizhi Tang, Yuan Wen, Huanqi Cao et al.PPoPP 2026
