# CHAD for Expressive Total Languages

arXiv: https://arxiv.org/abs/2110.00446 · HTML: https://mlsanity.com/paper/2110.00446/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Oct 2021.

## Built on by (most cited first, 1 of 1)

- [Position: Categorical Deep Learning is an Algebraic Theory of All Architectures](https://mlsanity.com/paper/2402.15332/) (2024)

## Abstract (arXiv)

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.