Representing Guardedness
FAU Erlangen-Nürnberg
Slides
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 aims to classify well-behavedness of cycles in various setting. 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, I will 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. I will generalize this fact by showing that representation of guarded effectful function spaces must rely on certain parametrized monads (in the sense of Uustalu). This provides a novel description of guardedness-as-structure, complementing the existing description of guardedness-as-property.
(The talk is based on yet unpublished work in progress).