由单子或共单子引起的计算效应的模式
Patterns for computational effects arising from a monad or a comonad
摘要：
本文提出了基于等式的逻辑证明一阶性质的程序设计语言涉及效果。我们提出了两个对偶推理系统模式，可以实例化与单子或comonads，以用于证明不同的效果的属性。第一种模式提供了可以在单子的Kleisli范畴和相关的comonad的coKleisli范畴中解释的推理规则。第二种模式以双重方式提供了推理规则，这些规则可以在comonad的coKleisli范畴和相关monad的Kleisli范畴中解释。该逻辑结合了一个3层效应系统，用于由纯项和另外两种称为“构造器/观察器”和“修改器”的效应组成的项，以及一个2层系统，用于“最大效应”和“强”方程。每个模式都提供了处理任何monad（分别为comonad）的通用规则，并且可以为每个效果扩展特定的规则。本文提出了两个用例：带有异常的语言（使用标准的一元语义）和带有状态的语言（使用不太标准的共元语义）。最后，我们证明了所得到的状态推理系统是Hilbert-Post完备的。
英文摘要：
This paper presents equational-based logics for proving first order properties of programming languages involving effects. We propose two dual inference system patterns that can be instanciated with monads or comonads in order to be used for proving properties of different effects. The first pattern provides inference rules which can be interpreted in the Kleisli category of a monad and the coKleisli category of the associated comonad. In a dual way, the second pattern provides inference rules which can be interpreted in the coKleisli category of a comonad and the Kleisli category of the associated monad. The logics combine a 3-tier effect system for terms consisting of pure terms and two other kinds of effects called 'constructors/observers' and 'modifiers', and a 2-tier system for 'up-to-effects' and 'strong' equations. Each pattern provides generic rules for dealing with any monad (respectively comonad), and it can be extended with specific rules for each effect. The paper presents two use cases: a language with exceptions (using the standard monadic semantics), and a language with state (using the less standard comonadic semantics). Finally, we prove that the obtained inference system for states is Hilbert-Post complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
