In the study of computational effects, it is important to consider the notion of computational effects with parameters. The need of such a notion arises when, for example, statically estimating the range of effects caused by a program, or studying the ways in which effects with local scopes are derived from effects with only the global scope. Extending the classical observation that computational effects can be modeled by monads, these computational effects with parameters are modeled by various mathematical structures including graded monads and indexed monads, which are two different generalizations of ordinary monads. The former has been employed in the semantics of effect systems, whereas the latter in the study of the relationship between the local state monads and the global state monads, each exemplifying the two situations mentioned above. However, despite their importance, the mathematical theory of graded and indexed monads is far less developed than that of ordinary monads. Here we develop the mathematical theory of graded and indexed monads from a 2-categorical viewpoint. We first introduce four 2-categories and observe that in two of them graded monads are in fact monads in the 2-categorical sense, and similarly indexed monads are monads in the 2-categorical sense in the other two. We then construct explicitly the Eilenberg--Moore and the Kleisli objects of graded monads, and the Eilenberg--Moore objects of indexed monads in the sense of Street in appropriate 2-categories among these four. The corresponding results for graded and indexed comonads also follow. We expect that the current work will provide a theoretical foundation to a unified study of computational effects with parameters, or dually (using the comonad variants), of computational resources with parameters, arising for example in Bounded Linear Logic.
Nowadays, are becoming increasingly important. For example, there are type systems called @cite_13 , which statically estimate the range of effects caused by a program. Effect systems achieve this estimation by introducing, instead of a single effect (e.g., global state), a family of effects parametrized by ranges (e.g., global state together with a set of registers specified, with the intuition being that it contains those registers that are manipulated in an execution of the program). On the other hand, there is an active line of research on the nature of @cite_12 @cite_9 @cite_8 @cite_22 (which, in addition to manipulating registers, is able to increase or decrease the number of registers in use), especially on its relation to global state. One attracting view @cite_22 is that local state is obtained by gluing'' a family of global states with different numbers of registers, and there again the idea of parameters shows itself.
@cite_22 @cite_8 @cite_9 @cite_13 @cite_12
2115785609 1963772255 2148457191 2046137117 1521014576
One main challenge of the theory of computational effects is to understand how to combine various notions of effects in a meaningful way. Here, we study the particular case of the local state monad, which we would like to express as the result of combining together a family of global state monads parametrized by the number of available registers. To that purpose, we develop a notion of indexed monad which refines and generalizes Power's recent notion of indexed Lawvere theory. One main achievement of the paper is to integrate the block structure necessary to encode allocation as part of the resulting notion of indexed state monad. We then explain how to recover the local state monad from the functorial data provided by our notion of indexed state monad. This reconstruction is based on the guiding idea that an algebra of the indexed state monad should be defined as a section of a 2-categorical notion of fibration associated to the indexed state monad by a Grothendieck construction. Starting with Moggi's work on monads as refined to Lawvere theories, we give a general construct that extends denotational semantics for a global computational effect canonically to yield denotational semantics for a corresponding local computational effect. Our leading example yields a construction of the usual denotational semantics for local state from that for global state. Given any Lawvere theory L, possibly countable and possibly enriched, we first give a universal construction that extends L, hence the global operations and equations of a given effect, to incorporate worlds of arbitrary finite size. Then, making delicate use of the final comodel of the ordinary Lawvere theory L, we give a construct that uniformly allows us to model block, the universality of the final comodel yielding a universal property of the construct. We illustrate both the universal extension of L and the canonical construction of block by seeing how they work in the case of state. Monads for global state and local state have been used to provide semantics of programming languages for many years. There is a computation- ally natural presentation of an ordinary Lawvere theory that corresponds to the monad on Set for global state, inevitably called the Lawvere theory for global state. Here, we introduce a notion of indexed Lawvere theory and use it to give a Lawvere-style account of local state, extending the theorem for global state to local state. En route, we develop the notion of comodel of a Lawvere theory and exploit a universal characterisation of the category of worlds for local state. Ultimately, we give both syntactic and semantic characterisations of the operation block that allows one to move between worlds and use them to characterise the monad for local state. We present a new approach to programming languages for parallel computers that uses an effect system to discover expression scheduling constraints. This effect system is part of a 'kinded' type system with three base kinds: types , which describe the value that an expression may return; effects , which describe the side-effects that an expression may have; and regions , which describe the area of the store in which side-effects may occur. Types, effects and regions are collectively called descriptions . Expressions can be abstracted over any kind of description variable -- this permits type, effect and region polymorphism. Unobservable side-effects can be masked by the effect system; an effect soundness property guarantees that the effects computed statically by the effect system are a conservative approximation of the actual side-effects that a given expression may have. The effect system we describe performs certain kinds of side-effect analysis that were not previously feasible. Experimental data from the programming language FX indicate that an effect system can be used effectively to compile programs for parallel computers. We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.