There is an alternative: `semantic', `denotational', `model theoretic' -- aiming to give meaning to the `marks on paper' by relating them to real world, or a model thereof, to something with which we have experience and intuition. Whereas operational reasoning is confined to rewriting rules -- that's all there is, -- denotational semantics lets us use whatever knowledge and intuition we have about our model. Denotational semantics excels at proving equational laws, used for reasoning and optimization. Denotational semantics also leads to optimization directly: normalization-by-evaluation, or optimization by calculation rather than rewriting.
This web page collects examples of applying the semantic, denotational approach to a variety of problems -- making a case for semantics.
One of the first definitions of denotational semantics (along with many other firsts) is given by Landin (Landin 1966, Sec 8):
As an illustration, Landin then describes the denotations of string expressions in terms of (natural language) strings such as `wine' or even equivalence classes of ISWIM-like expressions.``The commonplace expressions of arithmetic and algebra have a certain simplicity that most communications to computers lack. In particular, (a) each expression has a nesting subexpression structure, (b) each subexpression denotes something (usually a number, truth value or numerical function), (c) the thing an expression denotes, i.e., its `value', depends only on the values of its subexpressions, not on other properties of them.''
In the reference text (Mosses 1990, Sec 3.1), Mosses essentially repeats Landin's definition, adding: ``It should be noted that the semantic analyst is free to choose the denotations of phrases -- subject to compositionality''. He notes that letting phrases denote themselves is technically compositional and hence may be accepted as a denotational semantics -- which however has ``(extremely) poor abstractness''. Still, he continues, there are two cases where it is desirable to use phrases as denotations, e.g., for identifiers.
Thus from the very beginning there has been precedent of using
something other than abstract mathematical sets or domains as
denotations. Even syntactic objects may be used for semantics,
provided the compositionality principle is satisfied. In this paper
[Eff directly in OCaml], we take as semantic objects OCaml values,
equipped with extensional equality. In case of functions,
checking the equality involves reasoning if two OCaml functions, when
applied to the same arguments, return the extensionally equal
results. To be more precise, we check how the OCaml (byte-code)
interpreter evaluates the applications of these functions to the same
arguments. The behavior of the byte-code interpreter is well-defined;
the compilation of the fragment of OCaml we are using is also
well-understood (including Obj.magic, which operationally is the
identity). We give an example of such reasoning when justifying the
adequacy of the Core delimcc semantics.
Using an interpreter to define a language has long precedent, starting from (Reynolds, 1972). Such an approach was also mentioned in the survey (Schmidt, 1996):
``A pragmatist might view an operational or denotational semantics as merely an `interpreter' for a programming language. Thus, to define a semantics for a general-purpose programming language, one writes an interpreter that manipulates data structures like symbol tables (environments) and storage vectors (stores). For example, a denotational semantics for an imperative language might use an environment,e, and a store,s, along with an environment lookup operation,find, and a storage update operation,update. Since data structures like symbol tables and storage vectors are explicit, a language's subtleties are stated clearly and its flaws are exposed as awkward codings in the semantics.''
Peter J. Landin: The Next 700 Programming Languages
Comm. ACM, v9 N3, March 1966, pp. 157-166.
doi:10.1145/365230.365257
Peter D. Mosses: Denotational Semantics
In: Handbook of Theoretical Computer Science B: Formal Models and Semantics,
Ed. J. van Leewen, MIT Press, 1990. Chap 11, pp. 577-631.
David A. Schmidt: Programming Language Semantics
ACM Computing Surveys, v28 N1, March 1996, pp. 265-267.
doi:10.1145/234313.234419,
John C. Reynolds: Definitional Interpreters for
Higher-Order Programming Languages
Proc. of the ACM National Conference 1972.
Reprinted: Higher-Order and Symbolic Computation, v11 N4, 1998, pp. 363-397.
doi:10.1023/A:1010027404223
We present a solution relying on the framework of (algebraic, extensible) effects, which already proved itself for writing programs with multiple effects. Equipped with a fairly conventional denotational semantics, this framework turns useful, as we demonstrate, also for reasoning about and optimizing programs with multiple interacting effects. Unlike the conventional approach, equational laws are not imposed on programs/effect handlers, but induced from them: our starting point hence is a program (model), whose denotational semantics, besides being used directly, suggests and justifies equational laws and clarifies side-conditions. The main technical result is the introduction of the notion of equivalence modulo handlers (`modulo observation') or a particular combination of handlers -- and proving it to be a congruence. It is hence usable for reasoning in any context, not just evaluation contexts -- provided particular conditions are met.
Concretely, we describe several realistic handlers for non-determinism and elucidate their laws (some of which hold in the presence of any other effect). We demonstrate appropriate equational laws of non-determinism in the presence of global state, which have been a challenge to state and prove before.
In short, the paper is about:
Although the paper at times uses heavy machinery, the main ideas are explained in Section 2 on mere addition.
Joint work with Shin-Cheng Mu and Amr Sabry.
DSL of algebraic effects and handlers
The implementation of the calculus. It is used to run all the examples in the
paper. Thus, the equational laws discussed in the paper are not only proven
but also tested.
We present the embedding of Eff into OCaml, using the library of delimited continuations or the multicore OCaml branch. The embedding is systematic, lightweight, performant and supports even higher-order, `dynamic' effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.
As a side contribution, we demonstrate the correctness of our embedding of Eff in OCaml denotationally, relying on the ``tagless-final'' style of interpreter-based denotational semantics. We also present the novel denotational semantics of multiprompt delimited control that does not rely on continuation-passing-style (and is, hence, direct).
Joint work with KC Sivaramakrishnan.
eff1.ml [10K]
Encoding of Eff in OCaml+delimcc: the code for
Sections 2.2 and 4 of the paper.
The code relies on the delimcc library of delimited control.
queens_eff.ml [4K]
The n-queens benchmark (Sec 5 of the paper):
re-casting the Eff code into OCaml, using the
technique introduced in the paper. The code relies on the delimcc
library of delimited control.
delimcc_of_multicore.ml [3K]
delimcc interface realized in multicore OCaml: code for Sec 2.3.2 of the paper
many_one.eff [5K]
Code for Sec 3.1.1 of the paper, justifying the adequacy of
single-operation effects and showing the encoding of effects with
multiple operations
eff_semantics.ml [6K]
Core Eff in the tagless-final form and the `interpreter-based'
denotational semantics of Core Eff:
Sections 3.1.2 and 3.1.3 of the paper
delimcc_semantics.ml [7K]
Denotation of multiprompt delimited control: direct
`interpreter-based' semantics of Core delimcc. Sec 3.2 of the paper
translation.ml [2K]
The formalization of Eff in OCaml: the translation
from Core Eff to Core Delimcc, as another denotational
semantics of Core Eff. Sec 3.3 of the paper then argues the two
semantics are the same.
Makefile [2K]
How to build and run the examples and the benchmarks
The Eff language
<http://www.eff-lang.org/>
delimcc:
A direct implementation of delimited continuations for byte- and native-code
OCaml