4 ms·

What I don't like is that the effect handler is decoupled from the effect generator. In the code snippet, they define a "yield", and somehow this magically wor

What I don't like is that the effect handler is decoupled from the effect generator. In the code snippet, they define a "yield", and somehow this magically works with the call after that of `traverse`. What happens when you are deeper in a call stack and you accidentally or on purpose have to redefine yield? What if you want to use a generator in a generator? Also, the `fun yield( x : a ) : ()` syntax is highly unintuitive. It _takes_ an int and returns empty? So it's just a continuation? And magically it transfers control flow to the correct place? How does it know where that is? You also have to define the name "yield" thrice, once as the "effect declaration", and then twice as a function, once before the call to traverse, and once inside the effect declaration. These are questions you don't even need to worry about when the handler is a continuation (function) that you pass in as an argument. There's also a problem that koka seems to ignore, that for resumable coroutines of execution, you really want 2 kinds of resumptions. One that overwrites the `ret` address of the coroutine, and one that does not. The former is useful for generators like `traverse`, where you want to return to just after the latest call site, while the latter is useful for things like `throw`, where you always want to return to the first call site. I don't know guys. These "algebraic" effects just seem like really bad syntax sugar over delimited continuations.

ReleaseCandidat 3y ago
> In the code snippet, they define a "yield", and somehow this magically works With `with` you explicitely set the effect handler, no magic involved. > Also, the `fun yield( x : a ) : ()` syntax is highly unintuitive. It _takes_ an int and returns empty? So it's just a continuation? A function that does not return anything is (the poster child of) an impure function, that does nothing else but an (side) effect. That's why you need to call it as an effect and not a "normal" (pure) function. > And magically it transfers control flow to the correct place? How does it know where that is? It doesn't have to. The hidden `run` function (or whatever you want to call it) of the effect systém that actually calls the right effect handler has to know about that. The run function does something like (simplified) - see, that a effect handler with ID 'yield' is called - call the (currently registered) handler for 'yield' with the given arguments - call the continuation with the result of the handler
- whitim 3y ago
  The `run` function is actually quite optimized in Koka. At the point of the call to an effect function there is a O(1) lookup, due to this paper (https://www.microsoft.com/en-us/research/publication/generalized-evidence-passing-for-effect-handlers-or-efficient-compilation-of-effect-handlers-to-c/ https://www.microsoft.com/en-us/research/publication/general...). After that depends on whether a continuation actually needs to be captured or not. Many useful effects can be implemented as `val` or `fun` clauses which can be called / accessed in place without any unwinding of the stack. Only in cases where a continuation is required is the continuation built up.
  - ReleaseCandidat 3y ago
    Thanks for the link! Koka (and Lean too) has produced quite some interesting papers.
ctenb 3y ago
The first yield is just the effect name. There is a shorthand syntax for effects with only one function, such that you only define the name once: effect ctl yield( i : int ) : bool See bottom of this section https://koka-lang.github.io/koka/doc/book.html#sec-handling https://koka-lang.github.io/koka/doc/book.html#sec-handling. When handling the effect you don't 'define' the name, you implement it. Of course you have to mention the name then, just like e.g. with interface implementations
ctenb 3y ago
I'm not 100% sure what you mean with your second point. There are several kinds of handler types: `fun`, `ctl`, `final ctl`, `raw ctl`. The implementor of the handlers is restricted to what these handler types allow. You can implement both generator traversal and exception throwing in this system.

ReleaseCandidat 3y ago

> In the code snippet, they define a "yield", and somehow this magically works With `with` you explicitely set the effect handler, no magic involved. > Also, the `fun yield( x : a ) : ()` syntax is highly unintuitive. It _takes_ an int and returns empty? So it's just a continuation? A function that does not return anything is (the poster child of) an impure function, that does nothing else but an (side) effect. That's why you need to call it as an effect and not a "normal" (pure) function. > And magically it transfers control flow to the correct place? How does it know where that is? It doesn't have to. The hidden `run` function (or whatever you want to call it) of the effect systém that actually calls the right effect handler has to know about that. The run function does something like (simplified) - see, that a effect handler with ID 'yield' is called - call the (currently registered) handler for 'yield' with the given arguments - call the continuation with the result of the handler

whitim 3y ago
The `run` function is actually quite optimized in Koka. At the point of the call to an effect function there is a O(1) lookup, due to this paper (https://www.microsoft.com/en-us/research/publication/generalized-evidence-passing-for-effect-handlers-or-efficient-compilation-of-effect-handlers-to-c/ https://www.microsoft.com/en-us/research/publication/general...). After that depends on whether a continuation actually needs to be captured or not. Many useful effects can be implemented as `val` or `fun` clauses which can be called / accessed in place without any unwinding of the stack. Only in cases where a continuation is required is the continuation built up.
- ReleaseCandidat 3y ago
  Thanks for the link! Koka (and Lean too) has produced quite some interesting papers.

ctenb 3y ago

The first yield is just the effect name. There is a shorthand syntax for effects with only one function, such that you only define the name once: effect ctl yield( i : int ) : bool See bottom of this section https://koka-lang.github.io/koka/doc/book.html#sec-handling https://koka-lang.github.io/koka/doc/book.html#sec-handling. When handling the effect you don't 'define' the name, you implement it. Of course you have to mention the name then, just like e.g. with interface implementations

ctenb 3y ago

I'm not 100% sure what you mean with your second point. There are several kinds of handler types: `fun`, `ctl`, `final ctl`, `raw ctl`. The implementor of the handlers is restricted to what these handler types allow. You can implement both generator traversal and exception throwing in this system.