Lambda the Ultimate

Excellent find! They indeed look very closely related. This work too uses a type-level list of effects that are equivalent up to permutation (that are provided as proofs), which seems equivalent to the open union approach. Brady's paper seems to say that it can't currently model non-deterministic choice, but "Extensible Effects" paper does provide support for this if I recall correctly, so they are likely not exactly equivalent.

And a third one, by Kammar, Lindley and Oury, also at ICFP'13:

Handlers in action

Is there anything useful in these papers about managing and making effects more useful, or is it just more about restricting them and making sure they are accounted for during type checking? I'm always blown away about how different the FP, OOP, and systems communities look at this topic.

A good effect system will give you the power of first class coroutines. Typing effectful systems and being able to capture them first class is a huge advantage over the typical OOP situation where you have to manually copy a big chunk of the object graph to achieve something similar.

I don't get it, you mean continuations?

Can you elaborate or point me to a more detailed argument somewhere. I'm genuinely interested here as I'm entering the effect game myself (from the OO perspective), but with a focus on re-execution and rollbacks.

A good effects system allows you to override effects, to specify how they are handled - potentially in terms of a different or lower level effects model. There is a lot of flexibility here. Some effects systems look much like exception systems - i.e. you have effects handlers just like you have exception handlers. (Though, there is a significant difference that "hierarchical exceptions" make a lot more sense than "hierarchical effects". You won't be 'catching' a top-level effect then just dropping it.)

OO can achieve the same, e.g. using context objects or capabilities rather than ambient authority to handle the effects. But this takes much developer discipline. For some use cases, OO seems too expressive for precise control of effects because an object can encapsulate invocations of other objects, and thereby hide which effects are invoked from the client of the object. (Objects work well if only the creator of the object needs to control effects.)

Effects systems work best if you want something like ambient authority (where you don't need to pass authorities around explicitly) but also want precise control over those authorities, or some ability to compose and layer them.

I've been idly seeking good ways to reconcile object capabilities with effects systems. My best idea involves modeling capabilities in terms of typed tokens that prove entry in an external registry or memory. Invocation of a capability is then a controllable effect, without revealing anything about the capabilities (the tokens might or might not have an eq function). Creation/registration of capabilities is another controllable effect.

It sounds like effects in this context mean more like "exceptions" than say an imperative assignment to shared state. The latter kinds of effects do not really need to be "handled", though they have non-local consequences.

Which operations are part of the effects system is up to the language designer. So is the precision with which effects are distinguished. It would take dependent types to be precise down to the level of controlling access to individual variables or files.

There is no singular answer to 'what are effects'. To a Haskell programmer, effects are anything that doesn't fit into a pure function. To a Linear Logic programmer, effects might include 'information effects' such as duplicating or dropping information.

Assignment to a variable can certainly be an effect. The ability to control this effect might not seem useful until you decide that said variable should be stored in a database, or that uses of the variable by a specific subprogram should be logged, etc.

A major advantage of an expressive effects model is that developers might take a subprogram using high-level effects (e.g. canvas operations, like cairo) then implement all the needed operations. Developers can define their own effects models like virtual machines or DSLs.

But a major weakness of most effects models is that they don't really support optimization, e.g. if you have `x++; x+=2; x++` it's unclear that we can rewrite this to `x+=4`. Indeed, depending on how the `++` and `+=` effects are handled (e.g. potentially printing some message), it may be an invalid optimization. I've been wondering how to address this issue (e.g. providing 'effect-classes' with required equational laws, or assumed rewrite rules) but I haven't found a solution that seems verifiable in practice. This lack of support for local reasoning about a program's behavior, for optimization purposes among others, is one of the reasons I've been resistant to effects systems.

...making effects programmable. The idea is that you can specify an effect as a signature, and then specify effect handlers to let you *dynamically* choose the implementation of the effect. The reason they're called effect handlers is because of the way you can implement it.

Basically, when a program runs, you can install an effect handler in a dynamic scope, and when it tries to run an effectful operation, it will throw an exception holding the effect's name, arguments, and the continuation, so that the effect handler can do its thing and then resume execution.

So, for example, you can write a program that does stateful things, and then if you decide that you want all write operations to log themselves (say, to support rollback), you can just change the implementation of the handler, without changing any of client code.

IMO, the fact that this works is kind of wild, and the fact that it actually has a beautiful semantic theory behind it is just bonkers.

So let me translate this into a language I understand:

• Effects are basically abstract methods while handlers are implementations of those methods.
• Dispatch of effects to handlers are dynamically scoped.
• This enables some form of aspect-oriented programming :)

Dynamically scoped procedures are quite interesting, but the problem of type safety is similar to the problem of dynamic binding in general. Hmm...

This description is essentially correct, hence my description of the fact that it has a relatively simple denotational semantics with a good equational theory as "bonkers". :)

That is quite useful, thanks!

Whenever I look at ideas from Haskell, I always have to sort out what is interesting and what is just fighting the type system and to preserve purity. I know I shouldn't look at it this way, but I just don't see the beauty of those fights.

I'm supposing this is like Common Lisp condition handlers... why do you even need to give it the continuation? Isn't the effect handler running "on the (current) stack"?

One thing you can do is handle an effect like 'choose [1, 2, 3]' by resuming with each of the possible choices.

OK, thanks. Another question: are effect systems then anything other than a design pattern built on (delimited) continuations?

I'm sure they are equivalent in some sense (and Oleg can show you how to go back and forth), but IMO a good effect-handler system is much nicer to work with than delimited continuations. You have a little computation and the type tells you what kind of signals it raises. Each kind of signal has its own protocol that defines its interaction with the computation environment. When you are handling a signal from a computation, you may decide to suspend that computation and resume it later. It's all very straightforward and doesn't have the same mind-bending quality that continuations usually do.

Edit: And 'I'm sure that...' was a rhetorical device. I don't actually know they're equivalent. Composing effects modeled as delimited continuations doesn't sound like fun.

Delimited continuations are a "universal effect", in that any definable monadic effect can be expressed in terms of them. Andrezj Filinski proved this almost 20 years ago, in his paper Representing Monads. Here, "definable monadic effect" means any monadic effect whose unit and bind operations are definable in a purely functional language. (So state and continuations are both definable.)

So in a certain sense, all side-effects are a design pattern for delimited continuations. But there's a difference between a side-effect, and an effect system!

An effect system describes which side-effects may be visible to clients -- and many uses of side effects are not visible to clients. (For example, memoizing a function uses stateful side-effects, but does not change it's observable behavior.) So one of the most important features of any effect system is its support for effect masking, which is what lets you say, "This piece of code has an effect e, but since it won't be visible to clients, we can pretend it doesn't have that effect."

In other words, the difference between delimited continuations and effect systems is the difference between values and their types.

The distinction between handling a single effect and handling all effects generically was nagging at me in my response above. Even without the typing & hiding effects aspect, can you compose effects modeled with delimited continuations generally or must you attend to the composition on a case-by-case basis depending on what the particular effects are?