1 results
CHAD for expressive total languages
-
- Journal:
- Mathematical Structures in Computer Science / Volume 33 / Issue 4-5 / April 2023
- Published online by Cambridge University Press:
- 14 July 2023, pp. 311-426
-
- Article
-
- You have access
- Open access
- HTML
- Export citation
-
We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vákár (2021). ESOP, 607–634; Vákár and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) 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 analyzing 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.
