We make significant use of the notion of monads. A good way to think of a monad is as an abstract datatype that captures the side effects and actions inherent in the language being translated in the methods of the abstract datatype. An important feature of a monad is that also describes, in a purely functional way, how these effects and actions interact. Like any good abstract datatype, we are free to implement the actions in any way we want as long as our implementation behaves like its purely functional description.
The ultimate efficiency of the compiler depends on making good use of the low-level primitives of the target language. Monads are the glue that we use to tie high-level (purely functional) descriptions of languages to the low-level implementation features of the target environment.
A monad is a type constructor M (a type constructor is a function on types, which given a type produces a new type), and two polymorphic functions and . The way to interpret an expression with type M(a) is as a computation that represents a potential action and that also returns a value of type a.
An action might perform I/O, update a mutable variable, or raise an exception. One can implement a monad in a purely functional setting by emulating the actions. This is done by explicitly threading ``stores'', ``I/O streams'', or ``exception continuations'' in and out of all computations. We call such an emulation the reference implementation. Using a functional implementation allows equational reasoning about the reference implementation, however it is usually quite inefficient.
The two polymorphic functions unit and bind must meet the following three axioms:
where e[x/y] is the result of the substitution of the free occurrences of the variable x in e by the variable y.
The monadic operators, unit and bind, are called the standard morphisms of the monad. The unit operator takes a pure value and turns it into an empty action. The bind operator sequences two actions. A useful monad will also have non-standard morphisms that describe the primitive actions of the monad (like read the value from a variable and write a variable in the monad of mutable state).
For more background on the use of monads see [29, 31, 30].