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 parameterized 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的定义）来推广这一结论。这为保护性提供了一种作为程序内在范畴性质的描述，从而补充了现有将保护性视为范畴谓词的描述框架。