This looks fascinating! Is it straightforward to explain why Eff could not simply be implemented within the syntax of an existing language, say Haskell or ML?

Well, ML has handlers just for exceptions and those cannot be used to get general handlers. I suppose you could emulate eff in ML with delimited continuations, but I think you would end up with a "deep" embedding of eff.

People have tried to get something in Haskell, e.g., effects on Hackage. Judge for yourself.

I fail to understand why ressources have a different syntax than regular handler. Intuitively I would have thought they were just "handlers declared at toplevel for your convenience", but it seems like I missed something here.

Resources do not have access to the continuation, while ordinary handlers do.

It makes little sense for a "top-level handler" to be able to manipulate the continuation, since the continuation is open-ended in nature, i.e., it is not delimited. But this is not why we defined resources. We defined resources as a direct implementation of the theoretical idea of co-models.

Well, you could have continuation that map to the empty type as toplevel continuations, but it still makes sense to consider these not too valuable.

On the other hand, I don't see how comodels play in that picture. Am I missing something obvious?

A top-level continuation that maps to the empty type? Where would that come from? Or are you suggesting that there be a top-level "abort" operation (although that is an operation whose return type is empty). I'll let Matija explain the comodels.

This is what I had in mind yes.

I have advocated a top-level abort operation, but was unable to convince Matija. So far.

For comodels, observe the "real-world" effectful behaviour of operations: 1. write takes a string, writes it out, and yields a unit value, 2. read takes a unit value, reads a string, and yields it, 3. random_int (say) takes integer bounds, generates a random integer according to the state of the pseudo-random generator, sets the new state, and yields the generated integer. In general, an operation $op : A \to B$ takes a parameter of type $A$, interacts with the "real-world", and yields a result of type $B$.

If you take $W$ to be the set of all possible worlds, operations correspond to maps $A \times W \to B \times W$ – they take the parameter and the current world state, and yield a result and the new world state. And this is exactly what comodels for a given collection of operations are: sets $W$ equipped with a map $A \times W \to B \times W$ for each operation $op : A \to B$. As a bonus, comodels are dual to models and thus a natural extension of the algebraic theory of effects.

Comodels are dubbed resources in eff and are implemented slightly differently. The main reason is that there is, of course, no datatype you can use to represent the set of all worlds $W$. For this reason, I was at first inclined to drop any explicit mention of $W$. Instead, only special built-in effects (for example standard I/O channel) would have resources and those resources would be implemented in effectful OCaml code, making $W$ implicit. Andrej argued that a programmer would still want to write her own resources, for example to implement a pseudo-random number generator. Thus, we decided to equip each resource with a state only it can access, and provided a syntax with which a programmer defines the desired behaviour.

What about toplevel handlers or other alternatives to resources? First imagine how a handler should handle a toplevel (non-delimited) continuation. As soon as a handler applies it to some value, the continuation never yields back control and whatever follows it in the handler is discarded. Furthermore, the continuation should be called at least once (I'll discuss this later), otherwise eff would abruptly exit.

Thus, each toplevel handler is more or less some computation followed by an application of the continuation to a given value. What if this computation triggers some operations? Since these operations happen at the toplevel, we cannot handle them as they have escaped all handlers. We had an implementation that worked like this for some time, but there were no obvious advantages, all while the implementation was hacked together, the behaviour was wildly unpredictable, and the (pretty neat, we probably agree) abstraction of effects that eff provides was broken.

In the end, we decided to allow only pure computations at the top-level. So, you have some pure computation that in the end passes a result to the toplevel continuation. But this is exactly what a resource does, except that you only compute the result while the passing to the continuation is implicit.

What if you do not call the continuation, but instead call some special toplevel abort operation? What exactly should this operation be, if it is not a standard exception?

1. If it is a special extension of eff that can be used only in resources, why would we use it? One reason was that for some exceptions, you want to have a nicer error message than the usual "Uncaught operation ...#raise ...". For this reason, we have a built-in function exception (declared in the pervasives) that generates exceptions with resources that do just that. So we can get the same benefit without any extensions.
2. If it is a special extension that can be used everywhere, it again breaks the abstraction of effects, as there is a way to perform effects without operations.

Thank you for the precisions.

Two comments:

1. It's unnecessarily confusing that you use c for built-in constants and computations, esp. since there is only a short phrase mentioning the first. Can you choose another metavariable for constants?

2. I'm confused about the typing of e#op, both in its own rule and in the handler rule. The only way to get an effect type E seems to be by introducing a computation with new, which is typed with the $\vdash_c$ judgment, but the aforementioned rules with e#op require typing the effect e with $\vdash_e$ judgment.

@Sean: Thanks for the comments. Regarding constants, yes of course, that is an unecessary slip up on our part. Regarding your second point: you are right, so the typical way of getting a e#op is to write something like let x = new E in .... x#op ... What did you expect? You could write (new E)#op in concrete syntax, but that would be useless and also it would be desugared into let x = new E in x#op.

Ah, okay. So, you're assuming a variable will be used as the expression e in e#op. I was missing where the coercion from computation to expression was taking place. It might be helpful to mention that, since you already mention val for coercing an expression to a computation.

It appears that let is the only way to get an expression with an E type. Is it possible to have a non-variable expression in e? If not, perhaps it's a simplification (and clarification) to directly use a variable, as in x#op.

I am not "assuming" that a variable will be used in e#op. Rather, this is a consequence of the fact that the syntax does not have any exprssions of effect types, other than variables. I don't think anything would be simplified if we restricted e in e#op to variables. We would just break orthogonality, so this does not sound like a good idea to me.

I said "assuming" because you said "typical." If it's a consequence, then it's not the typical way, it's the only way. Since it's the only way, I don't see the orthogonality that is broken.

Anyway, this is all very nitpicky. We read your paper in our reading club at Utrecht, and one of the comments that came up was that it was fuzzy how computations and expressions were distinguished. Now that I understand how you get from a computation to an expression, it's more clear. But I think something could possibly be improved in the explanation.

I you have a suggestion, I'd be very happy to hear. Perhaps an example earlier in the paper? Video lecutures?

[…] some variation of the StateT or ReaderT monad transformer should work well enough. Leveraging algebraic effects (or heterogeneous lists, or dependent types) we might effectively mix operations on multiple […]

[…] possible, using the rather well known monads or the funkier lenses or the more sophisticated algebraic effects. However, it is very difficult in general to make types match whatever arbitrary interface your […]