Expression refinement semantics are often complex. In particular,
semantics for the relatively simple notion of function application are
often disproportionately complex. Monads are frequently championed as
the `right' tool for structuring the semantics of function
application. In this paper, we consider the interaction between
monadic semantics and refinement semantics. We demonstrate that a
monad extended with a refinement ordering becomes an elegant tool for
structuring the semantics of expression refinement. We do not claim
that using monads to structure the semantics of function application
is a new idea, nor do we introduce novel semantic models for
non-deterministic languages. We simply demonstrate that the structure
provided by monads ensures a consistent semantic approach. We
illustrate this further by adding a facility for output to one of our
languages.
Errata
The semantic brackets should be dropped from the right-hand
sides of equations (13), (20), (26), (32), (41) and (47). This
means that refinement is only defined at the abstract level.
Defining it at the concrete level is trivial.
