[Haskell-cafe] manage effects in a DSL
oleg at okmij.org
oleg at okmij.org
Wed Jan 29 03:34:04 UTC 2014
Lindsey Kuper wrote:
> Lately I have gotten a lot of mileage out of thinking of monads as
> embedded DSLs.
This is in fact how Moggi suggested to view monads. I strongly suggest
the remarkable paper
Eugenio Moggi and Sonia Fagorzi
A Monadic Multi-stage Metalanguage
FOSSACS2003, pp. 358--374
http://www.disi.unige.it/person/MoggiE/ftp/fossacs03.pdf
Here are two most salient quotations:
An important principle of Haskell [PHA+ 97] is that pure functional
evaluation (and all the optimization techniques that come with it)
should not be corrupted by the addition of computational effects. In
Haskell this separation has been achieved through the use of monads
(like monadic IO and monadic state). When describing MMML we adopt
this principle not only at the level of types, but also at the level
of the operational semantics. In fact, we distinguish between
simplification (described by local rewrite rules) and computation
(that may cause side-effects).
...
We outline a general pattern for specifying the operational semantics
of monadic metalanguages, which distinguishes between transparent
simplification and programmable computation. This is possible because
in a monadic metalanguage there is a clear distinction between
term-constructors for building terms of computational types, and the
other term-constructors that are computationally irrelevant. For
computationally relevant term-constructors we give an operational
semantics that ensures the correct sequencing of computational
effects, e.g. by adopting some well-established technique for
specifying the operational semantics of programming languages (see
[WF94]), while for computationally irrelevant term-constructors it
suffices to give local simplification rules, that can be applied
non-deterministically (because they are semantic preserving).
I should point out a large design space of the embedded effectful
DSL. First of all, an embedded DSL does not have to be monadic. Monad
essentially corresponds to the let-form in embedded DSL:
let_ :: Exp a -> (a -> Exp b) -> Exp b
If we are implementing an offline DSL compiler, such a let_ form is
inappropriate since it presupposes the interleaving of compilation and
code generation. Indeed, according to the type of let_, the code for
the body of let_ may differ depending on the result of Exp a (that is,
the result of compiling and then running Exp a). Normally, we first
generate code, _then_ we compile it and then we run it.
Therefore, many DSLs will not have let_ form. Rather, they will have
app :: Exp (a -> b) -> Exp a -> Exp b
That is, DSL is an applicative rather than monadic. DSL may be even
simpler, see for example, Sec 3.4 of
http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf
for a simple DSL of communicating processes, which is not even
applicative. (Its realization in Haskell may use monads, but this is
an implementation detail. The full power of the implementation
language is not exposed to the DSL programmer.)
If the DSL is effectful, we may annotate the Exp type with a set of
effects that an expression may perform. The most familiar example is
the continuation monad Cont r a, which is annotated with the
answer-type r. If Cont r a is polymorphic over r, the computation is
pure. The type Cont Int a describes an impure computation, which may
abort with an Int value, for example. If we continue on this road we
quickly come to extensible-effects.
It may happen that one annotation is not enough: we need two, to
describe the (type)state of the computation before and after an
operation. The simplest example is locking, with the type state
showing the state of the lock (acquired or released). See
Sec 5.2 Tracking state and control in a parameterised monad
in the above typefun paper. The computational structure in question is
not a monad -- it is more general than that.
To summarize: the design space is large. The relevant computational
structure is not necessary a monad: it could be less powerful or more
powerful. One should resist jumping on the bandwagon of monads or free
monads, which are so (over)hyped these days. It's best to first decide
what sort of programs a DSL programmer should be able to write. The
computational structure (monad or something else) will be clearer
then.
More information about the Haskell-Cafe
mailing list