Handling Polymorphic Algebraic Effects
Abstract
Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism that allows abstracting not only expressions but also effects and handlers. Although polymorphism makes it possible to reuse and reason about effect implementations more effectively, it has long been known that a naive combination of polymorphic effects and letpolymorphism breaks type safety. Although type safety can often be gained by restricting letbound expressions—e.g., by adopting value restriction or weak polymorphism—we propose a complementary approach that restricts handlers instead of letbound expressions. Our key observation is that, informally speaking, a handler is safe if resumptions from the handler do not interfere with each other. To formalize our idea, we define a callbyvalue lambda calculus \(\lambda _\text {eff}^\text {let}\) that supports letpolymorphism and polymorphic algebraic effects and handlers, design a type system that rejects interfering handlers, and prove type safety of our calculus.
1 Introduction
Algebraic effects [20] and handlers [21] are a powerful abstraction mechanism to represent and implement control effects, such as exceptions, interactive I/O, mutable states, and nondeterminism. They are growing in popularity, thanks to their success in achieving modularity of effects, especially the clear separation between their interfaces and their implementations. An interface of effects is given as a set of operations—e.g., an interface of mutable states consists of two operations, namely, put and get—with their signatures. An implementation is given by a handler \( H \), which provides a set of interpretations of the operations (called operation clauses), and a \( \mathsf {handle} \)–\( \mathsf {with} \) expression \(\mathsf {handle} \, M \, \mathsf {with} \, H \) associates effects invoked during the computation of \( M \) with handler \( H \). Algebraic effects and handlers work as resumable exceptions: when an effect operation is invoked, the runtime system tries to find the nearest handler that handles the invoked operation; if it is found, the corresponding operation clause is evaluated by using the argument to the operation invocation and the continuation up to the handler. The continuation gives the ability to resume the computation from the point where the operation was invoked, using the result from the operation clause. Another modularity that algebraic effects provide is flexible composition: multiple algebraic effects can be combined freely [13].
In this work, we study an extension of algebraic effects and handlers with another typebased abstraction mechanism—parametric polymorphism [22]. In general, parametric polymorphism is a basis of generic programming and enhance code reusability by abstracting expressions over types. This work allows abstracting not only expressions but also effect operations and handlers, which makes it possible to reuse and reason about effect implementations that are independent of concrete type representations. Like in many functional languages, we introduce polymorphism in the form of letpolymorphism for its practically desirable properties such as decidable typechecking and type inference.
As is well known, however, a naive combination of polymorphic effects and letpolymorphism breaks type safety [11, 23]. Many researchers have attacked this classical problem [1, 2, 10, 12, 14, 17, 23, 24], and their common idea is to restrict the form of letbound expressions. For example, value restriction [23, 24], which is the standard way to make MLlike languages with imperative features and letpolymorphism type safe, allows only syntactic values to be polymorphic.
In this work, we propose a new approach to achieving type safety in a language with letpolymorphic and polymorphic effects and handlers: the idea is to restrict handlers instead of letbound expressions. Since a handler gives an implementation of an effect, our work can be viewed as giving a criterion that suggests what effects can cooperate safely with (unrestricted) letpolymorphism and what effects cannot. Our key observation for type safety is that, informally speaking, an invocation of a polymorphic effect in a letbound expression is safe if resumptions in the corresponding operation clause do not interfere with each other. We formalize this discipline into a type system and show that typeable programs do not get stuck.
Our contributions are summarized as follows.

We introduce a callbyvalue, statically typed lambda calculus \(\lambda _\text {eff}^\text {let}\) that supports letpolymorphism and polymorphic algebraic effects and handlers. The type system of \(\lambda _\text {eff}^\text {let}\) allows any letbound expressions involving effects to be polymorphic, but, instead, disallows handlers where resumptions interfere with each other.

To give the semantics of \(\lambda _\text {eff}^\text {let}\), we formalize an intermediate language \(\lambda _\text {eff}^{\varLambda }\) wherein type information is made explicit and define a formal elaboration from \(\lambda _\text {eff}^\text {let}\) to \(\lambda _\text {eff}^{\varLambda }\).

We prove type safety of \(\lambda _\text {eff}^\text {let}\) by type preservation of the elaboration and type soundness of \(\lambda _\text {eff}^{\varLambda }\).
We believe that our approach is complementary to the usual approach of restricting letbound expressions: for handlers that are considered unsafe by our criterion, the value restriction can still be used.
The rest of this paper is organized as follows. Section 2 provides an overview of our work, giving motivating examples of polymorphic effects and handlers, a problem in naive combination of polymorphic effects and letpolymorphism, and our solution to gain type safety with those features. Section 3 defines the surface language \(\lambda _\text {eff}^\text {let}\), and Sect. 4 defines the intermediate language \(\lambda _\text {eff}^{\varLambda }\) and the elaboration from \(\lambda _\text {eff}^\text {let}\) to \(\lambda _\text {eff}^{\varLambda }\). We also state that the elaboration is typepreserving and that \(\lambda _\text {eff}^{\varLambda }\) is type sound in Sect. 4. Finally, we discuss related work in Sect. 5 and conclude in Sect. 6. The proofs of the stated properties and the full definition of the elaboration are given in the full version at https://arxiv.org/abs/1811.07332.
2 Overview
We start with reviewing how monomorphic algebraic effects and handlers work through examples and then extend them to a polymorphic version. We also explain why polymorphic effects are inconsistent with letpolymorphism, if naively combined, and how we resolve it.
2.1 Monomorphic Algebraic Effects and Handlers
An expression of the form handle \( M \) with \( H \) handles effect operations invoked in \( M \) (which we call handled expression) according to the effect interpretations given by handler \( H \). A handler \( H \) consists of two parts: a single return clause and zero or more operation clauses. A return clause return x \(\rightarrow \) \( M' \) will be executed if the evaluation of \( M \) results in a value \( v \). Then, the value of \( M' \) (where x is bound to \( v \)) will be the value of the entire handle–with expression. For example, in the program above, if a nonzero number n is passed to f, the handle–with expression would return Some \((100{\slash }n)\) because div100 n returns \(100{\slash }n\). An operation clause \(\mathsf {op}\) x \(\rightarrow \) \( M' \) defines an implementation of effect op: if the evaluation of handled expression \( M \) invokes effect op with argument \( v \), expression \( M' \) will be evaluated after substituting \( v \) for x and the value of \( M' \) will be the value of the entire handle–with expression. In the program example above, if zero is given to f, then None will be returned because div100 0 invokes fail.
As shown above, algebraic effect handling is similar to exception handling. However, a distinctive feature of algebraic effect handling is that it allows resumption of the computation from the point where an effect operation was invoked. The next example demonstrates such an ability of algebraic effect handlers.
A resumption expression resume \( M \) in an operation clause makes it possible to return a value of \( M \) to the point where an effect operation was invoked. This behavior is realized by constructing a delimited continuation from the point of the effect invocation up to the handle–with expression that deals with the effect and passing the value of \( M \) to the continuation. We illustrate it by using the program above. When the handled expression #choose(1,2) + #choose(10,20) is evaluated, continuation Open image in new window is constructed. Then, the body resume (fst x) of the operation clause is evaluated after binding x to the invocation argument (1,2). Receiving the value 1 of fst (1,2), the resumption expression passes it to the continuation c and c[1] = 1 + #choose(10,20) is evaluated under the same handler. Next, choose is invoked with argument (10,20). Similarly, continuation Open image in new window is constructed and the operation clause for choose is executed again. Since fst (10,20) evaluates to 10, \(c'[\texttt {10}] = \texttt {1 + 10}\) is evaluated under the same handler. Since the return clause returns what it receives, the entire expression evaluates to 11.
Finally, we briefly review how an operation clause involving resumption expressions is typechecked [3, 13, 16]. Let us consider operation clause Open image in new window for Open image in new window of type signature Open image in new window . The typechecking is performed as follows. First, argument x is assigned the domain type \( A \) of the signature as it will be bound to an argument of an effect invocation. Second, for resumption expression resume \( M' \) in \( M \), (1) \( M' \) is required to have the codomain type \( B \) of the signature because its value will be passed to the continuation as the result of the invocation and (2) the resumption expression is assigned the same type as the return clause. Third, the type of the body \( M \) has to be the same as that of the return clause because the value of Open image in new window is the result of the entire handle–with expression. For example, the above operation clause for choose is typechecked as follows: first, argument x is assigned type Open image in new window ; second, it is checked whether the argument fst x of the resumption expression has int, the codomain type of choose; third, it is checked whether the body resume (fst x) of the clause has the same type as the return clause, i.e., int. If all the requirements are satisfied, the clause is well typed.
2.2 Polymorphic Algebraic Effects and Handlers
This section discusses motivation for polymorphism in algebraic effects and handlers. There are two ways to introduce polymorphism: by parameterized effects and by polymorphic effects.
An invocation #choose involves a parameterized effect of the form Open image in new window (where A denotes a type), according to the type of arguments: For example, #choose(true,false) has the effect bool choose and #choose(1,1) has int choose. Handlers are required for each effect Open image in new window .
In what follows, we show a polymorphic version of the examples we have seen, along with brief discussions on how polymorphic effects help with reasoning about effect implementations. Other practical examples of polymorphic effects can be found in Leijen’s work [16].
Typechecking of operation clauses could be extended in a straightforward manner. That is, an operation clause Open image in new window for an effect operation of signature Open image in new window would be typechecked as follows: first, \(\alpha \) is locally bound in the clause and Open image in new window is assigned type Open image in new window ; second, an argument of a resumption expression must have type Open image in new window (which may contain type variable \(\alpha \)); third, Open image in new window must have the same type as that of the return clause (its type cannot contain \(\alpha \) as \(\alpha \) is local) under the assumption that resumption expressions have the same type as the return clause. For example, let us consider typechecking of the above operation clause for Open image in new window . First, the typechecking algorithm allocates a local type variable \(\alpha \) and assigns type \(\alpha \times \alpha \) to y. The body has two resumption expressions, and it is checked whether the arguments fst y and snd y have the codomain type \(\alpha \) of the signature. Finally, it is checked whether the body is typed at int assuming that the resumption expressions have type int. The operation clause meets all the requirements, and, therefore, it would be well typed.
An obvious advantage of polymorphic effects is reusability. Without polymorphism, one has to declare many versions of choose for different types.
Another pleasant effect of polymorphic effects is that, thanks to parametricity, inappropriate implementations for an effect operation can be excluded. For example, it is not possible for an implementation of Open image in new window to resume with values other than the first or second element of y. In the monomorphic version, however, it is possible to resume with any integer, as opposed to what the name of the operation suggests. A similar argument applies to \(\texttt {fail}^\forall \); since the codomain type is \(\alpha \), which does not appear in the domain type, it is not possible to resume! In other words, the signature Open image in new window enforces that no invocation of \(\texttt {fail}^\forall \) will return.
2.3 Problem in Naive Combination with LetPolymorphism
Although polymorphic effects and handlers provide an ability to abstract and restrict effect implementations, one may easily expect that their unrestricted use with naive letpolymorphism, which allows any letbound expressions to be polymorphic, breaks type safety. Indeed, it does.
2.4 Our Solution
A standard approach to this problem is to restrict the form of letbound expressions by some means such as the (relaxed) value restriction [10, 23, 24] or weak polymorphism [1, 12]. This approach amounts to restricting how effect operations can be used.
In this paper, we seek for a complementary approach, which is to restrict how effect operations can be implemented.^{4} More concretely, we develop a type system such that letbound expressions are polymorphic as long as they invoke only “safe” polymorphic effects and the notion of safe polymorphic effects is formalized in terms of typing rules (for handlers).
 1.
continuation c uses g polymorphically, namely, as \(\texttt {bool} \rightarrow \texttt {bool}\) in g true and as \(\texttt {int} \rightarrow \texttt {int}\) in g 1;
 2.
c is invoked twice; and
 3.
the use of g as \(\texttt {bool} \rightarrow \texttt {bool}\) in the first invocation of c—where g is bound to Open image in new window —“alters” the type of \(\lambda \texttt {z2}.\) \(\texttt {z1}\) (passed to resume) from \(\alpha \rightarrow \alpha \) to \(\alpha \rightarrow \texttt {bool}\), contradicting the second use of g as \(\texttt {int} \rightarrow \texttt {int}\) in the second invocation of c.
The last point is crucial—if \(\lambda \texttt {z2}.\texttt {z1}\) were, say, \(\lambda \texttt {z2}.\texttt {z2}\), there would be no influence from the first invocation of c and the evaluation would succeed. The problem we see here is that the naive type system mistakenly allows interference between the arguments to the two resumptions by assuming that z1 and z2 share the same type.
3 Surface Language: \(\lambda _\mathbf {eff}^\mathbf {let}\)
3.1 Syntax
The syntax of \(\lambda _\text {eff}^\text {let}\) is given in Fig. 1. Effect operations are denoted by \(\mathsf {op}\) and type variables by \(\alpha \), \(\beta \), and \(\gamma \). An effect, denoted by \(\epsilon \), is a finite set of effect operations. We write \( \langle \rangle \) for the empty effect set. A type, denoted by \( A \), \( B \), \( C \), and \( D \), is a type variable; a base type \(\iota \), which includes, e.g., \( \mathsf {bool} \) and \( \mathsf {int} \); or a function type Open image in new window , which is given to functions that take an argument of type \( A \) and compute a value of type \( B \) possibly with effect \(\epsilon \). A type scheme \(\sigma \) is obtained by abstracting type variables. Terms, denoted by \( M \), consist of variables; constants (including primitive operations); lambda abstractions \( \lambda \! \, x . M \), which bind \( x \) in \( M \); function applications; letexpressions \(\mathsf {let} \, x = M_{{\mathrm {1}}} \, \mathsf {in} \, M_{{\mathrm {2}}} \), which bind \( x \) in \( M_{{\mathrm {2}}} \); effect invocations \( \texttt {\#} \mathsf {op} ( M ) \); \( \mathsf {handle} \)–\( \mathsf {with} \) expressions \(\mathsf {handle} \, M \, \mathsf {with} \, H \); and resumption expressions \(\mathsf {resume} \, M \). All type information in \(\lambda _\text {eff}^\text {let}\) is implicit; thus the terms have no type annotations. A handler \( H \) has a single return clause \(\mathsf {return} \, x \rightarrow M \), where \( x \) is bound in \( M \), and zero or more operation clauses of the form \(\mathsf {op} ( x ) \rightarrow M \), where \( x \) is bound in \( M \). A typing context \(\varGamma \) binds a sequence of variable declarations Open image in new window and type variable declarations \(\alpha \).
We introduce the following notations used throughout this paper. We write Open image in new window for Open image in new window where Open image in new window . We often omit indices (\( i \) and \( j \)) and index sets ( Open image in new window and Open image in new window ) if they are not important: e.g., we often abbreviate Open image in new window to Open image in new window or even to Open image in new window . Similarly, we use a bold font for other sequences ( Open image in new window for a sequence of types, Open image in new window for a sequence of values, etc.). We sometimes write Open image in new window to view the sequence \( \varvec{ \alpha } \) as a set by ignoring the order. Free type variables \( ftv ( \sigma ) \) in a type scheme \(\sigma \) and type substitution Open image in new window of Open image in new window for type variables Open image in new window in \( B \) are defined as usual (with the understanding that the omitted index sets for Open image in new window and Open image in new window are the same).
We suppose that each constant \( c \) is assigned a firstorder closed type \( ty ( c ) \) of the form Open image in new window and that each effect operation \(\mathsf {op}\) is assigned a signature of the form Open image in new window , which means that an invocation of \(\mathsf {op}\) with type instantiation Open image in new window takes an argument of Open image in new window and returns a value of Open image in new window . We also assume that, for Open image in new window and Open image in new window .
3.2 Type System
The type system of \(\lambda _\text {eff}^\text {let}\) consists of four judgments: wellformedness of typing contexts \(\vdash \varGamma \); well formedness of type schemes \(\varGamma \vdash \sigma \); term typing judgment \(\varGamma ; R \vdash M : A \,  \, \epsilon \), which means that \( M \) computes a value of \( A \) possibly with effect \(\epsilon \) under typing context \(\varGamma \) and resumption type \( R \) (discussed below); and handler typing judgment \(\varGamma ; R \vdash H : A \,  \, \epsilon \Rightarrow B \,  \, \epsilon '\), which means that \( H \) handles a computation that produces a value of \( A \) with effect \(\epsilon \) and that the clauses in \( H \) compute a value of \( B \) possibly with effect \(\epsilon '\) under \(\varGamma \) and \( R \).
A resumption type \( R \) contains type information for resumption.
Definition 1
Figure 2 shows the inference rules of the judgments (except for \(\varGamma \vdash \sigma \), which is defined by: \(\varGamma \vdash \sigma \) if and only if all free type variables in \(\sigma \) are bound by \(\varGamma \)). For a sequence of type schemes Open image in new window , we write Open image in new window if and only if every type scheme in Open image in new window is well formed under \(\varGamma \).
Wellformedness rules for typing contexts, shown at the top of Fig. 2, are standard. A typing context is well formed if it is empty Open image in new window or a variable in the typing context is associated with a type scheme that is well formed in the remaining typing context Open image in new window and a type variable in the typing context is not declared Open image in new window . For typing context \(\varGamma \), \( dom ( \varGamma ) \) denotes the set of type and term variables declared in \(\varGamma \).
Typing rules for terms are given in the middle of Fig. 2. The first six rules are standard for the lambda calculus with letpolymorphism and a typeandeffect system. If a variable \( x \) is introduced by a letexpression and has type scheme Open image in new window in \(\varGamma \), it is given type Open image in new window , obtained by instantiating type variables Open image in new window with wellformed types \( \varvec{ B } \). If \( x \) is bound by other constructors (e.g., a lambda abstraction), \( x \) is always bound to a monomorphic type and both \( \varvec{ \alpha } \) and \( \varvec{ B } \) are the empty sequence. Note that Open image in new window gives any effect \(\epsilon \) to the typing judgment for \( x \). In general, \(\epsilon \) in judgment \(\varGamma ; R \vdash M : A \,  \, \epsilon \) means that the evaluation of \( M \) may invoke effect operations in \(\epsilon \). Since a reference to a variable involves no effect, it is given any effect; for the same reason, value constructors are also given any effect. The rule Open image in new window means that the type of a constant is given by (metalevel) function \( ty \). The typing rules for lambda abstractions and function applications are standard in the lambda calculus equipped with a typeandeffect system. The rule Open image in new window gives lambda abstraction \( \lambda \! \, x . M \) function type Open image in new window if \( M \) computes a value of \( B \) possibly with effect \(\epsilon '\) by using \( x \) of type \( A \). The rule Open image in new window requires that (1) the argument type of function part \( M_{{\mathrm {1}}} \) be equivalent to the type of actual argument \( M_{{\mathrm {2}}} \) and (2) effect \(\epsilon '\) invoked by function \( M_{{\mathrm {1}}} \) be contained in the whole effect \(\epsilon \). The rule Open image in new window allows weakening of effects.
The next two rules are mostly standard for algebraic effects and handlers. The rule Open image in new window is applied to effect invocations. Since \(\lambda _\text {eff}^\text {let}\) supports implicit polymorphism, an invocation \( \texttt {\#} \mathsf {op} ( M ) \) of polymorphic effect \(\mathsf {op}\) of signature Open image in new window also accompanies implicit type substitution of wellformed types \( \varvec{ C } \) for \( \varvec{ \alpha } \). Thus, the type of argument \( M \) has to be \( A [ \varvec{ C } / \varvec{ \alpha } ] \) and the result of the invocation is given type \( B [ \varvec{ C } / \varvec{ \alpha } ] \). In addition, effect \(\epsilon \) contains \(\mathsf {op}\). The typeability of \( \mathsf {handle} \)–\( \mathsf {with} \) expressions depends on the typing of handlers Open image in new window , which will be explained below shortly.
The typing rules for handlers are standard [3, 13, 16]. The rule Open image in new window for a return clause \(\mathsf {return} \, x \rightarrow M \) checks that the body \( M \) is given a type under the assumption that argument \( x \) has type \( A \), which is the type of the handled expression. The effect \(\epsilon \) stands for effects that are not handled by the operation clauses that follow the return clause and it must be a subset of the effect \(\epsilon '\) that \( M \) may cause.^{5} A handler having operation clauses is typechecked by Open image in new window , which checks that the body of the operation clause \(\mathsf {op} ( x ) \rightarrow M \) for \(\mathsf {op}\) of signature Open image in new window is typed at the result type \( B \), which is the same as the type of the return clause, under the typing context extended with fresh assigned type variables \( \varvec{ \alpha } \) and argument \( x \) of type \( C \), together with the resumption type Open image in new window . The effect \( \epsilon \mathbin {\uplus } \{ \mathsf {op} \} \) in the conclusion means that the effect operation \(\mathsf {op}\) is handled by this clause and no other clauses (in the present handler) handle it. Our semantics adopts deep handlers [13], i.e., when a handled expression invokes an effect operation, the continuation, which passed to the operation clause, is wrapped by the same handler. Thus, resumption may invoke the same effect \(\epsilon '\) as the one possibly invoked by the clauses of the handler, hence Open image in new window in the resumption type.
4 Intermediate Language: \(\lambda _\mathbf {eff}^{\varLambda }\)
4.1 Syntax
The syntax of \(\lambda _\text {eff}^{\varLambda }\) is shown in Fig. 3. Values, denoted by \( v \), consist of constants and lambda abstractions. Polymorphic values, denoted by \( w \), are values abstracted over types. Terms, denoted by \( e \), and handlers, denoted by \( h \), are the same as those of \(\lambda _\text {eff}^\text {let}\) except for the following three points. First, type abstraction and type arguments are explicit in \(\lambda _\text {eff}^{\varLambda }\): variables and effect invocations are accompanied by a sequence of types and letbound expressions, resumption expressions, and operation clauses bind type variables. Second, a new term constructor of the form \( \texttt {\#} \mathsf {op} ( \varvec{ \sigma } , w , E ) \) is added. It represents an intermediate state in which an effect invocation is capturing the continuation up to the closest handler for \(\mathsf {op}\). Here, \( E \) is an evaluation context [6] and denotes a continuation to be resumed by an operation clause handling \(\mathsf {op}\). In the operational semantics, an operation invocation \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v ) \) is first transformed to \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v , [\,] ) \) (where \( [\,] \) denotes the empty context or the identity continuation) and then it bubbles up by capturing its context and pushing it onto the third argument. Note that \( \varvec{ \sigma } \) and \( w \) of \( \texttt {\#} \mathsf {op} ( \varvec{ \sigma } , w , E ) \) become polymorphic when it bubbles up from the body of a type abstraction. Third, each resumption expression \(\mathsf {resume} \, \varvec{ \alpha } \, x . e \) declares distinct (type) variables \( \varvec{ \alpha } \) and \( x \) to denote the (type) argument to an operation clause, whereas a single variable declared at \(\mathsf {op} ( x ) \rightarrow M \) and implicit type variables are used for the same purpose in \(\lambda _\text {eff}^\text {let}\). For example, the \(\lambda _\text {eff}^\text {let}\) operation clause \( \mathsf {choose}^{\forall } ( x ) \rightarrow \mathsf {resume} \, ( \mathsf {fst} \, x )\) is translated to \( \varLambda \! \, \alpha . \mathsf {choose}^{\forall } ( x ) \rightarrow \mathsf {resume} \, \beta \, y .( \mathsf {fst} \, y )\). This change simplifies the semantics.
4.2 Semantics
The semantics of \(\lambda _\text {eff}^{\varLambda }\) is given in the smallstep style and consists of two relations: the reduction relation \( \rightsquigarrow \), which is for basic computation, and the evaluation relation \( \longrightarrow \), which is for toplevel execution. Figure 4 shows the rules for these relations. In what follows, we write \( h ^\mathsf {return} \) for the return clause of handler \( h \), \( ops ( h ) \) for the set of effect operations handled by \( h \), and \( h ^{ \mathsf {op} } \) for the operation clause for \(\mathsf {op}\) in \( h \).
Most of the reduction rules are standard [13, 16]. A constant application \( c_{{\mathrm {1}}} \, c_{{\mathrm {2}}} \) reduces to \( \zeta ( c_{{\mathrm {1}}} , c_{{\mathrm {2}}} ) \) Open image in new window , where function \( \zeta \) maps a pair of constants to another constant. A function application \(( \lambda \! \, x . e ) \, v \) and a letexpression \(\mathsf {let} \, x = \varLambda \! \, \varvec{ \alpha } . v \, \mathsf {in} \, e \) reduce to \( e [ v / x ] \) Open image in new window and \( e [ \varLambda \! \, \varvec{ \alpha } . v / x ] \) Open image in new window , respectively. If a handled expression is a value \( v \), the \( \mathsf {handle} \)–\( \mathsf {with} \) expression reduces to the body of the return clause where \( v \) is substituted for the parameter \( x \) Open image in new window . An effect invocation \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v ) \) reduces to \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v , [\,] ) \) with the identity continuation, as explained above Open image in new window ; the process of capturing its evaluation context is expressed by the rules Open image in new window , Open image in new window , Open image in new window , Open image in new window , and Open image in new window . The rule Open image in new window can be applied only if the handler \( h \) does not handle \(\mathsf {op}\). The rule Open image in new window is applied to a letexpression where Open image in new window appears under a type abstraction with bound type variables Open image in new window . Since Open image in new window and \( w \) may refer to Open image in new window , the reduction result binds Open image in new window in both Open image in new window and \( w \). We write Open image in new window for a sequence Open image in new window , ..., Open image in new window of type schemes (where Open image in new window ).
The crux of the semantics is Open image in new window : it is applied when Open image in new window reaches the handler \( h \) that handles \(\mathsf {op}\). Since the handled term Open image in new window is constructed from an effect invocation Open image in new window , if the captured continuation \( E \) binds type variables Open image in new window , the same type variables Open image in new window should have been added to Open image in new window and \( v \) along the capture. Thus, the handled expression on the lefthand side of the rule takes the form Open image in new window (with the same type variables Open image in new window ).
The righthand side of Open image in new window involves three types of substitution: continuation substitution Open image in new window for resumptions, type substitution for Open image in new window , and value substitution for \( x \). We explain them one by one below. In the following, let Open image in new window and Open image in new window .
(The differences from the simple case are shaded.) The idea is to bind Open image in new window that appear free in Open image in new window and \( v \) by type abstraction at \( \mathsf {let} \) and to instantiate with the same variables at Open image in new window , where Open image in new window are bound by type abstractions in Open image in new window .
Continuation substitution is formally defined as follows:
Definition 2
The second and third clauses (for a handler) mean that continuation substitution is applied only to return clauses.
Type and Value Substitution. The type and value substitutions Open image in new window and Open image in new window , respectively, in Open image in new window are for (type) parameters in Open image in new window . The basic idea is to substitute Open image in new window for Open image in new window and Open image in new window for Open image in new window —similarly to continuation substitution. We erase free type variables Open image in new window in Open image in new window and \( v \) by substituting the designated base type \( \bot \) for all of them. (We write Open image in new window and Open image in new window for the types and value, respectively, after the erasure.)
The evaluation rule is ordinary: Evaluation of a term proceeds by reducing a subterm under an evaluation context.
4.3 Type System
The type system of \(\lambda _\text {eff}^{\varLambda }\) is similar to that of \(\lambda _\text {eff}^\text {let}\) and has five judgments: wellformedness of typing contexts \(\vdash \varGamma \); well formedness of type schemes \(\varGamma \vdash \sigma \); term typing judgment \(\varGamma ; r \, \vdash e \, : A \,  \, \epsilon \); handler typing judgment \(\varGamma ; r \, \vdash h : A \,  \, \epsilon \Rightarrow B \,  \, \epsilon '\); and continuation typing judgment Open image in new window . The first two are defined in the same way as those of \(\lambda _\text {eff}^\text {let}\). The last judgment means that a term obtained by filling the hole of \( E \) with a term having \( A \) under \(\varGamma , \varvec{ \alpha } \) is typed at \( B \) under \(\varGamma \) and possibly involves effect \(\epsilon \). A resumption type \( r \) is similar to \( R \) but does not contain an argument variable.
Definition 3
The typing rules for continuations are shown in the lower half of Fig. 6. They are similar to the corresponding typing rules for terms except that a subterm is replaced with a continuation. In Open image in new window , the continuation \(\mathsf {let} \, x = \varLambda \! \, \varvec{ \alpha } . E \, \mathsf {in} \, e \) has type Open image in new window because the hole of \( E \) appears inside the scope of \( \varvec{ \alpha } \).
4.4 Elaboration
This section defines the elaboration from \(\lambda _\text {eff}^\text {let}\) to \(\lambda _\text {eff}^{\varLambda }\). The important difference between the two languages from the viewpoint of elaboration is that, whereas the parameter of an operation clause is referred to by a single variable in \(\lambda _\text {eff}^\text {let}\), it is done by one or more variables in \(\lambda _\text {eff}^{\varLambda }\). Therefore, one variable in \(\lambda _\text {eff}^\text {let}\) is represented by multiple variables (required for each \( \mathsf {resume} \)) in \(\lambda _\text {eff}^{\varLambda }\). We use \( S \), a mapping from variables to variables, to make the correspondence between variable names. We write \( S \,\circ \, \{ x \, {\mapsto } \, y \} \) for the same mapping as \( S \) except that \( x \) is mapped to \( y \).
Selected elaboration rules are shown in Fig. 7; the complete set of the rules is found in the full version of the paper. The elaboration rules are straightforward except for the use of \( S \). A variable \( x \) is translated to \( S ( x )\) Open image in new window and, every time a new variable is introduced, \( S \) is extended: see the rules other than Open image in new window and Open image in new window .
4.5 Properties
We show type safety of \(\lambda _\text {eff}^\text {let}\), i.e., a welltyped program in \(\lambda _\text {eff}^\text {let}\) does not get stuck, by proving (1) type preservation of the elaboration from \(\lambda _\text {eff}^\text {let}\) to \(\lambda _\text {eff}^{\varLambda }\) and (2) type soundness of \(\lambda _\text {eff}^{\varLambda }\). Term \( M \) is a welltyped program of \( A \) if and only if \( \emptyset ; \mathsf {none} \vdash M : A \,  \, \langle \rangle \).
The first can be shown easily. We write \( \emptyset \) also for the identity mapping for variables.
Theorem 1
(Elaboration is typepreserving). If \( M \) is a welltyped program of \( A \), then \( \emptyset ; \mathsf {none} \vdash M : A \,  \, \langle \rangle \mathrel { \vartriangleright ^{ \emptyset } } e \) and \( \emptyset ; \mathsf {none} \, \vdash e \, : A \,  \, \langle \rangle \) for some \( e \).
We show the second—type soundness of \(\lambda _\text {eff}^{\varLambda }\)—via progress and subject reduction [25]. We write \(\varDelta \) for a typing context that consists only of type variables. Progress can be shown as usual.
Lemma 1
(Progress). If \(\varDelta ; \mathsf {none} \, \vdash e \, : A \,  \, \epsilon \), then (1) \( e \longrightarrow e' \) for some \( e' \), (2) \( e \) is a value, or (3) \( e \, = \, \texttt {\#} \mathsf {op} ( \varvec{ \sigma } , w , E ) \) for some \(\mathsf {op} \, \in \, \epsilon \), \( \varvec{ \sigma } \), \( w \), and \( E \).
A key lemma to show subject reduction is type preservation of continuation substitution.
Lemma 2
(Continuation substitution). Suppose that Open image in new window and Open image in new window and Open image in new window .
 1.
If Open image in new window , then Open image in new window .
 2.
If Open image in new window , then Open image in new window .
Using the continuation substitution lemma as well as other lemmas, we show subject reduction.
Lemma 3
 1.
If \(\varDelta ; \mathsf {none} \, \vdash e_{{\mathrm {1}}} \, : A \,  \, \epsilon \) and \( e_{{\mathrm {1}}} \rightsquigarrow e_{{\mathrm {2}}} \), then \(\varDelta ; \mathsf {none} \, \vdash e_{{\mathrm {2}}} \, : A \,  \, \epsilon \).
 2.
If \(\varDelta ; \mathsf {none} \, \vdash e_{{\mathrm {1}}} \, : A \,  \, \epsilon \) and \( e_{{\mathrm {1}}} \longrightarrow e_{{\mathrm {2}}} \), then \(\varDelta ; \mathsf {none} \, \vdash e_{{\mathrm {2}}} \, : A \,  \, \epsilon \).
We write Open image in new window if and only if \( e \) cannot evaluate further. Moreover, \( \longrightarrow ^{*} \) denotes the reflexive and transitive closure of the evaluation relation \( \longrightarrow \).
Theorem 2
(Type soundness of \(\lambda _\mathbf {eff}^{\varLambda }\)). If \(\varDelta ; \mathsf {none} \, \vdash e \, : A \,  \, \epsilon \) and \( e \longrightarrow ^{*} e' \) and Open image in new window , then (1) \( e' \) is a value or (2) \( e' \, = \, \texttt {\#} \mathsf {op} ( \varvec{ \sigma } , w , E ) \) for some \(\mathsf {op} \, \in \, \epsilon \), \( \varvec{ \sigma } \), \( w \), and \( E \).
Now, type safety of \(\lambda _\text {eff}^\text {let}\) is obtained as a corollary of Theorems 1 and 2.
Corollary 1
(Type safety of \(\lambda _\mathbf {eff}^\mathbf {let}\)). If \( M \) is a welltyped program of \( A \), there exists some \( e \) such that \( \emptyset ; \mathsf {none} \vdash M : A \,  \, \langle \rangle \mathrel { \vartriangleright ^{ \emptyset } } e \) and \( e \) does not get stuck.
5 Related Work
5.1 Polymorphic Effects and LetPolymorphism
Many researchers have attacked the problem of combining effects—not necessarily algebraic—and letpolymorphism so far [1, 2, 10, 12, 14, 17, 23, 24]. In particular, most of them have focused on MLstyle polymorphic references. The algebraic effect handlers dealt with in this paper seem to be unable to implement general MLstyle references—i.e., give an appropriate implementation to a set of effect operations new with the signature Open image in new window , get with Open image in new window , and put with Open image in new window for abstract datatype \( \alpha \, \mathsf {ref} \)—even without the restriction on handlers because each operation clause in a handler assigns type variables locally and it is impossible to share such type variables between operation clauses.^{6} Nevertheless, their approaches would be applicable to algebraic effects and handlers.
A common idea in the literature is to restrict the form of expressions bound by polymorphic let. Thus, they are complementary to our approach in that they restrict how effect operations are used whereas we restrict how effect operations are implemented.
Asai and Kameyama [2] study a combination of letpolymorphism with delimited control operators shift/reset [4]. They allow a letbound expression to be polymorphic if it invokes no control operation. Thus, the function f1 above would be rejected in their approach.
More recently, Kammar and Pretnar [14] show that parameterized algebraic effects and handlers do not need the value restriction if the type variables used in an effect invocation are not generalized. Thus, as the other work that restricts generalized type variables, their approach would reject function f1 but would accept f3.
5.2 Algebraic Effects and Handlers
Algebraic effects [20] are a way to represent the denotation of an effect by giving a set of operations and an equational theory that capture their properties. Algebraic effect handlers, introduced by Plotkin and Pretnar [21], make it possible to provide userdefined effects. Algebraic effect handlers have been gaining popularity owing to their flexibility and have been made available as libraries [13, 15, 26] or as primitive features of languages, such as Eff [3], Koka [16], Frank [18], and Multicore OCaml [5]. In these languages, letbound expressions that can be polymorphic are restricted to values or pure expressions.
Recently, Forster et al. [9] investigate the relationships between algebraic effect handlers and other mechanisms for userdefined effects—delimited control shift0 [19] and monadic reflection [7, 8]—conjecturing that there would be no typepreserving translation from a language with delimited control or monadic reflection to one with algebraic effect handlers. It would be an interesting direction to export our idea to delimited control and monadic reflection.
6 Conclusion
There has been a long history of collaboration between effects and letpolymorphism. This work focuses on polymorphic algebraic effects and handlers, wherein the type signature of an effect operation can be polymorphic and an operation clause has a type binder, and shows that a naive combination of polymorphic effects and letpolymorphism breaks type safety. Our novel observation to address this problem is that any letbound expression can be polymorphic safely if resumptions from a handler do not interfere with each other. We formalized this idea by developing a type system that requires the argument of each resumption expression to have a type obtained by renaming the type variables assigned in the operation clause to those assigned in the resumption. We have proven that a welltyped program in our type system does not get stuck via elaboration to an intermediate language wherein type information appears explicitly.
There are many directions for future work. The first is to address the problem, described at the end of Sect. 3, that renaming the type variables assigned in an operation clause to those assigned in a resumption expression is allowed for the argument of the clause but not for variables bound by lambda abstractions and letexpressions outside the resumption expression. Second, we are interested in incorporating other features from the literature on algebraic effect handlers, such as dynamic resources [3] and parameterized algebraic effects, and restriction techniques that have been developed for typesafe imperative programming with letpolymorphism such as (relaxed) value restriction [10, 23, 24]. For example, we would like to develop a type system that enforces the noninterfering restriction only to handlers implementing effect operations invoked in polymorphic computation. We also expect that it is possible to determine whether implementations of an effect operation have no interfering resumption from the type signature of the operation, as relaxed value restriction makes it possible to find safely generalizable type variables from the type of a letbound expression [10]. Finally, we are also interested in implementing our idea for a language with effect handlers such as Koka [16] and in applying the idea of analyzing handlers to other settings such as dependent typing.
Footnotes
 1.
Here, “; 1” is necessary to make the types of both branches the same; it becomes unnecessary when we introduce polymorphic effects.
 2.
We can think of more practical implementations, which choose one of the two arguments by other means, say, random values.
 3.
One might implement rand as another effect operation.
 4.
We compare our approach with the standard approaches in Sect. 5 in detail.
 5.
Thus, handlers in \(\lambda _\text {eff}^\text {let}\) are open [13] in the sense that a \( \mathsf {handle} \)–\( \mathsf {with} \) expression does not have to handle all effects caused by the handled expression.
 6.
One possible approach to dealing with MLstyle references is to extend algebraic effects and handlers so that a handler for parameterized effects can be connected with dynamic resources [3].
Notes
Acknowledgments
We would like to thank the anonymous reviewers for their valuable comments. This work was supported in part by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST (Sekiyama), and JSPS KAKENHI Grant Number JP15H05706 (Igarashi).
References
 1.Appel, A.W., MacQueen, D.B.: Standard ML of New Jersey. In: Maluszyński, J., Wirsing, M. (eds.) PLILP 1991. LNCS, vol. 528, pp. 1–13. Springer, Heidelberg (1991). https://doi.org/10.1007/3540544445_83CrossRefGoogle Scholar
 2.Asai, K., Kameyama, Y.: Polymorphic delimited continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239–254. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540766377_16CrossRefGoogle Scholar
 3.Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Methods Program. 84(1), 108–123 (2015). https://doi.org/10.1016/j.jlamp.2014.02.001MathSciNetCrossRefzbMATHGoogle Scholar
 4.Danvy, O., Filinski, A.: Abstracting control. In: LISP and Functional Programming, pp. 151–160 (1990). https://doi.org/10.1145/91556.91622
 5.Dolan, S., Eliopoulos, S., Hillerström, D., Madhavapeddy, A., Sivaramakrishnan, K.C., White, L.: Concurrent system programming with effect handlers. In: Wang, M., Owens, S. (eds.) TFP 2017. LNCS, vol. 10788, pp. 98–117. Springer, Cham (2018). https://doi.org/10.1007/9783319897196_6CrossRefGoogle Scholar
 6.Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992). https://doi.org/10.1016/03043975(92)900147MathSciNetCrossRefzbMATHGoogle Scholar
 7.Filinski, A.: Representing monads. In: Proceedings of the 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 446–457 (1994). https://doi.org/10.1145/174675.178047
 8.Filinski, A.: Monads in action. In: Proceedings of the 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 483–494 (2010). https://doi.org/10.1145/1706299.1706354
 9.Forster, Y., Kammar, O., Lindley, S., Pretnar, M.: On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control. PACMPL 1(ICFP), 13:1–13:29 (2017). https://doi.org/10.1145/3110257
 10.Garrigue, J.: Relaxing the value restriction. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 196–213. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540247548_15CrossRefGoogle Scholar
 11.Harper, R., Lillibridge, M.: Polymorphic type assignment and CPS conversion. Lisp Symb. Comput. 6(3–4), 361–380 (1993)CrossRefGoogle Scholar
 12.Hoang, M., Mitchell, J.C., Viswanathan, R.: Standard MLNJ weak polymorphism and imperative constructs. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science, LICS 1993 (1993)Google Scholar
 13.Kammar, O., Lindley, S., Oury, N.: Handlers in action. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 145–158 (2013). https://doi.org/10.1145/2500365.2500590
 14.Kammar, O., Pretnar, M.: No value restriction is needed for algebraic effects and handlers. J. Funct. Program. 27, e7 (2017). https://doi.org/10.1017/S0956796816000320MathSciNetCrossRefzbMATHGoogle Scholar
 15.Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, pp. 94–105 (2015). https://doi.org/10.1145/2804302.2804319
 16.Leijen, D.: Type directed compilation of rowtyped algebraic effects. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 486–499 (2017). http://dl.acm.org/citation.cfm?id=3009872
 17.Leroy, X., Weis, P.: Polymorphic type inference and assignment. In: Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 291–302 (1991). https://doi.org/10.1145/99583.99622
 18.Lindley, S., McBride, C., McLaughlin, C.: Do be do be do. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 500–514 (2017). http://dl.acm.org/citation.cfm?id=3009897
 19.Materzok, M., Biernacki, D.: A dynamic interpretation of the CPS hierarchy. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 296–311. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642351822_21CrossRefGoogle Scholar
 20.Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categ. Struct. 11(1), 69–94 (2003). https://doi.org/10.1023/A:1023064908962MathSciNetCrossRefzbMATHGoogle Scholar
 21.Plotkin, G.D., Pretnar, M.: Handlers of algebraic effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 80–94. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642005909_7CrossRefGoogle Scholar
 22.Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513–523 (1983)Google Scholar
 23.Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1–34 (1990). https://doi.org/10.1016/08905401(90)90018DMathSciNetCrossRefzbMATHGoogle Scholar
 24.Wright, A.K.: Simple imperative polymorphism. Lisp Symb. Comput. 8(4), 343–355 (1995)CrossRefGoogle Scholar
 25.Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994). https://doi.org/10.1006/inco.1994.1093MathSciNetCrossRefzbMATHGoogle Scholar
 26.Wu, N., Schrijvers, T., Hinze, R.: Effect handlers in scope. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell 2014, pp. 1–12 (2014). https://doi.org/10.1145/2633357.2633358
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.