一句话：提出类型系统追踪程序局部观察到的代数效应方程，避免全局平凡理论，支持可靠灵活的推理与优化。
代数效应可由基本操作及操作间方程描述，但许多有趣的效应处理器并不满足这些方程。现有方法通常假定平凡理论，从而牺牲推理能力与安全性。本文提出局部代数效应理论：类型系统跟踪程序子部分中实际观察到的方程，而非要求全局方程成立。由此得到既可靠又灵活的效应逻辑，使不同子程序可局部采用不同方程理论，并为实用优化与推理工具奠定基础。摘要未报告具体实现或实验评估，贡献主要在理论框架与类型规则设计。
Abstract Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimisations and reasoning tools.