Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.

翻译：类似于通过（强）单子计算的概念可用于分类各种杂质风格（包括异常、非确定性、概率、局部与全局存储），保护性概念在多种语境下对循环的良好行为进行分类。在其最一般形式中，保护性规范适用于一般对称幺半范畴，并进一步特化为笛卡尔范畴与余笛卡尔范畴，分别在这些范畴中支配保护递归与保护迭代。在此，我们更具体地处理按值调用保护迭代的语义。Levy、Power 和 Thielecke 曾指出，按值调用语言通常可在 Freyd 范畴中解释，但为了表示带有副作用的高阶函数空间，此类范畴必须典范地源于一个强单子。我们通过证明表示受保护的高阶函数空间需要特定的参数化单子（依 Uustalu 的定义），推广了这一事实。这为程序内在的范畴属性——保护性——提供了描述，补充了将保护性视为范畴上谓词的现有描述。