Programming Backpropagation with Reverse Handlers for Arrows

TL;DR

This paper presents a new programming language with categorical semantics that uses algebraic effects and handlers for arrows to symbolically construct neural networks and implement backpropagation through reverse handlers.

Contribution

It introduces reverse handlers for arrows and a formal categorical framework for neural networks, enabling high-level symbolic network descriptions with flexible backpropagation implementations.

Findings

Developed a type system and operational semantics for the language.

Introduced reverse handlers for backpropagation in neural networks.

Provided a categorical semantics with soundness and adequacy proofs.

Abstract

We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algebraic effects, and to assign implementations -- such as backpropagation computations -- to them via handlers. The advantage of this language design is that network descriptions become abstract and high-level, while implementations can be flexibly assigned to networks. We establish a rigorous foundation for our language by developing a type system, an operational semantics, a categorical semantics, and soundness and adequacy theorems. The technical core is the introduction of \emph{reverse handlers}, a novel handler mechanism for arrows for implementing backpropagation, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.