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.

Under review at MSCS

References in corpus (7)

• A Simple Differentiable Programming Language
• Automatic Differentiation in PCF
• Dialectica models of type theory
• A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
• In Search of Effectful Dependent Types
• Higher Order Automatic Differentiation of Higher Order Functions
• Functorial String Diagrams for Reverse-Mode Automatic Differentiation

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