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:


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