一句话：提出 Arrow 的逆向处理器与范畴语义，使神经网络可符号化构造并通过处理器实现反向传播。
本文在 Arrow 的代数效应与处理器框架内设计并实现神经网络，提出一种新语言及其范畴语义。网络可像代数效应一样被符号化构造，反向传播等具体实现则通过处理器灵活指派，从而让网络描述保持抽象、高层。作者建立了类型系统、操作语义与范畴语义，并证明可靠性与完备性（soundness and adequacy）。技术核心是面向 Arrow 的逆向处理器（reverse handlers），以及反向微分限制范畴（RDRC）上强 promonads 的新代数；其弦图为神经网络提供形式化图形语法与语义。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-18090,
title = {Programming Backpropagation with Reverse Handlers for Arrows},
author = {Takahiro Sanada and Keisuke Hoshino and Kenshin Hirai and Shin-ya Katsumata},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828704}
}