meltin.net

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.

Note:This version of the paper contains the following fixes compared to the originally published version:

• The semantic brackets have been 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.