Representing Guardedness in Call-by-Value and Guarded Parametrized Monads
CoRR(2024)
Abstract
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined