The marriage of effects and monads

PHILIP WADLER Avaya Labs and PETER THIEMANN Universität Freiburg, Germany

Gifford and others proposed an effect typing discipline to delimit the scope of computational effects within a program, while Moggi and others proposed monads for much the same purpose. Here we marry effects to monads, uniting two previously separate lines of research. In particular, we show that the type, region, and effect system of Talpin and Jouvelot carries over directly to an analogous system for monads, including a type and effect reconstruction algorithm. The same technique should allow one to transpose any effect system into a corresponding monad system.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.2 [Logics and meanings of programs]: Semantics of Programming Languages— Operational semantics

General Terms: Languages, Theory

Additional Key Words and Phrases: monad, effect, type, region, type reconstruction

1. INTRODUCTION

Computational effects, such as state or continuations, are powerful medicine. If taken as directed they may cure a nasty bug, but one must be wary of the side effects.

For this reason, many researchers in computing seek to exploit the benefits of computational effects while delimiting their scope. Two such lines of research are the effect typing discipline, proposed by Gifford and Lucassen [GL86; Luc87], and pursued by Talpin and Jouvelot [TJ92; TJ94; Tal93] among others, and the use of monads, proposed by Moggi [Mog89; Mog91], and pursued by Wadler [Wad90; Wad92; Wad93; Wad95] among others. Effect systems are typically found in strict languages, such as FX [GJLS87] (a variant of Lisp), while monads are typically found in lazy languages, such as Haskell [Has98].

Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. \begin{matrix}c \\ ◯ \end{matrix} 20TBD ACM 1529-3785/20TBD/0700-0001 $5.00 TBDTBD Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. \begin{matrix}c \\ ◯ \end{matrix} 20TBD ACM 1529-3785/20TBD/0700-0001 $5.00

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD, Pages 1–31.

2 · P. Wadler and P. Thiemann

In his pursuit of monads, Wadler wrote the following:

… the use of monads is similar to the use of effect systems …. An intriguing question is whether a similar form of type inference could apply to a language based on monads. [Wad92]

Half a decade later, we can answer that question in the affirmative. Goodness knows why it took so long, because the correspondence between effects and monads turns out to be surprisingly close.

The marriage of effects and monads. Recall that a monad language introduces a type T τ to represent a computation that yields a value of type τ and may have side effects. If the call-by-value translation of τ is τ^{†}, then we have that (τ → τ′)^{†}, where → represents a function that may have side effects, is equal to τ^{†} → T τ^{′†}, where → represents a pure function with no side effects.

Recall also that an effect system labels each function with its possible effects, so a function type is now written τ →^{σ} τ′, indicating a function that may have effects delimited by σ.

The innovation of this paper is to marry effects to monads, writing T^{σ} τ for a computation that yields a value in τ and may have effects delimited by σ. Now we have that (τ →^{σ} τ′)^{†} is τ^{†} → T^{σ} τ^{′†}.

The monad translation offers insight into the structure of the original effect system. In the original system, variables and lambda abstractions are labelled with the empty effect, and applications are labeled with the union of three effects (the effects of evaluating the function, the argument, and the function body). In the monad system, effects appear in just two places: the ‘unit’ of the monad, which is labeled with the empty effect, and the ‘bind’ of the monad, which is labeled with the union of two effects. The translation of variables and lambda abstractions introduces ‘unit’, hence they are labeled with an empty effect; and the translation of application introduces two occurrences of ‘bind’, hence it is labeled with a union of three effects (each ∪ symbol in σ ∪ σ′ ∪ σ′′ coming from one ‘bind’).

Transposing effects to monads. Numerous effect systems have been proposed, carrying more or less type information, and dealing with differing computational effects such as state, continuations, or communication [GL86; Luc87; JG89; TJ92; TJ94; Tal93; NNA97]. Tofte and others propose a system for analysing memory allocation based on effects [TT94; TB98]. Java contains a simple effect system, without effect variables, where each method is labeled with the exceptions it might raise [GJS96].

For concreteness, this paper works with a type, region, and effect system based on proposals by Talpin and Jouvelot [TJ92; Tal93; TJ94], where effects indicate which regions of store are initialised, read, or written. Talpin and Jouvelot’s results transpose in a straightforward way to a monad formulation. It seems clear that other effect systems can be transposed to monads in a similar way.

Applications. In Glasgow Haskell, the monad ST is used to represent computational effects on state [PW93; LP94]. All effects on state are lumped into a single monad. There is no way to distinguish an operation that reads the store from one that writes the store, or to distinguish operations that write two distinct regions of

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

The marriage of effects and monads · 3

the store (and hence cannot interfere with each other). The type, region, and effect system of Talpin and Jouvelot addresses precisely this problem, and the monadbased system described here could be applied directly to augment any particular instance of the ST monad with effects.

In fact, the letregion construct [TT94; TB98] (which was originally named private [LG88]) corresponds closely to the runST operator in Glasgow Haskell, where the index type plays the role of a region. For the one-region case, this connection has been formalized and proved correct for a simple call-by-value language with runST [SS99]. An alternative approach to monadic encapsulation uses a constant run with an interesting higher-order type [MP99]. In that approach, the monadic code is abstracted over the monadic operations, which are provided through the run constant.

Similarly, in Haskell the monad IO is used to represent all computational effects that perform input/output [PW93; PH97]. Dialects of Haskell extend this to call procedures written in other languages [PW93; FLMP99], deal with concurrency [PGF96], or handle exceptions [PRH^{+}99]. Again, all effects are lumped into a single monad, and again a variant of the system described here could be used to augment the IO monad with effects.

Monads labeled with effects can also be applied to optimizing strict languages such as Standard ML. Whereas Haskell requires the user to explicitly introduce monads, Standard ML can be regarded as implicitly introducing a monad everywhere, via Moggi’s translation from call-by-value lambda calculus into a monadic metalanguage. The implicit monad of Standard ML incorporates all side effects, including operations on references and input-output, much like a combination of Haskell’s ST and IO monads. As before, labeling the monad with effects can be used to delimit the scope of effects. In particular, where the monad is labeled with the empty effect, the corresponding expression is pure and additional optimizations may be applied. Or when the monad reads but does not write the store, certain operations may be commuted. This technique has been applied to intermediate languages for Standard ML compilers by Tolmach [Tol98] and by Benton, Kennedy, and Russel [BKR98]. Our work can be regarded as complementary to theirs: we provide the theory and they provide the practice.

Summary of results. Talpin and Jouvelot present (i) a type system with effects, (ii) a semantics, with a proof that types and effects are consistent with the semantics (iii) a type and effect reconstruction algorithm, with a proof that it is sound and complete. We review each of these results, following it by the corresponding result for the monad system. We also recall the call-by-value translation from lambda calculus into a monad language, and show that this translation preserves (i) types, (ii) semantics, and (iii) the principal types derived by the reconstruction algorithms.

By and large, we stick to the notation and formulation of Talpin and Jouvelot [TJ92; Tal93; TJ94]. However, we differ in a few particulars.

Talpin and Jouvelot [TJ92] use a simplified treatment of the polymorphic binding let x = v in e. While their type inference algorithm makes use of type schemes, their correctness proof elides them by assuming that let x = v in e is expanded to e[x := v]. In contrast, here we use standard type schemes throughout.

In subsequent work [TJ94; Tal93], Talpin and Jouvelot also adopt type schemes

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

throughout. However, they go beyond the present framework in admitting nonvalues to have polymorphic types. To achieve this goal, they refine effects to also include the type of the effected reference and have the generalization step only abstract those variables that are neither mentioned in the type environment nor in the current effect. In addition, their calculus includes implicit effect masking in the

style of letregion.

Also, Talpin and Jouvelot follow the classic work of Tofte [Tof87], using an evaluation-style operational semantics (‘big step’). In contrast, we follow the approach of Wright and Felleisen [WF94] and use an operational semantics based on reduction (‘small step’). As noted by Wright and Felleisen, this leads to a simpler proof: instead of a complex relation between values and types (specified as a greatest fixpoint), we can use the existing type relation (specified by structural induction).

The monad translation we use is standard. It was introduced by Moggi [Mog89; Mog91], and has been further studied by Hatcliff and Danvy [HD94] and Sabry and Wadler [SW97]. Our reduction semantics for the monad is new. It most closely resembles the work of Hatcliff and Danvy, but they did not deal with state and therefore did not have to distinguish between pure reductions and those with computational effects, as we do here.

This paper is a revised version of [Wad98]. Changes include the use of type schemes (as in [TJ94; Tal93]); the use of an optimized monad translation (which greatly simplifies the proof that the translation preserves the semantics); the introduction of evaluation contexts in the operational semantics (which follows more closely the development of Wright and Felleisen); and the correction of a some errors in the original (for instance, rule (get0 ) should not have been included in Monad).

The results are all obtained by straightforward application of well-known techniques. We do give some proofs to illustrate minor unexpected technical subtleties. However, in general results for effect systems transpose to monads without much effort.

Value polymorphism. Some care is required when mixing computational effects with polymorphic types, lest soundness be forfeit. One approach, due to Tofte [Tof87] and used in the original SML [MTH90], introduces ‘imperative’ type variables in the presence of computational effects. Numerous other approaches have been suggested, including some based on effects [Wri92; TJ94]. However, by far the simplest is value polymorphism. This approach was noted by Tofte [Tof87], promoted by Leroy [Ler93] and Wright [Wri95], and used in the revised SML [MTHM97]. It restricts polymorphism to values, a subclass of expressions that can have no computational effects. Talpin and Jouvelot [TJ92] used value polymorphism, and we do so here.

There is a potential problem. Moggi’s original monad translation was monomorphic. How should it be extended to polymorphism? Several years ago Eugenio Moggi, John Hughes, and Philip Wadler held a discussion where they attempted to add polymorphism to the translation and failed. However, they did not consider value polymorphism, which was less popular back then.

In this paper, we extend the monad translation to include value polymorphism.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

The extension is presented for the monad system with effects, but applies equally well when effects are absent. In retrospect, the extension seems obvious, since the monad translation handles values specially. Indeed, similar uses of value polymorphism have been proposed by Harper and Lillibridge [HL93] (for CPS with call/cc) and by Barthe, Hatcliff, and Thiemann [BHT98] (for a configurable monadic metalanguage in the style of Pure Type Systems).

One might say that value polymorphism fits monads to a ‘T’.

Outline. The remainder of this paper is organised as follows. Section 2 introduces the effect type system and the corresponding type system for monads, it introduces the monad translation and shows that it preserves types. Section 3 presents an operational semantics for effects and a corresponding semantics for monads, shows each semantics sound with respect to types, and shows that the monad translation preserves semantics. Section 4 presents a type, region, and effect reconstruction algorithm for effects and a corresponding algorithm for monad, shows each algorithm is sound and complete, and shows that the monad translation relates the two algorithms. Section 5 concludes.

2. TYPES

This section introduces two languages and their type systems, and the translation between them. The first language, Effect, is a call-by-value lambda calculus with operations on a store. Its type system includes regions and effects. The second language, Monad, is based on Moggi’s monadic metalanguage extended with the same store operations, and with a type system augmented by the same regions and effects. We extend the usual monad translation to include effects, and show that it preserves typings.

2.1 Types for Effect

The language Effect and its type system is shown in Figure 1. There are three syntactic classes, values, non-values, and expressions. A value is either an identifier, a lambda abstraction, or a recursive function binding. A non-value is either an application, a polymorphic let binding for values, a monomorphic ilet binding for expressions with imperative effects, or one of three primitive operations on the store, which allocate a new reference, get the value of a reference, or set a reference to a new value. An expression is either a value or a non-value.

A region is either a region variable or a region constant. An effect is either an effect variable, the empty effect, the union of two effects, or one of three effects corresponding to the three operations on the store, each of which is labelled with the region of store affected. Equality on effects is modulo the assumption that ∪ is associative, commutative, idempotent, and has ∅ as a unit. We write σ ⊒ σ′ when σ = σ ∪ σ′.

A type is either a type variable, a function type (labelled with the effect that occurs when the function is applied), or a reference type (labelled with the region in which the reference is located). A type scheme τ̂ has the form ∀ᾱ, γ̄, ς̄.τ where ᾱ, γ̄, ς̄ are (possibly empty) sequences of type, region, and effect variables.

A type environment E maps identifiers to type schemes. We write E_{x} for the environment with x removed from its domain, {x ↦ τ̂} for the environment that

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

6 · P. Wadler and P. Thiemann

x ∈ Id

v ∈ Val  v ::= x | λx. e | rec x. λx′. e
n ∈ NonVal  n ::= e e′ | ilet x = e in e′ | let x = v in e | new e | get e | set e e′
e ∈ Exp  e ::= v | n

r ∈ RegConst γ ∈ RegVar

ρ ∈ Region  ρ ::= γ | r

ς ∈ EffVar

σ ∈ Effect  σ ::= ς | ∅ | σ ∪ σ′ | init(ρ) | read(ρ) | write(ρ)

α ∈ TyVar

τ ∈ Type  τ ::= α | τ →^{σ} τ′ | ref_{ρ} τ
τ̂ ∈ TyScheme τ̂ ::= ∀ᾱ, γ̄, ς̄.τ
E ∈ TyEnv  = Id → TyScheme
θ ∈ Subst  = (TyVar → Type) × (RegVar → Region) × (EffVar → Effect)
(var) \frac{τ̂ ⪰ τ}{E_{x} ∪ \{x ↦ τ̂\} ⊢_{eff} x : τ ! ∅}  (does) \frac{E ⊢_{eff} e : τ ! σ  σ′ ⊒ σ}{E ⊢_{eff} e : τ ! σ′}
(abs) \frac{E_{x} ∪ \{x ↦ τ\} ⊢_{eff} e : τ′ ! σ}{E ⊢_{eff} λx. e : τ →^{σ} τ′ ! ∅}  (app) \frac{E ⊢_{eff} e : τ →^{σ′′} τ′ ! σ  E ⊢_{eff} e′ : τ ! σ′}{E ⊢_{eff} e e′ : τ′ ! σ ∪ σ′ ∪ σ′′}

(let) \frac{E ⊢_{eff} v : τ ! ∅ E_{x} ∪ \{x ↦ gen(E, τ)\} ⊢_{eff} e : τ′ ! σ}{E ⊢_{eff} let x = v in e : τ′ ! σ}

(ilet) \frac{E ⊢_{eff} e : τ ! σ E_{x} ∪ \{x ↦ τ\} ⊢_{eff} e′ : τ′ ! σ′}{E ⊢_{eff} ilet x = e in e′ : τ′ ! σ ∪ σ′}

(rec) \frac{E_{x,x′} ∪ \{x ↦ τ →^{σ} τ′, x′ ↦ τ\} ⊢_{eff} e : τ′ ! σ}{E ⊢_{eff} rec x. λx′. e : τ →^{σ} τ′ ! ∅}

(new) \frac{E ⊢_{eff} e : τ ! σ}{E ⊢_{eff} new e : ref_{ρ} τ ! σ ∪ init(ρ)}

(get) \frac{E ⊢_{eff} e : ref_{ρ} τ ! σ}{E ⊢_{eff} get e : τ ! σ ∪ read(ρ)} (set) \frac{E ⊢_{eff} e : ref_{ρ} τ ! σ E ⊢_{eff} e′ : τ ! σ′}{E ⊢_{eff} set e e′ : τ ! σ ∪ σ′ ∪ write(ρ)}

Fig. 1. The effect calculus, Effect

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

e ∈ MonExp  e ::= x | λx. e | rec x. e | e e′ | let x = e in e′

                      | <e> | let x ⇐ e in e′ | new e | get e | set e e′

τ ∈ MonType  τ ::= α | τ → τ′ | T^{σ} τ | ref_{ρ} τ
τ̂ ∈ MonTyScheme τ̂ ::= ∀ᾱ, γ̄, ς̄.τ
E ∈ MonTyEnv  = Id → MonTyScheme
θ ∈ Subst  = (TyVar → MonType) × (RegVar → Region) × (EffVar → Effect)

(var) \frac{τ̂ ⪰ τ}{E_{x} ∪ \{x ↦ τ̂\} ⊢_{mon} x : τ}  (does) \frac{E ⊢_{mon} e : T^{σ} τ  σ′ ⊒ σ}{E ⊢_{mon} e : T^{σ′} τ}

(abs) \frac{E_{x} ∪ \{x ↦ τ\} ⊢_{mon} e : τ′}{E ⊢_{mon} λx. e : τ → τ′}  (app) \frac{E ⊢_{mon} e : τ → τ′  E ⊢_{mon} e′ : τ}{E ⊢_{mon} e e′ : τ′}

(let) \frac{E ⊢_{mon} e : τ E_{x} ∪ \{x ↦ gen(E, τ)\} ⊢_{mon} e′ : τ′}{E ⊢_{mon} let x = e in e′ : τ′}

(unit) \frac{E ⊢_{mon} e : τ}{E ⊢_{mon} <e> : T^{∅} τ}  (bind) \frac{E ⊢_{mon} e : T^{σ} τ  E_{x} ∪ \{x ↦ τ\} ⊢_{mon} e′ : T^{σ′} τ′}{E ⊢_{mon} let x ⇐ e in e′ : T^{σ∪σ′} τ′}

(rec) \frac{E_{x} ∪ \{x ↦ τ\} ⊢_{mon} e : τ}{E ⊢_{mon} rec x. e : τ} (new) \frac{E ⊢_{mon} e : τ}{E ⊢_{mon} new e : T^{init(ρ)} ref_{ρ} τ}

(get) \frac{E ⊢_{mon} e : ref_{ρ} τ}{E ⊢_{mon} get e : T^{read(ρ)} τ}  (set) \frac{E ⊢_{mon} e : ref_{ρ} τ  E ⊢_{mon} e′ : τ}{E ⊢_{mon} set e e′ : T^{write(ρ)} τ}

Fig. 2. The monad language, Monad

maps identifier x to type scheme τ̂, E ∪ E′ for the union of two maps with disjoint domains, and E ⊇ E′ when the first map contains the second. Similar notation will be used later for substitutions and stores.

We write free(τ), free(τ̂) and free(E) for the set of free type, region, and effect variables in a type, type scheme, or type environment. We write e[x := v] for the capture-avoiding substitution of value v for variable x in expression e, and we write free(e) for the free identifiers of an expression.

We define generic instances and generalization in the usual way. A substitution θ maps type variables to types, region variables to regions, and effect variables to effects. We say that type scheme τ̂′ is a generic instance of the type scheme τ̂, written τ̂ ⪰ τ̂′, if τ̂ = ∀ᾱ, γ̄, ς̄.τ and τ̂′ = ∀ᾱ′, γ̄′, ς̄′.τ′ and there is a substitution

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

θ such that τ′ = θτ, where the domain of θ is restricted to the free variables of τ (that is, dom(θ) = {ᾱ, γ̄, ς̄}) and the bound variables of τ̂′ are not free in τ̂ (that is, {ᾱ′, γ̄′, ς̄′} ∩ free(τ̂) = ∅). We say that type scheme τ̂ is the generalization of type τ with respect to environment E, written τ̂ = gen(E, τ), if τ̂ = ∀ᾱ, γ̄, ς̄.τ where {ᾱ, γ̄, ς̄} = free(τ) \ free(E).

A typing E ⊢_{eff} e : τ ! σ indicates that expression e yields a value of type τ and has effect delimited by σ, where the type environment E maps the free identifiers of e to types.

In the rule for abstraction, (abs), the effect is empty because evaluation immediately returns the function, with no side effects. The effect on the function arrow is the same as the effect for the function body, because applying the function will have the same side effects as evaluating the body. In the rule for application, (app), the effect is the union of the effects for evaluating the function, evaluating the argument, and applying the function.

Each let binding construct comes with its own typing rule. Rule (let) handles polymorphic let binding of values, and rule (ilet) handles monomorphic ilet binding of expressions with imperative effects. Rules (let) and (var) use type schemes in the usual way.

Rule (does) permits a form of subeffecting. Effects indicate an upper bound on the side effects an expression may have, and so may always be made larger. The rules for the three primitive operations, (new), (get), and (set), add the corresponding effect to the effects for their arguments. The region in the effect matches the region in the reference type.

The following lemmas are standard results for type and effect systems. They state that syntactic values have no effects and that substitution of values preserves typing. Their proofs are straightforward.

Lemma 2.1. (Values are pure) If E ⊢_{eff} v : τ ! σ then E ⊢_{eff} v : τ ! ∅.

Lemma 2.2. (Value substitution) Let E = E_{x} ∪ {x ↦ τ}. If E ⊢_{eff} e : τ′ ! σ and E ⊢_{eff} v : τ ! ∅ then E ⊢_{eff} e[x := v] : τ′ ! σ.

2.2 Types for Monad

Whereas Effect is a call-by-value language, with side effects occuring when any expression is evaluated, Monad is a call-by-name language, with side effects occuring only at top-level. All computations with side effects are represented by the new monad type.

We use call-by-name for monads to stress the relation to Haskell. Like Plotkin’s CPS translation, the image of Moggi’s monad translation is indifferent: it delivers identical results regardless whether the monad language uses call-by-value or callby-name [Plo75; HD94; SW97].

The language Monad and its type system is shown in Figure 2. The distinction between values and expressions is no longer relevant for polymorphism, since evaluation has no side effects. However, there are monad values which serve as results of a computation in Monad. Expressions are extended with two new forms for manipulating monads (we describe these shortly). Regions and effects are as before. The function type τ →^{σ} τ′ of before is here broken into the pure function type τ → τ′, and the monad type T^{σ} τ, representing a computation that yields a value of type τ

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

and has effects delimited by σ.

The monad unit <e> denotes the computation that immediately returns the value of e, with no effects. Hence in (unit) the effect is empty. The monad bind let x ⇐ e in e′ denotes the computation that first performs computation e, binds x to the result, and then performs computation e′. Hence in (bind) the effect is the union of the effects of its two subcomputations. (The forms <e> and let x ⇐ e in e′ are written in Haskell as return e and e >>= λx. e′, respectively.)

Polymorphic binding let x = e in e′ is distinct from monad bind. Since expressions have no side effects, there is no need to restrict polymorphism to values. The remaining rules are straightforward adjustments of the previous forms. The three primitive operations, since they involve computational effects, have monad types.

2.3 The translation

Figure 3 shows the translation from Effect to Monad. It is a typed call-by-value monad translation, similar to the standard translation given by Sabry and Wadler [SW97]. The translation given here is optimized so as not to introduce certain ‘administrative’ redexes. Although this makes the translation more complex, it simplifies the proof (to be given in the next section) that the translation preserves the semantics.

We write τ^{†} for the translation of a type, v^{†} for the translation of a value, e^{∗} for the translation of an expression, and E^{†} for the translation of a type environment.

As is well known, the monad translation preserves typing, a property that continues hold for our systems with effects.

Proposition 2.3. (Translation preserves types)

—If E ⊢_{eff} v : τ ! ∅ then E^{†} ⊢_{mon} v^{†} : τ^{†}. —If E ⊢_{eff} e : τ ! σ then E^{†} ⊢_{mon} e^{∗} : T^{σ} τ^{†}.

The proof is by induction on the structure of type derivations.

The translation of let works out neatly thanks to value polymorphism. Whereas the translation of an expression is in a monad, and so must be bound with the nonpolymorphic monad bind, the translation of a value is not in a monad, and can safely be bound with the polymorphic let.

The figure also shows the grammar of expressions and types in Monad that are in the image of the translation from values, expressions (after closure under reduction), and types in Effect. In the image, application always has some translated value for function and argument, ordinary let always binds to a translated value, and monad unit always contains a translated value.

3. SEMANTICS

This section presents operational semantics of the two languages. The reduction system for Effect is standard, save for instrumentation to trace operations on the store, which is used to demonstrate consistency between semantics and effects. The reduction system for Monad appears to be new, even without the instrumentation. It resembles that of Hatcliff and Danvy [HD94], but differs in distinguishing two sorts of reductions, those that may have side effects and those that do not. For both effects and monads, we show that the type and effect system is sound, modifying the

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

α^{†} ≡ α
(τ →^{σ} τ′)^{†} ≡ τ^{†} → T^{σ} τ^{′†}
(ref_{ρ} τ)^{†} ≡ ref_{ρ} τ^{†}
(∀ᾱ, γ̄, ς̄.τ)^{†} ≡ ∀ᾱ, γ̄, ς̄.τ^{†}
x^{†} ≡ x
(λx. e)^{†} ≡ λx. e^{∗}
(rec x. λx′. e)^{†} ≡ rec x. λx′. e^{∗}
v^{∗} ≡ <v^{†}>
(n e)^{∗} ≡ let x ⇐ n^{∗} in (x e)^{∗}
(v n)^{∗} ≡ let x ⇐ n^{∗} in (v x)^{∗}
(v v′)^{∗} ≡ v^{†} v^{′†}
(let x = v in e)^{∗} ≡ let x = v^{†} in e^{∗}
(ilet x = e in e′)^{∗} ≡ let x ⇐ e^{∗} in e^{′∗}
(new n)^{∗} ≡ let x ⇐ n^{∗} in (new x)^{∗}
(new v)^{∗} ≡ new v^{†}
(get n)^{∗} ≡ let x ⇐ n^{∗} in (get x)^{∗}
(get v)^{∗} ≡ get v^{†}
(set n e)^{∗} ≡ let x ⇐ n^{∗} in (set x e)^{∗}
(set v n)^{∗} ≡ let x ⇐ n^{∗} in (set v x)^{∗}
(set v v′)^{∗} ≡ set v^{†} v^{′†}
(x_{1} : τ_{1}, …, x_{n} : τ_{n})^{†} ≡ x_{1} : τ_{1}^{†}, …, x_{n} : τ_{n}^{†}
v̇ ∈ TranVal v̇ ::= x | λx. ė | rec x. λx′. ė
ė ∈ TranExp ė ::= v̇ v̇′ | let x = v̇ in ė | <v̇> | let x ⇐ ė in ė′

                         | new v̇ | get v̇ | set v̇ v̇′

τ̇ ∈ TranType τ̇ ::= α | τ̇ → T^{σ} τ̇′ | ref_{ρ} τ̇

Fig. 3. Translation from Effect to Monad

results of Wright and Felleisen [WF94] to take effects and monads into account. We also show that the translation preserves semantics, in that it preserves instrumented reduction.

3.1 Semantics for Effect

The operational semantics for Effect is shown in Figure 4. Locations l are a designated subset of the variables. By convention, a location is never used as the bound variable in a lambda or let expression. A store s maps locations to values. A trace f is the semantic equivalent of an effect, where regions are replaced by locations.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

l ∈ Location  ⊆ Id
s ∈ Store  = Location → Value
f ∈ Trace  f ::= ∅ | f ∪ f′ | init(l) | read(l) | write(l)
EvaluationContext E ::= [ ] | E e | v E | ilet x = E in e

                              | new E | get E | set E e | set v E

(beta)  s, (λx. e)v ⟶^{∅}_{eff} s, e[x := v]
(rec)  s, (rec x. λx′. e)v ⟶^{∅}_{eff} s, (λx′. e[x := rec x. λx′. e])v
(letv)  s, let x = v in e ⟶^{∅}_{eff} s, e[x := v]
(let)  s, ilet x = v in e ⟶^{∅}_{eff} s, e[x := v]
(new)  s, new v ⟶^{init(l)}_{eff} s ∪ {l ↦ v}, l fresh l ∉ dom(s)
(get)  s_{l} ∪ {l ↦ v}, get l ⟶^{read(l)}_{eff} s_{l} ∪ {l ↦ v}, v
(set) s_{l} ∪ {l ↦ v}, set l v′ ⟶^{write(l)}_{eff} s_{l} ∪ {l ↦ v′}, v′

(context) \frac{s, e ⟶^{f}_{eff} s′, e′}{s, E[e] ⟶^{f}_{eff} s′, E[e′]} (step) \frac{s, e ⟶^{f}_{eff} s′, e′}{s, e ⟶ ⟶^{f}_{eff} s′, e′}

(refl) \overline{s, e ⟶ ⟶^{∅}_{eff} s, e}  (tran) \frac{s, e ⟶ ⟶^{f}_{eff} s′, e′  s′, e′ ⟶ ⟶^{f′}_{eff} s′′, e′′}{s, e ⟶ ⟶^{f∪f′}_{eff} s′′, e′′}

Fig. 4. Semantics for Effect

If l ∉ dom(s), we write s ∪ {l ↦ v} for the store that maps location l to value v and otherwise behaves like s. We let s_{l} range over stores that do not bind l, that is, l ∉ dom(s_{l}).

An evaluation state is a pair s, e where all free variables of e are locations in s (free(e) ⊆ dom(s)) and the same holds for all stored values (∀l ∈ dom(s), free(s(l)) ⊆ dom(s)). A single reduction step is written s, e ⟶^{f}_{eff} s′, e′, where s, e is the state before the step, f is a trace of the effect of the step, and s′, e′ is the state after the step.

Rule (beta) specifies function application; the language Effect is call-by-value as the argument must be a value for the rule to apply. The rule leaves the store unchanged and is labeled with an empty effect. Rules (rec) and (let) are similar. Rules (new), (get), and (set) perform actions on the store and have corresponding effects. Rule (context) forms the contextual closure of reduction with respect to evaluation contexts. An evaluation context E is an expression with a hole in place of

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

l ∈ Location ⊆ Id
s ∈ Store  = Location → MonExp
Monad context M ::= [ ] | let x ⇐ M in e
Operator context O ::= [ ] | get [ ] | set [ ] e
Pure context  P ::= [ ] | P e
(beta)  (λx. e′)e ⟶_{mon} e′[x := e]
(rec)  rec x. e ⟶_{mon} e[x := rec x. e]
(let)  let x = e in e′ ⟶_{mon} e′[x := e]
(bind) s, let x ⇐ <e>in e′  ⟶^{∅}_{mon} s, e′[x := e]
(new)  s, new e ⟶^{init(l)}_{mon} s ∪ {l ↦ e}, <l> fresh l ∉ dom(s)
(get)  s_{l} ∪ {l ↦ e}, get l ⟶^{read(l)}_{mon} s_{l} ∪ {l ↦ e}, <e>
(set) s_{l} ∪ {l ↦ e}, set l e′ ⟶^{write(l)}_{mon} s_{l} ∪ {l ↦ e′}, <e′>

(monad) \frac{s, e ⟶^{f}_{mon} s′, e′}{s, M[e] ⟶^{f}_{mon} s′, M[e′]} (operator) \frac{e ⟶_{mon} e′}{s, O[e] ⟶^{∅}_{mon} s, O[e′]}

(pure) \frac{e ⟶_{mon} e′}{P [e] ⟶_{mon} P [e′]} (step) \frac{s, e ⟶^{f}_{mon} s′, e′}{s, e ⟶ ⟶^{f}_{mon} s′, e′}

(refl) \overline{s, e ⟶ ⟶^{∅}_{mon} s, e}  (tran) \frac{s, e ⟶ ⟶^{f}_{mon} s′, e′  s′, e′ ⟶ ⟶^{f′}_{mon} s′′, e′′}{s, e ⟶ ⟶^{f∪f′}_{mon} s′′, e′′}

Fig. 5. Semantics for Monad

the next sub-expression to be evaluated. Defining E ::= [ ] | E e | v E | … specifies the order of evaluation, since the function in an application must be reduced to a value before the argument is elegible for reduction. The handling of the operations on the store is similar. Finally, rules (step), (refl), and (tran) specify ⟶ ⟶^{f}_{eff} as the reflexive and transitive closure of ⟶^{f}_{eff}.

There are additional judgements to relate stores to type environments, and traces to effects. Write E ⊢_{eff} s if dom(s) = dom(E) and, for each l ∈ dom(s), if E(l) = ref_{ρ} τ then E ⊢_{eff} s(l) : τ ! ∅. Write E ⊧_{eff} f ! σ if

for each init(l) in f we have E(l) = ref_{ρ} τ and init(ρ) ⊑ σ,

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

for each read(l) in f we have E(l) = ref_{ρ} τ and read(ρ) ⊑ σ, for each write(l) in f we have E(l) = ref_{ρ} τ and write(ρ) ⊑ σ.

Write E ⊢_{eff} s, e : τ ! σ if s, e is an evaluation state and E ⊢_{eff} s and E ⊢_{eff} e : τ ! σ. Reduction preserves types and is consistent with effects.

Proposition 3.1. (Subject reduction) If E ⊢_{eff} s, e : τ ! σ and s, e ⟶^{f}_{eff} s′, e′ then there exists some E′ ⊇ E such that E′ ⊢_{eff} s′, e′ : τ ! σ and E′ ⊧_{eff} f ! σ.

The proof is by case analysis on the definition of s, e ⟶^{f}_{eff} s′, e′.

The form of a value is determined by its type.

Lemma 3.2. (Canonical forms) Let s, v be an evaluation state and E ⊢_{eff} s, v : τ ! ∅.

(1 ) If τ = τ′ →^{σ} τ′′ then v is either λx. e or rec x. λx′. e. (2 ) If τ = ref_{ρ} τ then v is a location l ∈ dom(s).

The proof is by case analysis on τ.

A well-typed evaluation state is never stuck.

Proposition 3.3. (Progress) Suppose E ⊢_{eff} s, e : τ ! σ. Either e is a value or there exists s′, e′ and f such that

s, e ⟶^{f}_{eff} s′, e′.

The proof is by induction on the derivation of E ⊢_{eff} s, e : τ ! σ. The complete proof is given in Appendix A.1.

Write s, e ⇑_{eff}^{f} if there is an infinite reduction

s, e ⟶^{f_{0}}_{eff} s_{1}, e_{1} ⟶^{f_{1}}_{eff} s_{2}, e_{2} ⟶^{f_{2}}_{eff} ⋯

with f = ⋃ f_{i}. Then we have the following.

Proposition 3.4. (Type soundness) If E ⊢_{eff} s, e : τ ! σ then there exists E′ ⊇ E so that either

—s, e ⇑_{eff}^{f} and E′ ⊧_{eff} f ! σ, or

—s, e ⟶ ⟶^{f}_{eff} s′, v and E′ ⊢_{eff} s′, v : τ ! ∅ and E′ ⊧_{eff} f ! σ.

Type soundness is an immediate corrollary of progress.

It is interesting to consider which expressions would give problems during evaluation. An evaluation state s, e is stuck if e is not a value and there is no f, s′, e′ such that s, e ⟶^{f}_{eff} s′, e′. A simple case analysis shows that a state is stuck if and only if it has one of the following forms:

e = E[v v′], where v is a location, e = E[get v], where v is not a location or v ∉ dom(s), or e = E[set v v′], where v is not a location or v ∉ dom(s).

Stuck expressions are not typable.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

3.2 Semantics for Monad

Figure 5 shows the operational semantics for Monad. Locations and traces are as before, but a store now maps locations to expressions. There are two notions of reduction.

Pure reductions do not access the store and have no effect. They are written e ⟶_{mon} e′. Rule (beta) specifies function application; the language Monad is callby-name as the argument need not be a value for the rule to apply. The rule is pure and makes no reference to the store. Rules (rec) and (let) are similar.

Monadic reductions perform sequencing and execute the operations on the store. They may have an effect and are written s, e ⟶^{f}_{mon} s, e′. Rule (bind) simplifies a monadic bind of a monadic unit; it leaves the store unchanged and is labeled with an empty effect. (But it is not a pure operation: this prevents reduction of ill-typed expressions such as (let x ⇐ <(λy. y)>in x)z, where the monadic expression is not at top-level.) Rules (new), (get), and (set) perform actions on the store and have corresponding effects.

There are three sorts of contexts, monad contexts M, operator contexts O, and pure contexts P, and three corresponding context rules. Rule (monad) forms the contextual closure of monadic reductions over monadic reductions through a monad context M; rule (operator) forms the contextual closure of monadic reductions over pure reductions through an operator context O; and rule (pure) forms the contextual closure of pure reductions over pure reductions through a pure context P. (These rules permit reduction of sensible expressions such as (λy. let x ⇐ <y>in x)z, where an application yields a monadic expression at toplevel.) Since the monad language is call-by-name, pure contexts do not reduce the argument of a function. Since expressions, not values, are placed in the store, operator contexts neither reduce the argument of new nor the second argument of

set.

As before, rules (step), (refl), and (tran) specify ⟶ ⟶^{f}_{mon} as the reflexive and transitive closure of ⟶^{f}_{mon}. The relations E ⊢_{mon} s, E ⊢_{mon} s, e : τ, and E ⊧_{mon} f ! σ are defined, mutatis mutandis, as for Effect.

As before, reduction preserves types and is consistent with effects.

Proposition 3.5. (Subject reduction)

—If E ⊢_{mon} e : τ and e ⟶_{mon} e′ then E ⊢_{mon} e′ : tau.

—If E ⊢_{mon} s, e : T^{σ} τ and s, e ⟶^{f}_{mon} s′, e′ then there exists some E′ ⊇ E such that E′ ⊢_{mon} s′, e′ : T^{σ} τ and E′ ⊧_{mon} f ! σ.

The proof is by induction on the definitions of e ⟶_{mon} e′ and s, e ⟶^{f}_{mon} s′, e′. We define values for the calculus Monad as follows.

v ∈ MonVal v ::= l | λx. e | <e>.

As before, the form of a value is determined by its type.

Lemma 3.6. (Canonical forms) Let s, v be an evaluation state and E ⊢_{mon} s, v : τ.

(1 ) If τ = τ′ → τ′′ then v = λx. e.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

(2 ) If τ = T^{σ} τ′ then v = <e>. (3 ) If τ = ref_{ρ} τ then v = l ∈ Location and l ∈ dom(s).

The proof is by case analysis on τ.

As before, a well-typed evaluation is never stuck.

Proposition 3.7. (Progress) Suppose that E ⊢_{mon} s, e : τ. Then either e ∈ MonVal or there exist f, s′, e′ such that s, e ⟶^{f}_{mon} s′, e′.

The proof is by induction on the derivation of E ⊢_{eff} s, e : τ ! σ.

As before, type soundness is an immediate corrollary of progress.

Proposition 3.8. (Type soundness) If E ⊢_{mon} s, e : τ then there exists E′ ⊇ E so that either

—s, e ⇑_{mon}^{f} and E′ ⊧_{mon} f ! σ, or

—s, e ⟶ ⟶^{f}_{mon} s′, v and E′ ⊢_{mon} s′, v : τ and E′ ⊧_{mon} f ! σ.

In both cases, if τ = T^{σ′} τ′ then σ = σ′, otherwise σ = ∅.

As before, it is interesting to consider which expressions would give problems during evaluation. Now an evaluation state s, e is stuck if one of the following conditions holds:

e = M[O[P [v e]]], where v is not a lambda, e = M[let x ⇐ v in e], where v is not a monad unit, e = M[get v], where v is not a location or v ∉ dom(s), e = M[set v e], where v is not a location or v ∉ dom(s).

Again, stuck expressions are not typable.

3.3 Translation

It is well known that the monad translation preserves semantics, and this property continues to hold for the instrumented semantics. A key to the correspondence is that if a term in Effect is translated to Monad then the resulting term has subterms of the form e′ e or ilet x = e in e′ or <e> only when e is the image of an Effectvalue, that is, only when e has the form v̇.

If s is a store in Effect, then we write s^{†} for the corresponding store in Monad, where s^{†}(l) = (s(l))^{†} for each l ∈ dom(s).

Translation commutes with substitution of Effect-values.

Lemma 3.9. For all e ∈ Exp and v ∈ Val, e^{∗}[x := v^{†}] = (e[x := v])^{∗}.

Formally, preservation of semantics corresponds to a simulation result between Effect and Monad. The reduction of a term in Effect runs almost in lock-step with the reduction of its image in Monad. Sometimes an additional administrative reduction is required. For instance, consider a reduction in Effect,

n v′ ⟶^{f}_{eff} v v′

where n^{∗} ⟶^{f}_{mon} v^{†} (disregarding the store component for simplicity). The image of this reduction in Monad is given by

(n v′)^{∗} = let x ⇐ n^{∗} in x v^{′†} ⟶^{f}_{mon} let x ⇐ <v^{†}>in x v^{′†} ⟶_{mon} v^{†} v^{′†} = (v v′)^{∗}

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

which requires one extra administrative reduction. Hence, each reduction in Effect gives rise to one or two corresponding reductions in Monad.

Another peculiarity arises in the translation of stuck terms. Given a stuck term in Effect, its image in Monad can sometimes perform one reduction step before it gets stuck, too. This is a consequence of translating the call-by-value recursion operator in Effect to a call-by-name recursion operator in Monad. If the original term is stuck because of some rec x. λx′. e, then the translated term must unwind the recursion once before it becomes stuck, too.

Proposition 3.10. (Translation preserves semantics)

(1 ) If s, e ⟶^{f}_{eff} s′, e′ then either s^{†}, e^{∗} ⟶^{f}_{mon} s^{′†}, e^{′∗}, or s^{†}, e^{∗} ⟶^{f}_{mon} s^{′†}, e_{0} and

e_{0} ⟶_{mon} e^{′∗}.

(2 ) If s, e ⟶ ⟶^{f}_{eff} s′, e′ then s^{†}, e^{∗} ⟶ ⟶^{f}_{mon} s^{′†}, e^{′∗}.

(3 ) If s, e ⇑_{eff}^{f} then s^{†}, e^{∗} ⇑_{mon}^{f}. (4 ) If s, e is stuck then either s^{†}, e^{∗} is stuck or e^{∗} ⟶_{mon} e_{0} where s^{†}, e_{0} is stuck.

The proofs of 1 and 4 are by induction on the definitions of ⟶^{f}_{eff}, and the proofs of 2 and 3 are by induction on ⟶ ⟶^{f}_{eff}. The complete proofs are given in Appendix A.2.

As mentioned in the previous section, the proof is considerably simplified by the use of an optimizing translation. The non-optimized translation introduces many additional administrative redexes, which obscure the correspondence between the effect and monad systems.

Another choice which simplifies the proof is the use of two syntactically distinct forms for let, a polymorphic let binding of values and a monomorphic let binding of expressions with imperative effects. Without this distinction, it is still possible to obtain a simulation result, but at the price of a contrived monad translation.

Note that the image of the translation does not include all possible stuck expressions in Monad. In particular, the P context is always trivial because the monad translation moves computations out of the argument positions. The monad translation also guarantees that the reduction (bind) never gets stuck.

4. TYPE RECONSTRUCTION

This section presents type, region, and effect reconstruction algorithms for the two languages. The reconstruction algorithm for Effect, due to Talpin and Jouvelot, closely resembles Milner’s original type reconstruction algorithm [Mil78]. Effects are handled by accumulating a set of constraints, similar to the handling of subtypes in Mitchell’s inference algorithm [Mit91]. It is straightforward to transpose the reconstruction algorithm from Effect to Monad. Both algorithms are sound and complete, and typings yielded by the two algorithms are related by the translation between the two languages.

4.1 Unification

A substitution maps type variables to types, region variables to regions, and effect variables to effects. The substitution id is the identity substitution. Substitutions and the unification algorithms for Effect are shown in Figure 6, and the modifications for Monad are shown in Figure 7.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

θ ∈ Subst = (TyVar → Type) × (RegVar → Region) × (EffVar → Effect)
U_{eff}(α, α′) = {α ↦ α′}
U_{eff}(α, τ) = if α ∈ free(τ) then fail else {α ↦ τ}
U_{eff}(τ, α) = U_{eff}(α, τ)

U_{eff}(τ_{0} →^{ς} τ_{1}, τ′_{0} →^{ς′} τ′_{1}) = let \begin{matrix}θ = \{ς ↦ ς′\} \\ θ′ = U_{eff}(θτ_{0}, θτ′_{0}) \\ θ′′ = U_{eff}(θ′θτ_{1}, θ′θτ′_{1}) \end{matrix}

in θ′′θ′θ
U_{eff}(ref_{γ} τ, ref_{γ′} τ′) = \begin{matrix}let & \begin{matrix}θ = \{γ ↦ γ′\} \\ θ′ = U_{eff}(θτ, θτ′) \end{matrix} \\ in & θ′θ \end{matrix}
U_{eff}(−, −) = fail

Fig. 6. Unification of Effect Types

θ ∈ Subst = (TyVar → MonType) × (RegVar → Region) × (EffVar → Effect)

U_{mon}(τ_{0} → τ_{1}, τ′_{0} → τ′_{1}) = let \begin{matrix}θ = U_{mon}(τ_{0}, τ′_{0}) \\ θ′ = U_{mon}(θτ_{1}, θτ′_{1}) \end{matrix}

in θ′θ

U_{mon}(T^{ς} τ, T^{ς′} τ′) = let \begin{matrix}θ = \{ς ↦ ς′\} \\ θ′ = U_{mon}(θτ, θτ′) \end{matrix}

in θ′θ

Fig. 7. Changes to the unification algorithm for Monad

κ ∈ Constraint = ℘(EffVar × Effect)
μ ∈ EffModel = EffVar → Effect

\begin{aligned}K(∅) & = & id \\ K(\{ς ⊒ σ\} ∪ κ) & = & let μ = K(κ) in \{ς ↦ ς ∪ μ(σ)\} ∘ μ \end{aligned}

Fig. 8. Constraints

ω ∈ V ar  = TyVar + RegVar + EffVar
τ̂ ∈ TyScheme τ̂ ::= ∀ω̄. (τ, κ)
E ∈ TyEnv  = Id → TyScheme

I_{eff}(E, κ, x) = let \begin{matrix}new & ω̄′ \\ ∀ω̄. (τ, κ′) = E(x) \\ θ = \{ω̄ ↦ ω̄′\} \end{matrix}

in ⟨id, θτ, ∅, κ ∪ θκ′⟩

I_{eff}(E, κ, λx. e) = let \begin{matrix}new α, ς \\ ⟨θ, τ, σ, κ′⟩ = I_{eff}(E_{x} ∪ \{x ↦ α\}, κ, e) \end{matrix}

in ⟨θ, θα →^{ς} τ, ∅, κ′ ∪ {ς ⊒ σ}⟩

I_{eff}(E, κ, rec x. λx′. e) = let \begin{matrix}new α, α′, ς \\ ⟨θ, τ, σ, κ′⟩ = I_{eff}(E_{x,x′} ∪ \{x ↦ α →^{ς} α′, x′ ↦ α\}, κ, e) \\ θ′ = U_{eff}(θα′, τ) \end{matrix}

in ⟨θ′θ, θ′θ(α →^{ς} α′), ∅, θ′(κ′ ∪ {θς ⊒ σ})⟩

I_{eff}(E, κ, e e′) = let new α, ς

⟨θ, τ, σ, κ′⟩ = I_{eff}(E, κ, e) ⟨θ′, τ′, σ′, κ′′⟩ = I_{eff}(θE, κ′, e′)

θ′′ = U_{eff}(θ′τ, τ′ →^{ς} α)

in ⟨θ′′θ′θ, θ′′α, θ′′(θ′σ ∪ σ′ ∪ ς), θ′′κ′′⟩

I_{eff}(E, κ, let x = v in e) = let ⟨θ, τ, ∅, κ′⟩ = I_{eff}(E, κ, v)

ω̄ = (free(K(κ′)τ)) \ free(K(κ′)θE) κ′′ = {ς ⊒ σ ∈ κ′ | ς ∈ ω̄} κ′′′ = κ′ \ κ′′ ⟨θ′, τ′, σ, κ′′′′⟩ = I_{eff}(θE_{x} ∪ {x ↦ ∀ω̄. (τ, κ′′)}, κ′′′, e)

in ⟨θ′θ, τ′, σ, κ′′′′⟩

I_{eff}(E, κ, ilet x = e in e′) = let \begin{matrix}⟨θ, τ, σ, κ′⟩ = I_{eff}(E, κ, e) \\ ⟨θ′, τ′, σ′, κ′′⟩ = I_{eff}(θE_{x} ∪ \{x ↦ τ\}, κ′, e) \end{matrix}

in ⟨θ′θ, τ′, σ ∪ σ′, κ′′⟩

Initial type environment

E(new) = ∀α, γ, ς. (α →^{ς} ref_{γ} α, {ς ⊒ init(γ)})
E(get) = ∀α, γ, ς. (ref_{γ} α →^{ς} α, {ς ⊒ read(γ)})
E(set) = ∀α, γ, ς, ς′. (ref_{γ} α →^{ς} α →^{ς′} α, {ς′ ⊒ write(γ)})

Fig. 9. Type reconstruction for Effect

I_{mon}(E, κ, x) = let \begin{matrix}new & ω̄′ \\ ∀ω̄. (τ, κ′) = E(x) \\ θ = \{ω̄ ↦ ω̄′\} \end{matrix}

in ⟨id, θτ, κ ∪ θκ′⟩

I_{mon}(E, κ, λx. e) = let \begin{matrix}new α \\ ⟨θ, τ, κ′⟩ = I_{mon}(E_{x} ∪ \{x ↦ α\}, κ, e) \end{matrix}

in ⟨θ, θα → τ, κ′⟩

I_{mon}(E, κ, rec x. e) = let new α ⟨θ, τ, κ′⟩ = I_{mon}(E_{x} ∪ {x ↦ α}, κ, e) θ′ = U_{mon}(θα, τ)

in ⟨θ′θ, θ′τ, θ′κ′⟩

I_{mon}(E, κ, e e′) = let new α ⟨θ, τ, κ′⟩ = I_{mon}(E, κ, e) ⟨θ′, τ′, κ′′⟩ = I_{mon}(θE, κ′, e′) θ′′ = U_{mon}(θ′τ, τ′ → α)

in ⟨θ′′θ′θ, θ′′α, θ′′κ′′⟩

I_{mon}(E, κ, let x = e in e′) = let ⟨θ, τ, κ⟩ = I_{mon}(E, κ, e)

ω̄ = (free(K(κ′)τ)) \ free(K(κ′)θE) κ′′ = {ς ⊒ σ ∈ κ′ | ς ∈ ω̄} κ′′′ = κ′ \ κ′′ ⟨θ′, τ′, κ′′′′⟩ = I_{mon}(θE_{x} ∪ {x ↦ ∀ω̄. (τ, κ)}, κ′′′, e′)

in ⟨θ′θ, τ′, κ′′′′⟩

I_{mon}(E, κ, <e>) = let \begin{matrix}new ς \\ ⟨θ, τ, κ′⟩ = I_{mon}(E, κ, e) \end{matrix}

in ⟨θ, T^{ς} τ, κ′⟩

I_{mon}(E, κ, let x ⇐ e in e′) = let new α, α′, ς, ς′, ς′′

⟨θ, τ, κ′⟩ = I_{mon}(E, κ, e) θ′ = U_{mon}(τ, T^{ς} α) ⟨θ′′, τ′, κ′′⟩ = I_{mon}(E ∪ {x ↦ θ′α}, θ′κ′, e′) θ′′′ = U_{mon}(τ′, T^{ς′} α′)

in ⟨θ′′′θ′′θ′θ, T^{ς′′} θ′′′α′, θ′′′(κ′′ ∪ {ς′′ ⊒ θ′′θ′ς ∪ ς′})⟩

Initial type environment

E(new) = ∀α, γ, ς. (α → T^{ς} ref_{γ} α, {ς ⊒ init(γ)})
E(get) = ∀α, γ, ς. (ref_{γ} α → T^{ς} α, {ς ⊒ read(γ)})
E(set) = ∀α, γ, ς′. (ref_{γ} α → α → T^{ς′} α, {ς′ ⊒ write(γ)})

Fig. 10. Type reconstruction for Monad

A key trick in the reconstruction algorithm is to ensure that all effects and regions are represented by variables, to simplify unification. A type, type scheme, type environment, or substitution is normalised if the only regions and effects it contains are variables. (This notion is also present in the work of Talpin and Jouvelot, but only implicitly.)

The unification algorithms U_{eff}(τ, τ′) and U_{mon}(τ, τ′) take two normalised types and return a normalised substitution θ.

Proposition 4.1. (Unification) Let U be one of U_{eff} or U_{mon}.

—(Sound) If θ = U(τ, τ′) then θτ = θτ′ (with θ, τ, τ′ normalised). —(Complete) If θτ = θτ′ then there exist θ′ and θ′′ such that θ′ = U(τ, τ′) and

θ = θ′′θ′ (with τ, τ′, θ′ normalised).

The proof is standard, as normalisation eliminates any potentially tricky cases.

4.2 Constraints

Constraints and the constraint solution algorithm are shown in Figure 8. A set of constraints κ is a set of inequations of the form ς ⊒ σ, asserting that ς encompasses at least the effect σ.

A substitution μ is a solution of κ, written μ ⊧ κ, if μς ⊒ μσ for each inequation ς ⊒ σ in κ. Such a solution always exists.

The constraint solution algorithm K(κ) takes a constraint set and returns a substitution μ which solves κ. It assumes that effect variables on the left hand side of constraints in κ are distinct, which can be achieved by repeatedly merging two constraints ς ⊒ σ and ς ⊒ σ′ into one constraint ς ⊒ σ ∪ σ′.

Proposition 4.2. (Constraint solution)

—(Sound) K(κ) ⊧ κ. —(Complete) If μ ⊧ κ then μ = μ ∘ K(κ).

The proof is given in Appendix A.3.

The algorithm is identical to the one in Talpin’s thesis [TJ94; Tal93]. It computes a principal solution of the constraint set κ, independently of the order in which the constraints are visited. (The algorithm is subtly different to their earlier algorithm Min [TJ92]. Algorithm Min yields a solution, which is minimal with respect to the ordering ⊒ defined by μ ⊒ μ′ iff, for all ς ∈ dom(μ′), μ(s) ⊒ μ′(s). Unfortunately, this ordering is not defined in their paper.)

4.3 Reconstruction for Effect

Type schemes and the reconstruction algorithm for Effect are shown in Figure 9. A different flavor of type schemes is introduced which fits better with the type inference. Following [TJ94; Tal93], such a reconstruction scheme has the form ∀ω̄. (τ, κ) where ω̄ is a sequence of type, region, or effect variables; the scheme is normalised if τ is normalised. Such a scheme represents all types of the form θτ where θ ⊧ κ and the domain of θ is contained in ω̄. Reconstruction environments are taken to map identifiers to type schemes; the environment is normalised if all types in it are normalised. We write {ω̄ ↦ ω̄′} for a substitution, when ω̄ and ω̄′

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

have the same length, and each has type, region, and effect variables in the same positions as the other.

The reconstruction algorithm I_{eff}(E, κ, e) takes a normalised reconstruction environment E, an initial constraint set κ, and an expression e, and returns a quadruple ⟨θ, τ, σ, κ′⟩, with θ and τ normalised. It fails if some unification within it fails. The substitution θ is idempotent, and τ, σ, and κ′ are invariant under θ. The algorithm is essentially drawn from Talpin and Jouvelot’s later work [TJ94].

To relate a reconstruction scheme to an equivalent type scheme, we exploit the algorithm for solving constraints in Figure 8. If τ̂ is a type reconstruction scheme, we define \overline{τ̂} = τ̂′ where τ̂ = ∀ᾱ, γ̄, ς̄. (τ, κ) and τ̂′ = ∀ᾱ, γ̄, ς̄. K(κ)(τ). We define \overline{E} by pointwise extension: \overline{E}(x) = \overline{E(x)} for each x ∈ dom(E).

To state completeness, we use the generic instance relation τ̂ ⪰ τ̂′ defined in Section 2. We define E ⪰ E′ by pointwise extension: it holds if E(x) ⪰ E′(x) for each x ∈ dom(E).

The reconstruction algorithm is sound and complete.

Proposition 4.3. (Type reconstruction)

—(Sound) If I_{eff}(E, κ, e) = ⟨θ, τ, σ, κ′⟩ and μ = K(κ′) then μθ\overline{E} ⊢_{eff} e : μτ!μσ, with

E, θ, and τ normalised. —(Complete) Let E be a normalised reconstruction environment, let E′ be a type en-

vironment such that \overline{E} ⪰ E′, and let θ ⊧ κ. If θE′ ⊢_{eff} e : τ ! σ then I_{eff}(E, κ, e) = ⟨θ′, τ′, σ′, κ′⟩ and there exists a substitution θ′′ such that θ′′θ′\overline{E} ⪰ θE′ and τ = θ′′τ′ and σ ⊇ θ′′σ′ and θ′′ ⊧ κ′, with θ′ and τ′ normalised.

The proof for the first part is by induction on the structure of expressions, and for the second by induction on the structure of type derivations. (A similar proof is given by Talpin and Jouvelot [TJ94]. In their earlier work [TJ92], the proof skips the case of polymorphic ‘let’ binding, assuming such bindings have been expanded out.)

Another way to obtain a reconstruction result would be to introduce arrow effects as proposed by Tofte and others [TT94]. In fact, type schemes with arrow effects are equivalent to the reconstruction type schemes introduced in the present section: simply replace each arrow effect ς.σ by the effect variable ς and add the constraint ς ⊒ σ.

4.4 Reconstruction for Monad

The reconstruction algorithm for Monad is shown in Figure 9. The unification algorithm, type schemes, and type environments are as before, with types for Monad replacing types for Effect, mutatis mutandis. Constraints carry over without change.

The reconstruction algorithm I_{mon}(E, κ, e) takes a type environment E, an initial constraint set κ, and an expression e, and returns a triple ⟨θ, τ, κ′⟩, or fails if some unification within it fails. The reconstruction algorithm is easily transposed to the new setting. It has much the same structure as before, the largest difference being that effects are mentioned only in monad types, and effects in types are always represented by variables, so a few extra constraints are required.

It is also easy to transpose the results regarding the algorithm.

Proposition 4.4. (Type reconstruction)

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

—(Sound) If I_{mon}(E, κ, e) = ⟨θ, τ, κ′⟩ and μ = K(κ′) then μθ\overline{E} ⊢_{mon} e : μτ, with E,

θ, and τ normalised. —(Complete) Let E be a normalised reconstruction environment, E′ a type environ-

ment such that \overline{E} ⪰ E′, and let θ ⊧ κ. If θE′ ⊢_{mon} e : τ then I_{mon}(E, κ, e) = ⟨θ′, τ′, κ′⟩ and there exists a substitution θ′′ such that θ′′θ′\overline{E} ⪰ θE and τ = θ′′τ′ and θ′′ ⊧ κ′, with θ′ and τ′ normalised.

4.5 Translation

The two reconstruction algorithms yield results that are related by the translation. Write κ ≃ κ′ if for all μ we have μ ⊧ κ if and only if μ ⊧ κ′. The translation is extended to apply to reconstruction schemes by taking (∀ω̄. (τ, κ))^{†} = ∀ω̄. (τ^{†}, κ).

Proposition 4.5. (Translation preserves type reconstruction) If I_{eff}(E, κ, e) = ⟨θ′, τ′, σ′, κ′⟩ and I_{mon}(E^{†}, κ, e^{∗}) = ⟨θ′′, τ′′, κ′′⟩ then there exist ς and μ such that T^{ς} τ^{†} = τ′ and θ′ = μθ′′ and σ′ = μς and κ′ ≃ μκ′′.

The proof is by induction on the structure of expressions.

5. CONCLUSIONS

We have verified the conjecture, first broached half a decade past, that effect systems can be adapted to monads. We have demonstrated this for the specific case of the type, region, and effect system of Talpin and Jouvelot, but it seems clear that any effect system can be adapted to monads in a similar way.

Here are points for future work.

Denotational semantics. It is straightforward to provide semantics for effects and monads in a denotational style. In this semantics, the instrumentation can be factored out as a separate monad transformer. The factoring uses the well known result that if T X is a monad, then so is T_{A} X = T (X × A), where A is a monoid. In this case, A is taken to be the monoid of traces, with identity ∅ and operator ∪.

Coherent semantics. An alternative approach to denotational semantics might be to eliminate the instrumentation, and associate with each effect σ a different monad T^{σ}. For state, one traditionally defines T X = S → X × S where the store S is a mapping from locations to values. Here one might define T^{σ} τ = S_{σ} → X×S^{σ} where S_{σ} is a store restricted to contain only locations in regions ρ such that read(ρ) or init(ρ) is in σ, and S^{σ} is a store restricted to contain only locations in regions ρ such that init(ρ) or write(ρ) is in σ. Corresponding to each effect inclusion σ ⊆ σ′ there should be a monad morphism T^{σ} → T^{σ′}. In order to ensure coherence in the style of Breazu-Tannen et al. [BCGS91], we should expect transitivity of inclusions to correspond to composition of the corresponding morphisms.

A general theory of effects and monads. As hypothesised by Moggi and as born out by practice, most computational effects can be viewed as a monad. Does this provide the possibility to formulate a general theory of effects and monads, avoiding the need to create a new effect system for each new effect?

Acknowledgements. Thanks to Mads Tofte, Jon Riecke, Matthias Felleisen, and J.-P. Talpin for comments on earlier drafts of this paper.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

REFERENCES

Gilles Barthe, John Hatcliff, and Peter Thiemann. Monadic type systems: Pure type systems for impure settings (preliminary report). In Proceedings of HOOTS’97, volume 10 of ENTCS. Elsevier, 1998.

N. Benton, A. Kennedy, and G. Russell, Compiling Standard ML to Java Bytecodes, ACM 3’rd

International Conference on Functional Programming, Baltimore, September 1998. V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov, Inheritance as explicit coercion,

Information and Computation, 93(1):172–221, 1991. Reprinted in C. A. Gunter and J. C. Mitchell, editors, Theoretical aspects of object-oriented programming, MIT Press, 1994.

Sigbjorn Finne, Daan Leijen, Erik Meijer, and Simpon Peyton Jones. Calling Hell from Heaven and Heaven from Hell. 4’th ACM International Conference on Functional Programming, Paris, September 1999.

D. K. Gifford and J. M. Lucassen, Integrating functional and imperative programming, ACM

Conference on Lisp and Functional Programming, Cambridge, Massachusetts, August 1986. D. K. Gifford, P. Jouvelot, J. M. Lucassen, and M. A. Sheldon, FX-87 Reference Manual, Technical

report MIT/LCS/TR-407, MIT Laboratory for Computer Science, September 1987. James Gosling, Bill Joy, and Guy Steele, The Java Language Specification, Java Series, Sun

Microsystems, 1996. Haskell98, a non-strict, purely functional language. http://www.haskell.org, December 1998. J. Hatcliff and O. Danvy, A generic account of continuation-passing styles, ACM Symposium on

Principles of Programming Languages, Portland, Oregon, January 1994. Robert Harper and Mark Lillibridge. Polymorphic type assignment and cps conversion. LISP

and Symbolic Computation, 6(4):361–380, 1993. P. Jouvelot and D. K. Gifford, Reasoning about continuations with control effects, Technical

report MIT/LCS/TM-378, MIT Laboratory for Computer Science, January 1989. M. P. Jones, Functional programming with overloading and higher-order polymorphism, in J.

Jeuring and E. Meijer, editors, Advanced Functional Programming, LNCS 925, Springer Verlag, 1995.

J. Launchbury and S. L. Peyton Jones, Lazy functional state threads, ACM Conference on Pro-

gramming Language Design and Implementation, Orlando, Florida, 1994. Xavier Leroy. Polymorphism by name for references and continuations. In Conference Record

of POPL ’93: The 20^{st} ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 220–231, Charleston, South Carolina, USA, January 1993. ACM Press.

John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Conference Record of POPL ’88: The 15^{rd} ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47–57, San Diego, California, 1988. ACM Press.

J. M. Lucassen, Types and effects, towards the integration of functional and imperative programming, Ph.D. Thesis, Technical report MIT/LCS/TR-408, MIT Laboratory for Computer Science, August 1987.

R. Milner, A theory for type polymorphism in programming, Journal of Computer and Systems

Science, 17:348–375, 1978. J. C. Mitchell, Type inference with simple subtypes, Journal of Functional Programming,

1(3):245–286, 1991. J. C. Mitchell, Foundations for programming languages, MIT Press, 1996. E. Moggi and F. Palumbo, Monadic Encapsulation of Effects: A Revised Approach, HOOTS ’99

Higher Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science 26, Elsevier Science, 1999.

R. Milner, M. Tofte, and R. Harper, The Definition of Standard ML, MIT Press, 1990. R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML (Revised),

MIT Press, 1997. E. Moggi, Computational lambda calculus and monads, IEEE Symposium on Logic in Computer

Science, Asilomar, California, June 1989. E. Moggi, Notions of computation and monads, Information and Computation, 93(1), 1991.

Hanne Riis Nielson, Flemming Nielson, and Torben Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In Mads Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.

Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow, and Fergus Henderson. A semantics for imprecise exceptions. In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), SIGPLAN Notices, Atlanta, Georgia, USA, May 1999. SIGPLAN Notices 34(5).

J. Peterson and K. Hammond, editors, Haskell 1.4, a non-strict, purely functional language,

Technical report, Yale University, April 1997. G. Plotkin, Call-by-name, call-by-value, and the λ-calculus, Theoretical Computer Science, 1:125–

159, 1975. Simon Peyton Jones, Andrew Gordon, and Sigbjrn Finne. Concurrent Haskell. In Conference

Record of POPL ’96: The 23^{rd} ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 295–308, St. Petersburg Beach, Florida, USA, 21–24 January 1996. ACM Press.

S. L. Peyton Jones and P. Wadler, Imperative functional programming, ACM Symposium on

Principles of Programming Languages, Charleston, South Carolina, January 1993. Miley Semmelroth and Amr Sabry. Monadic Encapsulation in ML. 4’th ACM International Con-

ference on Functional Programming, pages 8–17, Paris, September 1999. Amr Sabry and Philip Wadler, A reflection on call-by-value, ACM Transactions on Programming

Languages and Systems, 19(6):916–941, November 1997. (An earlier version appeared in 1’st ACM International Conference on Functional Programming, Philadelphia, May 1996.)

J.-P. Talpin and P. Jouvelot, Polymorphic type, region, and effect inference, Journal of Functional

Programming, 2(3):245–271, July 1992. J.-P. Talpin and P. Jouvelot, The type and effect discipline, Information and Computation,

111(2):245–296, 1994. J.-P. Talpin, Theoretical and Practical Aspects of Type and Effect Inference, PhD Thesis, Ecole

des Mines de Paris and University Paris VI, 1993. M. Tofte, Operational semantics and polymorphic type inference, PhD Thesis, University of Ed-

inburgh, 1987. M. Tofte and L. Birkedal, A region inference algorithm, Transactions on Programming Languages

and Systems, November 1998 (to appear). Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a

stack of regions. In Proceedings of the 21th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188–201, January 1994.

A. Tolmach, Optimizing ML using a hierarchy of monadic types. Workshop on Types in Compi-

lation, Kyoto, March 1998. P. Wadler, Comprehending monads, ACM Conference on Lisp and Functional Programming,

Nice, France, June 1990. P. Wadler, The essence of functional programming (Invited talk), ACM Symposium on Principles

of Programming Languages, Albuquerque, New Mexico, January 1992. P. Wadler, Monads for functional programming, in M. Broy, editor, Program Design Calculi,

NATO ASI Series, Springer Verlag, 1993. Also in J. Jeuring and E. Meijer, editors, Advanced Functional Programming, LNCS 925, Springer Verlag, 1995.

P. Wadler, How to declare an imperative (Invited talk), International Logic Programming Sym-

posium, Portland, Oregon, MIT Press, December 1995. P. Wadler, The marriage of effects and monads, ACM 3’rd International Conference on Functional

Programming, Baltimore, September 1998. A. Wright and M. Felleisen, A syntactic approach to type soundness, Information and Computa-

tion, 115(1):38–94, November 1994. A. Wright, Typing references by effect inference, 4th European Symposium on Programming,

Rennes, France, February 1992, Springer-Verlang LNCS 582. A. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, 8:343–355, 1995.

A. PROOFS

A.1 Progress

Proposition 3.3 (Progress) Suppose E ⊢_{eff} s, e : τ ! σ. Either e is a value or there exists s′, e′ and f such that

s, e ⟶^{f}_{eff} s′, e′.

Proof. By induction on the derivation of E ⊢_{eff} s, e : τ ! σ. In each case, we have that E ⊢_{eff} s and E ⊢_{eff} e : τ ! σ.

Case (var) \frac{τ̂ ⪰ τ}{E_{x} ∪ \{x ↦ τ̂\} ⊢_{eff} x : τ ! ∅} . A value.

Case (does) \frac{E ⊢_{eff} e : τ ! σ σ′ ⊒ σ}{E ⊢_{eff} e : τ ! σ′} . The claim is immediate by the inductive

hypothesis.

Case (abs) \frac{E_{x} ∪ \{x ↦ τ\} ⊢_{eff} e : τ′ ! σ}{E ⊢_{eff} λx. e : τ →^{σ} τ′ ! ∅} . A value.

Case (app) \frac{E ⊢_{eff} e_{1} : τ →^{σ′′} τ′ ! σ E ⊢_{eff} e_{2} : τ ! σ′}{E ⊢_{eff} e_{1} e_{2} : τ′ ! σ ∪ σ′ ∪ σ′′} . By induction, either s, e_{1} ⟶^{f}_{eff}

s′, e′_{1} or e_{1} is a value v_{1}.

In the first case, rule (context) yields that s, e_{1} e_{2} ⟶^{f}_{eff} s′, e′_{1} e_{2}.

If e_{1} = v_{1}, a value, then, by induction, either s, e_{2} ⟶^{f}_{eff} s′, e′_{2} or e_{2} is a value.

In the first case, rule (context) yields that s, v_{1} e_{2} ⟶^{f}_{eff} s′, v_{1} e′_{2}.

If e_{2} = v_{2}, a value, then the canonical forms lemma 3.2 applied to v_{1} yields that v_{1} is either λx. e or rec x. λx′. e. In both cases, the expression is a redex using either (beta) or (rec).

Case (let) \begin{matrix}E ⊢_{eff} v : τ ! ∅ \\ E_{x} ∪ \{x ↦ gen(E, τ)\} ⊢_{eff} e : τ′ ! σ \\ E ⊢_{eff} let x = v in e : τ′ ! σ \end{matrix} . This expression is a redex.

Case (ilet) \begin{matrix}E ⊢_{eff} e_{1} : τ ! σ \\ E_{x} ∪ \{x ↦ τ\} ⊢_{eff} e_{2} : τ′ ! σ′ \\ E ⊢_{eff} ilet x = e_{1} in e_{2} : τ′ ! σ ∪ σ′ \end{matrix} . By induction, either e_{1} is a

value, in which case the whole expression is a redex, or s, e_{1} ⟶^{f}_{eff} s′, e′_{1}. In the latter case, the whole expression reduces due to (context).

Case (rec) \frac{E_{x,x′} ∪ \{x ↦ τ →^{σ} τ′, x′ ↦ τ\} ⊢_{eff} e : τ′ ! σ}{E ⊢_{eff} rec x. λx′. e : τ →^{σ} τ′ ! ∅} . A value.

Case (new) \frac{E ⊢_{eff} e : τ ! σ}{E ⊢_{eff} new e : ref_{ρ} τ ! σ ∪ init(ρ)} . By induction, either e is a value,

in which case the whole expression is a redex, or s, e ⟶^{f}_{eff} s′, e′. In the latter case, the whole expression reduces, too, by rule (context).

Case (get) \frac{E ⊢_{eff} e : ref_{ρ} τ ! σ}{E ⊢_{eff} get e : τ ! σ ∪ read(ρ)} . By induction, either e is a value, in

which case the canonical forms lemma 3.2 shows that e = l ∈ Location, l ∈ dom(s), and hence the whole expression is a redex, or s, e ⟶^{f}_{eff} s′, e′. In the latter case, the whole expression reduces by rules (context).

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

Case (set) \frac{E ⊢_{eff} e_{1} : ref_{ρ} τ ! σ E ⊢_{eff} e_{2} : τ ! σ′}{E ⊢_{eff} set e_{1} e_{2} : τ ! σ ∪ σ′ ∪ write(ρ)} . By induction, either e_{1} is a

value, in which case the canonical forms lemma 3.2 shows that e_{1} = l ∈ Location and l ∈ dom(s), or s, e_{1} ⟶^{f}_{eff} s′, e′_{1}. In the latter case, the whole expression reduces by rules (context).

If e_{1} = l then, by induction, either e_{2} is a value, in which case the whole expression is a redex, or s, e_{2} ⟶^{s}′_{eff}, e′_{2}. In the latter case, the whole expression reduces by (context).

A.2 Translation preserves semantics

Proposition 3.10 (Translation preserves semantics)

(1 ) If s, e ⟶^{f}_{eff} s′, e′ then either s^{†}, e^{∗} ⟶^{f}_{mon} s^{′†}, e^{′∗}, or s^{†}, e^{∗} ⟶^{f}_{mon} s^{′†}, e_{0} and

e_{0} ⟶_{mon} e^{′∗}.

(2 ) If s, e ⟶ ⟶^{f}_{eff} s′, e′ then s^{†}, e^{∗} ⟶ ⟶^{f}_{mon} s^{′†}, e^{′∗}.

(3 ) If s, e ⇑_{eff}^{f} then s^{†}, e^{∗} ⇑_{mon}^{f}.

(4 ) If s, e is stuck then either s^{†}, e^{∗} is stuck or e^{∗} ⟶_{mon} e_{0} where s^{†}, e_{0} is stuck.

Proof. Item 1 by induction on the definition of ⟶^{f}_{eff}.

Case (beta): s, (λx. e)v ⟶^{∅}_{eff} s, e[x := v].

s^{†}, ((λx. e)v)^{∗}
=  s^{†}, (λx. e)^{†} v^{†}
=  s^{†}, (λx. e^{∗}) v^{†}
⟶^{∅}_{mon} s^{†}, e^{∗}[x := v^{†}]
=  s^{†}, (e[x := v])^{∗}

Case (rec): s, (rec x. λx′. e)v ⟶^{∅}_{eff} s, (λx′. e[x := rec x. λx′. e])v.

s^{†}, (rec x. λx′. e)^{†} v^{†}
=  s^{†}, (rec x. λx′. e^{∗}) v^{†}
⟶^{∅}_{mon} s^{†}, (λx′. e^{∗}[x := rec x. λx′. e^{∗}]) v^{†}
=  s^{†}, (λx′. e^{∗}[x := (rec x. λx′. e)^{†}]) v^{†}
=  s^{†}, ((λx′. e[x := rec x. λx′. e])v)^{∗}

Case (letv): s, let x = v in e ⟶^{∅}_{eff} s, e[x := v].

s^{†}, (let x = v in e)^{∗}
=  s^{†}, let x = v^{†} in e^{∗}
⟶^{∅}_{mon} s^{†}, e^{∗}[x := v^{†}]
=  s^{†}, (e[x := v])^{∗}

Case (let): s, ilet x = v in e ⟶^{∅}_{eff} s, e[x := v].

s^{†}, (ilet x = v in e)^{∗}

=  s^{†}, let x ⇐ v^{∗} in e^{∗}
=  s^{†}, let x ⇐ <v^{†}>in e^{∗}
⟶^{∅}_{mon} s^{†}, e^{∗}[x := v^{†}]
=  s^{†}, (e[x := v])^{∗}

Case (new): s, new v ⟶^{init(l)}_{eff} s ∪ {l ↦ v}, l where l ∉ dom(s).

s^{†}, (new v)^{∗}

=  s^{†}, new v^{†}
⟶^{init(l)}_{mon} s^{†} ∪ {l ↦ v^{†}}, <l>
=  s ∪ {l ↦ v}^{†}, l^{∗}

Case (get): s_{l} ∪ {l ↦ v}, get l ⟶^{read(l)}_{eff} s_{l} ∪ {l ↦ v}, v.

s_{l} ∪ {l ↦ v}^{†}, (get l)^{∗}

=  s_{l}^{†} ∪ {l ↦ v^{†}}, get l
⟶^{read(l)}_{mon} s_{l}^{†} ∪ {l ↦ v^{†}}, <v^{†}>
=  s_{l} ∪ {l ↦ v}^{†}, v^{∗}

Case (set): s_{l} ∪ {l ↦ v}, set l v′ ⟶^{write(l)}_{eff} s_{l} ∪ {l ↦ v′}, v′.

(s_{l} ∪ {l ↦ v})^{†}, (set l v′)^{∗}

=  s_{l}^{†} ∪ {l ↦ v^{†}}, set l v^{′†}
⟶^{write(l)}_{mon} s_{l}^{†} ∪ {l ↦ v^{′†}}, <v^{′†}>
=  (s_{l} ∪ {l ↦ v′})^{†}, v^{′∗}

Case (context) \frac{s, n ⟶^{f}_{eff} s′, e′}{s, E[n] ⟶^{f}_{eff} s′, E[e′]} . The expression, n, must be a non-value because otherwise the reduction would be impossible.

Subcase E = [ ] e.

s^{†}, (n e)^{∗}
=  s^{†}, let x ⇐ n^{∗} in (x e)^{∗}
⟶^{f}_{mon} by induction, and context M
s^{†}, let x ⇐ e^{′∗} in (x e)^{∗}

If e′ ∈ NonVal then

= s^{†}, (e′ e)^{∗}

If e′ = v′ ∈ Val then

=  s^{†}, let x ⇐ v^{′∗} in (x e)^{∗}
=  s^{†}, let x ⇐ <v^{′†}>in (x e)^{∗}
⟶^{∅}_{mon} s^{†}, (x e)^{∗}[x := v^{′†}]
=  s^{†}, (v′ e)^{∗}

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

28 · P. Wadler and P. Thiemann

Subcase E = v [ ].

s^{†}, (v n)^{∗}
=  s^{†}, let x ⇐ n^{∗} in (v x)^{∗}
⟶^{f}_{mon} by induction, and context M
s^{†}, let x ⇐ e^{′∗} in (v x)^{∗}

If e′ ∈ NonVal then

= s^{†}, (v e′)^{∗}

If e′ = v′ ∈ Val then

=  s^{†}, let x ⇐ v^{′∗} in (v x)^{∗}
=  s^{†}, let x ⇐ <v^{′†}>in (v x)^{∗}
⟶^{∅}_{mon} s^{†}, (v x)^{∗}[x := v^{′†}]
=  s^{†}, (v v′)^{∗}

Subcase E = ilet x = [ ] in e.

s^{†}, (ilet x = n in e)^{∗}

=  s^{†}, let x ⇐ n^{∗} in e^{∗}
⟶^{f}_{mon} by induction, and context M
s^{†}, let x ⇐ e^{′∗} in e^{∗}
=  s^{†}, (ilet x = e′ in e)^{∗}

Subcase E = new [ ].

s^{†}, (new n)^{∗}
=  s^{†}, let x ⇐ n^{∗} in (new x)^{∗}
⟶^{f}_{mon} by induction, and context M
s^{†}, let x ⇐ e^{′∗} in (new x)^{∗}

If e′ ∈ NonVal then

= s^{†}, (new e′)^{∗}

If e′ = v′ ∈ Val then

=  s^{†}, let x ⇐ v^{′∗} in (new x)^{∗}
=  s^{†}, let x ⇐ <v^{′†}>in (new x)^{∗}
⟶^{∅}_{mon} s^{†}, (new x)^{∗}[x := v^{′†}]
=  s^{†}, (new v′)^{∗}

Subcase E = get [ ].

s^{†}, (get n)^{∗}
=  s^{†}, let x ⇐ n^{∗} in (get x)^{∗}
⟶^{f}_{mon} by induction, and context M
s^{†}, let x ⇐ e^{′∗} in (get x)^{∗}

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

If e′ ∈ NonVal then

= s^{†}, (get e′)^{∗}

If e′ = v′ ∈ Val then

=  s^{†}, let x ⇐ v^{′∗} in (get x)^{∗}
=  s^{†}, let x ⇐ <v^{′†}>in (get x)^{∗}
⟶^{∅}_{mon} s^{†}, (get x)^{∗}[x := v^{′†}]
=  s^{†}, (get v′)^{∗}

Subcase E = set [ ] e. Analogous to E = [ ] e. Subcase E = set v [ ]. Analogous to E = v [ ]. Item 2 by induction on the definition of ⟶ ⟶^{f}_{eff}. Item 3 is immediate from item 2. Item 4 requires an inductive proof, again: Case l v′, where l ∈ Location. (l v′)^{∗} = l^{†} v^{′†} = l v^{′†} is stuck because l is not a lambda. Case get v, where v is not a location or v ∉ dom(s). (get v)^{∗} = get v^{†}. There are three cases for v. Subcase v = l ∈ Location and l ∉ dom(s). Then get l^{†} = get l is stuck because l ∉ dom(s^{†}) = dom(s). Subcase v = λx. e. Then get (λx. e)^{†} = get λx. e^{∗} is stuck because v^{†} is not a location. Subcase v = rec x. λx′. e. Then

get (rec x. λx′. e)^{†}
=  get (rec x. λx′. e^{∗})
⟶_{mon} get (λx′. e^{∗}[x := rec x. λx′. e^{∗}])

which is stuck because λx′…. is not a location.

Case set v v′, where v is not a location or v ∉ dom(s). (set v v′)^{∗} = set v^{†} v^{′†}. Analogous to subcase get v. Case if s, e is stuck, then s, E[e] is stuck. By definition of stuck, e must be a

non-value.

Subcase E = [ ] e′. (e e′)^{∗} = let x ⇐ e^{∗} in (x e′)^{∗}. By induction, s^{†}, e^{∗} is stuck so that e^{∗} has the

form M[e_{0}], where e_{0} is one of the cases in the definition of stuck. Hence, for some monad context M′,

(e e′)^{∗}
= let x ⇐ M[e_{0}] in (x e′)^{∗}
= M′[e_{0}]

This proves the claim.

Subcase E = v [ ]. (v e)^{∗} = let x ⇐ e^{∗} in (v x)^{∗}. Stuck by analogous reasoning as in the previous

subcase.

Subcase E = ilet x = [ ] in e′.

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

(ilet x = e in e′)^{∗} = let x ⇐ e^{∗} in e^{′∗}. Stuck by analogous reasoning as in the previous subcase.

Subcase E = new [ ]. (new e)^{∗} = let x ⇐ e^{∗} in (new x)^{∗}. Stuck by analogous reasoning as in the pre-

vious subcase.

Subcase E = get [ ]. (get e)^{∗} = let x ⇐ e^{∗} in (get x)^{∗}. Analogous. Subcase E = set [ ] e′. (set e e′)^{∗} = let x ⇐ e^{∗} in (set x e′)^{∗}. Analogous to subcase e e′. Subcase E = set v [ ]. (set v e)^{∗} = let x ⇐ e^{∗} in (set v x)^{∗}. Analogous to subcase v e.

A.3 Constraint solution

Proposition 4.2 (Constraint solution)

—(Sound) K(κ) ⊧ κ.

—(Complete) If μ ⊧ κ then μ = μ ∘ K(κ).

Proof. To show soundness, suppose that the constraint set has the form κ∪{ς ⊒ σ}. Now,

K(κ ∪ {ς ⊒ σ})(ς)
= ({ς ↦ ς ∪ K(κ)(σ)} ∘ K(κ))(ς)
= {ς ↦ ς ∪ K(κ)(σ)}(ς)
= ς ∪ K(κ)(σ)
⊒ ({ς ↦ ς ∪ K(κ)(σ)} ∘ K(κ))(σ)
= K(κ ∪ {ς ⊒ σ})(σ)

Completeness is shown by induction on κ. Case ∅ is immediate. Case κ ∪ {ς ⊒ σ}. Let μ′ = μ ∘ K(κ ∪ {ς ⊒ σ}) = μ ∘ {ς ↦ ς ∪ K(κ)(σ)} ∘ K(κ). Show that, for each

ς′, μ′(ς′) = μ(ς′).

First, observe that μ ∘ {ς ↦ ς ∪ K(κ)(σ)} = μ by considering this substitution on ς.

μ({ς ↦ ς ∪ K(κ)(σ)}(ς))

= μ(ς ∪ K(κ)(σ))
= μ(ς) ∪ μ(K(κ)(σ))

[by the inductive hypothesis]

= μ(ς) ∪ μ(σ)

[since μ solution]

= μ(ς)

There are three cases to consider. Subcase ς′ ∉ dom(K(κ)) and ς′ ≠ ς. μ′(ς′) = μ({ς ↦ ς ∪ K(κ)(σ)}(K(κ)(ς′))) = μ(ς′).

ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD 20TBD.

The marriage of effects and monads · 31

Subcase ς′ = ς.

μ′(ς)

= μ({ς ↦ ς ∪ K(κ)(σ)}(K(κ)(ς)))

[since ς ∉ dom(K(κ))]

= μ({ς ↦ ς ∪ K(κ)(σ)}(ς))

[by the preceding observation]

= μ(ς)

Subcase ς′ ∈ dom(K(κ)).

μ′(ς′)

= μ({ς ↦ ς ∪ K(κ)(σ)}(K(κ)(ς′)))

[by the preceding observation]

= μ(K(κ)(ς′))
= μ(ς′)

Received November 1999; revised February 2001; accepted March 2001.