论文标题
是什么使一个强大的单调?
What Makes a Strong Monad?
论文作者
论文摘要
强大的单调对于有效语言的指定语义中的多种应用很重要,在这种语言的指示语义中,需要实力来对具有自由变量的计算进行测序。力量是非平凡的:很难确定单月是否有任何力量,而单调可以多种方式强大。因此,我们回顾了一些有关力量的最重要的事实,并证明了一些新事实。特别是,我们提供了强大的功能器和强大的单调的许多等效特征,并提供一些保证优势存在或独特性的条件。我们从三种不同的角度看强度:单类类别V的动作,对V的富集以及对V的动力。我们主要是出于效应语义的动机,但结果在其他情况下也很有用。
Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is non-trivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.