Explicit Effect Subtyping
Abstract
As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an MLlike language with native support for handlers, has a subtypingbased effect system on which an effectaware optimizing compiler could be built. Unfortunately, in our experience, implementing optimizations for Eff is overly errorprone because its core language is implicitlytyped, making code transformations very fragile.
To remedy this, we present an explicitlytyped polymorphic core calculus for algebraic effect handlers with a subtypingbased typeandeffect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations.
Our typingdirected elaboration comes with a constraintbased inference algorithm that turns an implicitlytyped Efflike language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content.
1 Introduction
Algebraic effect handlers [17, 18] are quickly maturing from a theoretical model to a practical language feature for userdefined computational effects. Yet, in practice they still incur a significant performance overhead compared to native effects.
Our earlier efforts [22] to narrow this gap with an optimising compiler from Eff [2] to OCaml showed promising results, in some cases reaching even the performance of handtuned code, but were very fragile and have been postponed until a more robust solution is found. We believe the main reason behind this fragility is the complexity of subtyping in combination with the implicit typing of Eff’s core language, further aggravated by the “garbage collection” of subtyping constraints (see Sect. 7).^{1}

First, in Sect. 3 we present ImpEff, a polymorphic implicitlytyped calculus for algebraic effects and handlers with a subtypingbased typeandeffect system. ImpEff is essentially a (desugared) source language as it appears in the compiler frontend of a language like Eff.

Next, Sect. 4 presents ExEff, the core calculus, which combines explicit System Fstyle polymorphism with explicit coercions for subtyping in the style of BreazuTannen et al. [3]. This calculus comes with a typeandeffect system, a smallstep operational semantics and a proof of typesafety.

Section 5 specifies the typingdirected elaboration of ImpEff into ExEff and presents a type inference algorithm for ImpEff that produces the elaborated ExEff term as a byproduct. It also establishes that the elaboration preserves typing, and that the algorithm is sound with respect to the specification and yields principal types.

Finally, Sect. 6 defines SkelEff, which is a variant of ExEff without effect information or coercions. SkelEff is also representative of Multicore Ocaml’s support for algebraic effects and handlers [6], which is a possible compilation target of Eff. By showing that the erasure from ExEff to SkelEff preserves semantics, we establish that ExEff’s coercions are computationally irrelevant and that, despite the existence of multiple proofs for the same subtyping, there is no coherence problem. To enable erasure, ExEff annotates its types with (type) skeletons, which capture the erased counterpart and are, to our knowledge, a novel contribution.

Our paper comes with two software artefacts: an ongoing implementation^{2} of a compiler from Eff to OCaml with ExEff at its core, and an Abella mechanisation^{3} of Theorems 1, 2, 6, and 7. Remaining theorems all concern the inference algorithm, and their proofs closely follow [20].
The full version of this paper includes an appendix with omitted figures and can be found at http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW711.abs.html.
2 Overview
This section presents an informal overview of the ExEff calculus, and the main issues with elaborating to and erasing from it.
2.1 Algebraic Effect Handlers
The main premise of algebraic effects is that impure behaviour arises from a set of operations such as \(\mathtt {Get}\) and \(\mathtt {Set}\) for mutable store, \(\mathtt {Read}\) and \(\mathtt {Print}\) for interactive input and output, or \(\mathtt {Raise}\) for exceptions [17]. This allows generalizing exception handlers to other effects, to express backtracking, cooperative multithreading and other examples in a natural way [2, 18].
Assume operations \(\mathtt {Tick} : \mathtt {Unit}\rightarrow \mathtt {Unit}\) and \(\mathtt {Tock} : \mathtt {Unit}\rightarrow \mathtt {Unit}\) that take a unit value as a parameter and yield a unit value as a result. Unlike special builtin operations, these operations have no intrinsic effectful behaviour, though we can give one through handlers. For example, the handler Open image in new window replaces all calls of \(\mathtt {Tick}\) by printing out “tick” and similarly for \(\mathtt {Tock}\). But there is one significant difference between the two cases. Unlike exceptions, which always abort the evaluation, operations have a continuation waiting for their result. It is this continuation that the handler captures in the variable k and potentially uses in the handling clause. In the clause for \(\mathtt {Tick}\), the continuation is resumed by passing it the expected unit value, whereas in the clause for \(\mathtt {Tock}\), the operation is discarded. Thus, if we handle a computation emitting the two operations, it will print out “tick” until a first “tock” is printed, after which the evaluation stops.
2.2 Elaborating Subtyping
Consider the computation \(\mathtt {do}~{x} \leftarrow {\mathtt {Tick}~{\mathtt {unit}}} ;{f~x}\) and assume that f has the function type \(\mathtt {Unit}\rightarrow \mathtt {Unit}~!~\{\mathtt {Tock}\}\), taking unit values to unit values and perhaps calling \(\mathtt {Tock}\) operations in the process. The whole computation then has the type \(\mathtt {Unit}~!~\{\mathtt {Tick},\mathtt {Tock}\}\) as it returns the unit value and may call \(\mathtt {Tick}\) and \(\mathtt {Tock}\).
The above typing implicitly appeals to subtyping in several places. For instance, \(\mathtt {Tick}~{\mathtt {unit}}\) has type \(\mathtt {Unit}~!~\{\mathtt {Tick}\}\) and f x type \(\mathtt {Unit}~!~\{\mathtt {Tock}\}\). Yet, because they are sequenced with \(\mathtt {do}\), the type system expects they have the same set of effects. The discrepancies are implicitly reconciled by the subtyping which admits both \(\{\mathtt {Tick}\} \leqslant \{\mathtt {Tick},\mathtt {Tock}\}\) and \(\{\mathtt {Tock}\} \leqslant \{\mathtt {Tick},\mathtt {Tock}\}\).
2.3 Polymorphic Subtyping for Types and Effects
2.4 Guaranteed Erasure with Skeletons
One of our main requirements for ExEff is that its effect information and subtyping can be easily erased. The reason is twofold. Firstly, we want to show that neither plays a role in the runtime behaviour of ExEff programs. Secondly and more importantly, we want to use a conventionally typed (System Flike) functional language as a backend for the Eff compiler.
At first, erasure of both effect information and subtyping seems easy: simply drop that information from types and terms. But by dropping the effect variables and subtyping constraints from the type of \( f \), we get \(\forall \alpha , \alpha '. (\mathtt {Unit}\rightarrow \alpha ) \rightarrow \alpha '\) instead of the expected type \(\forall \alpha . (\mathtt {Unit}\rightarrow \alpha ) \rightarrow \alpha \). In our naive erasure attempt we have carelessly discarded the connection between \(\alpha \) and \(\alpha '\). A more appropriate approach to erasure would be to unify the types in dropped subtyping constraints. However, unifying types may reduce the number of type variables when they become instantiated, so corresponding binders need to be dropped, greatly complicating the erasure procedure and its metatheory.
3 The ImpEff Language
This section presents ImpEff, a basic functional calculus with support for algebraic effect handlers, which forms the core language of our optimising compiler. We describe the relevant concepts, but refer the reader to Pretnar’s tutorial [21], which explains essentially the same calculus in more detail.
3.1 Syntax
Figure 1 presents the syntax of the source language. There are two main kinds of terms: (pure) values v and (dirty) computations c, which may call effectful operations. Handlers h are a subsidiary sort of values. We assume a given set of operations \(\mathtt {Op}\), such as \(\mathtt {Get}\) and \(\mathtt {Put}\). We abbreviate \({{\mathtt {Op}_1}\,{x}\,{k}} \mapsto c_{\mathtt {Op}_1}, \ldots , {{\mathtt {Op}_n}\,{x}\,{k}} \mapsto c_{\mathtt {Op}_n}\) as \([{{\mathtt {Op}}\,{x}\,{k}} \mapsto c_\mathtt {Op}]_{\mathtt {Op}\in \mathcal {O}}\), and write \(\mathcal {O}\) to denote the set \(\{ \mathtt {Op}_1, \dots , \mathtt {Op}_n \}\).
3.2 Typing
Figure 2 presents the typing rules for values and computations, along with a typingdirected elaboration into our target language ExEff. In order to simplify the presentation, in this section we focus exclusively on typing. The parts of the rules that concern elaboration are highlighted in gray and are discussed in Sect. 5.
Values. Typing for values takes the form Open image in new window , and, given a typing environment \(\varGamma \), checks a value v against a value type A.
Rule TmVar handles term variables. Given that x has type \((\forall \overline{\varsigma }. \overline{\alpha :\tau }. \forall \overline{\delta }. \overline{\pi } \Rightarrow A )\), we appropriately instantiate the skeleton (\(\overline{\varsigma }\)), type (\(\overline{\alpha }\)), and dirt (\(\overline{\delta }\)) variables, and ensure that the instantiated wanted constraints \(\overline{\sigma (\pi )}\) are satisfied, via side condition Open image in new window . Rule TmCastV allows casting the type of a value v from \( A \) to \( B \), if \( A \) is a subtype of \( B \) (upcasting). As illustrated by Rule TmTmAbs, we omit freshness conditions by adopting the Barendregt convention [1]. Finally, Rule TmHand gives typing for handlers. It requires that the righthand sides of the return clause and all operation clauses have the same computation type (\( B \,!\,\varDelta \)), and that all operations mentioned are part of the toplevel signature \(\varSigma \).^{4} The result type takes the form \( A ~!~\varDelta \,\cup \,\mathcal {O}\Rrightarrow B ~!~\varDelta \), capturing the intended handler semantics: given a computation of type \( A ~!~\varDelta \cup \mathcal {O}\), the handler (a) produces a result of type \( B \), (b) handles operations \(\mathcal {O}\), and (c) propagates unhandled operations \(\varDelta \) to the output.
Computations. Typing for computations takes the form Open image in new window , and, given a typing environment \(\varGamma \), checks a computation c against a type \(\underline{C}\).
Constraint Entailment. The specification of constraint entailment takes the form Open image in new window and is presented in Fig. 3. Notice that we use \(\rho \) instead of \(\pi \), which allows us to capture subtyping between two value types, computation types or dirts, within the same relation. Subtyping can be established in several ways:
Rule CoVar handles given assumptions. Rules VCoRefl and DCoRefl express that subtyping is reflexive, for both value types and dirts. Notice that we do not have a rule for the reflexivity of computation types since, as we illustrate below, it can be established using the reflexivity of their subparts. Rules VCoTrans, CCoTrans and DCoTrans express the transitivity of subtyping for value types, computation types and dirts, respectively. Rule VCoArr establishes inequality of arrow types. As usual, the arrow type constructor is contravariant in the argument type. Rules VCoArrL and CCoArrR are the inversions of Rule VCoArr, allowing us to establish the relation between the subparts of the arrow types. Rules VCoHand, CCoHL, and CCoHR work similarly, for handler types. Rule CCoComp captures the covariance of type constructor (!), establishing subtyping between two computation types if subtyping is established for their respective subparts. Rules VCoPure and DCoImpure are its inversions. Finally, Rules DCoNil and DCoOp establish subtyping between dirts. Rule DCoNil captures that the empty dirty set \(\emptyset \) is a subdirt of any dirt \(\varDelta \) and Rule DCoOp expresses that dirt subtyping preserved under extension with the same operation \(\mathtt {Op}\).
WellFormedness of Types, Constraints, Dirts, and Skeletons. The relations Open image in new window and Open image in new window check the wellformedness of value and computation types respectively. Similarly, relations Open image in new window and Open image in new window check the wellformedness of constraints and dirts, respectively.
4 The ExEff Language
4.1 Syntax
Figure 4 presents ExEff’s syntax. ExEff is an intensional type theory akin to System F [7], where every term encodes its own typing derivation. In essence, all abstractions and applications that are implicit in ImpEff, are made explicit in ExEff via new syntactic forms. Additionally, ExEff is impredicative, which is reflected in the lack of discrimination between value types, qualified types and type schemes; all noncomputation types are denoted by \( T \). While the impredicativity is not strictly required for the purpose at hand, it makes for a cleaner system.
Coercions. Of particular interest is the use of explicit subtyping coercions, denoted by \(\gamma \). ExEff uses these to replace the implicit casts of ImpEff (Rules TmCastV and TmCastC in Fig. 2) with explicit casts \(({v} \vartriangleright {\gamma })\) and \(({c} \vartriangleright {\gamma })\).
Essentially, coercions \(\gamma \) are explicit witnesses of subtyping derivations: each coercion form corresponds to a subtyping rule. Subtyping forms a partial order, which is reflected in coercion forms \({\gamma _1} \gg {\gamma _2}\), \(\langle { T } \rangle \), and \(\langle {\varDelta } \rangle \). Coercion form \({\gamma _1} \gg {\gamma _2}\) captures transitivity, while forms \(\langle { T } \rangle \) and \(\langle {\varDelta } \rangle \) capture reflexivity for value types and dirts (reflexivity for computation types can be derived from these).
Subtyping for skeleton abstraction, type abstraction, dirt abstraction, and qualification is witnessed by forms \(\forall \varsigma . \gamma \), \(\forall \alpha . \gamma \), \(\forall \delta . \gamma \), and \(\pi \Rightarrow \gamma \), respectively. Similarly, forms \({\gamma }[{\tau }]\), \({\gamma }[{ T }]\), \({\gamma }[{\varDelta }]\), and \({\gamma _1}@{\gamma _2}\) witness subtyping of skeleton instantiation, type instantiation, dirt instantiation, and coercion application, respectively.
Syntactic forms \(\gamma _1 \rightarrow \gamma _2\) and \(\gamma _1 \Rrightarrow \gamma _2\) capture injection for the arrow and the handler type constructor, respectively. Similarly, inversion forms \(\textit{left}({\gamma })\) and \(\textit{right}({\gamma })\) capture projection, following from the injectivity of both type constructors.
Coercion form \(\gamma _1~!~\gamma _2\) witnesses subtyping for computation types, using proofs for their components. Inversely, syntactic forms \(\textit{pure}({\gamma })\) and \(\textit{impure}({\gamma })\) witness subtyping between the value and dirtcomponents of a computation coercion.
4.2 Typing
WellFormedness of Types, Constraints, Dirts and Skeletons. The definitions of the judgements that check the wellformedness of ExEff value types (\({\varGamma } \vdash _{{\scriptscriptstyle \mathtt { T }}} { T } : {\tau }\)), computation types (\({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {\underline{ C }}}} {\underline{ C }} : {\tau }\)), dirts ( Open image in new window ), and skeletons (\({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {\tau }}} {\tau }\)) are equally straightforward as those for ImpEff.
Coercion Typing. Coercion typing formalizes the intuitive interpretation of coercions we gave in Sect. 4.1 and takes the form \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {co}}} {\gamma } : {\rho }\). It is essentially an extension of the constraint entailment relation of Fig. 3.
4.3 Operational Semantics
Figure 7 presents selected rules of ExEff’s smallstep, callbyvalue operational semantics. For lack of space, we omit \(\beta \)rules and other common rules and focus only on cases of interest.
Although unusual, this stratification can also be found in Crary’s coercion calculus for inclusive subtyping [4], and, more recently, in System F\(_\text {C}\) [25]. Stratification is crucial for ensuring type preservation. Consider for example the expression \(({\mathtt {return}~{5}} \vartriangleright {\langle {\mathtt {int}} \rangle \,!\,\emptyset _{\{\mathtt {Op}\}}})\), of type \(\mathtt {int}\,!\,\{\mathtt {Op}\}\). We can not reduce the expression further without losing effect information; removing the cast would result in computation \((\mathtt {return}~{5})\), of type \(\mathtt {int}\,!\,\emptyset \). Even if we consider type preservation only up to subtyping, the redex may still occur as a subterm in a context that expects solely the larger type.
Secondly, we need to make sure that casts do not stand in the way of evaluation. This is captured in the socalled “push” rules, all of which appear in Fig. 7.
In relation \({v} \leadsto _\mathrm {v}^{} {v'}\), the first rule groups nested casts into a single cast, by means of transitivity. The next three rules capture the essence of push rules: whenever a redex is “blocked” due to a cast, we take the coercion apart and redistribute it (in a typepreserving manner) over the subterms, so that evaluation can progress.
The last four rules are concerned with effect handling. The first of them pushes a coercion on the handler “outwards”, such that the handler can be exposed and evaluation is not stuck (similarly to the push rule for term application). The second rule behaves similarly to the push/beta rule for sequencing computations. Finally, the last two rules are concerned with handling of operations. The first of the two captures cases where the called operation is handled by the handler, in which case the respective clause of the handler is called. As illustrated by the rule, like Pretnar [20], ExEff features deep handlers: the continuation is also wrapped within a \(\mathtt {with}\)\(\mathtt {handle}\) construct. The last rule captures cases where the operation is not covered by the handler and thus remains unhandled.
We have shown that ExEff is type safe:
Theorem 1

If \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {v}}} {v} : { T }\) then either v is a result value or \({v} \leadsto _\mathrm {v}^{} {v'}\) and \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {v}}} {v'} : { T }\).

If \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {c}}} {c} : {\underline{ C }}\) then either c is a result computation or \({c} \leadsto _\mathrm {c}^{} {c'}\) and \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {c}}} {c'} : {\underline{ C }}\).
5 Type Inference and Elaboration
This section presents the typingdirected elaboration of ImpEff into ExEff. This elaboration makes all the implicit type and effect information explicit, and introduces explicit termlevel coercions to witness the use of subtyping.
After covering the declarative specification of this elaboration, we present a constraintbased algorithm to infer ImpEff types and at the same time elaborate into ExEff. This algorithm alternates between two phases: (1) the syntaxdirected generation of constraints from the ImpEff term, and (2) solving these constraints.
5.1 Elaboration of ImpEff into ExEff
The grayed parts of Fig. 2 augment the typing rules for ImpEff value and computation terms with typingdirected elaboration to corresponding ExEff terms. The elaboration is mostly straightforward, mapping every ImpEff construct onto its corresponding ExEff construct while adding explicit type annotations to binders in Rules TmTmAbs, TmHandler and TmOp. Implicit appeals to subtyping are turned into explicit casts with coercions in Rules TmCastV and TmCastC. Rule TmLet introduces explicit binders for skeleton, type, and dirt variables, as well as for constraints. These last also introduce coercion variables \(\omega \) that can be used in casts. The binders are eliminated in rule TmVar by means of explicit application with skeletons, types, dirts and coercions. The coercions are produced by the auxiliary judgement Open image in new window , defined in Fig. 3, which provides a coercion witness for every subtyping proof.
As a sanity check, we have shown that elaboration preserves types.
Theorem 2

If Open image in new window then \({ elab _{\scriptscriptstyle \varGamma }({\varGamma })} \vdash _{{\scriptscriptstyle \mathtt {v}}} {v'} : { elab _{\scriptscriptstyle S }({ A })}\).

If Open image in new window then \({ elab _{\scriptscriptstyle \varGamma }({\varGamma })} \vdash _{{\scriptscriptstyle \mathtt {c}}} {c'} : { elab _{\scriptscriptstyle \underline{ C }}({\underline{ C }})}\).
Here \( elab _{\scriptscriptstyle \varGamma }({\varGamma })\), \( elab _{\scriptscriptstyle S }({ A })\) and \( elab _{\scriptscriptstyle \underline{ C }}({\underline{ C }})\) convert ImpEff environments and types into ExEff environments and types.
5.2 Constraint Generation and Elaboration
A substitution \(\sigma \) is a solution of the set \(\mathcal {P}\), written as \(\sigma \,\models \,\mathcal {P}\), if we get derivable judgements after applying \(\sigma \) to all constraints in \(\mathcal {P}\).
Values. Constraint generation for values takes the form Open image in new window . It takes as inputs a set of wanted constraints \(\mathcal {Q}\), a typing environment \(\varGamma \), and a ImpEff value v, and produces a value type \( A \), a new set of wanted constraints \(\mathcal {Q}'\), a substitution \(\sigma \), and a ExEff value \(v'\).
Unlike standard HM, our inference algorithm does not keep constraint generation and solving separate. Instead, the two are interleaved, as indicated by the additional arguments of our relation: (a) constraints \(\mathcal {Q}\) are passed around in a stateful manner (i.e., they are input and output), and (b) substitutions \(\sigma \) generated from constraint solving constitute part of the relation output. We discuss the reason for this interleaved approach in Sect. 5.4; we now focus on the algorithm.
The rules are syntaxdirected on the input ImpEff value. The first rule handles term variables x: as usual for constraintbased type inference the rule instantiates the polymorphic type \((\forall \bar{\varsigma }. \overline{\alpha :\tau }. \forall \bar{\delta }. \bar{\pi } \Rightarrow A )\) of x with fresh variables; these are placeholders that are determined during constraint solving. Moreover, the rule extends the wanted constraints \(\mathcal {P}\) with \(\bar{\pi }\), appropriately instantiated. In ExEff, this corresponds to explicit skeleton, type, dirt, and coercion applications.
More interesting is the third rule, for term abstractions. Like in standard HindleyDamasMilner [5], it generates a fresh type variable \(\alpha \) for the type of the abstracted term variable x. In addition, it generates a fresh skeleton variable \(\varsigma \), to capture the (yet unknown) shape of \(\alpha \).
As explained in detail in Sect. 5.3, the constraint solver instantiates type variables only through their skeletons annotations. Because we want to allow local constraint solving for the body c of the term abstraction the opportunity to produce a substitution \(\sigma \) that instantiates \(\alpha \), we have to pass in the annotation constraint \(\alpha : \varsigma \).^{6} We apply the resulting substitution \(\sigma \) to the result type \(\sigma (\alpha ) \rightarrow \underline{ C }\).^{7}
Finally, the fourth rule is concerned with handlers. Since it is the most complex of the rules, we discuss each of its premises separately:
Firstly, we infer a type \( B _r\,!\,\varDelta _r\) for the right hand side of the \(\mathtt {return}\)clause. Since \(\alpha _r\) is a fresh unification variable, just like for term abstraction we require \(\alpha _r : \varsigma _r\), for a fresh skeleton variable \(\varsigma _r\).
Secondly, we check every operation clause in \(\mathcal {O}\) in order. For each clause, we generate fresh skeleton, type, and dirt variables (\(\varsigma _i\), \(\alpha _i\), and \(\delta _i\)), to account for the (yet unknown) result type \(\alpha _i\,!\,\delta _i\) of the continuation k, while inferring type \( B _{\mathtt {Op}_i}\,!\,\varDelta _{\mathtt {Op}_i}\) for the righthandside \(c_{\mathtt {Op}_i}\).
Computations. The judgement Open image in new window generates constraints for computations.
The first rule handles term applications of the form \(v_1\,v_2\). After inferring a type for each subterm (\( A _1\) for \(v_1\) and \( A _2\) for \(v_2\)), we generate the wanted constraint \(\sigma _2( A _1) \leqslant A _2 \rightarrow \alpha \,!\,\delta \), with fresh type and dirt variables \(\alpha \) and \(\delta \), respectively. Associated coercion variable \(\omega \) is then used in the elaborated term to explicitly (up)cast \(v_1'\) to the expected type \( A _2 \rightarrow \alpha \,!\,\delta \).
The third rule handles polymorphic letbindings. First, we infer a type \( A \) for v, as well as wanted constraints \(\mathcal {Q}_v\). Then, we simplify wanted constraints \(\mathcal {Q}_v\) by means of function \(\mathtt {solve}\) (which we explain in detail in Sect. 5.3 below), obtaining a substitution \(\sigma _1'\) and a set of residual constraints \(\mathcal {Q}_v'\).
The fourth rule handles operation calls. Observe that in the elaborated term, we upcast the inferred type to match the expected type in the signature.
The fifth rule handles sequences. The requirement that all computations in a \(\mathtt {do}\)construct have the same dirt set is expressed in the wanted constraints \(\sigma _2(\varDelta _1) \leqslant \delta \) and \(\varDelta _2 \leqslant \delta \) (where \(\delta \) is a fresh dirt variable; the resulting dirt set), witnessed by coercion variables \(\omega _1\) and \(\omega _2\). Both coercion variables are used in the elaborated term to upcast \(c_1\) and \(c_2\), such that both draw effects from the same dirt set \(\delta \).
Finally, the sixth rule is concerned with effect handling. After inferring type \( A _1\) for the handler v, we require that it takes the form of a handler type, witnessed by coercion variable \(\omega _1 : \sigma _2( A _1) \leqslant (\alpha _1\,!\,\delta _1 \Rrightarrow \alpha _2\,!\,\delta _2)\), for fresh \(\alpha _1, \alpha _2, \delta _1, \delta _2\). To ensure that the type \( A _2\,!\,\varDelta _2\) of c matches the expected type, we require that \( A _2\,!\,\varDelta _2 \leqslant \alpha _1\,!\,\delta _1\). Our syntax does not include coercion variables for computation subtyping; we achieve the same effect by combining \(\omega _2 : A _2 \leqslant \alpha _1\) and \(\omega _3 : \varDelta _2 \leqslant \delta _1\).
Theorem 3
(Soundness of Inference). If Open image in new window then for any \(\sigma '\,\models \,\mathcal {Q}\), we have Open image in new window , and analogously for computations.
Theorem 4
(Completeness of Inference). If Open image in new window then we have Open image in new window and there exists \(\sigma '\,\models \,\mathcal {Q}\) and \(\gamma \), such that \(\sigma '(v'') = v'\) and Open image in new window . An analogous statement holds for computations.
5.3 Constraint Solving
Theorem 5
(Correctness of Solving). For any set \(\mathcal {Q}\), the call \(\mathtt {solve}(\bullet ; \bullet ; \mathcal {Q})\) either results in a failure, in which case \(\mathcal {Q}\) has no solutions, or returns \((\sigma , \mathcal {P})\) such that for any \(\sigma '\,\models \,\mathcal {Q}\), there exists \(\sigma ''\,\models \,\mathcal {P}\) such that \(\sigma ' = \sigma '' \cdot \sigma \).
The solver is invoked with \(\mathtt {solve}(\bullet ;\, \bullet ;\, \mathcal {Q})\), to process the constraints \(\mathcal {Q}\) generated in the first phase of the algorithm, i.e., with an empty substitution and no processed constraints. The \(\mathtt {solve}\) function is defined by case analysis on the queue.
The first case applies when both skeletons are the same type variable \(\varsigma \). Then the equality trivially holds. Hence we drop it and proceed with solving the remaining constraints. The next two cases apply when either \(\tau _1\) or \(\tau _2\) is a skeleton variable \(\varsigma \). If the occurs check fails, there is no finite solution and the algorithm signals failure. Otherwise, the constraint is solved by instantiating the \(\varsigma \). This additional substitution is accumulated and applied to all other constraints \(\mathcal {P},\mathcal {Q}\). Because the substitution might have modified some of the already processed constraints \(\mathcal {P}\), we have to revisit them. Hence, they are all pushed back onto the queue, which is processed recursively.
The next three cases consider three different ways in which the two skeletons can have the same instantiated toplevel structure. In those cases the equality is decomposed into equalities on the subterms, which are pushed onto the queue and processed recursively.
The last catchall case deals with all ways in which the two skeletons can be instantiated to different structures. Then there is no solution.
Auxiliary function \( skeleton ({ A })\) computes the skeleton of \( A \).
The second case, \(\emptyset \leqslant \varDelta '\), always holds and is discharged by instantiating \(\omega \) to \(\emptyset _{\varDelta '}\). The third case, \(\delta \leqslant \emptyset \), has only one solution: \(\delta \mapsto \emptyset \) with coercion \(\emptyset _\emptyset \). The fourth case, \(\mathcal {O}\cup \delta \leqslant \mathcal {O}'\), has as many solutions as there are subsets of \(\mathcal {O}'\), provided that \(\mathcal {O}\subseteq \mathcal {O}'\). We then simplify the constraint to \(\delta \leqslant \mathcal {O}'\), which we move to the set of processed constraints. The fifth case, \(\mathcal {O}\leqslant \mathcal {O}'\), holds iff \(\mathcal {O}\subseteq \mathcal {O}'\). The last case, \(\mathcal {O}\leqslant \mathcal {O}' \cup \delta '\), is like the first, but without a dirt variable in the lefthand side. We can satisfy it in a similar fashion, by partially instantiating \(\delta '\) with \((\mathcal {O}\setminus \mathcal {O}') \cup \delta ''\)—where \(\delta ''\) is a fresh dirt variable. Now the constraint is satisfied and can be discarded.
5.4 Discussion
At first glance, the constraint generation algorithm of Sect. 5.2 might seem needlessly complex, due to eager constraint solving for letgeneralization. Yet, we want to generalize at local \(\mathtt {let}\)bound values over both type and skeleton variables,^{9} which means that we must solve all equations between skeletons before generalizing. In turn, since skeleton constraints are generated when solving subtyping constraints (Sect. 5.3), all skeleton annotations should be available during constraint solving. This can not be achieved unless the generated constraints are propagated statefully.
6 Erasure of Effect Information from ExEff
6.1 The SkelEff Language
Discussion. The main point of SkelEff is to show that we can erase the effects and subtyping from ExEff to obtain types that are compatible with a System Flike language. At the termlevel SkelEff also resembles a subset of Multicore OCaml [6], which provides native support for algebraic effects and handlers but features no explicit polymorphism. Moreover, SkelEff can also serve as a staging area for further elaboration into System Flike languages without support for algebraic effects and handlers (e.g., Haskell or regular OCaml). In those cases, computation terms can be compiled to one of the known encodings in the literature, such as a free monad representation [10, 22], with delimited control [11], or using continuationpassing style [13], while values can typically be carried over as they are.
6.2 Erasure
Figure 11 defines erasure functions \(\epsilon ^{\sigma }_{\mathrm {v}}(v)\), \(\epsilon ^{\sigma }_{\mathrm {c}}(c)\), \(\epsilon ^{\sigma }_{\mathrm {V}}( T )\), \(\epsilon ^{\sigma }_{\mathrm {C}}(\underline{ C })\) and \(\epsilon ^{\sigma }_{\mathrm {E}}(\varGamma )\) for values, computations, value types, computation types, and type environments respectively. All five functions take a substitution \(\sigma \) from the free type variables \(\alpha \) to their skeleton \(\tau \) as an additional parameter.
Thanks to the skeletonbased design of ExEff, erasure is straightforward. All types are erased to their skeletons, dropping quantifiers for type variables and all occurrences of dirt sets. Moreover, coercions are dropped from values and computations. Finally, all binders and elimination forms for type variables, dirt set variables and coercions are dropped from values and type environments.
The expected theorems hold. Firstly, types are preserved by erasure.^{10}
Theorem 6
(Type Preservation). If \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {v}}} {v} : { T }\) then \({\epsilon ^{\emptyset }_{\mathrm {E}}(\varGamma )} \vdash _{{\scriptscriptstyle \mathtt {ev}}} {\epsilon ^{\varGamma }_{\mathrm {v}}(v)} : {\epsilon ^{\varGamma }_{\mathrm {V}}( T )}\). If \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {c}}} {c} : {\underline{ C }}\) then \({\epsilon ^{\emptyset }_{\mathrm {E}}(\varGamma )} \vdash _{{\scriptscriptstyle \mathtt {ec}}} {\epsilon ^{\varGamma }_{\mathrm {c}}(c)} : {\epsilon ^{\varGamma }_{\mathrm {C}}(\underline{ C })}\).
Here we abuse of notation and use \(\varGamma \) as a substitution from type variables to skeletons used by the erasure functions.
Finally, we have that erasure preserves the operational semantics.
Theorem 7
(Semantic Preservation). If \({v} \leadsto _\mathrm {v}^{} {v'}\) then \({\epsilon ^{\sigma }_{\mathrm {v}}(v)} \equiv ^{\leadsto }_\mathrm {v} {\epsilon ^{\sigma }_{\mathrm {v}}(v')}\). If \({c} \leadsto _\mathrm {c}^{} {c'}\) then \({\epsilon ^{\sigma }_{\mathrm {c}}(c)} \equiv ^{\leadsto }_\mathrm {c} {\epsilon ^{\sigma }_{\mathrm {c}}(c')}\).
In both cases, \(\equiv ^{\leadsto }\) denotes the congruence closure of the step relation in SkelEff. The choice of substitution \(\sigma \) does not matter as types do not affect the behaviour.
7 Related Work and Conclusion
Eff’s Implicit Type System. The most closely related work is that of Pretnar [20] on inferring algebraic effects for Eff, which is the basis for our implicitlytyped ImpEff calculus, its type system and the type inference algorithm. There are three major differences with Pretnar’s inference algorithm.
Firstly, our work introduces an explicitlytyped calculus. For this reason we have extended the constraint generation phase with the elaboration into ExEff and the constraint solving phase with the construction of coercions.
Secondly, we add skeletons to guarantee erasure. Skeletons also allow us to use standard occurscheck during unification. In contrast, unification in Pretnar’s algorithm is inspired by Simonet [24] and performs the occurscheck up to the equivalence closure of the subtyping relation. In order to maintain invariants, all variables in an equivalence class (also called a skeleton) must be instantiated simultaneously, whereas we can process one constraint at a time. As these classes turn out to be surrogates for the underlying skeleton types, we have decided to keep the name.
Finally, Pretnar incorporates garbage collection of constraints [19]. The aim of this approach is to obtain unique and simple type schemes by eliminating redundant constraints. Garbage collection is not suitable for our use as type variables and coercions witnessing subtyping constraints cannot simply be dropped, but must be instantiated in a suitable manner, which cannot be done in general.
Consider for instance a situation with type variables \(\alpha _1\), \(\alpha _2\), \(\alpha _3\), \(\alpha _4\), and \(\alpha _5\) where \(\alpha _1 \leqslant \alpha _3\), \(\alpha _2 \leqslant \alpha _3\), \(\alpha _3 \leqslant \alpha _4\), and \(\alpha _3 \leqslant \alpha _5\). Suppose that \(\alpha _3\) does not appear in the type. Then garbage collection would eliminate it and replace the constraints by \(\alpha _1 \leqslant \alpha _4\), \(\alpha _2 \leqslant \alpha _4\), \(\alpha _1 \leqslant \alpha _5\), and \(\alpha _2 \leqslant \alpha _5\). While garbage collection guarantees that for any ground instantiation of the remaining type variables, there exists a valid ground instantiation for \(\alpha _3\), ExEff would need to be extended with joins (or meets) to express a generically valid instantiation like \(\alpha _1 \sqcup \alpha _2\). Moreover, we would need additional coercion formers to establish \(\alpha _1 \leqslant (\alpha _1 \sqcup \alpha _2)\) or \((\alpha _1 \sqcup \alpha _2) \leqslant \alpha _4\).
As these additional constructs considerably complicate the calculus, we propose a simpler solution. We use ExEff as it is for internal purposes, but display types to programmers in their garbagecollected form.
Calculi with Explicit Coercions. The notion of explicit coercions is not new; Mitchell [15] introduced the idea of inserting coercions during type inference for MLbased languages, as a means for explicit casting between different numeric types.
BreazuTannen et al. [3] also present a translation of languages with inheritance polymorphism into System F, extended with coercions. Although their coercion combinators are very similar to our coercion forms, they do not include inversion forms, which are crucial for the proof of type safety for our system. Moreover, BreazuTannen et al.’s coercions are terms, and thus can not be erased.
Much closer to ExEff is Crary’s coercion calculus for inclusive subtyping [4], from which we borrowed the stratification of value results. Crary’s system supports neither coercion abstraction nor coercion inversion forms.
System F\(_\text {C}\) [25] uses explicit typeequality coercions to encode complex language features (e.g. GADTs [16] or type families [23]). Though ExEff’s coercions are proofs of subtyping rather than type equality, our system has a lot in common with it, including the inversion coercion forms and the “push” rules.
Future Work. Our plans focus on resuming the postponed work on efficient compilation of handlers. First, we intend to adjust program transformations to the explicit type information. We hope that this will not only make the optimizer more robust, but also expose new optimization opportunities. Next, we plan to write compilers to both Multicore OCaml and standard OCaml, though for the latter, we must first adapt the notion of erasure to a target calculus without algebraic effect handlers. Finally, once the compiler shows promising preliminary results, we plan to extend it to other Eff features such as userdefined types or recursion, allowing us to benchmark it on more realistic programs.
Footnotes
 1.
For other issues stemming from the same combination see issues #11 and #16 at https://github.com/matijapretnar/eff/issues/.
 2.
 3.
 4.
We capture all defined operations along with their types in a global signature \(\varSigma \).
 5.
Observe that operation values do not feature an outermost cast operation, as the coercion can always be pushed into its continuation.
 6.
This hints at why we need to pass constraints in a stateful manner.
 7.
Though \(\sigma \) refers to ImpEff types, we abuse notation to save clutter and apply it directly to ExEff entities too.
 8.
We implicitly annotate every type variable with its skeleton: \(\alpha ^{\tau }\).
 9.
As will become apparent in Sect. 6, if we only generalize at the top over skeleton variables, the erasure does not yield local polymorphism.
 10.
Typing for SkelEff values and computations take the form \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {ev}}} {v} : {\tau }\) and \({\varGamma } \vdash _{{\scriptscriptstyle \mathtt {ec}}} {c} : {\tau }\).
Notes
Acknowledgements
We would like to thank the anonymous reviewers for careful reading and insightful comments. Part of this work is funded by the Flemish Fund for Scientific Research (FWO). This material is based upon work supported by the Air Force Office of Scientific Research under award number FA95501710326.
References
 1.Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 3. NorthHolland, Amsterdam (1981)zbMATHGoogle Scholar
 2.Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Logic Algebraic Program. 84(1), 108–123 (2015)MathSciNetCrossRefGoogle Scholar
 3.BreazuTannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as implicit coercion. Inf. Comput. 93, 172–221 (1991)MathSciNetCrossRefGoogle Scholar
 4.Crary, K.: Typed compilation of inclusive subtyping. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, pp, 68–81. ACM, New York (2000)Google Scholar
 5.Damas, L., Milner, R.: Principal typeschemes for functional programs. In: Proceedings of the 9th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 1982, pp. 207–212. ACM, New York (1982)Google Scholar
 6.Dolan, S., White, L., Sivaramakrishnan, K., Yallop, J., Madhavapeddy, A.: Effective concurrency through algebraic effects. In: OCaml Workshop (2015)Google Scholar
 7.Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)zbMATHGoogle Scholar
 8.Hillerström, D., Lindley, S.: Liberating effects with rows and handlers. In: Chapman, J., Swierstra, W. (eds.) Proceedings of the 1st International Workshop on TypeDriven Development, TyDe@ICFP 2016, Nara, Japan, 18 September 2016, pp. 15–27. ACM (2016)Google Scholar
 9.Jones, M.P.: A theory of qualified types. In: KriegBrückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 287–306. Springer, Heidelberg (1992). https://doi.org/10.1007/3540552537_17CrossRefGoogle Scholar
 10.Kammar, O., Lindley, S., Oury, N.: Handlers in action. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming, ICFP 2014, pp. 145–158. ACM (2013)Google Scholar
 11.Kiselyov, O., Sivaramakrishnan, K.: Eff directly in OCaml. In: OCaml Workshop (2016)Google Scholar
 12.Leijen, D.: Koka: programming with row polymorphic effect types. In: Levy, P., Krishnaswami, N. (eds.) Proceedings of 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014. EPTCS, vol. 153, pp. 100–126 (2014)MathSciNetCrossRefGoogle Scholar
 13.Leijen, D.: Type directed compilation of rowtyped algebraic effects. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 486–499. ACM (2017)Google Scholar
 14.Lindley, S., McBride, C., McLaughlin, C.: Do be do be do. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 500–514. ACM (2017). http://dl.acm.org/citation.cfm?id=3009897
 15.Mitchell, J.C.: Coercion and type inference. In: Proceedings of the 11th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, POPL 1984, pp. 175–185. ACM, New York (1984)Google Scholar
 16.Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unificationbased type inference for GADTs. In: ICFP 2006 (2006)CrossRefGoogle Scholar
 17.Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categ. Struct. 11(1), 69–94 (2003)MathSciNetCrossRefGoogle Scholar
 18.Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Log. Methods Comput. Sci. 9(4) (2013)Google Scholar
 19.Pottier, F.: Simplifying subtyping constraints: a theory. Inf. Comput. 170(2), 153–183 (2001). https://doi.org/10.1006/inco.2001.2963MathSciNetCrossRefzbMATHGoogle Scholar
 20.Pretnar, M.: Inferring algebraic effects. Log. Methods Comput. Sci. 10(3) (2014)Google Scholar
 21.Pretnar, M.: An introduction to algebraic effects and handlers, invited tutorial. Electron. Notes Theoret. Comput. Sci. 319, 19–35 (2015)MathSciNetCrossRefGoogle Scholar
 22.Pretnar, M., Saleh, A.H., Faes, A., Schrijvers, T.: Efficient compilation of algebraic effects and handlers. Technical report CW 708, KU Leuven Department of Computer Science (2017)Google Scholar
 23.Schrijvers, T., Peyton Jones, S., Chakravarty, M., Sulzmann, M.: Type checking with open type functions. In: ICFP 2008, pp. 51–62. ACM (2008)CrossRefGoogle Scholar
 24.Simonet, V.: Type inference with structural subtyping: a faithful formalization of an efficient constraint solver. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 283–302. Springer, Heidelberg (2003). https://doi.org/10.1007/9783540400189_19CrossRefGoogle Scholar
 25.Sulzmann, M., Chakravarty, M.M.T., Peyton Jones, S., Donnelly, K.: System F with type equality coercions. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI 2007, pp. 53–66. ACM, New York (2007)Google Scholar
 26.Wansbrough, K., Peyton Jones, S.L.: Once upon a polymorphic type. In: POPL, pp. 15–28. ACM (1999)Google Scholar
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 book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book'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.