Home

Inferring algebraic effects

Logical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:

We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.

Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial.

By Ohad Kammar at 2014-09-27 23:16 | Functional | Implementation | Paradigms | Semantics | Theory | other blogs | 15479 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The Eff type checker lacks

The Eff type checker lacks an occurs check which means you're going to experience a lot of infinite loops when playing around with it. Except for that it's a really fascinating language - playing around with it a little has helped me understand exteff and why monads aren't the end of the effects story!

The way that you specify effects (and are able to do things like add multiprompt delimited continuations to the language in 3 lines of code!) reminds me a bit of the language in Hagino's thesis which let you define lambda as a data type for the first time. In his IAS talk Andrej explained that he will be using the ideas to improve proof assistants.

Since this is a very unique language in its space I'm looking forward to seeing what kinds of code it's going to be able to condense down into very short elegant expressions. Does anyone have some suggestions for what to try recasting in Eff?

By Alex1 at Sun, 2014-09-28 08:29 | login or register to post comments

Sorry about the lack of

Sorry about the lack of occurs check. I've been meaning to add it for some time, and I added a half-working version to the master branch just now. Hopefully this will resolve at least some infinite loops.

If you want to try writing something nicer in Eff, you could try Danvy & Filinski's optimised CPS transformation, which currently uses shift/reset. See: https://gist.github.com/orchid-hybrid/715f0b7eba3d902699fa

By matijapretnar at Sun, 2014-09-28 18:09 | login or register to post comments

Continuations - overkill?

I find it a bit of an overkill that the handler receives a full blown continuation. I asked previously about this on LtU, and the answer was that that's for doing things like nondeterminism, where a handler will (potentially) invoke the continuation multiple times. So if I don't need to be able to express nondeterminism with handlers, it should be enough to just call the handler on the stack (with an implicit continuation), like a Common Lisp restartable condition handler, right?

By Manuel J. Simoni at Sun, 2014-09-28 16:02 | login or register to post comments

What kind of overkill?

Are you concerned about performance? Or just that the average handler-implementer can't be trusted with a continuation? Or that even the wisest of handler-implementers shouldn't have to bother with continuations most of the time? Or something else?

Seems like Eff provides a primitive that you'd want to occasionally (often?) abstract over. You could imagine some simple macros that hide the continuation for typical return-once usages.

By Brandon Bloom at Sun, 2014-09-28 16:25 | login or register to post comments

It seems to me that the

It seems to me that the continuation argument is superfluous in all use cases except where the continuation might be invoked multiple times (which is a pretty esoteric use case) and I'd like to know if this intuition is correct, or if there's something I'm missing.

Also, performance is an issue, too. Capturing and reinstating a continuation for each reference cell access is a bit too much.

By Manuel J. Simoni at Sun, 2014-09-28 16:44 | login or register to post comments

Even with 0 or 1 times...

You don't have to just concern yourself with how many times the continuation is called, but also *when* it is called. And what happens before or after it.

What about if you want to call the continuation zero times? For example when aborting a computation. Maybe even aborting conditionally (or, more accurately, resuming conditionally).

What about if you want to wrap computation around the continuation invocation? For example the pure emulation of ML's mutable refs discussed in the original Eff paper. The intermediate return value from the continuation is a function of the current state, which must be supplied by the handler.

As for performance: The same compilation techniques that GHC employees on monads in Haskell can be applied to effects in Eff. Because impurities are encoded as dataflow to, from and of continuations, you can basically just inline them away.

By Brandon Bloom at Sun, 2014-09-28 18:12 | login or register to post comments

No, in the usual cases, you

No, in the usual case, you call the continuation once because you need to resume it. If you leave out the call, the continuation is thrown away, just like in exception handlers. There is no implicit way of resuming the continuation.

If you want performance, you've come to the wrong place. Eff is currently in a prototype stage and though we are working on it, we are at least one PhD thesis away from efficient evaluation. So far, two optimisations seem plausible.

First, you could use resources, which are a generalisation of reference cells and capture the kind of effectful behaviour where an operation modifies some internal state and returns a value back to the continuation. In addition to reference cells, examples are I&O, pseudorandom number generators, various persistent data-structures, … Right now, Eff still traverses the whole handler stack to see that no handler captures the operation, and only then invokes the resource. However, it would be a simple fix to figure out that there will be no matching handler so you can invoke the resource immediately

A more complicated optimisation is to recognise handlers that end with a call to the continuation (similar to tail recursion), and in this case just run additional commands instead of pausing the continuation, running the additional commands, and then resuming the continuation.

By matijapretnar at Sun, 2014-09-28 18:25 | login or register to post comments

Headsup: Efficient handler compilation

As Matija said, we're still prototyping usage, but some people are already looking at optimisation! Steven Keuchel (in joint work with Tom Schrijvers) presented in this year's Implementation and Application of Functional Languages (IFL 2014) some first steps towards efficient implementations of effect handlers.

By Ohad Kammar at Sat, 2014-10-04 17:39 | login or register to post comments