Relative monads provide a controlled view of computation. We generalise the monadic metalanguage to a relative setting and give a complete semantics with strong relative monads. Adopting this perspective, we generalise two existing program calculi from the literature. We provide a linear-non-linear language for graded monads, LNL-RMM, along with a semantic proof that it is a conservative extension of the graded monadic metalanguage. Additionally, we provide a complete semantics for the arrow calculus, showing it is a restricted relative monadic metalanguage. This motivates the introduction of ARMM, a computational lambda calculus-style language for arrows that conservatively extends the arrow calculus.
翻译:相对单子为计算提供了受控的视角。本文将单子元语言推广至相对设置,并给出了具有强相对单子的完整语义。基于这一视角,我们推广了文献中已有的两种程序演算。我们提出了用于分级单子的线性-非线性语言LNL-RMM,并通过语义证明其是分级单子元语言的保守扩展。此外,我们为箭头演算提供了完整语义,证明其是一种受限的相对单子元语言。这促使我们引入ARMM——一种用于箭头的计算λ演算风格语言,该语言保守地扩展了箭头演算。