A Logical View of Effects - Semantic Scholar

in IO monad, which allows programmers to use effects ...... gineering Theories of Software Construction. IOS. Press, Amsterdam, 2001. [34] S. L. Peyton Jones ...
212KB Sizes 1 Downloads 345 Views
A Logical View of Effects Sungwoo Park and Robert Harper Computer Science Department Carnegie Mellon University {gla,rwh}@cs.cmu.edu

Abstract Despite their invaluable contribution to the programming language community, monads as a foundation for the study of effects have three problems: they make it difficult to combine effects; they enforce sequentialization of computations by the syntax; they prohibit effect-free evaluations from invoking effectful computations. Building on the judgmental formulation and the possible worlds interpretation of modal logic, we propose a logical analysis of effects based upon the view monads are not identified with effects. Our analysis leads to a language called λ→ ° which distinguishes between control effects and world effects, enforces sequentialization of computations only by the semantics, and logically explains the invocation of computations from evaluations. λ→ ° also serves as a unified framework for studying Haskell and ML, which have traditionally been studied separately. 1


Motivation Since their introduction to the programming language community, monads [23, 24] have been considered as an elegant means of structuring programs and incorporating effects into purely functional languages. An example of a functional language that makes extensive use of monads is Haskell [30]. At the program level, it provides a type class Monad to support modular programming; at the language design level, it uses monads for a modular semantics of effects and provides a builtin IO monad, which allows programmers to use effects without compromising its properties as a purely functional language. While they are a success as a tool for modular programming, monads as a foundation for the study of effects have the following three problems: Combining effects. It is well-known that monads do not combine well with each other [14, 12, 20]. This means that although monads provide a modular way

to develop semantics for individual effects, they fail to give a modular semantics when all effects are present together. Hence the identification between monads and effects makes it difficult to combine effects at the language design level. Haskell avoids this problem by confining all kinds of effects – mutable references, input/output, exception, concurrency, and so on – to the IO monad, but it does not provide a justification for the assumption that individual monads combine into a single monad. Sequentialization by the syntax. Unlike effectfree/pure evaluations, effectful/impure computations are sequential by their nature. This, however, does not mean that their syntax must also be in a sequential form. Unfortunately the return and bind constructs of the monadic syntax (e.g., return and >>= in Haskell) force programmers to strictly follow the sequential order of computations. This becomes increasingly inconvenient as the code grows in size. Entering and escaping from monads. Monads allow computations to freely invoke evaluations, but not vice versa. In essence, we can neither enter monads (and initiate computations) during evaluations nor escape from monads (and return results of computations) back to evaluations, because of effects that computations may produce. In the case of Haskell, this means that we cannot write functions of type IO A −> A, which are particularly useful for benign effects (e.g., accessing read-only files). In order to overcome this limitation, Haskell provides two constructs: unsafePerformIO [34, 33] and runST [17, 18, 19]. However, unsafePerformIO is unsafe (as its name suggests) because in principle, it can destroy the distinction between evaluations and computations. runST, albeit an ingenious solution, does not have a Hindley-Milner type. It also lacks extensibility because it is specific to mutable references; moreover it initiates computations only with an empty store.


tinuations are usually considered as control effects, but only when their reduction rules are not accepted as the basic redu