Effects Without Monads: Non-determinism
Back to the Meta Language

We reflect on programming with complicated effects, recalling an undeservingly forgotten alternative to monadic programming and checking to see how well it can actually work in modern functional languages.

We adopt and argue the position of factoring an effectful program into a first-order effectful DSL with a rich, higher-order `macro' system. Not all programs can be thus factored. Although the approach is not general-purpose, it does admit interesting programs. The effectful DSL is likewise rather problem-specific and lacks general-purpose monadic composition, or even functions. On the upside, it expresses the problem elegantly, is simple to implement and reason about, and lends itself to non-standard interpretations such as code generation (compilation) and abstract interpretation. A specialized DSL is liable to be frequently extended; the experience with the tagless-final style of DSL embedding shown that the DSL evolution can be made painless, with the maximum code reuse.

We illustrate the argument on a simple but representative example of a rather complicated effect -- non-determinism, including committed choice. Unexpectedly, it turns out we can write interesting non-deterministic programs in an ML-like language just as naturally and elegantly as in the functional-logic language Curry -- and not only run them but also statically analyze, optimize and compile. The richness of the Meta Language does, in reality, compensate for the simplicity of the effectful DSL.

The key idea goes back to the origins of ML as the Meta Language for the Edinburgh LCF theorem prover. Instead of using ML to build theorems, we now build (DSL) programs.



How to cope with the complexity of writing programs? How to structure computations? Many methodologies have been proposed over the decades: procedures, structured programming, OOP, AOP, algebraic specifications and modules, higher-order functions, laziness -- and, lately, monads and their many generalizations. Although monads are not the only way to organize (effectful) computations, they are by all accounts receiving disproportionate attention (just do a quick Google search). In ML, monads have been introduced more (Swamy et al, ICFP 2011) or less (Carette et al, SCP 2011) formally and underlie the widely used OCaml libraries Lwt and Async.

This position paper seeks to draw attention to a non-monadic alternative: Rather than structuring (effectful) programs as monads -- or applicatives, arrows, etc., -- we approach programming as a (micro) language design. We determine what data structures and (effectful) operations seem indispensable for the problem at hand -- and design a no-frills language with just these domain-specific features. We embed this bare-bone DSL into OCaml, relying on OCaml's extensive facilities for abstraction and program composition (modules, objects, higher-order functions), as well as on its parsing and type checking.

We state the main points of our argument in Points to argue. We hasten to say that the key insight is rather old (Wand, Th.Comp.Sci. 1982), quite resembling algebraic specifications (see Wirsing's comprehensive survey in the Handbook of Theoretical Computer Science B). In fact, it is the insight behind the original ML, as a scripting language for the Edinburgh LCF theorem prover -- only applied to programs rather than theorems. What has not been clear is how simple an effectful DSL may be while remaining useful. How convenient is it, especially compared to the monadic encodings? How viable is it to forsake the generality of first-class functions and monads and what benefits may come? We report on an experiment set out to explore these questions.

The present paper follows the style of Hughes (Why functional programming matters, 1989), Hudak (Building domain-specific embedded languages, 1996) and Goguen (Higher order functions considered unnecessary for higher order programming, 1988) -- or, for mathematically inclined, Polya (How to solve it, 1945) -- arguing from examples. Just like those arguments, it is indeed hard to grasp the limitations and applicability, and it is hard to formalize. Problem solving in general is a skill to learn rather than an algorithm to implement; it is inherently informal. Even in mathematics, how to prove theorems is an art and a judgement; one acquires it not by following rigorous descriptions but by reading existing proofs and doing exercises. This is the format we follow in the paper.

nondet-paper.pdf [309K]
The paper published in the Electronic Proceedings in Theoretical Computer Science EPTCS 294, 2019, pp. 15-40 (Post-Proceedings ML 2017) DOI: 10.4204/EPTCS.294.2

M. Gordon, R. Milner, L. Morris, M. Newey and C. Wadsworth: A Metalanguage for Interactive Proof in LCF
Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, 1978



This present paper comes as the result of decade-long long experience with the tagless-final style of DSL embedding and the re-discovering and polishing of extensible effects. It was prompted however by the following message, posted on the Caml-list by Christoph Hoeger in March 2017:
``Assume a simple OCaml program with two primitives that can cause side-effects:
    let counter = ref 0
    let incr x = counter := !counter + x ; !counter
    let put n = counter := n; !counter
    put (5 + let f x = incr x in f 3)
This example can be transformed into a pure program using a counter monad (using ppx_monadic syntax):
      i <-- let f x = incr x in f 3 ;
      p <-- put (5 + i)
      return p
For a suitable definition of bind and return, both programs behave equivalently. My question is: How can one automatically translate a program of the former kind to the latter?''
The message left me puzzled about its author's goals and motivations. It is hard to imagine he preferred the monadic program for its verbose notation, replete with irrelevant names like i and p. Was the author after purity? That is a mirage we lay bare in Sec. 6. Was he attracted to the separation of effectful and non-effectful code and the possibility of multiple interpretations of effects (`the overriding of the semicolon')? These good properties are not unique to monads. The other, often forgotten, ways of dealing with side-effects ought to be more widely known.

The second cue came about a month later, observing students solving an exercise to compute all permutations of a given list of integers. The reader may want to try doing that in their favorite language. Albeit a simple exercise, the code is often rather messy and not obviously correct. In the functional-logic language Curry built around non-determinism, computing a permutation is strikingly elegant: mere foldr insert []. It is the re-statement of the specification: a permutation is moving the elements of the source list one-by-one into some position in the initially empty list. The code immediately tells that the number of possible permutations (possible choices of permutations) of n elements is n!. From its very conception in the 1950s, non-determinism was called for to write clear specifications -- and then to make them executable. Can we write the list permutation code just as elegantly in a language that was not designed with non-determinism in mind and offers no support for it? How far can we extend it?

The origins of non-determinism

Having an Effect


Points to argue

The primary goal for the paper is to report on the experiment set out to explore the viability and consequences of a particular method of writing effectful programs. Although all the ingredients have been known (some of them for so long that they are almost forgotten), how well the approach actually works for interesting problems can only be determined empirically.

Along with the describing the experiment and its ramifications, we also offer an argument: why this approach is worth exploring in the first place. The points of the argument, reverberating throughout the paper, are collected below:

Effects are not married to monads
The discussion after the first presentation of this paper, at the ML Family workshop 2017, was one of many indications that monads have a special, almost cult status in the minds of functional programmers. There is no doubt that monads clearly delineate effectful computations, in syntax and in types, and offer the reasoning principles (equational laws) about effectful programs. What many do not seem to realize is that these benefits are not unique to monads, or that not all effects are expressible with monads (which was noted already by Wadler 1994), or that the flexibility of the monadic encoding (`overriding semicolon') is limited. Code generation and abstract interpretation, for example, do not fit the monadic framework (see Sec. 5).

Although this point may be obvious to some, the caml-list (as noted in earlier), Reddit, Stack Overflow, etc. discussion places are awash with misunderstandings and irrational exuberance towards monads. The argument pointing out their proper place and limitations is worth repeating.

Separate rather than combine higher-order and effects
The present paper is an exploration of a less common approach to writing reusable, properly abstracted effectful programs. Rather than combining effectful operations with modules, objects, higher-order functions, we separate them. First we determine the data types and operations needed for the problem at hand, and define the corresponding domain-specific language (DSL). The language is often first-order, and its operations have a number of domain-specific effects (such as references to application-specific context, communication, logging, etc).

Since the DSL is intentionally without abstraction or syntactic sugar -- just enough to express the problem at hand, however ungainly -- programming in it directly is a chore. That is why we endow it with a very expressive `preprocessor', by embedding into a metalanguage with rich abstractions like functions, definitions, modules, etc.

Not all problems can be thus factored into a first-order DSL and a higher-order metalanguage (e.g., the factoring does not support arbitrary higher-order effectful functions). Therefore, how well the factoring works in practice and if it is worth paying attention to become empirical questions. The paper describes one case study, exploring how far we can push this approach.

General vs. specific: it is a trade-off
The approach to be evaluated in the present paper -- the factoring of an effectful program into a simple DSL and a rich preprocessor -- is not general purpose. The non-deterministic DSL is not general purpose either: we introduce only those data types and operations that are needed for the problem at hand and its close variations. Domain-specific, narrow solutions should not be always looked down upon, we argue.

The compelling case for (embedded) DSLs has been already made, by Hudak, 1996. The present paper is another case study. We also demonstrate, in Sec. 5, one more advantage of an embedded DSL: the ability to evaluate the same DSL code in several ways. We can not only (slowly) interpret the code, but also perform static analyses such as abstract interpretation, and generate (faster) code.

The advantages of the domain-specific approach have to be balanced against the applicability (how wide is the domain, does it let us do something interesting or practically significant) and extensibility (how easy it is to extend the program and the domain and reuse the existing code). This is a trade-off, which the case study in the present paper is to help evaluate.

Thus we do not argue that the domain-specific approach is `better'. We do argue, however, against the presumption (evidenced in the received comments on the drafts of this paper) that one always has to strive for the general solution. Premature generalization and abstraction, like premature optimization, is not a virtue.

Try domain-specific first
When deciding which approach to effects fits the problem at hand, we advocate trying a specialized solution (such as the DSL factoring) first. Typically, whether it works out or not becomes clear very soon; if it does not, little effort is wasted because the approach is so simple.


The rest of the paper

The structure of the paper is as follows. Sec. 2 describes the main experiment: can we write the list permutation in OCaml as elegantly as in Curry. Specifically, Sec. 2.1 introduces the intentionally very simple, essentially first-order, DSL for the specific domain of non-deterministic computations on integer lists, and Sec. 2.2 uses it to express the list permutation. The readers can see for themselves how good (simple, understandable, close to Curry) it looks. A way to make the DSL embedding seamless is described in Sec. 2.3. Several `standard' implementations of the DSL are discussed in Sec. 3, whereas Sec. 4 extends the DSL and its implementation with the committed choice and presents another classical Curry example: slow sort. Thus the factoring of an effectful computation into a first-order DSL and a powerful metalanguage turns out to be viable -- an outcome that was not at all clear at the beginning.

Our language is truly domain-specific: for example, it offers no abstraction mechanism of its own and no general monadic interface for writing effectful computations. As an upside, the DSL admits useful non-standard implementations. Sec. 5 shows three. In particular, Sec. 5.2 describes an abstract interpretation, to statically estimate the degree of non-determinism of a DSL term. The code-generation interpretation -- the DSL compiler -- is presented in Sec. 5.3.

Sec. 6 discusses the presented factoring approach, answering several commonly heard objections. The main theoretical ideas have all been known in isolation, often for many decades, as we review in Sec. 7.

nondet-paper.pdf [309K]
The full paper, published in the Electronic Proceedings in Theoretical Computer Science EPTCS 294, 2019, pp. 15-40 (Post-Proceedings ML 2017) DOI: 10.4204/EPTCS.294.2

0README.dr [<1K]
The complete source for all the code described in the paper



We have described a direct alternative to the monadic encoding of effects: a bare-bone domain-specific language with effectful operations. The DSL is blended into a metalanguage such as OCaml; therefore, it can be kept tiny, with no abstraction facilities of its own, or even functions. The metalanguage, serving as an inordinarily expressive macro system, compensates. We have also argued for the principle of avoiding premature generalizations and abstractions.

We have reported only one experiment, which -- combined with the related LMS experience -- suggests that the DSL-metalanguage factoring approach to effectful programming is viable. More experiments are needed to better grasp its usefulness. Specifically we would like to try examples in the scope of Async or Lwt libraries. A bigger exercise would be to re-implement the programming language Icon -- another language with built-in non-determinism.

One may wonder how the history of (meta) programming might have turned out if the ML evolution had taken a different turn: kept using ML as the Meta Language as it was initially designed for, but building objects other than formulas and theorems -- in particular, programs.