VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 495

The following is a special case of the above, and is directly comparable with
defining binary statement sequencing in the Oxford style, as illustrated in the
previous section:

M[mk-Compound(<s1,s2>)](env) = M[s1](env); M[s2](env)

Also the VDM definition of the denotations of conditional statements is rather
similar to the corresponding definition in the Oxford style:

M[mk-If(e,th,el)] =
def b: M[e](env);
if b then M[th](env) else M[el](env)

Our final illustration of the VDM style of denotational semantics is the assign-
ment statement:

M[mk-Assign(lrs,rhs)](env) =
def l: M[lhs](env);
def v: M[rhs](env);
STR := c STR + [ l → v ]

5 The Monadic Style

This style of denotational semantics was introduced by Eugenio Moggi at the
end of the 1980s [21]. His original motivation was to generalise the categorical
semantics of partiality to “other notions of computation”; he subsequently re-
alised that it also allows a much higher degree of modularity and extensibility
in semantic descriptions.
The main technical innovations were to let denotations be elements of monads ,
and to construct monads incrementally using monad transformers . Monads and
monad transformers provide various combinators, which are closely related to
some of those used by Scott and Strachey [3], and even more closely to some
of those provided by VDM [18]. Like the latter, the monadic combinators have
a simple operational reading. The monadic style of denotational semantics has
been exploited in several theoretical studies, but it appears that, despite its clear
mathematical foundations and advantages regarding modularity, it has not yet
been used to describe any major programming language.

5.1 Domains and Operations

The monads used in the monadic style of denotational semantics provide the de-
notations of phrases of programs, and are generally defined in terms of domains.

Monads. A monad consists of a domain constructor T , mapping value domains
D to computation domains T ( D ), together with two polymorphic operations:

- Return : D → T ( D );

- >> =: T ( A ) × ( A → T ( B )) → T ( B )