一句话：提出可对任意计算泛化的 HM 多态类型系统，证明代数效应与处理器的可靠性，无需值限制。
本文研究 call-by-value 下代数效应与处理器的多态类型安全性，尤其是值限制的必要性。传统 Hindley–Milner 多态在存在引用单元、续延等计算效应时，若泛化任意计算会破坏可靠性，因此通常只泛化值。作者给出一个直接、可靠的 HM 多态类型系统，允许对任意计算做类型变量泛化，并证明其可靠性；证明在 Twelf 中机器化验证。随后分析效应处理器相对于状态效应的表达能力：作者猜想仅靠处理器无法表达引用单元，但证明它能模拟动态作用域状态，表明动态绑定也不需值限制。
Abstract We present a straightforward, sound, Hindley–Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley–Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.