CHAD: Combinatory Homomorphic Automatic Differentiation

TL;DR

CHAD introduces a principled, correct, and compositional method for automatic differentiation in expressive programming languages, generating purely functional code with formal correctness guarantees.

Contribution

It presents a homomorphic, source-code transformation approach for AD that is applicable to expressive languages and maintains correctness through a logical-relations argument.

Findings

Generates code with linear types or in standard functional languages.

Proves correctness by showing the derivative semantics match calculus derivatives.

Applicable to higher-order languages manipulating statically sized arrays.

Abstract

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.