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.

翻译：本文提出一种新的编程语言及其范畴语义，旨在代数效应与箭头处理器的框架内设计与实现神经网络。我们的语言能够以与代数效应相同的方式符号化构建神经网络，并通过处理器为其分配实现（例如反向传播计算）。该语言设计的优势在于网络描述变得抽象且高层次，同时实现可以灵活地分配给网络。我们通过开发类型系统、操作语义、范畴语义以及可靠性与充分性定理，为本语言建立了严格的理论基础。其技术核心在于引入反向处理器——一种用于实现反向传播的新型箭头处理器机制，并结合在反向微分限制范畴（RDRC）上强前幺半群的新代数结构，其弦图形式为神经网络提供了形式化的图形语法与语义。