Author: Eugenio Moggi (University of Edinburgh)
Reference: Information and computation 93.1 (1991): 55-92
Why this paper? Cited by Normalization for Fitch-Style Modal Calculi, Probabilistic Programming and Multiverse Models of Type Theory, and Denotational Semantics of General Store and Polymorphism in my Google Scholar recommendations.
This famous paper suggested the use of the important but rather abstract category theoretic concept known as a monad to assist with reasoning about programming languages and programs that feature side effects. A side effect is an aspect of computation that cannot be easily described as a final output of a deterministic program, variously because it refers to output that happens during computation (such as printing to the screen), a failure to create an output (such as crashing with an error), or an opportunity for something (such as a user) to interact with the computation. The monad (typically written T) of choice depends on which type of side effect(s) one wishes to incorporate. Having chosen the monad, we can draw a distinction between the values of a type A - the sort of thing one can use as an input - and the type TA of computations of type A. This fine-grained distinction allows one to formally discuss the side effects, and not merely the result, of a program of interest.
The style in which Moggi presents his monads are at least as important as the concept itself, as he suggests introducing them, with new notation and equational rules, into a lambda calculus, both as a ‘metalanguage’ for reasoning about programming languages with side effects, and as a programming language in its own right. This has been influential in the use of monads in programming in Haskell and other languages.
No comments:
Post a Comment