In recent work, we have proposed a new axiomatic approach to unifying notions of guardedness, where the main idea is to provide an abstract notion of guardedness applicable to a wide range of (mutually incompatible) models spanning from the topos of trees to infinite-dimensional Hilbert spaces. A specific, and yet generic, instance of this notion is effectful guarded iteration.

As originally argued by Moggi, strong monads can be regarded as carriers of computational effects, and thus the arising computational metalanguage can be viewed as a generic programming language over these effects. We extend this perspective by proposing an analogous metalanguage parameterized with a notion of guardedness and equipping it with guarded iteration. In doing so, we follow the approach of Geron and Levy who already explored the case of unguarded iteration by suitably extending a fine-grain call-by-value language, a refined variant of Moggi’s language. A key ingredient we borrow from Geron and Levy’s work is the exception raising/handling mechanism, allowing for an efficient organization of while-loops via rising and iterative exception handling.