A case for semantics

 
``Mathematics is a game played according to certain simple rules with meaningless marks on paper.'' This quote, attributed to David Hilbert, sums up what one may call the `syntactic', `operational', `proof theoretic', Post-system approach to reasoning, programming, and reasoning about programming. Computation is re-writing of formulas -- programs or program configurations -- until a formula of a particular shape emerges, taken to be the result. Type checking is putting together a typing judgment like a jigsaw puzzle. Optimization is also a mechanical re-writing. The popular textbook `Types and programming languages' is all about reductions and derivations, syntactic manipulations of formulas -- expressions and propositions. Denotational semantics is barely a passing mention.

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.


 

What are denotations, exactly?

Denotational semantics is often described (see, e.g., Wikipedia) as giving interpretations to expressions (syntactic objects) through mathematical objects. What are those things, precisely? Can OCaml code be a `mathematical object'? It is worth to take a moment to reflect on what exactly denotational semantics is.

One of the first definitions of denotational semantics (along with many other firsts) is given by Landin (Landin 1966, Sec 8):

``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.''
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.

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.''
References
Eff Directly in OCaml
The above introduction to denotational semantics appears as Sec 3.1.4 in that paper.

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

 

Not by Equations Alone: Reasoning with Extensible Effects

The challenge of reasoning about programs with (multiple) effects such as mutation, jumps or IO dates back to the inception of program semantics in the works of Strachey and Landin. Using monads to represent individual effects and the associated equational laws to reason about them proved exceptionally effective. Even then it is not always clear what laws are to be associated with a monad -- for a good reason, as we show for non-determinism. Combining expressions using different effects brings challenges not just for monads, which do not compose, but also for equational reasoning: the interaction of effects may invalidate their individual laws, as well as induce emerging properties that are not apparent in the semantics of individual effects. Overall, the problems are judging the adequacy of a law; determining if or when a law continues to hold upon addition of new effects; and obtaining and easily verifying emergent laws.

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.

Version
The current version is December 2020
References
denot.pdf [503K]
The paper published in Journal of Functional Programming, v. 31, 2021, e2 doi:10.1017/S0956796820000271

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.

 

Eff Directly in OCaml

The language Eff is an OCaml-like language serving as a prototype implementation of the theory of algebraic effects, intended for experimentation with algebraic effects on a large scale.

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.

Version
The current version is December 2018
References
caml-eff.pdf [746K]
The paper published in the Electronic Proceedings in Theoretical Computer Science (EPTCS), v285, 2018, pp. 23-58. doi:10.4204/EPTCS.285.2

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