Programming Backpropagation with Reverse Handlers for Arrows
This work offers a new, abstract, and high-level approach to neural network design and implementation for programming language researchers and practitioners, but it is primarily a theoretical contribution without empirical validation.
The paper introduces a programming language with categorical semantics that uses algebraic effects and handlers for arrows to construct neural networks symbolically and assign backpropagation implementations via reverse handlers. It provides a rigorous foundation with type system, operational semantics, and soundness/adequacy theorems.
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 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.