We introduce Combinatory Homomorphic Automatic Differentiation (CHAD), a principled, pure, provably correct define-then-run method for performing forward- and reverse-mode automatic differentiation (AD) on programming languages with expressive features. It implements AD as a compositional, type-respecting source-code transformation that generates purely functional code. This code transformation is principled in the sense that it is the unique homomorphic (structure-preserving) extension to expressive languages of Elliott's well-known and unambiguous definitions of AD for a first-order functional language. Correctness of the method follows by a compositional logical-relations argument that shows that the semantics of the syntactic derivative is the usual calculus derivative of the semantics of the original program. In their most elegant formulation, the transformations generate code with linear types. However, the code transformations can be implemented in a standard functional language lacking linear types: while the correctness proof requires tracking linearity, the actual transformations do not. In fact, even in a standard functional language, we can get all the type safety that linear types give us: we can implement all linear types used to type the transformations as abstract types by using a basic module system. In this paper, we detail the method when applied to a simple higher-order language for manipulating statically sized arrays. However, we explain how the methodology applies, more generally, to functional languages with other expressive features. Finally, we discuss how the scope of CHAD extends beyond applications in AD to other dynamic program analyses that accumulate data in a commutative monoid.

翻译：我们提出组合同态自动微分（CHAD），这是一种用于对具有表达性特征的编程语言执行前向和反向模式自动微分（AD）的原则性、纯函数式且可证明正确的先定义后运行方法。它将AD实现为一种组合的、保持类型的源代码变换，生成纯函数式代码。该代码变换具有原则性，因为它是对Elliott在一阶函数式语言中关于AD的著名且无歧义定义的唯一同态（保持结构）扩展到表达性语言。该方法的正确性通过组合逻辑关系论证得以证明，表明语法导数的语义是原始程序语义的通常微积分导数。在其最优雅的表述中，这些变换生成具有线性类型的代码。然而，这些代码变换可以在缺乏线性类型的标准函数式语言中实现：虽然正确性证明需要追踪线性性，但实际变换并不需要。事实上，即使在标准函数式语言中，我们也能获得线性类型所提供的全部类型安全性：通过使用基本模块系统，我们可以将用于类型化这些变换的所有线性类型实现为抽象类型。本文详细阐述了该方法应用于操作静态大小数组的简单高阶语言时的情形，并解释了该方法如何更普遍地适用于具有其他表达性特征的函数式语言。最后，我们讨论了CHAD的应用范围如何超越自动微分领域，扩展到在交换幺半群中累积数据的其他动态程序分析。