Escaping references in Eff and resources

In the paper "Programming with Algebraic Effects and Handlers" there is the issue where references (dynamic instances of a state effect, defined using algebraic effects) can propagate outside the scope of the handler. I assume the problem here is that calling an operation on the reference would result in an "unhandled operation" run-time error. "Resources" are introduced to remedy this problem, they seem like implicit handlers around the whole program.

What I was wondering is, if one had an effect system that tracked called operations then would references propagating outside the handler scope still be a problem? The unhandled operations called on the reference would be known statically in the effect system and so these problems can be ruled out, run-time errors of this kind wouldn't appear.

Resources would still be useful to reduce verbosity and to fully emulate ML-style references, but they would no longer be needed to avoid run-time errors if one had a sufficient effect system. Am I right in thinking this?

The problem "Does a reference escape its scope?" is undecidable. An effect system can only overapproximate the answer to the question, so there will necessarily by tricky situations in which the compiler will claim that a reference might be escaping its scope, but it really won't. However, this is unlikely to be a real problem. After all, if a sophisticated compiler can't tell whether a reference is escaping its scope, how can we expect humans to do it?

Note that there are uses of references where we want them to escape scope. Here are some such cases:

1. A function memo which takes another function f and returns its memoized form. Typically memo creates a local reference in which it stores the cache.

2. A self-optimizing data structure such as a self-balancing tree uses local references in the background, so that it can modify itself. Such structures are often referentially transparent, i.e., the optimizaiton has no observable effect other than better efficiency.

3. It is unrealistic to expect that nobody will ever implement any stateful data structures. These need to use state, and they must be allowed to escape the scope in which they were created, or else the structure of the entire program becomes a hostage to correct scoping of handlers.

A similar issue arises regarding instances of effects. A realistic programming language must allow dynamic creation of new effect instances. Some situations which require this are:

• opening any number of files or communication channels: each is an instance of an effect, and we cannot tell at compile-time how many we need,

• creating a list of references, where do not know ahead of time how many will be created.

Multicore OCaml simulates instances with first-class modules. To my mind that is a hack, as they're using the genericity of modules to simulate generation of fresh names, and as far as I can tell, it's difficult to write a handler that captures all instances of a given effect.

Let me also say that resources are not a hack. They are inspired by comodels by Plotkin and Powers. I find it a pity that the people who're doing effects largely ignore resources. They think it's possible to write programs without local references. That's just denial for the sake of theoretical simplicity.

• Thanks Andrej, I think resources finally "clicked" for me! I wonder if you read "Eff Directly in OCaml". In it they define a New effect that creates a dynamic instance and also wraps it in a handler. They say they don't need resources. I don't understand how that would handle any escaping references though, since a reference could easily escape the wrapped handler in a lambda function. Have you seen this paper by any chance? – Labbekak Apr 10 '18 at 20:11
• Yes, that's a nice one. The new_prompt is the source of "freshness" and then they do the rest with it. It kind of makes sense that as soon as one has a basic "new" effect, the other kinds of dynamic behavior (such as allocation of new references) should be expressible. – Andrej Bauer Apr 10 '18 at 20:51
• I was also wondering why resources are defined inline with no access to the continuation. Instead of "new E @ h" where h is some handler or variable. – Labbekak Apr 11 '18 at 7:49
• A resource is handled at the top level, i.e., an operation for it was not handled at all and so it propagated all the way to the top. The continuation at that moment is not delimited. It is the rest of the future of the universe, so to speak, i.e., it's the kind of continuation that is known in Scheme. While in principle we could give the resource access to such a continuation, it's probably not a good idea. Suppose the resource decided to invoke the continuation twice, what would that mean? That we now have two instances of the toplevel? – Andrej Bauer Apr 11 '18 at 8:12