Handling Polymorphic Algebraic Effects

Exception. Our first example is exception handling, shown in an ML-like language below.

Some and None are constructors of datatype option. Line 1 declares an effect operation fail, which signals that an anomaly happens, with its signature \(\texttt {unit} \hookrightarrow \texttt {unit}\), which means that the operation is invoked with the unit value (), causes some effect, and may return the unit value. The function div100, defined in Lines 3–5, is an example that uses fail; it returns the number obtained by dividing 100 by argument x if x is not zero; otherwise, if x is zero, it raises an exception by calling effect operation fail.¹ In general, we write #op(\( M \)) for invoking effect operation op with argument \( M \). The function f (Lines 7–10) calls div_100 inside a handle–with expression, which returns Some n if div_100 returns integer n normally and returns None if it invokes fail.

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.

Choice. The next example is effect choose, which returns one of the given two arguments.

As usual, \( A_{{\mathrm {1}}} \times A_{{\mathrm {2}}} \) is a product type, (\( M_{{\mathrm {1}}} \), \( M_{{\mathrm {2}}} \)) is a pair expression, and fst is the first projection function. The first line declares that effect choose is for choosing integers. The handled expression #choose(1,2) + #choose(10,20) intuitively suggests that there would be four possible results—11, 21, 12, and 22—depending on which value each invocation of choose returns. The handler in this example always chooses the first element of a given pair² and returns it by using a resume expression, and, as a result, the expression in Lines 3–5 evaluates to 11.

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 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 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 for of type signature . 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 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 ; 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.

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.

The former is used to parameterize the declaration of an effect by types. For example, one might declare:

An invocation #choose involves a parameterized effect of the form (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 .

The latter is used to give a polymorphic type to an effect. For example, one may declare

In this case, the effect can be invoked with different types, but all invocations have the same effect choose. One can implement a single operation clause that can handle all invocations of choose, regardless of argument types. Koka supports both styles [16] (with the value restriction); we focus, however, on the latter in this paper. A type system for parameterized effects lifting the value restriction is studied by Kammar and Pretnar [14] (see Sect. 5 for comparison).

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].

Polymorphic Exception. First, we extend the exception effect fail with polymorphism.

The polymorphic type signature of effect \(\texttt {fail}^\forall \), given in Line 1, means that the codomain type \(\alpha \) can be any. Thus, we do not need to append the dummy value -1 to the invocation of \(\texttt {fail}^\forall \) by instantiating the bound type variable \(\alpha \) with int (the shaded part).

Choice. Next, let us make choose polymorphic.

The function random_walk implements random walk; it takes the current coordinate x, chooses whether it stops, and, if it decides to continue, recursively calls itself with a new coordinate. In the definition, is used twice with different types: bool and int. Lines 11–12 give an interpretation, which calls rand to obtain a random float,³ and returns either the first or the second element of y.

Typechecking of operation clauses could be extended in a straightforward manner. That is, an operation clause for an effect operation of signature would be typechecked as follows: first, \(\alpha \) is locally bound in the clause and is assigned type ; second, an argument of a resumption expression must have type (which may contain type variable \(\alpha \)); third, 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 . 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.

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 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 enforces that no invocation of \(\texttt {fail}^\forall \) will return.

We develop a counterexample, inspired by Harper and Lillibridge [11], below.

The function f first binds g to the invocation result of op. The expression #get_id() is given type \(\alpha \rightarrow \alpha \) and the naive let-polymorphism would assign type scheme \(\forall \alpha . \alpha \rightarrow \alpha \) to g, which makes both g true and g 0 (and thus the definition of f) well typed.

An intended use of f is as follows:

The operation clause for get_id resumes with the identity function \(\lambda \)z.z. It would be well typed under the typechecking procedure described in Sect. 2.2 and it safely returns 1.

However, the following strange expression

will get stuck, although this expression would be well typed: both and \(\lambda \)z2. z1 could be given type \(\alpha \rightarrow \alpha \) by assigning both z1 and z2 type \(\alpha \), which is the type variable local to this clause. Let us see how the evaluation gets stuck in detail. When the handled expression f () invokes effect get_id, the following continuation will be constructed:Next, the body of the operation clause get_id is evaluated. It immediately resumes and reduces towherewhich is the continuation c under the same handler. The evaluation proceeds as follows (here, ):Here, the hole in \(c'\) is filled by function (\(\lambda \)z2.true), which returns a Boolean value, though the hole is supposed to be filled by a function of \(\forall \alpha .\,\alpha \rightarrow \alpha \). This weird gap triggers a run-time error:

We stop here because true + 1 cannot reduce.

A standard approach to this problem is to restrict the form of let-bound 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.⁴ More concretely, we develop a type system such that let-bound 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).

To see what are “safe” effects, let us examine the above counterexample to type safety. The crux of the counterexample is that

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.

Based on this observation, the typing rule for resumption is revised to disallow interference between different resumptions by separating their types: for each resume M in the operation clause for , M has to have type \(B'\) obtained by renaming all type variables \(\alpha _i\) in B with fresh type variables \(\alpha _i'\). In the case of get_id, the two resumptions should be called with \(\beta \rightarrow \beta \) and \(\gamma \rightarrow \gamma \) for fresh \(\beta \) and \(\gamma \); for the first resume to be well typed, z1 has to be of type \(\beta \), although it means that the return type of \(\lambda \)z2.z1 (given to the second resumption) is \(\beta \), making the entire clause ill typed, as we expect. If a clause does not have interfering resumptions likeorit will be well typed.

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 , 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; let-expressions \(\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 and type variable declarations \(\alpha \).

We introduce the following notations used throughout this paper. We write for where . We often omit indices (\( i \) and \( j \)) and index sets ( and ) if they are not important: e.g., we often abbreviate to or even to . Similarly, we use a bold font for other sequences ( for a sequence of types, for a sequence of values, etc.). We sometimes write 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 of for type variables in \( B \) are defined as usual (with the understanding that the omitted index sets for and are the same).

We suppose that each constant \( c \) is assigned a first-order closed type \( ty ( c ) \) of the form and that each effect operation \(\mathsf {op}\) is assigned a signature of the form , which means that an invocation of \(\mathsf {op}\) with type instantiation takes an argument of and returns a value of . We also assume that, for and .

The type system of \(\lambda _\text {eff}^\text {let}\) consists of four judgments: well-formedness 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.

If \( M \) is not a subterm of an operation clause, it is typechecked under \( R = \mathsf {none} \), which means that \( M \) cannot contain resumption expressions. Otherwise, suppose that \( M \) is a subterm of an operation clause \(\mathsf {op} ( x ) \rightarrow M' \) that handles effect \(\mathsf {op}\) of signature and computes a value of \( C \) possibly with effect \(\epsilon \). Then, \( M \) is typechecked under , which means that argument \( x \) to the operation clause has type \( A \) and that resumptions in \( M \) are effectful functions from \( B \) to \( C \) with effect \(\epsilon \). Note that type variables occur free only in \( A \) and \( B \) but not in \( C \).

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 , we write if and only if every type scheme in is well formed under \(\varGamma \).

Well-formedness rules for typing contexts, shown at the top of Fig. 2, are standard. A typing context is well formed if it is empty or a variable in the typing context is associated with a type scheme that is well formed in the remaining typing context and a type variable in the typing context is not declared . 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 let-polymorphism and a type-and-effect system. If a variable \( x \) is introduced by a let-expression and has type scheme in \(\varGamma \), it is given type , obtained by instantiating type variables with well-formed 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 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 means that the type of a constant is given by (meta-level) function \( ty \). The typing rules for lambda abstractions and function applications are standard in the lambda calculus equipped with a type-and-effect system. The rule gives lambda abstraction \( \lambda \! \, x . M \) function type if \( M \) computes a value of \( B \) possibly with effect \(\epsilon '\) by using \( x \) of type \( A \). The rule 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 allows weakening of effects.

The next two rules are mostly standard for algebraic effects and handlers. The rule 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 also accompanies implicit type substitution of well-formed 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 , which will be explained below shortly.

The last typing rule is the key to gaining type safety in this work. Suppose that we are given resumption type . Intuitively, is the type of the continuation for resumption and, therefore, argument \( M \) to \( \mathsf {resume} \) is required to have type \( B \). As we have discussed in Sect. 2, we avoid interference between different resumptions by renaming \( \varvec{ \alpha } \), the type parameters to the effect operation, to fresh type variables \( \varvec{ \beta } \), in typechecking \( M \). Freshness of \( \varvec{ \beta } \) will be ensured when well-formedness of typing contexts \(\varGamma _{{\mathrm {1}}} , \varGamma _{{\mathrm {2}}} , \varvec{ \beta } , \ldots \) is checked at the leaves of the type derivation. The type variables \( \varvec{ \alpha } \) in the type of \( x \), the parameter to the operation, are also renamed for \( x \) to be useful in \( M \). To see why this renaming is useful, let us consider an extension of the calculus with pairs and typechecking of an operation clause for \( \mathsf {choose}^{\forall } \) of signature :Variable \( x \) is assigned product type \( \alpha \times \alpha \) for fresh type variable \(\alpha \) and the body \(\mathsf {resume} \, ( \mathsf {fst} \, x )\) is typechecked under the resumption type for some \(\epsilon \) and \( A \) (see the typing rules for handlers for details). To typecheck \(\mathsf {resume} \, ( \mathsf {fst} \, x )\), the argument \( \mathsf {fst} \, x \) is required to have type \(\beta \), freshly generated for this \( \mathsf {resume} \). Without applying renaming also to \( x \), the clause would not typecheck. Finally, also requires that (1) the typing context contains \( \varvec{ \alpha } \), which should have been declared at an application of the typing rule for the operation clause that surrounds this \( \mathsf {resume} \) and (2) effect \(\epsilon \), which may be invoked by resumption of a continuation, be contained in the whole effect \(\epsilon '\). The binding \( x \, \mathord {:} \, D \) in the conclusion means that parameter \( x \) to the operation clause is declared outside the resumption expression.

The typing rules for handlers are standard [3, 13, 16]. The rule 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.⁵ A handler having operation clauses is typechecked by , which checks that the body of the operation clause \(\mathsf {op} ( x ) \rightarrow M \) for \(\mathsf {op}\) of signature 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 . 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 in the resumption type.

Finally, we show how the type system rejects the counterexample given in Sect. 2. The problem is in the following operation clause.where \(\mathsf {op}\) has effect signature . This clause is typechecked under resumption type for some \(\epsilon \). By , the two resumption expressions are assigned two different type variables \(\gamma _{{\mathrm {1}}}\) and \(\gamma _{{\mathrm {2}}}\), and the arguments \( \lambda \! \, z_{{\mathrm {1}}} . ( \mathsf {resume} \, \lambda \! \, z_{{\mathrm {2}}} . z_{{\mathrm {1}}} ) ; z_{{\mathrm {1}}} \) and \( \lambda \! \, z_{{\mathrm {2}}} . z_{{\mathrm {1}}} \) are required to have and , respectively. However, \( \lambda \! \, z_{{\mathrm {2}}} . z_{{\mathrm {1}}} \) cannot because \( z_{{\mathrm {1}}} \) is associated with \(\gamma _{{\mathrm {1}}}\) but not with \(\gamma _{{\mathrm {2}}}\).

Remark. The rule allows only the type of the argument to an operation clause to be renamed. Thus, other variables bound by, e.g., lambda abstractions and let-expressions outside the resumption expression cannot be used as such a type. As a result, more care may be required as to where to introduce a new variable. For example, let us consider the following operation clause (which is a variant of the example of \( \mathsf {choose}^{\forall } \) above).The variable \( x \) is assigned \( \alpha \times \alpha \) first and the resumption requires \( y \) to be typed at fresh type variable \(\beta \). This clause would be rejected in the current type system because \( \mathsf {fst} \, x \) appears outside \( \mathsf {resume} \) and, therefore, \( y \) is given type \(\alpha \), not \(\beta \). This inconvenience may be addressed by moving down the let-binding in some cases: e.g., \(\mathsf {resume} \, ( \mathsf {let} \, y = \mathsf {fst} \, x \, \mathsf {in} \, y )\) is well typed.

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 let-bound 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.

Evaluation contexts, denoted by \( E ^{ \varvec{ \alpha } } \), are standard for the lambda calculus with call-by-value, left-to-right evaluation except for two points. First, they contain the form \(\mathsf {let} \, x = \varLambda \! \, \varvec{ \alpha }. E ^{ \varvec{ \beta } } \, \mathsf {in} \, e_{{\mathrm {2}}} \), which allows the body of a type abstraction to be evaluated. Second, the metavariable \( E \) for evaluation contexts is indexed by type variables \( \varvec{ \alpha } \), meaning that the hole in the context appears under type abstractions binding \( \varvec{ \alpha } \). For example, \(\mathsf {let} \, x = \varLambda \! \, \alpha . \mathsf {let} \, y = \varLambda \! \, \beta . [\,] \, \mathsf {in} \, e_{{\mathrm {2}}} \, \mathsf {in} \, e_{{\mathrm {1}}} \) is denoted by \( E ^{\alpha ,\beta }\) and, more generally, is denoted by . (Here, stands for the concatenation of the two sequences and .) If \(\varvec{ \alpha } \) is not important, we simply write \( E \) for \( E ^{ \varvec{ \alpha } } \). We often use the term “continuation” to mean “evaluation context,” especially when it is expected to be resumed.

As usual, substitution of for in is defined in a capture-avoiding manner. Since variables come along with type arguments, the case for variables is defined as follows:Application of substitution to , where , is undefined. We define free type variables and and \( E \), respectively, as usual.

The semantics of \(\lambda _\text {eff}^{\varLambda }\) is given in the small-step style and consists of two relations: the reduction relation \( \rightsquigarrow \), which is for basic computation, and the evaluation relation \( \longrightarrow \), which is for top-level 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}}} ) \) , where function \( \zeta \) maps a pair of constants to another constant. A function application \(( \lambda \! \, x . e ) \, v \) and a let-expression \(\mathsf {let} \, x = \varLambda \! \, \varvec{ \alpha } . v \, \mathsf {in} \, e \) reduce to \( e [ v / x ] \) and \( e [ \varLambda \! \, \varvec{ \alpha } . v / x ] \) , 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 \) . An effect invocation \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v ) \) reduces to \( \texttt {\#} \mathsf {op} ( \varvec{ A } , v , [\,] ) \) with the identity continuation, as explained above ; the process of capturing its evaluation context is expressed by the rules , , , , and . The rule can be applied only if the handler \( h \) does not handle \(\mathsf {op}\). The rule is applied to a let-expression where appears under a type abstraction with bound type variables . Since and \( w \) may refer to , the reduction result binds in both and \( w \). We write for a sequence , ..., of type schemes (where ).

The crux of the semantics is : it is applied when reaches the handler \( h \) that handles \(\mathsf {op}\). Since the handled term is constructed from an effect invocation , if the captured continuation \( E \) binds type variables , the same type variables should have been added to and \( v \) along the capture. Thus, the handled expression on the left-hand side of the rule takes the form (with the same type variables ).

The right-hand side of involves three types of substitution: continuation substitution for resumptions, type substitution for , and value substitution for \( x \). We explain them one by one below. In the following, let and .

Continuation Substitution. Let us start with a simple case where the sequence is empty. Intuitively, continuation substitution replaces a resumption expression in the body \( e \) with \( E' [ v' ] \), where \( v' \) is the value of \( e' \), and substitutes and \( v \) (arguments to the invocation of \(\mathsf {op}\)) for and \( z \), respectively. Therefore, assuming \( \mathsf {resume} \) does not appear in \( e' \), we define to be (for fresh \( y \)). Note that the evaluation of \( e' \) takes place outside of \( E \) so that an invocation of an effect in \( e' \) is not handled by handlers in \( E \). When is not empty,

(The differences from the simple case are shaded.) The idea is to bind that appear free in and \( v \) by type abstraction at \( \mathsf {let} \) and to instantiate with the same variables at , where are bound by type abstractions in .

Continuation substitution is formally defined as follows:

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 and , respectively, in are for (type) parameters in . The basic idea is to substitute for and for —similarly to continuation substitution. We erase free type variables in and \( v \) by substituting the designated base type \( \bot \) for all of them. (We write and 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.

The type system of \(\lambda _\text {eff}^{\varLambda }\) is similar to that of \(\lambda _\text {eff}^\text {let}\) and has five judgments: well-formedness 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 . 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.

The typing rules for terms, shown in Fig. 5, and handlers, shown in the upper half of Fig. 6, are similar to those of \(\lambda _\text {eff}^\text {let}\) except for a new rule , which is applied to an effect invocation with a continuation. Let . Since \(\mathsf {op}\) should have been invoked with and \( v \) under type abstractions with bound type variables , the argument \( v \) has type under the typing context extended with . Similarly, the hole of expects to be filled with the result of the invocation, i.e., a value of . Since the continuation denotes the context before the evaluation, its result type matches with the type of the whole term.

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 , the continuation \(\mathsf {let} \, x = \varLambda \! \, \varvec{ \alpha } . E \, \mathsf {in} \, e \) has type because the hole of \( E \) appears inside the scope of \( \varvec{ \alpha } \).

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 \).

Elaboration is defined by two judgments: term elaboration judgment \( \varGamma ; R \vdash M : A \, | \, \epsilon \mathrel { \vartriangleright ^{ S } } e \), which denotes elaboration from a typing derivation of judgment \(\varGamma ; R \vdash M : A \, | \, \epsilon \) to \( e \) with \( S \), and handler elaboration judgment \( \varGamma ; R \vdash H : A \, | \, \epsilon \, \Rightarrow B \, | \, \epsilon ' \mathrel { \vartriangleright ^{ S } } h \), which denotes elaboration from a typing derivation of judgment \(\varGamma ; R \vdash H : A \, | \, \epsilon \Rightarrow B \, | \, \epsilon '\) to \( h \) with \( S \).

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 )\) and, every time a new variable is introduced, \( S \) is extended: see the rules other than and .

We show type safety of \(\lambda _\text {eff}^\text {let}\), i.e., a well-typed 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 well-typed 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.

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.

A key lemma to show subject reduction is type preservation of continuation substitution.

Using the continuation substitution lemma as well as other lemmas, we show subject reduction.

We write if and only if \( e \) cannot evaluate further. Moreover, \( \longrightarrow ^{*} \) denotes the reflexive and transitive closure of the evaluation relation \( \longrightarrow \).

Now, type safety of \(\lambda _\text {eff}^\text {let}\) is obtained as a corollary of Theorems 1 and 2.

Many researchers have attacked the problem of combining effects—not necessarily algebraic—and let-polymorphism so far [1, 2, 10, 12, 14, 17, 23, 24]. In particular, most of them have focused on ML-style polymorphic references. The algebraic effect handlers dealt with in this paper seem to be unable to implement general ML-style references—i.e., give an appropriate implementation to a set of effect operations new with the signature , get with , and put with 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.⁶ 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.

Value restriction [23, 24], a standard way adopted in ML-like languages, restricts polymorphic let-bound expressions to syntactic values. Garrigue [10] relaxes the value restriction so that, if a let-bound expression is not a syntactic value, type variables that appear only at positive positions in the type of the expression can be generalized. Although the (relaxed) value restriction is a quite clear criterion that indicates what let-bound expressions can be polymorphic safely and it even accepts interfering handlers, it is too restrictive in some cases. We give an example for such a case below.

In the definition of function f1, variable g is used polymorphically. Execution of this function under an appropriate handler would succeed, and in fact our calculus accepts it. By contrast, the (relaxed) value restriction rejects it because the let-bound expression is not a syntactic value and the type variable appear in both positive and negative positions, and so g is assigned a monomorphic type. A workaround for this problem is to make a function wrapper that calls either of fst or snd depending on the Boolean value chosen by :

However, this workaround makes the program complicated and incurs additional run-time cost for the branching and an extra call to the wrapper function.

Asai and Kameyama [2] study a combination of let-polymorphism with delimited control operators shift/reset [4]. They allow a let-bound expression to be polymorphic if it invokes no control operation. Thus, the function f1 above would be rejected in their approach.

Another research line to restrict the use of effects is to allow only type variables unrelated to effect invocations to be generalized. Tofte [23] distinguishes between applicative type variables, which cannot be used for effect invocations, and imperative ones, which can be used, and proposes a type system that enforces restrictions that (1) type variables of imperative operations can be instantiated only with types wherein all type variables are imperative and (2) if a let-bound expression is not a syntactic value, only applicative type variables can be generalized. Leroy and Weis [17] allow generalization only of type variables that do not appear in a parameter type to the reference type in the type of a let-expression. To detect the hidden use of references, their type system gives a term not only a type but also the types of free variables used in the term. Standard ML of New Jersey (before ML97) adopted weak polymorphism [1], which was later formalized and investigated deeply by Hoang et al. [12]. Weak polymorphism equips a type variable with the number of function calls after which a value of a type containing the type variable will be passed to an imperative operation. The type system ensures that type variables with positive numbers are not related to imperative constructs, and so such type variables can be generalized safely. In this line of research, the function f1 above would not typecheck because generalized type variables are used to instantiate those of the effect signature, although it could be rewritten to an acceptable one by taking care not to involve type variables in effect invocation.

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.

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 user-defined 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, let-bound 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 user-defined effects—delimited control shift0 [19] and monadic reflection [7, 8]—conjecturing that there would be no type-preserving 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.