CHAD for Expressive Total Languages

Abstract

We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) to total functional programming languages with expressive type systems featuring the combination of - tuple types; - sum types; - inductive types; - coinductive types; - function types. We achieve this by analysing the categorical semantics of such types in $\Sigma$-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward and reverse mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

arXiv commentUnder review at MSCS

References in corpus (12)

• A Simple Differentiable Programming Language
• Automatic Differentiation in PCF
• Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
• Non-canonical isomorphisms
• Dialectica models of type theory
• In Search of Effectful Dependent Types
• A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
• Semantic Factorization and Descent
• Higher Order Automatic Differentiation of Higher Order Functions
• Pseudoalgebras and non-canonical isomorphisms
• Functorial String Diagrams for Reverse-Mode Automatic Differentiation
• Descent Data and Absolute Kan Extensions

Cited by in corpus (4)

• Higher Order Automatic Differentiation of Higher Order Functions
• Efficient CHAD
• Automatic Differentiation for ML-family languages: correctness via logical relations
• Topological lax comma categories