Representing Layered Monads

Andrzej Filinski

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade, DK-8000 Aarhus C, Denmark

                                    andrzej@brics.dk

Abstract

There has already been considerable research on constructing modular, monad-based specifications of computational effects (state, exceptions, nondeterminism, etc.) in programming languages. We present a simple framework in this tradition, based on a Church-style effect-typing system for an ML-like language. The semantics of this language is formally defined by a series of monadic translations, each one expanding away a layer of effects. Such a layered specification is easy to reason about, but its direct implementation (whether by parameterized interpretation or by actual translation) is often prohibitively inefficient.

By exploiting deeper semantic properties of monads, however, it is also possible to derive a vastly more efficient implementation: we show that each layer of effects can be uniformly simulated by continuation-passing, and further that multiple such layers can themselves be simulated by a standard semantics for call/cc and mutable state. Thus, even multi-effect programs can be executed in Scheme or SML/NJ at full native speed, generalizing an earlier single-effect result. As an example, we show how a simple resumptionbased semantics of concurrency allows us to directly simulate a shared-state program across all possible dynamic interleavings of execution threads.

1 Introduction

By now, monads are firmly established as an key concept in functional programming, both as a semantic framework for ML-like languages [Mog89], and as a structuring technique for purely functional programs with computational effects [Wad92]. But the situation is less clear for the prospect of using monads to structure multiple, potentially intertwined effects: although a number of frameworks for this have been proposed [Mog90, Ste94, CF94, LHJ95, Esp95], none seem to have gained overwhelming acceptance.

This is perhaps not surprising, since a truly modular characterization of computational effects is probably an illspecified problem, with no unique solution. Nevertheless, most monad-based formalisms tend to leave at least two areas with definite room for improvement:

• Conceptual overhead. It is usually clear how a single monad in isolation represents a particular notion of computational effect (such as mutable state or exceptions), and how individual effect-operations (such as reading and writing of the state, or raising and handling of exceptions) are expressed in terms of the monadic structure. But with multiple effects, the initial cost is higher: each notion of effect must now be specified in an integrable form, and the specification of the operations must likewise be further parameterized. In some cases, operations for one effect are even fundamentally incompatible with the monadic structure of another, significantly complicating the semantics of the resulting language.

• Practical overhead. A distinct problem with monadbased executable specifications of interacting effects is computational efficiency. Although explicit, purely functional definitions of effects make it easier to reason about programs, in practice key monads (such as state) are usually implemented imperatively by the compiler [LPJ95]. The efficiency problems are compounded for multi-level effects: in a naive implementation, the cost of each computational step is generally directly proportional to the total number of effects being modeled; and “built-in” monads are generally not integrable in a multi-effect framework with the same flexibility as user-specified ones.

Although the present paper is hardly the final word on either subject, it does present a framework for monadic effects addressing both problems in a novel way: conceptually, it offers a simple declarative specification based on nested translations, and practically, an efficient imperative implementation in terms of low-level control and state primitives. In more detail, each notion of effect is specified independently by a formal monadic translation (state-passing, exception-passing, etc.), which also defines two protooperations, monadic reflection and reification. These establish a (trivial) bijection between opaque and transparent representations of an effect-computation, allowing us to define the usual effect-operations in terms of the transparent representation, and then write general programs using only the abstract, opaque form. This specification is purely local, and can be written independently for each effect.

Secondly, we show that each such monadic translation can be simulated by a continuation-passing translation, which re-

∗

Basic Research in Computer Science (http://www.brics.dk),

Centre of the Danish National Research Foundation.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.

To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.

POPL 99, San Antonio, Texas, USA Copyright ACM 1999 1-58113-095-3/99/01...$5.00

\frac{Γ(x) = τ}{Γ ⊢ x : τ / 𝔫}  \frac{Σ(c) = ∀α⃗. τ}{Γ ⊢ cτ⃗ : τ[τ⃗/α⃗] / 𝔫}  \frac{Γ, x: τ_{1} ⊢ E : τ_{2} / e}{Γ ⊢ λx^{τ_{1}}.E : (τ_{1} →^{e} τ_{2}) / 𝔫}  \frac{Γ ⊢ E_{1} : (τ_{1} →^{e} τ_{2}) / 𝔫  Γ ⊢ E_{2} : τ_{1} / 𝔫}{Γ ⊢ E_{1} E_{2} : τ_{2} / e}

\frac{Γ ⊢ E : 0 / 𝔫}{Γ ⊢ V E : τ / e}  \overline{Γ ⊢ () : 1 / 𝔫}  \frac{Γ ⊢ E_{1} : τ_{1} / 𝔫  Γ ⊢ E_{2} : τ_{2} / 𝔫}{Γ ⊢ (E_{1}, E_{2}) : τ_{1} × τ_{2} / 𝔫}  \frac{Γ ⊢ E : τ_{1} × τ_{2} / 𝔫}{Γ ⊢ π_{1} E : τ_{1} / 𝔫}  \frac{Γ ⊢ E : τ_{1} × τ_{2} / 𝔫}{Γ ⊢ π_{2} E : τ_{2} / 𝔫}

\frac{Γ ⊢ E : τ_{1} / 𝔫}{Γ ⊢ inl E : τ_{1} + τ_{2} / 𝔫}  \frac{Γ ⊢ E : τ_{2} / 𝔫}{Γ ⊢ inr E : τ_{1} + τ_{2} / 𝔫}  \frac{Γ ⊢ E : τ_{1} + τ_{2} / 𝔫  Γ, x_{1}: τ_{1} ⊢ E_{1} : τ / e  Γ, x_{2}: τ_{2} ⊢ E_{2} : τ / e}{Γ ⊢ case(E, x_{1}.E_{1}, x_{2}.E_{2}) : τ / e}

\frac{Γ ⊢ E : τ / 𝔫}{Γ ⊢ val^{e} E : τ / e}  \frac{Γ ⊢ E_{1} : τ_{1} / e  Γ, x: τ_{1} ⊢ E_{2} : τ_{2} / e}{Γ ⊢ let^{e} x ⇐ E_{1} in E_{2} : τ_{2} / e}  \frac{Γ ⊢ E_{1} : τ_{1} / e_{1}  Γ, x: τ_{1} ⊢ E_{2} : τ_{2} / e_{2}  e_{1} ≺ e_{2}}{Γ ⊢ let^{e_{1},e_{2}} x ⇐ E_{1} in E_{2} : τ_{2} / e_{2}}

\overline{e ⪯ e}  \frac{e_{1} ⪯ e  e ≺ e_{2}}{e_{1} ⪯ e_{2}}  \overline{ι ≤ ι} (ι=α,b,1,0)  \frac{τ′_{1} ≤ τ_{1}  e ⪯ e′  τ_{2} ≤ τ_{2}}{τ_{1} →^{e} τ_{2} ≤ τ′_{1} →^{e′} τ′_{2}}  \frac{τ_{1} ≤ τ′_{1}  τ_{2} ≤ τ′_{2}}{τ_{1} ⋄ τ_{2} ≤ τ′_{1} ⋄ τ′_{2}} (⋄ =×,+)

\frac{Γ ⊢ E_{1} : τ_{1} / e_{1}  Γ, x: τ_{1} ⊢ E_{2} : τ_{2} / e_{2}  e_{1} ⪯ e_{2}}{Γ ⊢ let^{e_{1}⪯e_{2}} x ⇐ E_{1} in E_{2} : τ_{2} / e_{2}}  \frac{Γ ⊢ E : τ / e  τ ≤ τ′  e ⪯ e′}{Γ ⊢ E : τ′ / e′}

Figure 1: Effect-typing and subtyping rules

tains the original transparent representation of effects, but substitutes a different opaque one. We use this result to show correctness of a direct implementation of the protooperations in terms of the control operators shift and reset. As previously shown [Fil94, Fil96], these operators can themselves be implemented by Scheme-style primitives call/cc and state, but this “uses up” the call/cc operation of the host language. Here we show how, in addition to defining shift and reset, we can “regenerate” a call/cc that can be used to implement other effects without interference. Thus, a whole monadic tower can be embedded in a language with Scheme-like primitive effects.

Accordingly, the paper is structured as follows: in Section 2, we present the translation-based specification of monadic effects. In Section 3, we show correctness of the continuation-based implementation using logical relations; we also present a concrete realization of the construction in SML/NJ. Section 4 contains a few practical examples, including a simulation of shared-state concurrency. Finally, Section 5 compares the present results with related work on monad layering and control operators, and Section 6 presents some conclusions and outlines future work.

2 Specifying layered effects

In this section, we introduce a simple functional language with a type system for keeping track of effect-behavior of terms, and show how this language can be systematically extended by new, programmer-defined effects.

2.1 A multi-effect language

For the purpose of the formal results, it will be convenient to work with a syntax in which all computational steps are explicitly sequenced. That is, the results of all non-trivial operations must be explicitly named, as in A-normal or monadic normal forms [FSDF93, HD94]. (Ultimately, however, we will still be able to write concrete programs in ML notation, with implicit call-by-value sequencing.)

We further refine this language with a type system for keeping track of effects, very similar to Tolmach’s and (to a lesser degree) Wadler’s intermediate languages for ML [Tol98, Wad98]. However, we will use effect-types prescriptively, to define a new language, rather than descriptively, to analyze an already given one.

The raw syntax is thus as follows:

τ ::= α | b | τ_{1} →^{e} τ_{2} | 1 | τ_{1} × τ_{2} | 0 | τ_{1} + τ_{2}
E ::= x | c_{τ_{1},...,τ_{n}} | λx^{τ}.E | E_{1} E_{2} | () | V E | (E_{1}, E_{2})

| π_{1} E | π_{2} E | inl E | inr E | case(E, x_{1}.E_{1}, x_{2}.E_{2}) | val^{e} E | let^{e} x ⇐ E_{1} in E_{2} | let^{e_{1},e_{2}} x ⇐ E_{1} in E_{2}

e ::= 𝔫 | 𝔭 | ⋯

Here e ranges over a set of effect names, which classify the range of effects of an expression: the typing judgment Γ ⊢ E : τ / e states that under typing assumptions Γ (mapping variables to types), E has type τ, and possible effects e.

In particular, the effect 𝔫 (none) means that evaluation of E has no effects, and that E therefore behaves as a value for the purpose of equational reasoning. Another distinguished effect is 𝔭 (partiality), which indicates that evaluation of E may diverge, but has no other effects.

The typing rules are displayed in Figure 1. They are parameterized by an effect-layering relation ≺, with e_{1} ≺ e_{2} expressing that e_{2} is layered immediately above e_{1}, in a sense to be made precise in the next section. (Typically it means that e_{2} was defined by a formal translation into a language with e_{1}-effects.) ⪯ is the reflexive, transitive closure of ≺. We sometimes use pattern-matching binding syntax instead of projections; and in particular, we write λ().E for λx^{1}.E. We also often write τ_{1} →^{𝔫} τ_{2} simply as τ_{1} → τ_{2}, and Γ ⊢ E : τ / 𝔫 as Γ ⊢ E : τ.

A complete program is a closed term of base type. For simplicity, we may also put restrictions on the potentially “escaping” effects of such programs, in preference to complicating the top-level semantics. (For example, we may require that a complete program handles all exceptions it may raise, using a catch-all exception wrapper.)

The language is also parameterized by a signature Σ assigning (potentially polymorphic) types to the basic constants in the language. These would typically include the standard arithmetic functions, and in particular a family of CBV fixed-point operators,

fix_{α_{1},α_{2}}^{e} : ((α_{1} →^{e} α_{2}) → α_{1} →^{e} α_{2}) → α_{1} →^{e} α_{2} (𝔭 ⪯ e)

(Note that all recursively defined functions will thus have at least the effect of partiality.) Although complete programs will be monomorphic, we need the extra generality of type schemas in order to define monad components as polymorphic terms in Section 2.3.

The last two lines of Figure 1 add implicit subeffecting and subtyping to the language. (But note that the only subtyping relations introduced are changes of effect-annotations.) We can expand all occurrences of the general let-construct into the two primitive ones as follows:

let^{e⪯e} x ⇐ E_{1} in E_{2} = let^{e} x ⇐ E_{1} in E_{2}
let^{e_{1}⪯e_{2}} x ⇐ E_{1} in E_{2} =

let^{e,e_{2}} x ⇐ (let^{e_{1}⪯e} x ⇐ E_{1} in val^{e} x) in E_{2}

Similarly, well-typed terms in the system with subsumption can be expanded into the system without, by replacing all instances of the last rule by appropriate coercion terms:

χ^{τ/e≤τ′/e′}(E) = let^{e⪯e′} x ⇐ E in val^{e′} χ^{τ≤τ′}(x)
χ^{ι≤ι}(a) = a
χ^{τ_{1}→^{e}τ_{2}≤τ′_{1} →^{e′}τ′_{2}}(f) = λa.χ^{τ_{2}/e≤τ′_{2}/e′}(f (χ^{τ′_{1}≤τ_{1}}(a)))
χ^{τ_{1}×τ_{2}≤τ′_{1}×τ′_{2}}(p) = (χ^{τ_{1}≤τ′_{1}}(π_{1} p), χ^{τ_{2}≤τ′_{2}}(π_{2} p))
χ^{τ_{1}+τ_{2}≤τ′_{1}+τ′_{2}}(s) = case(s, \begin{matrix}x_{1}. inl (χ^{τ_{1}≤τ′_{1}}(x_{1})) \\ x_{2}. inr (χ^{τ_{2}≤τ′_{2}}(x_{2}))) \end{matrix}

As always with subtyping systems, there is a potential coherence problem: the semantics must ensure that different ways of inserting coercions in a program give the same result. We will see that for our application, this is automatically ensured (see the note following Theorem 11).

2.2 Layered monads and effect-semantics

For concreteness, we present a denotational semantics of our language in the setting of CPOs (chain-complete posets, not necessarily containing least elements) and continuous functions. This specific choice is not essential, however.

We start with a standard concept:

Definition 1 A monad T consists of a triple (T, η, ⋆), where T maps every CPO A to a CPO of A-computations; η is a family of value-inclusion functions η_{A} : A → T A; and ⋆ (normally written infix) is a family of binding functions ⋆_{A,B} : T A × (A → T B) → T B; such that for any f : A → T B and g : B → T C,

η a ⋆ f = f a, t ⋆ η = t, and (t ⋆ f) ⋆ g = t ⋆ (λa. f a ⋆ g)

(We generally omit the type subscripts on η and ⋆ when they are clear from the context.) When f : A → B, we also define T f = λt. t ⋆ (η ∘ f) : T A → T B; and when f : A → T B, f^{∗} = λt. t ⋆ f : T A → T B.

Intuitively, elements of T A represent effectful computations yielding values in A. η a represents the trivial (effectfree) computation of a, while t⋆f represents the computation consisting of evaluating t to a value a (possibly with some effects), followed by evaluating f a (again possibly with effects). The monad laws ensure that the sequencing of effects is well-behaved.

A very simple monad is the identity monad, with IA = A, η_{A} a = a, and t⋆f = f t. An important non-trivial example is the lifting monad, where the computation-type constructor is domain-theoretic lifting, LA = A_{⊥}; unit is the inclusion, η a = [a]; and binding is strict extension, ⊥ ⋆ f = ⊥ and [a] ⋆ f = fa.

We now introduce a concept useful for stacking monads:

Definition 2 A layering of a monad T over another monad \overline{T} = (\overline{T} , \overline{η}, \overline{⋆}) consists of a function family ζ_{A} : \overline{T} (T A)→T A, such that each (T A, ζ_{A}) is a \overline{T} -algebra [ML71, VI.2], i.e.,

ζ_{A} ∘ \overline{η}_{T A} = id_{T A} and ζ_{A} ∘ id\overline{∗} ; \overline{T} (T A) = ζ_{A} ∘ \overline{T} ζ_{A}

and such that every f^{∗} is a \overline{T} -algebra morphism, i.e.,

f^{∗} ∘ ζ_{A} = ζ_{B} ∘ \overline{T} f^{∗} : \overline{T} (T A) → T B

The definition of layering is a bit more technical, but captures the requirement that a \overline{T} -computation can be meaningfully interpreted as a more general T -computation. When T is explicitly constructed in terms of \overline{T}, we can generally obtain a suitable ζ directly from the shape of T, as shown in Section 2.3. And the additional condition on f^{∗} is usually immediate to verify – informally it expresses that the T -computation represented by t ⋆ f performs any latent \overline{T} - effects in t “first”.

Any monad T can be layered over itself by id_{T A}^{∗} : T (T A) → T A. And, if T is layered over \overline{T} by ζ, and \overline{T} over \overline{\overline{T}} by \overline{ζ}, then T is also layered over \overline{\overline{T}} by ζ_{A} ∘ \overline{ζ}_{T A} ∘ \overline{\overline{T}} \overline{η}_{T A} : \overline{\overline{T}} (T A) → T A.

When T is layered over \overline{T} , we can also define a computation-inclusion or lifting [LHJ95, Tol98] function family i_{A} = ζ_{A} ∘ \overline{T} η_{A} : \overline{T} A → T A. This is easily checked to be a monad morphism [Mog90], i.e., to satisfy the equations

i_{A} (\overline{η}_{A} a) = η_{A} a and i_{B} (t′ \overline{⋆} f) = i_{A} t′ ⋆ (λa.i_{B} (f a))

Conversely, given a monad morphism i : \overline{T} → T, we can obtain a layering by ζ_{A} = id_{T A}^{∗} ∘ i_{A}. Both formulations allow us to define a “mixed” binding operation ˜⋆_{A,B} : \overline{T} A × (A → T B) → T B by:

t′ ˜⋆_{A,B} f = (i_{A} t′) ⋆_{A,B} f = ζ_{B} (t′ \overline{⋆}_{A,T B} (λa.\overline{η}_{T B} (f a)))

Defining layering in terms of inclusions may seem more natural, but it turns out that taking ζ as the primitive notion leads to a more direct implementation of monadic effects in Section 3.

Any monad can be trivially layered over identity by taking ζ_{A} t = t. It can be layered over lifting when each T A is a pointed CPO (i.e., has a least element ⊥_{T A}, allowing ζ ⊥ = ⊥_{T A} and ζ [t] = t) and f^{∗} is always strict (that is, if the original computation t has a divergence-effect, then so will t⋆ f). Conversely, if T is layered over lifting, T A is necessarily pointed (because for any t ∈ T A, ζ ⊥ ⊑ ζ [t] = t), and f^{∗} is strict (because f^{∗} (ζ ⊥) = ζ (Lf^{∗}⊥) = ζ ⊥).

We can now define a semantics of our language. This will be done in the style of Church, i.e., we only give meanings to well-typed terms:

Definition 3 (effect-semantics) A semantics L of an effect-language L assigns first to every base type b, a CPO B(b); and to every effect e, a monad E(e) = (T^{e}, η^{e}, ⋆^{e}), such that if e′ ≺ e then E(e) is layered over E(e′) by ζ^{e}. This assignment induces a semantics of general L-type phrases as follows. Let ϱ be an assignment of CPOs to type variables in α⃗. Then for any type τ over α⃗, we define a CPO L[[τ]]_{ϱ}, as follows:

L[[α]]_{ϱ} = ϱ α
L[[b]]_{ϱ} = B(b)
L[[τ_{1} × τ_{2}]]_{ϱ} = L[[τ_{1}]]_{ϱ} × L[[τ_{2}]]_{ϱ}
L[[τ_{1} + τ_{2}]]_{ϱ} = L[[τ_{1}]]_{ϱ} + L[[τ_{2}]]_{ϱ}
L[[τ_{1} →^{e} τ_{2}]]_{ϱ} = L[[τ_{1}]]_{ϱ} → T^{e}L[[τ_{2}]]_{ϱ}

This also extends straightforwardly to a semantics of type assignments,

L[[Γ]]_{ϱ} = ∏_{x∈dom Γ} L[[Γ(x)]]_{ϱ}

Further, L must assign to every constant c of L a family of elements C(c)A⃗ ∈ L[[Σ(c)]]_{[α⃗↦A⃗]}. Then we define for every well-typed term Γ ⊢α⃗ E : τ/e, its meaning L[[E]]_{ϱ} : L[[Γ]]_{ϱ} → T^{e}L[[τ]]_{ϱ} (omitting the subscript ϱ on all semantic brackets):

L[[x]]ρ = ρx
L[[c_{τ_{1},...,τ_{n}}]]ρ = C(c)_{L[[τ_{1}]],...,L[[τ_{n}]]}
L[[λx^{τ}.E]]ρ = λa^{L[[τ]]}.L[[E]]ρ[x ↦ a]
L[[E_{1} E_{2}]]ρ = L[[E_{1}]]ρ(L[[E_{2}]]ρ)
L[[val^{e} E]]ρ = η^{e} (L[[E]]ρ)
L[[let^{e} x ⇐ E_{1} in E_{2}]]ρ = L[[E_{1}]]ρ ⋆^{e} (λa.L[[E_{2}]]ρ[x ↦ a])
L[[let^{e_{1},e_{2}} x ⇐ E_{1} in E_{2}]]ρ =

ζ^{e_{2}}(L[[E_{1}]]ρ ⋆^{e_{1}} (λa.η^{e_{1}} (L[[E_{2}]]ρ[x ↦ a])))

(together with straightforward clauses for sums and products).

Finally, L must include a collection of result interpretation functions ξ_{b}^{e} : T^{e}B(b) → P_{⊥} from meanings of complete programs to observations, where P is some countable set of final outputs, such as character strings. For a complete program, ⊢ E : b / e, we can then define

L̂[[E]] = ξ_{b}^{e} (L[[E]]_{∅} ∅)

In the standard semantics of the language, we take E(𝔫) as the identity monad and E(𝔭) as lifting. (An implementation semantics, however, may use a different interpretation: for example, we can give a continuation-based semantics of partiality; the result interpretation function must then be adjusted appropriately.) We will also always use the standard interpretation of fix,

C(fix^{e})_{A_{1},A_{2}} = λf^{(A_{1}→T^{e}A_{2})→A_{1}→T^{e}A_{2}}.⨆_{i∈ω} f^{i}(λa.⊥_{T^{e}A_{2}})

where T^{e}A_{2} is pointed because e is layered above partiality.

We can reason about terms in the language by means of a formal equational theory, including in particular the equations

(λx.E_{1})E_{2} = E_{1}[E_{2}/x]
λx.E x = E (x∉F V (E))
val^{𝔫} E = E
let^{e_{1}⪯e_{2}} x ⇐ val^{e_{1}} E_{1} in E_{2} = E_{2}[E_{1}/x]
let^{e} x ⇐ E in val^{e} x = E

let^{e_{2}⪯e_{3}} x_{2} ⇐ (let^{e_{1}⪯e_{2}} x_{1} ⇐ E_{1} in E_{2}) in E_{3}

=

let^{e_{1}⪯e_{3}} x_{1} ⇐ E_{1} in let^{e_{2}⪯e_{3}} x_{2} ⇐ E_{2} in E_{3}

(x_{1}∉F V (E_{3}))

(together with the usual ones for products and sums). Note that the strong βη-rules for functions are only valid because we restrict the terms in an application to have no effects.

2.3 Adding a new effect

Of course, we can always enrich the language by adding a new effect at the level of the semantics. But a wide variety of effects can also be defined purely syntactically:

Definition 4 A formal monad T over effect ē in L consists of a type constructor and three polymorphic terms,

T− : Type → Type
glue_{α} : (1 →^{ē} Tα) → Tα
unit_{α} : α → Tα
bind_{α_{1},α_{2}} : Tα_{1} × (α_{1} → Tα_{2}) → Tα_{2}

Such a T denotes an (actual) monad L[[T]]^{m} = (T, η, ⋆, ζ) layered over E(ē) in a semantics L of L if L[[Tα]]_{[α ↦ A]} = T A, L[[glue_{α}]]_{[α ↦ A]}∅ = λt. ζ_{A} (t()), L[[unit_{α}]]_{[α ↦ A]}∅ = η_{A}, and L[[bind_{α_{1},α_{2}}]]_{[α_{1} ↦ A_{1},α_{2} ↦ A_{2}]}∅ = (⋆_{A_{1},A_{2}}).

Note that we do not require that T denote a monad for all interpretations of the effect ē. For example, the formal list monad (used to give a semantics of nondeterminism in Section 4.2) can only be properly layered over a commutative monad [KW93], such as partiality.

The component glue can usually be constructed systematically from just the form of T, as follows:

Tα  glueT_{α} : (1 →^{ē} Tα) → Tα
Fα →^{ē} Gα λt.λa.letē f ⇐ t() in f a
Fα →^{𝔫} T′α λt.λa.glueT′_{α} (λ().letē f ⇐ t() in valē f a)
T_{1}α × T_{2}α λt.(\begin{matrix}glueT_{1}_{α} (λ().letē p ⇐ t() in valē π_{1} p), \\ glueT_{2}_{α} (λ().letē p ⇐ t() in valē π_{2} p)) \end{matrix}

(In fact, in most cases, the first rule alone suffices.) It is easy to check that such a glue^{T} satisfies the \overline{T} -algebra conditions of Definition 2; and the verification of the additional property of bind is usually straightforward.

Given T we construct an extension L^{T} of L, with a new effect 𝔱 and new proto-operations, monadic reflection and reification [Fil94]:

reflect_{α}^{𝔱} : Tα →^{𝔱} α
reify_{α}^{𝔱} : (1 →^{𝔱} α) → Tα

When E : Tτ/𝔫, we often write μ^{𝔱}(E) : τ/𝔱 for reflect_{τ}^{𝔱} E; and conversely, when E : τ/𝔱, [E]^{𝔱} : Tτ/𝔫 for reify^{𝔱} (λ().E). Informally, evaluating μ(E) performs the action represented by the datum E, while [E] returns a datum representing the action that would result from evaluating E.

Note that L^{T} is a proper extension of L: any L-program is still a valid L^{T} program with the same meaning. This means that we can define the semantics of L^{T} by a formal monadic translation |−|_{T} back into L, expanding out only the new type and term constructors into their L-definitions.

First, the translation of an effect e is an effect-type constructor |e|_{T}:

|𝔱|α = Tα/𝔫
|e|α = α/e (e ≠ 𝔱)

For types, only function spaces have a non-trivial translation:

|τ_{1} →^{e} τ_{2}| = |τ_{1}| →^{e′} τ′_{2} where τ′_{2}/e′ = |e||τ_{2}|

And finally, we define a translation |−|_{T} of terms: if Γ ⊢ E : τ / e then |Γ|_{T} ⊢ |E|_{T} : |e|_{T}|τ|_{T}. Again, the only nontrivial clauses are:

|val^{𝔱} E| = unit_{|τ|} |E|

|let^{𝔱} x ⇐ E_{1} in E_{2}| = bind_{|τ_{1}|,|τ_{2}|} (|E_{1}|, λx^{|τ_{1}|}.|E_{2}|)
|let^{ē,𝔱} x ⇐ E_{1} in E_{2}| =

glue_{|τ_{2}|} (λ().letē x ⇐ |E_{1}| in valē |E_{2}|)

|reflect_{τ}^{𝔱} | = λt^{T|τ|}.t
|reify_{τ}^{𝔱} | = λt^{1→T|τ|}.t()

This syntactic translation agrees with the denotational semantics:

Lemma 5 L[[|−|_{T}]] = L^{T} [[−]] where L^{T} is the semantics of L^{T} determined by extending L with E(𝔱) = T = L[[T]]^{m}, C(reflect)_{A} = λt^{T A}.t, and C(reify)_{A} = λt^{1→T A}.t().

For example, given some base type exn of exception names, the formal monad Ex of exceptions is defined by:

Tα = 1 →^{ē} (α + exn)
glue_{α} = λt^{1\underrightarrow{ē}Tα}.λ().letē r ⇐ t() in r ()
unit_{α} = λa^{α}.λ(). inl a
bind_{α_{1},α_{2}} = λ(t, f)^{Tα_{1}×(α_{1}→Tα_{2})}.λ().

letē r ⇐ t() in case(r, a.f a(), x.valē inr x)

This does in fact denote a monad for any monadic interpretation of ē. Calling the new effect 𝔢𝔵, we can define operations in L^{T} with types

raise_{α} : exn →^{𝔢𝔵} α
handle_{α} : (1 →^{𝔢𝔵} α) → (exn →^{𝔢𝔵} α) →^{𝔢𝔵} α

in terms of the proto-operations:

raise_{α} = λx^{exn}.μ^{𝔢𝔵}(λ().valē inr x)
handle_{α} = λt^{1\underrightarrow{𝔢𝔵} α}.λh^{exn\underrightarrow{𝔢𝔵} α}.let^{ē,𝔢𝔵} r ⇐ [t()]^{𝔢𝔵} () in case(r, a.val^{𝔢𝔵} a, x.hx)

That is, raise constructs an exception-computation that immediately returns with a right-tagged x, and reflects that as an 𝔢𝔵-effect. Conversely handle reifies t into a ē-computation of a sum-typed value, performs that computation, and either returns the result or passes the exception name to the handler h. It is easy to check that the semantics of these operations capture the usual behavior of ML-style exceptions, even in the presence of state as an ē-effect.

Note that we can often reason about L^{T}-programs directly, without either expanding them into L-programs, or computing their denotational meanings. In particular, we have the following sound equations for well-typed terms:

μ([E]) = E
[μ(E)] = E
[val^{𝔱} E] = unit E
[let^{𝔱} x ⇐ E_{1} in E_{2}] = bind ([E_{1}], λx.[E_{2}])
[let^{e⪯𝔱} x ⇐ E_{1} in E_{2}] =

glue(λ().let^{e⪯ē} x ⇐ E_{1} in valē[E_{2}]) (e⪯ē≺𝔱)

From these, and the equations at the end of Section 2.2, it is easy to derive laws about the particular operations, such as

let^{𝔢𝔵} r ⇐ raisex in E = raisex
handle(λ().val^{𝔢𝔵} a)h = val^{𝔢𝔵} a
handle(λ().raisex)h = hx

2.4 Effect-ordering and monadic reflection

The hierarchical organization among the effects is crucial to the translation-based definition. Although being able to integrate effects “flatly” (i.e., with no mutual ordering) might seem a desirable goal, often different orderings correspond to different intended semantics, as illustrated below.

An important consequence of the layering is that some source terms are meaningless, even if their effect-erasures are simply-typable. Specifically, attempting to apply the reification operator of a lower-level effect to a higher-level computation has no counterpart in a program written with explicit effect-passing, and thus cannot be given a well-defined meaning by the translation. Where appropriate, the desired meaning of such a construct must instead be expressed explicitly. As a simple example, let us analyze this issue in the context of mutable state and exceptions.

We saw the definitions of raise and handle in Section 2.3. Similarly, using the formal state monad St, with type constructor

ST α = state →^{ē} (α × state)

for some base type state, we can define a new effect 𝔰𝔱, with operations

get : 1 →^{𝔰𝔱} state
set : state →^{𝔰𝔱} 1
withst_{α} : state × (1 →^{𝔰𝔱} α) →^{ē} α

as follows:

get = λ().μ^{𝔰𝔱}(λs.valē (s, s))
set = λn.μ^{𝔰𝔱}(λs.valē ((), n))
withst_{α} = λ(s, t).letē (a, s′) ⇐ [t()]^{𝔰𝔱} s in valē a

But how do these operations interact with those for exceptions?

First, consider the ML-like layering of exceptions above state above partiality, 𝔭 ≺ 𝔰𝔱 ≺ 𝔢𝔵, with the state persistent across exceptions. The composite translation, defining away first exceptions and then state, corresponds to the following effect type:

||α/𝔢𝔵|_{EX} |_{ST} = |1 →^{𝔰𝔱} α + exn|_{ST}

= 1 → state →^{𝔭} (α + exn) × state

That is, when started in some initial state from state, a computation may diverge; or it may result in a new state together with either an α-value or raised exception from exn. The proto-operators have types:

reify_{α}^{𝔰𝔱} : (1 →^{𝔰𝔱} α) → state →^{𝔭} α × state
reflect_{α}^{𝔰𝔱} : (state →^{𝔭} α × state) →^{𝔰𝔱} α
reify_{α}^{𝔢𝔵} : (1 →^{𝔢𝔵} α) → 1 →^{𝔰𝔱} (α + exn)
reflect_{α}^{𝔢𝔵} : (1 →^{𝔰𝔱} (α + exn)) →^{𝔢𝔵} α

In this setting, we can always coerce a 𝔰𝔱-computation into an 𝔢𝔵-computation (and with the subtyping system, this coercion can be left implicit). This means that the previous definition of handle, based on 𝔢𝔵-reification, works without changes even when the expression being guarded has only state-effects (which includes partiality-effects).

But if we want to extend withst to computations which may raise exceptions, we must explicitly account for those.

For example, we can define a more general operation

withst’_{α} : state × (1 →^{𝔢𝔵} α) →^{𝔢𝔵} α
withst’_{α} =

λ(s, t).let^{𝔢𝔵} (r, s′) ⇐ [[t()]^{𝔢𝔵} ()]^{𝔰𝔱} s in μ^{𝔢𝔵}(λ(). val^{𝔰𝔱} r)

Here we first explicitly 𝔢𝔵-reify the original computation of α into a 𝔰𝔱-computation of α+exn, perform the original withstoperation, and finally 𝔢𝔵-reflect back the result, which may have the effect of raising an exception.

Note that when withst’, is applied to a computation that provably does not have exception-effects, its behavior also provably coincides with the original withst. That is, we can show

withst’(s, λ().let^{𝔰𝔱,𝔢𝔵} x ⇐ E in val^{𝔢𝔵} x) = let^{𝔭⪯𝔢𝔵} x ⇐ withst(s, λ().E) in val^{𝔢𝔵} x

using the equations from the end of Section 2.3. In a general optimizer for higher-order programs, however, it seems preferable to maintain explicit effect-types everywhere, as advocated by Tolmach [Tol98].

Note also that the behavior of withst’ differs from that of a more naive definition,

withst”_{α} =

λ(s, t).let^{𝔰𝔱,𝔢𝔵} o ⇐ get() in let^{𝔰𝔱,𝔢𝔵} () ⇐ sets in let^{𝔢𝔵} r ⇐ t() in let^{𝔰𝔱,𝔢𝔵} () ⇐ seto in val^{𝔢𝔵} r

Here, an unhandled exception raised in t() does modify the global state, which makes an observable difference if the exception is eventually handled somewhere.

Yet both versions behave the same on programs that never actually raise exceptions. Thus, it is not sufficient to merely require that programs in the original language (partiality and state) should retain their meaning in the extended language (partiality, state, and exceptions); the interactions of effects need to be considered explicitly in each case.

On the other hand, suppose we want a transactional semantics with transient state layered atop exceptions, corresponding to effect-type

||α/𝔰𝔱|_{ST} |_{EX} = |state →^{𝔢𝔵} α × state|_{EX} = state → 1 →^{𝔭} (α × state) + exn

Here the type already shows that the state must be discarded if a computation aborts with an exception. When 𝔭 ≺ 𝔢𝔵 ≺ 𝔰𝔱, the monad reflection operators have types

reify_{α}^{𝔰𝔱} : (1 →^{𝔰𝔱} α) → state →^{𝔢𝔵} α × state
reflect_{α}^{𝔰𝔱} : (state →^{𝔢𝔵} α × state) →^{𝔰𝔱} α
reify_{α}^{𝔢𝔵} : (1 →^{𝔢𝔵} α) → 1 →^{𝔭} (α + exn)
reflect_{α}^{𝔢𝔵} : (1 →^{𝔭} (α + exn)) →^{𝔢𝔵} α

Thus, 𝔰𝔱-reification of any computation is well-defined, but we need to explicitly define the meaning of 𝔢𝔵-reifying a computation which may have state effects, as when handling exceptions. In this case, a natural revised definition of handle is

handle’_{α} = λt^{1\underrightarrow{𝔰𝔱} α}.λh^{exn\underrightarrow{𝔰𝔱} α}.

μ^{𝔰𝔱}(λs.let^{ē,𝔢𝔵} r ⇐ [[t()]^{𝔰𝔱} s]^{𝔢𝔵} () in case(r, (a, s′).val^{𝔢𝔵} (a, s′), x.[hx]^{𝔰𝔱} s)) where the state threading is made explicit before 𝔢𝔵reification.

It is worth reiterating that these considerations typically only arise when we want to assign well-defined meanings to all terms in a language without an effect-typing system, but with effect-delimiting operations such as handle or withst. If we are only using reflection and reification as a more concise notation for programs written with explicit effect-passing, such conflicts have by definition already been resolved in the original program.

3 Implementing layered effects

The previous section describes a framework for adding programmer-defined effects to an ML-like language. However, a direct implementation of this semantics would be problematic for several reasons:

• In the context of a full programming language, it requires us to effectively write a full language processor, including parser, type checker, module system, standard library, etc.; or, at the very least, perform major surgery on an existing implementation.

• Each level of translation imposes a potentially substantial execution-time overhead – especially for programs which only rarely use any particular effect, but must still provide the infrastructure for connecting such scattered uses.

• Perhaps most significantly, the semantics is given by induction on explicitly sequenced, fully effect-annotated terms. Although this verbosity is essentially equivalent to writing a program in explicit monadic style, it imposes an uncomfortably heavy burden on the programmer accustomed to ML’s anonymous (and, given a guarantee of left-to-right call-by-value evaluation, often completely implicit) sequencing of computations.

In this section we show how all of these problems can be solved. In doing so, we demonstrate that the monad equations and the layering conditions are not merely arbitrary category-theoretic overhead, or a mere convenience for manual or automated reasoning about programs, but are in fact the key to a vastly more efficient implementation of the specification.

The result falls in two parts: (1) that each individual monadic translation can be uniformly simulated by a layer of continuation-passing, and (2) that any tower of continuation-passing layers can be simulated by a single notion of effect comprising Scheme-style first-class continuations and mutable state.

We phrase these simulations in terms of realizations of one language in another, where a realization of an effectlanguage L′ ⊇ L replaces (not necessarily injectively) every new effect of L′ with an effect of L, and every new constant of L′ by a term of L, such that the meanings of complete L′-programs are preserved.

3.1 Relating monadic effects to continuationpassing

It is a fairly simple observation that continuation-passing can simulate monadic style [PW93], but actually showing that the translations are equivalent is surprisingly complicated.

This was sketched in [Fil94] for a single effect in an otherwise completely pure language; unfortunately the retractionbased approach [MW85] used there does not seem to generalize well to more general settings, such as unrestricted recursion. In [Fil96], the proof was redone with admissible relations in the style of [Rey74], and extended to a base language with arbitrary pre-existing effects; and that approach does generalize to the multi-effect language of the previous section, as sketched in the following.

One major complication is that to obtain a proper simulation, we must pick the answer type for the CPS transform “large enough”. In particular, this means that we cannot use a simple base type, but will need a recursively defined type of answers in the implementation language L_{μ} (the specification language L ⊂ L_{μ} remains simply typed).

Let ē be some effect of L, 𝔨 (gothic “k”) a new effect name, and ω some fixed type with effects from L extended with 𝔨. We then define L^{K} as L extended with ē ≺ 𝔨, and two new constants shift and reset, with types

shift_{α} : ((α →^{ē} ω) →^{𝔨} ω) →^{𝔨} α
reset : (1 →^{𝔨} ω) →^{ē} ω

We write S_{α}k. E as syntactic sugar for shift_{α} (λk.E), and #E for reset(λ().E). (Conversely, we have shift_{α} = λh. S_{α}k. hk and reset = λt. #(t()).)

Informally, Sk. E evaluates E with k bound to a functional representation of the current evaluation context, but with E itself evaluated in an empty context. Conversely, #E evaluates E in an empty evaluation context, and returns the result to the current context. For example, writing out all the sequencing explicitly,

letē r ⇐ #(let^{𝔨} n ⇐ (Sk. letē x ⇐ k 3 in k x) in val^{𝔨} 2 × n) in valē 1 + r

= valē 1 + 2 × (2 × 3) = valē 13

Much like for general effects, we give the formal semantics of L^{K} by a continuation-passing translation into L_{μ}. For any type χ, we define first a parameterized translation of the effect 𝔨 as an effect-type constructor:

|𝔨|_{K(χ)}α = ((α →^{ē} χ) →^{ē} χ)/𝔫

Let ω̂ = μχ. |ω|_{K(χ)}, with isomorphisms

ϕ : |ω|_{K(ω̂)} → ω̂ and ψ : ω̂ → |ω|_{K(ω̂)}

(Note that if ω does not contain any 𝔨-effects, so that |ω|_{K(χ)} does not actually depend on χ, we can simply take ω̂ = ω and the isomorphisms as identities.) We can then define the formal monad K of ω̂-continuations by

T^{𝔨}α = Kα = (α →^{ē} ω̂) →^{ē} ω̂
glue^{𝔨} t = λk.letē r ⇐ t() in r k
unit^{𝔨} a = λk.k a
bind^{𝔨} (t, f) = λk.t(λa.f ak)

It is easy to check that this determines an actual monad K = L[[K]]^{m} for any interpretation of ē.

We use the formal monad to define the syntactic translation |−|_{K}, extended with the clauses for the specialized control operators:

|shift_{τ} | = λh^{(|τ|\underrightarrow{ē}|ω|)→(|ω|\underrightarrow{ē}ω̂)\underrightarrow{ē}ω̂}.λk^{|τ|\underrightarrow{ē}ω̂}.
h(λx^{|τ|}.letē a ⇐ k x in valē ψ a) (λr^{|ω|}.valē ϕr)

|reset| = λt^{1→(|ω|\underrightarrow{ē}ω̂)\underrightarrow{ē}ω̂}.
letē a ⇐ t()(λr^{|ω|}.valē ϕr) in valē ψ a

(We could also have these operators explicitly in terms of μ^{𝔨}(−), [−]^{𝔨}, ϕ and ψ; the result of the translation would be the same.)

Note that shift and reset are the only operations that actually depend on the choice of ω̂ as the answer type. As usual for a continuation-passing translation, everything else is parametric in the answer type.

Further, let d be a sufficiently large type to embed any L^{T}- type at which we want to reify. (For any particular program, this can always be chosen as a finite sum; and if we only need to reify at outermost level, e.g., for state, it can even be a base type.) More precisely, let ℵ be a (finite or infinite) set of types, with functions

in_{τ} : τ →^{𝔫} d and out_{τ} : d →^{𝔭} τ

for every τ in ℵ, such that out_{τ} (in_{τ} a) = val^{𝔭} a for any τvalue a.

For the actual simulation, we now take ω = Td, allowing us to define a realization ΦT^{𝔱,𝔨} of L^{T} in L^{K} by Φ(𝔱) = 𝔨, and

Φ(reflect_{α}^{𝔱}) ≡

λt^{Tα}.S_{α}k^{α\underrightarrow{ē}Td}. val^{𝔨} bind_{α,d} (t, λa^{α}.glue_{d}(λ().k a))

Φ(reify_{α}^{𝔱}) ≡

λt^{1\underrightarrow{𝔨}α}.glue_{α} (λ().

letē r ⇐ #(let^{𝔨} a ⇐ t() in val^{𝔨} unit_{d}(in_{α}a))

in valē bind_{d,α} (r, λd^{d}.let^{𝔭} x ⇐ out_{α} d in unit_{α} x))

We want to show that for every L^{T}-program ⊢ E : b/𝔭, the two translations give the same result. More precisely, we will show that given a specification semantics L_{s} and implementation semantics L_{i} of L, such that for complete L-programs, E, L̂_{s}[[E]] = L̂_{i}[[E]], then also L̂_{s}[[|E|_{T}]] = L̂_{i}[[|E{ΦT^{𝔱,𝔨}}|_{K}]] for complete L^{T}-programs E. But we cannot show this statement (or any simple variation of it) directly by induction on E: the problem is that at higher types, there is no direct equational characterization of the relationship between |E|_{T} and |E|_{K}. Instead, we use a more general relational invariant, that will give us the original equation as a special case.

We say that a relation R ⊆ A × A′ between two CPOs A and A′ is admissible if it is chain-complete, i.e., if the least upper bounds of pointwise R-related chains are also Rrelated. We write ARel(A, A′) for the set of all admissible relations between A and A′.

Definition 6 A logical relation R between L_{s} and L_{i} of an effect-language L assigns to every base type b a relation B^{r}(b) ∈ ARel(B_{s}(b), B_{i}(b)) between their interpretations; and to every effect e, a relational action E^{r}(e), mapping any relation R ∈ ARel(A, A′) to E^{r}(e)R ∈ ARel(T_{s}^{e}A, T_{i}^{e}A).

Let ϱ and ϱ′ map type variables from α⃗ to CPOs, and for each α let θα ∈ ARel(ϱα, ϱ′α). For any type τ over α⃗, we then define a relation R[[τ]]_{θ} ∈ ARel(L_{s}[[τ]]_{ϱ}, L_{i}[[τ]]_{ϱ′}) by:

R[[α]]_{θ} = θα
R[[b]]_{θ} = B^{r}(b)
R[[τ_{1} × τ_{2}]]_{θ} = {((a_{1}, a_{2}), (a′_{1}, a′_{2})) |
(a_{1}, a′_{1}) ∈ R[[τ_{1}]]_{θ} ∧ (a_{2}, a′_{2}) ∈ R[[τ_{2}]]_{θ}}
R[[τ_{1} + τ_{2}]]_{θ} = {((1, a_{1}), (1, a′_{1})) | (a_{1}, a′_{1}) ∈ R[[τ_{1}]]_{θ}} ∪
{((2, a_{2}), (2, a′_{2})) | (a_{2}, a′_{2}) ∈ R[[τ_{2}]]_{θ}}
R[[τ_{1} →^{e} τ_{2}]]_{θ} = {(f, f′) | ∀(a, a′) ∈ R[[τ_{1}]]_{θ}.
(f a, f′ a′) ∈ E^{r}(e)(R[[τ_{2}]]_{θ})}

It is easy to check that these relations are all admissible.

Moreover, the relations must respect interpretations of effects and constants: for every e of L we require that,

1. If ē ≺ e and (t, t′) ∈ E^{r}(ē)(E^{r}(e)R) then (ζ_{s}^{e}_{A} t, ζ_{i}^{e}_{A′} t′) ∈ E^{r}(e)R.

2. If (a, a′) ∈ R then (η_{s}^{e}_{A} a, η_{i}^{e}_{A′} a′) ∈ E^{r}(e)R.

3. If (t, t′) ∈ E^{r}(e)R_{1} and for every (a, a′) ∈ R_{1}, (f a, f′ a′) ∈ E^{r}(e)R_{2} then (t ⋆_{s}^{e} f, t′ ⋆_{i}^{e} f′) ∈ E^{r}(e)R_{2}.

And for c : ∀α⃗. τ in Σ_{L}, and any relation-environment θ with θα_{i} ∈ ARel(A_{i}, A′_{i}) for each α_{i},

(C_{s}(c)A⃗, C_{i}(c)A⃗′) ∈ R[[τ]]_{θ}

Finally, we require that related meanings of complete programs are interpreted as the same observation, i.e., if (p, p′) ∈ E^{r}(e)B^{r}(b) then ξ_{s}_{b}^{e} p = ξ_{i}_{b}^{e} p′.

For our purposes it suffices to take the relation at base types to be simple equality, i.e.,

B^{r}(b) = {(n, n) | n ∈ B(b)}

When L_{i} also interprets 𝔭 as the lifting monad, we can define the relational action of 𝔭 by:

E^{r}(𝔭)R = {(⊥, ⊥)} ∪ {([a], [a′]) | (a, a′) ∈ R}

(Note that then E^{r}(𝔭)B^{r}(b) becomes simply the equality relation on B(b)_{⊥}.) In other cases, we must explicitly construct a suitable action, as in the proof of Theorem 11 later.

We can now state the usual logical-relations lemma, straightforwardly extended to effects and polymorphic terms:

Lemma 7 (Logical relations lemma) Let there be given a logical relation between L_{s} and L_{i}. Let α⃗ be a list of type variables, ϱ and ϱ′ type environments, and θ a relation environment, such that for each α, θα ∈ ARel(ϱα, ϱ′α). Let Γ be a type assignment over α⃗, and let ρ and ρ′ be environments such that for every x ∈ dom Γ, ρx ∈ L_{s}[[τ]]_{ϱ}, ρ′x ∈ L_{i}[[τ]]_{ϱ′}, and (ρx, ρ′ x) ∈ R[[Γ(x)]]_{θ}. Then for every well-typed term Γ ⊢α⃗ E : τ/e,

(L_{s}[[E]]_{ϱ}ρ, L_{i}[[E]]_{ϱ′}ρ′) ∈ E^{r}(e)(R[[τ]]_{θ})

Proof. Straightforward induction on E.

Note that the standard interpretations of fix^{e} are always related. This is easily seen by fixed-point induction, using the fact that R[[τ_{1} →^{e} τ_{2}]]_{θ} is admissible and contains (⊥, ⊥) when 𝔭 ⪯ e (follows from Definition 6(1–3)).

Much as we previously interpreted a type constructor as a CPO constructor, we can define for any type constructor T its relational action, T^{r} : ARel(A, A′) → ARel(L_{s}[[Tα]]_{[α↦A]}, L_{i}[[Tα]]_{[α↦A]}) by T^{r}R = R[[Tα]]_{[α↦R]}.

Suppose now we have a logical relation between semantics L_{s} and L_{i} of language L, and we want to extend it to L^{T}, where we take E_{s}(𝔱) = T and E_{i}(𝔱) = K in the extended semantics. We then need to define E^{r}(𝔱). Intuitively, we are representing a T -computation t by the K-computation u = λk. k^{∗}t. So we want something like

(t, u) ∈ E^{r}(𝔱)R ⟺ (λk. t ⋆ k, u) ∈ K^{r}R where K^{r} is the natural choice: two K-computations u and u′ are related by K^{r}R if for all continuations k and k′ mapping R-related values to T^{r}O-related results, uk is T^{r}Orelated to u′ k′, for some suitable relation O on u. But how to pick O? A suitable answer is to take O as the intersection (always admissible) of all the relational interpretations we will actually need. Formally:

Lemma 8 The relational action E^{r}(𝔱) of 𝔱 defined by

E^{r}(𝔱)R = {(t, u) ∈ T A × KA′ |
∀τ ∈ ℵ. ∀O ∈ ARel(L_{s}[[τ]], L_{i}[[d]]).
∀k : A → L_{s}[[Tτ]], k′ : A′ → L_{i}[[Td]].

(∀(a, a′) ∈ R. (k a, ζ (ψ (k′ a′))) ∈ T^{r}O)

⇒ (t ⋆ k, ζ (ψ (uk′))) ∈ T^{r}O}

extends the logical relation between semantics L_{s} and L_{i} of L to one between L_{s}^{T} and L_{i}^{K} ∘ ΦT^{𝔱,𝔨} of L^{T}.

Proof. Relatively direct verification for both the new effect 𝔱 and the new constants reflect^{𝔱} and reify^{𝔱} [Fil96]. For the latter two, we use the fact that (by Lemma 7) the interpretations of the term components of T are related, even if T does not actually define a monad in L_{i}.

Theorem 9 (T-K simulation) Let L_{s} and L_{i} be related semantics of L, and let E be a complete L^{T}-program, i.e., ⊢ E : b / 𝔭. Then L̂_{s}[[|E|_{T}]] = L̂_{i}[[|E{ΦT^{𝔱,𝔨}}|_{K}]].

Proof. By Lemmas 7 and 8, (L_{s}[[|E|_{T}]]∅, L_{i}[[|E{Φ_{T}|_{K}}^{𝔱,𝔨}]]∅) ∈ E^{r}(𝔭)B^{r}(b), from which the result follows by the assumption on ξ_{s} and ξ_{i}.

3.2 Relating continuation-passing to primitive effects

Let us now consider an implementation language essentially like Scheme or SML/NJ, i.e., containing first-class continuations and state as primitive effects. To keep things simple, we consider all state to be allocated before program execution proper begins.

That is, for a state-assignment Δ mapping ref-cell names v to types, the language Lcs_{Δ} contains the basic syntax from Section 2 (products, sums, functions), a single effect 𝔠𝔰, and constants

escape_{α} : ((α →^{𝔠𝔰} 0) →^{𝔠𝔰} 0) →^{𝔠𝔰} α
get^{v} : 1 →^{𝔠𝔰} Δ(v)
set^{v} : Δ(v) →^{𝔠𝔰} 1

escape is a simple variation on call/cc, interdefinable with both Scheme’s and SML/NJ’s operators. We usually write !v for get^{v}() and v := E for set^{v} E.

The formal semantics of this language is also Scheme-like [KCR98]: we interpret 𝔠𝔰 as the continuation-state monad,

T^{𝔠𝔰}A = A → S_{Δ} → P_{⊥}
η^{𝔠𝔰} a = λκ.λσ.κaσ
t ⋆^{𝔠𝔰} f = λκ.λσ.t(λa.λσ′.f aκσ′)σ

where S_{Δ} = ∏_{v∈dom Δ} L[[Δ(v)]]. (Note that, since the types in Δ may themselves contain 𝔠𝔰-annotations, S_{Δ} is a recursively defined CPO. We elide the associated isomorphisms for conciseness.)

Then the interpretations of the operations are given by

C(escape)_{A} = λf.λκ.λσ.f (λa^{A}.λκ′.λσ′.κaσ′)(λz^{0}.Vz)σ
C(get^{v}) = λ().λκ.λσ.κ(σ v)σ
C(set^{v}) = λa.λκ.λσ.κ()(σ[v ↦ a])

We also define ξ_{b}^{𝔠𝔰} t = t(λa.λσ′.[print_{b} a])σ_{0}, where the initial store σ_{0} is some fixed element of S_{Δ}.

We add a new effect 𝔨 over 𝔠𝔰 and shift/reset to this language as described in Section 3.1, to obtain LK ; cs_{Δ}. Much as before, we now view the continuation-passing transform as the specification of the new language, and define a different implementation.

To see how to obtain such an implementation, consider the interpretation of a 𝔨-effect:

L[[|τ/𝔨|_{K}]] = L[[(|τ|_{K} →^{𝔠𝔰} ω̂) →^{𝔠𝔰} ω̂]]

= (L[[|τ|]] → (L[[ω̂]] → S_{Δ} → P_{⊥}) → S_{Δ} → P_{⊥})

→ (L[[ω̂]] → S_{Δ} → P_{⊥}) → S_{Δ} → P_{⊥} = (L[[|τ|]] → (L[[ω̂]] → S_{Δ} → P_{⊥}) × S_{Δ} → P_{⊥})

→ (L[[ω̂]] → S_{Δ} → P_{⊥}) × S_{Δ} → P_{⊥} = (L[[|τ|]] → S′ → P_{⊥}) → S′ → P_{⊥}

That is, the composite semantics is also a continuation-state semantics, only with a larger state. This suggests that we can implement LK ; cs_{Δ} by a simple embedding into Lcs_{Δ′}, where Δ′ extends Δ with a new cell to hold the metacontinuation [DF90, Fil96] of the original computation.

Formally, we define the realization Φ_{v:¬ω}^{𝔨,𝔠𝔰} by Φ(𝔨) = Φ(𝔠𝔰) = 𝔠𝔰 (thus conflating two previously distinct layers of effects), and

Φ(reset) =

λt^{1\underrightarrow{𝔠𝔰} ω}.escape_{ω} (λk^{ω\underrightarrow{𝔠𝔰} 0}.

let^{𝔠𝔰} m ⇐!v

in (\begin{matrix}v := (λa^{ω}.v := m; k a); \\ let^{𝔠𝔰} r ⇐ t() in let^{𝔠𝔰} m ⇐!v in mr)) \end{matrix}

Φ(shift_{α}) =

λh^{(α\underrightarrow{𝔠𝔰} ω)\underrightarrow{𝔠𝔰} ω}.escape_{α} (λk^{α\underrightarrow{𝔠𝔰} 0}. let^{𝔠𝔰} r ⇐ h(λv^{α}.Φ(reset)(λ().let^{𝔠𝔰} z ⇐ k v in V z)) in let^{𝔠𝔰} m ⇐!v in mr)

Φ(escape_{α}) =

λh^{(α\underrightarrow{𝔠𝔰} 0)\underrightarrow{𝔠𝔰} 0}.escape_{α} (λk^{α\underrightarrow{𝔠𝔰} 0}. let^{𝔠𝔰} m ⇐!v in (v := err; h(λα^{a}.(v := m; k a))))

where (E_{1}; E_{2}) ≡ let^{𝔠𝔰} () ⇐ E_{1} in E_{2}, v is a new cell with Δ′(v) = ω →^{𝔠𝔰} 0, and err : ω →^{𝔠𝔰} 0 is an error continuation that will never actually be invoked in an effect-type-correct program.

The realization ensures that the newly exported escape respects the meta-continuation used by shift and reset. ^{1} But the more significant aspect of the construction is that it eliminates an entire layer of effects (technically, it conflates two layers of state-passing into a single layer with a larger state), making 𝔨- vs. 𝔠𝔰-annotation on vals and lets unnecessary. Formally, we have the following result:

Theorem 10 (K-CS simulation) Let E be a complete program of LK ; cs_{Δ}, ⊢ E : b / 𝔠𝔰. Then

L̂cs_{Δ}[[|E|_{K}]] = L̂cs_{Δ′} [[E{Φ_{v:¬ω}^{𝔨,𝔠𝔰}}]]

where Δ′ = (Δ, v: ω →^{𝔠𝔰} 0) for v ∉ dom Δ.

Proof. (Sketched.) The proof is based on a logical relation between semantics L_{cs_{Δ}}^{K} and L_{cs′_{Δ}} ∘ Φ of LK_{cs_{Δ}}. For this, we define the relational actions of two effects in the source language,

E^{r}(𝔨)R = \{(t, t′) | \begin{matrix}∀k, κ′. (∀(a, a′) ∈ R. k a ≍ κ′ a′) \\ ⇒ tk ≍ t′ κ′\} \end{matrix}
E^{r}(𝔠𝔰)R = \{(t, t′) | \begin{matrix}∀k, κ′. (∀(a, a′) ∈ R. k a ≍ κ′ a′) \\ ⇒ λκ.t(λa.k aκ) ≍ t′ κ′\} \end{matrix}

using auxiliary relations on intermediate answers, (≍) ∈ ARel((L[[ω]] → S_{Δ} → P_{⊥}) → S_{Δ} → P_{⊥}, S_{Δ′} → P_{⊥}):

u ≍ v ⟺ ∀κ, σ, σ′. (κ, σ) ◁ σ′ ⇒ uκσ = v σ′

on metacontinuation-state pairs, (◁) ∈ ARel((L[[ω]] → S_{Δ} → P_{⊥}) × S_{Δ}, S_{Δ′}):

(κ, σ) ◁ σ′ ⟺ (σ, σ′) ∈ R[[Δ]] ∧ ∀(r, r′) ∈ R[[ω]], (σ_{1}, σ′_{1}) ∈ R[[Δ]], κ_{0}. κr σ′_{1} = σ′ v r′ κ_{0}σ′_{1}

and on state, R[[Δ]] ∈ ARel(S_{Δ}, S_{Δ′},):

R[[Δ]] = {(σ, σ′) | ∀v ∈ Δ. (σ v, σ′ v) ∈ R[[Δ(v)]]_{∅}}

Note that these relations are mutually recursively defined. Thus, their existence is not automatic, but can be established fairly easily using Pitts’s techniques [Pit96, Fil96]. We can then check directly that the interpretations of all constants in the two semantics are related by the corresponding relations, so the result follows by Lemma 7.

Putting all the pieces together, we finally obtain our main result:

Theorem 11 (T^{∗}-CS^{∗} simulation) For any formal monad T, define the composite realization of L^{T} in L_{cs} by ΦT^{𝔱,𝔠𝔰} = Φ_{v_{𝔱}:¬Td}^{𝔨,𝔠𝔰} ∘ ΦT^{𝔱,𝔨}. Let L_{0} be the basic language with no effects other than 𝔫 and 𝔭, with the standard semantics L_{0}, and let Φ^{𝔭,𝔠𝔰} be the realization Φ(𝔭) = 𝔠𝔰. Let T_{1}, … T_{n} denote a sequence of monads, each layered over the previous one (and T_{1} over 𝔭). Then there exists a store-typing Δ, such that for any complete L_{0}^{T_{1},...,T_{n}}-program ⊢ E : b/𝔭,

L̂_{0}[[|···|E|_{T_{n}} ⋯ |_{T_{1}}]] = L̂cs_{Δ}[[E{Φ^{𝔭,𝔠𝔰}}{ΦT_{1}^{𝔱,𝔠𝔰} } ⋯ {ΦT_{n}^{𝔱,𝔠𝔰} }]]

Proof. For the base case, we need to relate the standard lifting semantics of 𝔭 to the continuation-based one: when R ∈ Rel(A, A′), we take

E^{r}(𝔭)R = {(t, t′) ∈ A_{⊥} × ((A′ → S_{Δ} → P_{⊥}) → S_{Δ} → P_{⊥}) |

∀κ, κ′, σ_{0}. (∀(a, a′) ∈ R, σ. κa = κ′a′σ)

⇒ t ⋆^{𝔭} κ = t′ κ′ σ_{0}}

The general theorem then follows by induction on n, using Lemma 5 and Theorems 9 and 10 in each step.

Writing Φ for the composite realization, we also note that for all effects e_{1} ⪯ e_{2}, L_{cs}[[(let^{e_{1}⪯e_{2}} x ⇐ E_{1} in E_{2}){Φ}]] = L_{cs}[[let^{𝔠𝔰} x ⇐ E_{1}{Φ} in E_{2}{Φ}]], and thus for all coercions L_{cs}[[χ(E){Φ}]] = L_{cs}[[E]]. That is, the effect-annotations do not actually matter for the purpose of program evaluation, and in particular, we can write our source programs in ML’s implicit-sequencing syntax, with the standard elaboration into single-effect monadic normal forms.

1This redefinition can also be seen as a more principled justification for the practice of redefining the call/cc made available to the programmer in order to accommodate an implementation of dynamic-wind in Scheme [Ree92, KCR98], and for the implicit adaptation of the callcc/throw primitives in SML/NJ to also save and restore exception handlers [BCL^{+}98].

abstype abstype abstype void = VOID of of of void
with with with fun fun fun coerce (VOID v) = coerce v
end end end;
signature signature signature ESCAPE =
sig sig sig
val val val escape : (('a -> void) -> void) -> 'a
end end end;
structure structure structure Escape0 : ESCAPE =
struct struct struct
fun fun fun escape h =
SMLofNJ.Cont.callcc (fn fn fn k =>
coerce (h (fn fn fn x => SMLofNJ.Cont.throw k x)))
end end end;
signature signature signature CTRL =
sig sig sig
type type type ans
val val val shift : (('a -> ans) -> ans) -> 'a
val val val reset : (unit -> ans) -> ans
include include include ESCAPE
end end end;
functor functor functor RepCPS (type type type ans
structure structure structure E : ESCAPE) :
CTRL where where where type type type ans = ans  =
struct struct struct
type type type ans = ans
fun fun fun initmk a = raise raise raise Fail "Unexpected control effect"
val val val mk = ref (initmk : ans -> void)
fun fun fun abort v = !mk v
fun fun fun reset t =
E.escape (fn fn fn k =>
let let let val val val m = !mk
in in in mk := (fn fn fn a => (mk := m; k a));
abort (t ())
end end end)
fun fun fun shift h =
E.escape (fn fn fn k =>
abort (h (fn fn fn v =>
reset (fn fn fn () => coerce (k v)))))
fun fun fun escape h =
E.escape (fn fn fn k =>
let let let val val val m = !mk
in in in mk := initmk; h (fn fn fn a => (mk := m; k a)) end end end)
end end end;

Figure 2: Representing continuation-passing with escapes and state

3.3 Representation in SML/NJ

As suggested by the development, the construction applies directly to a language with first-class continuations and state, such as Scheme or SML/NJ. We show it here for the latter (in SML’97 syntax [MTHM97]), using parameterized modules to represent syntactic realizations.

Figure 2 is a straightforward encoding of the controloperator construction from Section 3.2. Figure 3 shows a simple implementation of the universal type required for the answer-embedding in Lemma 8; an alternative implementation in terms of SML’s extensible datatype exn of exception names is also possible. Finally, Figure 4 shows the implementation of monadic proto-operations using control operators from Section 3.1. (The monad component show and the corresponding operation run are not formally part of the construction, but are useful for visualization of the effect layering.)

signature signature signature DYNAMIC =
sig sig sig
   exception exception exception Dynamic
   type type type dyn
   val val val newdyn : unit -> ('a -> dyn) * (dyn -> 'a)
end end end;
structure structure structure Dynamic :> DYNAMIC =
struct struct struct
   exception exception exception Dynamic
   datatype datatype datatype dyn = DYN of of of unit -> unit
   fun fun fun newdyn () =
      let let let val val val r = ref NONE
      in in in (fn fn fn a => DYN (fn fn fn () => r := SOME a),
          fn fn fn (DYN d) =>
             (r := NONE; d ();
              case case case !r of of of SOME a => a
                       | NONE => raise raise raise Dynamic))
      end end end
end end end;

Figure 3: A universal type, with a state-based implementation

4 Examples and applications

In this section, we show two examples of programming with effects in direct style. The first simply explores further the ordering of exceptions and state. The second, more substantial, shows how we to use layered monads to simulate nondeterministic behavior in a shared-state concurrent program.

4.1 Exceptions and state

Using the definitions of the exception and state monads from Figure 5, we can represent a language with exceptions layered over state, as familiar from ML:

structure structure structure E = Eff0;
structure structure structure E = Represent (structure structure structure M = Exceptions
                         structure structure structure E = E);
structure structure structure Rex = E
structure structure structure ExcOps = ExceptionOps(structure structure structure R = Rex);
structure structure structure E = Represent (structure structure structure M = State
                         structure structure structure E = E)
structure structure structure Rst = E
structure structure structure StateOps = StateOps(structure structure structure R = Rst);
val val val t1 = E.run (fn fn fn () => (StateOps.set 3; "ok"));
(* val t1 = "<st: 3>ok" : string *)
val val val t2 = E.run (fn fn fn () =>
           (StateOps.set 4; ExcOps.fraise "err"; "ok"));
(* val t2 = "<st: 4><exn: err>" : string *)
val val val t3 = E.run (fn fn fn () =>
           (StateOps.set 5;
            ExcOps.fhandle
             (fn fn fn () => (StateOps.set 8;
                        ExcOps.fraise "err"; "ok"))
             (fn fn fn x => x ^", " ^
                Int.toString (StateOps.get ()))))
(* val t3 = "<st: 8>err, 8" : string *)

Let us now switch the order of the two effect-definition blocks in the prologue, putting the state-block first. Then running the same three examples gives:

val val val t1' = E.run (fn fn fn () => (StateOps.set 3; "ok"));
(* val t1' = "<st: 3>ok" : string *)
val val val t2' = E.run (fn fn fn () =>

signature signature signature MONAD =
sig sig sig
type type type 'a t
val val val unit : 'a -> 'a t
val val val bind : 'a t * ('a -> 'b t) -> 'b t
val val val glue : (unit -> 'a t) -> 'a t
val val val show : string t -> string
end end end;
signature signature signature RMONAD =
sig sig sig
structure structure structure M : MONAD
val val val reflect : 'a M.t -> 'a
val val val reify : (unit -> 'a) -> 'a M.t
end end end;
signature signature signature EFFREP =
sig sig sig
include include include ESCAPE
val val val run : (unit -> string) -> string
end end end;
structure structure structure Eff0 : EFFREP =
struct struct struct
open open open Escape0
fun fun fun run t = t ()
end end end;
functor functor functor Represent (structure structure structure M : MONAD
structure structure structure E : EFFREP) :
sig sig sig include include include RMONAD  include include include EFFREP end end end =
struct struct struct
structure structure structure C = RepCPS (type type type ans = Dynamic.dyn M.t
structure structure structure E = E)
structure structure structure M = M
fun fun fun reflect m =
C.shift (fn fn fn k =>
M.bind (m, fn fn fn a => M.glue (fn fn fn () => k a)))
fun fun fun reify t =
let let let val val val (in_d, out_d) = Dynamic.newdyn ()
in in in M.glue (fn fn fn () =>
M.bind (C.reset (fn fn fn () =>
M.unit (in_d (t ()))),
M.unit o out_d))
end end end
val val val escape = C.escape
fun fun fun run t = M.show (reify (fn fn fn () => E.run t))
end end end;

Figure 4: Representing monadic effects with continuationpassing

(StateOps.set 4; ExcOps.fraise "err"; "ok"));
(* val t2' = "<exn: err>" : string *)
val val val t3' = E.run (fn fn fn () =>
(StateOps.set 5;
ExcOps.fhandle
(fn fn fn () => (StateOps.set 8;
ExcOps.fraise "err"; "ok"))
(fn fn fn x => x ^", " ^
Int.toString (StateOps.get ()))))
(* uncaught exception Fail: Unexpected control effect
raised at: ctrl.sml:29.25-29.57 *)

Here, the computation of t2' shows that a raised exception simply discards the current state. t3' shows what happens when we attempt to execute an effect-ill-typed program: the state-effect in the first argument to fhandle is meaningless in this ordering of effects. Consequently, the translation-based specification says nothing about the meaning of the program, and the simulation theorem does not constrain the behavior of the implementation.

structure structure structure Exceptions (*: MONAD*) =
struct struct struct
datatype datatype datatype 'a res = OK of of of 'a | EXN of of of string
type type type 'a t = unit -> 'a res
fun fun fun glue t = fn fn fn () => t () ()
fun fun fun unit a = fn fn fn () => OK a
fun fun fun bind (t, f) =
   fn fn fn () => case case case t () of of of OK a => f a () | EXN s => EXN s
fun fun fun show t =
   case case case t () of of of OK s => s | EXN x => "<exn: " ^x ^">"
end end end;
functor functor functor ExceptionOps (structure structure structure R :
                      RMONAD where where where M = Exceptions) :
sig sig sig
   val val val fraise : string -> 'a
   val val val fhandle : (unit -> 'a) -> (string -> 'a) -> 'a
end end end =
struct struct struct
open open open Exceptions
fun fun fun fraise s = R.reflect (fn fn fn () => EXN s)
fun fun fun fhandle t h =
   case case case R.reify t () of of of OK a => a | EXN s => h s
end end end;
structure structure structure State : MONAD =
struct struct struct
type type type state = int
type type type 'a t = state -> 'a * state
fun fun fun glue t = fn fn fn s => t () s
fun fun fun unit a = fn fn fn s => (a,s)
fun fun fun bind (t, f) =
   fn fn fn s => let let let val val val (a,s') = t s in in in f a s' end end end
fun fun fun show t =
   let let let val val val (a,s) = t 0
   in in in if if if s = 0 then then then a
               else else else "<st: " ^Int.toString s ^">" ^a
   end end end
end end end;
functor functor functor StateOps (structure structure structure R : RMONAD where where where M = State) :
sig sig sig
   val val val get : unit -> int
   val val val set : int -> unit
end end end =
struct struct struct
fun fun fun get () = R.reflect (fn fn fn s => (s, s))
fun fun fun set n = R.reflect (fn fn fn s => ((), n))
end end end;
structure structure structure ListMonad : MONAD =
struct struct struct
type type type 'a t = unit -> 'a list
fun fun fun glue t = fn fn fn () => t () ()
fun fun fun unit a = fn fn fn () => [a]
fun fun fun mapcan f [] = []
  | mapcan f (h::t) = f h @ mapcan f t
fun fun fun bind (t, f) =
   fn fn fn () => mapcan (fn fn fn a => f a ()) (t ())
fun fun fun disp [] = "<fail>"
  | disp [x] = x
  | disp (h::t) = h ^" <or> " ^disp t
fun fun fun show t = disp (t ())
end end end;

Figure 5: Some simple monads and their operations

4.2 Shared-state concurrency

As a larger example, we will consider the monadic approach to modeling concurrency, as sketched in [Mog90], based on the semantic concept of resumptions [Sch86]. (Strictly speaking, this example goes beyond the language outlined in Section 2.1 by using a (positive) recursively defined type in the monad specifications. The relevant theorem extends easily to this case, however.)

The monad of ē-resumptions is given by

Tα = μβ. 1 →^{ē} (α + β)

with straightforward unit and extension operations. That is, a resumption-computation of α is a ē-computation that yields either an α-value (representing the final result), or another resumption-computation (representing the remaining computation). The ML representation of the monad and its associated operations can be found in Figure 6.

As long as all resumption-computations suspend periodically (e.g., by calling yield()), this setup can directly simulate the parallel-or operation [Plo77], which returns true if either of of its arguments evaluates to true, false if both evaluate to false, and diverges in all other cases. Note that, because por constructs another resumption-computation, the branches of a parallel-or can themselves contain parallel subcomputations.

More generally, we can model a concurrent system as a collection of resumption-computations, corresponding to the runnable processes. A scheduler flattens this collection into a single computation by repeatedly picking out an element of the collection, running it for a single step, and (if it has not yet terminated) putting it back into the collection. Individual processes can communicate by e.g., a shared store if ē contains state-effects. Alternatively, we can use a more refined monad,

Tα = μβ. 1 →^{ē} (α + req × (rsp → β))

Here, a computation that suspends now produces a request of type req, and must be resumed with response of type rsp. With this setup, and a suitable structure on requests and responses, it is simple to write an scheduler matching up senders and receivers in purely functional style. And while similar in efficiency to a traditional call/cc-based thread package [Wan80], such a system also achieves a direct relationship to the usual denotational specification.

We will instead pursue another important aspect of concurrency: instead of making the scheduler pick runnable processes in a strict round-robin fashion, we can make it choose non-deterministically which process to run at each step. That is, we can layer the entire construction atop a nondeterminism monad:

structure structure structure E = Eff0;
structure structure structure E = Represent (structure structure structure E = E
structure structure structure M = Resumptions)
structure structure structure Rrs = E
structure structure structure ParOps = ParallelOps (structure structure structure R = Rrs)
structure structure structure E = Represent (structure structure structure E = E
structure structure structure M = State)
structure structure structure Rst = E
structure structure structure Cell = StateOps (structure structure structure R = Rst);
structure structure structure E = Represent (structure structure structure E = E
structure structure structure M = ListMonad)
structure structure structure Rls = E
structure structure structure Conc = ConcurOps (structure structure structure RR = Rrs
structure structure structure RL= Rls);
structure structure structure Shared =
struct struct struct
fun fun fun store n = (ParOps.yield (); Cell.set n)
fun fun fun fetch () = (ParOps.yield (); Cell.get ())
end end end;

structure structure structure Resumptions (* : MONAD *) =
struct struct struct
datatype datatype datatype 'a res = DONE of of of 'a | SUSP of of of 'a t
withtype withtype withtype 'a t = unit -> 'a res
fun fun fun glue t = fn fn fn () => t () ()
fun fun fun unit a = fn fn fn () => DONE a
fun fun fun step (DONE a, f) = f a ()
  | step (SUSP t, f) = SUSP (bind (t, f))
and and and bind (t, f) = fn fn fn () => step (t (), f)
fun fun fun disp (DONE a) = a
  | disp (SUSP t) = show t
and and and show t = disp (t ())
end end end;
functor functor functor ParallelOps (structure structure structure R :
                     RMONAD where where where M = Resumptions) :
sig sig sig
   val val val yield : unit -> unit
   val val val por : (unit -> bool) * (unit -> bool) -> bool
end end end =
struct struct struct
open open open Resumptions
fun fun fun yield () = R.reflect (fn fn fn () => SUSP (unit ()))
fun fun fun por (t1, t2) =
   let let let fun fun fun step (DONE true, _) = DONE true
         | step (DONE false, p) = p ()
         | step (SUSP t1, t2) = SUSP (rpor (t2, t1))
       and and and rpor (t1, t2) () = step (t1 (), t2)
   in in in R.reflect (rpor (R.reify t1, R.reify t2)) end end end
end end end;
functor functor functor ConcurOps (structure structure structure RR :
                   RMONAD where where where M = Resumptions
                structure structure structure RL :
                   RMONAD where where where M = ListMonad) :
sig sig sig
   val val val par : (unit -> 'a) * (unit -> 'b) -> 'a * 'b
   val val val atomically : (unit -> 'a) -> 'a
end end end =
struct struct struct
open open open Resumptions
fun fun fun atomically t =
   let let let fun fun fun step (DONE a, y) = if if if y then then then SUSP (unit a)
                                   else else else DONE a
         | step (SUSP t, y) = step (t (), true)
       and and and atom t () = step (t (), false)
   in in in RR.reflect (atom (RR.reify t)) end end end
fun fun fun par (t1, t2) =
  let let let fun fun fun step (DONE a, DONE b) = DONE (a,b)
        | step (DONE a, SUSP tb) =
             SUSP (bind (tb, fn fn fn b => unit (a,b)))
        | step (SUSP ta, DONE b) =
             SUSP (bind (ta, fn fn fn a => unit (a,b)))
        | step (SUSP ta, SUSP tb) = SUSP (rpar (ta, tb))
      and and and rpar (t1, t2) () =
         if if if RL.reflect (fn fn fn ()=>[true, false])
            then then then step (t1 (), SUSP t2)
            else else else step (SUSP t1, t2 ())
  in in in RR.reflect (rpar (RR.reify t1, RR.reify t2)) end end end
end end end;

Figure 6: Resumption monad and associated operations

val val val t1 = E.run (fn fn fn () =>
        (Conc.par (fn fn fn () => Shared.store 3,
                   fn fn fn () => Shared.store
                              (Shared.fetch () + 1));
         Int.toString (Shared.fetch ())))
(* val t1 =
"<st: 4>4 <or> <st: 4>4 <or> <st: 1>1 <or> <st: 3>3 \
\<or> <st: 4>4 <or> <st: 1>1 <or> <st: 3>3 <or> <st: 1>1 \
\<or> <st: 3>3 <or> <st: 3>3" *)

val val val t2 = E.run (fn fn fn () =>
(Conc.par (fn fn fn () => Shared.store 3,
fn fn fn () => Conc.atomically (fn fn fn () =>
Shared.store
(Shared.fetch () + 1)));
Int.toString (Shared.fetch ())))
(* val t2 =
"<st: 4>4 <or> <st: 3>3 <or> <st: 3>3 <or> <st: 3>3 \
\<or> <st: 3>3 <or> <st: 3>3" *)

Here, we see that bracketing a part of the concurrent computation as an atomic section reduces the set of possible changes to the store. While the number of possible interleavings easily gets astronomical in any substantial concurrent program, the simulation is perfectly usable for exhaustively testing individual fragments, such as mutual-exclusion protocols.

Further refinements are possible. For example, by layering a data monad (Tα = int →^{ē} α) above resumptions, we can model thread-specific data, where a running computation can perform a the equivalent of a getpid() call to obtain its own thread’s unique identifier. We can provide thread-local exceptions, or global ones for aborting the entire concurrent system. We can add an output monad for tracing, but inspect it only for nondeterministic paths in which an exception is raised, and so on.

5 Related work

There are already a large number of proposals for layering effects, both for structuring denotational semantics [Mog90, Esp95] and functional programs [KW93, Ste94, LHJ95]. Generally, however, these approaches pursue modularity in a “flat” multi-effect language, without an explicit effect-typing system. Accordingly, a central problem in such frameworks concerns defining the various effect-operations in such a way that they “lift through” other effects that may be present. For specific effects, more or less ad hoc solutions do exist, but operations that involve reification-like behavior (such as exception handling) do not seem to admit any general solution.

The approach presented in this paper is less ambitious: the basic translation-derived framework exposes the layering explicitly in the effect-types of the proto-operations. Thus, those conflicts that are not automatically resolvable by effect-subsumption must either be exposed to the programmer as typing restrictions that go beyond simple typability (akin to, e.g., keeping track of a function’s exceptioneffects in Java), or the desired semantics must be explicitly encoded in the definitions of the programmer-visible operations. Of course, existing results about lifting specific operations through particular monads can be used for that.

A further difference is that most executable specifications based on monad constructors actually construct and use the full compound monad – explicitly or implicitly – during actual evaluation of programs, usually at a substantial cost. Here, we make a strong distinction between the simple but inefficient specification, and the efficient but (especially for multiple layers) not easily analyzable implementation, taking care only that they agree on the meanings of complete programs.

A second line of related work concerns implementation of various computational paradigms using control operators directly, without involving monads at all. Examples include uses of basic call/cc for thread packages [Wan80] and imperative backtracking [HDM93]; simple composable-control [FWFD88, DF92] for nondeterminism and other basic effects, and a number of proposals for hierarchical control [DF90, SF90, GRR95] to represent general layered effects. Most of these are based on operational definitions of the control operators in terms of their actions on evaluation contexts (although many also include sample implementations in terms of Scheme primitives).

Again, we take a more minimalist approach here: we view control operators not as an explicitly exposed programming abstraction in its own right, but only as a means to the end of implementing a monadic specification. (Of course, sometimes – although surprisingly rarely – the most natural description of a computational effect is in fact in terms of continuations; the monadic framework encompasses this as simply another instance.) This frees us from the constraint of defining a general-purpose control mechanism with intuitive operational behavior, and allows us to provide instead a “lean and mean” implementation, which can be formally analyzed without too much work.

6 Conclusions

To be practically compelling, a monad-based framework for effects needs to minimize overhead, both conceptual and computational. We address the former concern by basing the specification on the intuitively familiar concept of definitional translation (“explaining away an effect”), and the latter by an efficient implementation that keeps execution cost at roughly native levels, as long as the effect-invoking and effect-delimiting operations are comparatively rare – as is indeed the case in most functional programs.

In other words, we aim to steer clear of two extremes: on the one hand “the specification is the implementation”, resulting from executing a monad-based specification (of, e.g., exceptions) literally; and on the other hand, “the implementation is the specification”, resulting from taking a particular imperative implementation (e.g., a thread package) as a guide to specifying interactions with other effects. Instead, we propose a paradigm – monadic reflection – to uniformly relate a layered declarative specification of an effect tower to its ultimate imperative implementation in terms of low-level primitives.

Although the implementation presented here is nominally complete in an operational sense, it should still be viewed as a proof-of-concept prototype, rather than a final solution. That is, the construction establishes that – beyond availability of call/cc and references – no further support from the compiler or runtime system is needed to efficiently implement layered effects. But this does not mean that such support would be undesirable. In particular, a type system for actually enforcing the effect-restrictions statically would be a big help in constructing large programs. To be practical, this would probably need to be largely reconstructionbased, with only minimal explicit annotations; it should also include support for some notion of effect-polymorphism.

On the semantic side, further refinements are also possible. In particular, it should be possible to extend the formal simulation result to “effect-recursive monads”, in which the new effect being defined is implicitly used in its own specification (e.g., for a higher-order state, we can store procedures that themselves have state-effects). This would also allow for a more uniform treatment of continuation monads with non-base answer types. It would also be worth investigating whether the present results for simulating a linear ⪯-hierarchy can be extended to more general orders.

Acknowledgments

The author is sincerely indebted to Olivier Danvy for a number of perceptive comments, as well as to the POPL reviewers and everyone who influenced earlier versions of this work.

References

[BCL^{+}98] Edoardo Biagioni, Ken Cline, Peter Lee, Chris Okasaki, and Chris Stone. Safe-for-space threads in Standard ML. Higher-Order and Symbolic Computation, 11(2), 1998.

[CF94] Robert Cartwright and Matthias Felleisen. Extensible denotational language specifications. In Masami Hagiya and John C. Mitchell, editors, Symposium on Theoretical Aspects of Computer Software, number 789 in Lecture Notes in Computer Science, pages 244–272, Sendai, Japan, April 1994.

[DF90] Olivier Danvy and Andrzej Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, June 1990.

[DF92] Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[Esp95] David A. Espinosa. Semantic Lego. PhD thesis, Graduate School of Arts and Sciences, Columbia University, May 1995.

[Fil94] Andrzej Filinski. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 446–457, Portland, Oregon, January 1994.

[Fil96] Andrzej Filinski. Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1996. Technical Report CMU–CS–96–119.

[FSDF93] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the SIGPLAN ’93 Conference on Programming Language Design and Implementation, 1993.

[FWFD88] Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. Abstract continuations: A mathematical semantics for handling full functional jumps. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 52–62, Snowbird, Utah, July 1988.

[GRR95] Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Functional Programming and Computer Architecture, pages 12–23, 1995.

[HD94] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994.

[HDM93] Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465–484, October 1993. (A preliminary version appeared in Proceedings of the 1991 Symposium on Principles of Programming Languages).

[KCR98] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(3):7–105, 1998. Also appears in ACM SIGPLAN Notices 33(9), September 1998.

[KW93] David J. King and Philip Wadler. Combining monads. In J. Launchbury and P. M. Sansom, editors, Functional Programming, Glasgow 1992, pages 134–143, Ayr, Scotland, 1993. Springer-Verlag.

[LHJ95] Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 333–343, San Francisco, California, January 1995.

[LPJ95] John Launchbury and Simon L. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293–341, December 1995.

[ML71] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.

[Mog89] Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California, June 1989. IEEE.

[Mog90] Eugenio Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, April 1990.

[MTHM97] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML. The MIT Press, revised edition, 1997.

[MW85] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, number 193 in Lecture Notes in Computer Science, pages 219–224, Brooklyn, June 1985.

[Pit96] Andrew M. Pitts. Relational properties of domains. Information and Computation, 127(2):66–90, June 1996.

[Plo77] Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255, December 1977.

[PW93] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 71–84, Charleston, South Carolina, January 1993.

[Ree92] Jonathan Rees. The Scheme of things: The June 1992 meeting. Lisp Pointers, 5(4):40–45, 1992.

[Rey74] John C. Reynolds. On the relation between direct and continuation semantics. In Jacques Loeckx, editor, 2nd Colloquium on Automata, Languages and Programming, number 14 in Lecture Notes in Computer Science, pages 141–156, Saarbrücken, West Germany, July 1974.

[Sch86] David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., 1986.

[SF90] Dorai Sitaram and Matthias Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67– 99, January 1990.

[Ste94] Guy L. Steele, Jr. Building interpreters by composing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 472–492, Portland, Oregon, January 1994.

[Tol98] Andrew Tolmach. Optimizing ML using a hierarchy of monadic types. In Xavier Leroy and Atsushi Ohori, editors, Types in Compilation, Second International Workshop, number 1473 in Lecture Notes in Computer Science, pages 97–115, Kyoto, Japan, March 1998.

[Wad92] Philip Wadler. The essence of functional programming (invited talk). In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, January 1992.

[Wad98] Philip Wadler. The marriage of effects and monads. In International Conference on Functional Programming, 1998.

[Wan80] Mitchell Wand. Continuation-based multiprocessing. In Conference Record of the 1980 LISP Conference, pages 19–28, Stanford, California, August 1980.