Plan to support "explicit effect in result type of an operation"?

[complyue]

https://github.com/koka-lang/koka/blob/9f400dd22ef16729d0eca8fbf1d2170fe670d320/samples/handlers/named/file.kk#L14

I'd expect the signature of fun read-line() here to bear io (or similar) effect, i.e. : io string, but currently it errs out:

an explicit effect in result type of an operation is not allowed (yet)

The demo so far reads whole file content into RAM before performing action, thus reasonable; but it's not so right in reading long/streaming content like this.

Seems there's some plan to support "explicit effect in result type of an operation"?

[TimWhiting]

To me it doesn't make sense to use the effect annotation to restrict or state effects (since a different handler for the same effect could be implemented using an in-memory file system, or a networked file system, or even a random file-system - for testing).

I am however curious what @daanx meant by the fact that it is not allowed (yet), and what he had in mind.

Personally I'm of the opinion that we should implement something like bidirectional effects - from Biernacki et al where the operation is intended to be run under some effects/handlers from the call site.

For example, we ran into this in our design of (https://github.com/koka-community/html/pulls) where we wanted to run some operations under a handler from the call site (html-tree).

As far as specifics I don't think Koka needs to follow the design of Biernacki completely. In fact, it might make sense to have an inline fun variant of a operation which uses effects / handlers from the call site. Whether that means all of the handlers from the call site, or just reinstalling the ones we care about, and what that means as far as typing and control flow, it seems like there is a large design space. I guess that is why I prefer to have a special inline fun operation variant, in case we want inline ctl which would have different control flow behavior, reinstalling the handler after yielding, rather than running under the handlers at the call site.

Of course the typing rules might force us to one way or the other, or even require us to give effect types in the effect declaration rather than just different operation effect inference / typing in handlers.

[complyue]

I put more thoughts into this, and maybe "bidirectional effects" is about sorta "implicit callbacks" provided to outer effect handlers?

But the original question I'd ask, is sorta about whether the caller of read-line() should be aware of io exceptions prone, and whether the caller should be able to "handle" possible io exceptions on its own right.

The caller would understand fun read-line(): string as if it's a total function? The caller has only the option to let the outer scope to handle any possible side-effects prone? What if it already read half of the file content, and the next read-line() call suffered network disconnection? How can it do some back-rolling wrt partially received file contents?

[TimWhiting]

Okay, I think I see your point.

For normal effects, the operations and handlers are separate, there is an optimized "dynamic lookup" for the closest handler, which we cannot always know statically, so we don't necessarily know which effects the handler relies on to implement the effect. When you call an operation you get the effect type of the operation as a 'required' effect which must be handled somewhere up the call stack. This is a kind of abstraction. We just know for example that some log handler will take care of the operation - be that via file / network / in memory / debug logging. This separates the "what to do" from "how to do it". The what is defined and abstracted over by the operation clauses for the effect. The computation using that effect defines "what to do", and then later the handler defines "how to do it", which can be specified in different ways.

It is the same with named effects, though the dynamic lookup for the closest handler doesn't happen. It might look like read-line is total, but in fact it is just the same as before, read-line is an abstraction of what to do, and it essentially emits the file effect, but the evidence for the effect handler is already available, including the handlers under which the named effect was created. The runtime switches to that context to handle the effect and then resumes to the point of operation call with the answer. It seems like making some of the effects be handled using handlers in the context of the point of call, breaks the abstraction. Now just some of "how to do" something is mixed in with the use of the abstraction in "what to do".

I think it would be best instead to make any potential failure that needs to be determined in the "what to do" side, explicit in the operation definition. In this case, I would change read-line to return error<string> or something. But if the failure modes can reasonable be handled uniformly for any usage of the effect in the handler itself I would attempt to handle it there, since that is where "how to do / handle" something is defined.

[complyue]

I see, so among many design choices we could have, fun read-line(): error<string> goes with a value-level solution that total-function-esque, and fun read-line(): io string might need bidirectional-effects, can I understand it like this?

[TimWhiting]

Yes. I believe that sums it up. Going with the value level solution, you could then choose to call other operations on the handler when certain errors happen (to reinitiate network connection or something). This exposes some of the implementation details of the handler (that it has potential to need connection/reconnection). Alternatively the handler could also choose not to expose any errors, or an API to reconnect, and let the user configure the named effect with options for reconnecting etc when creating the named effect, which would allow a more general interface that isn't necessarily tied to I/O, and would have a uniform strategy for dealing with these issues, instead of every usage of the read-line() having to deal with the error, and potentially handling it differently. So I guess that is the tradeoff I was trying to explain, do you want the error to be dealt with the same for every usage of a specific named handler (doesn't mean that you can't create other named handlers with different options). Or does every call to the operation need to consider and choose a different way of handling the error condition. I would probably err on the side of the putting that logic in the handler / handler configuration and create different handlers for different strategies, and if needed provide an additional separate operation try-read-line() for the error case if you think the user might want to customize the strategy on a case by case basis.

As far as bidirectional-effects. I want to clarify that I don't know what Daan means in this error message:

an explicit effect in result type of an operation is not allowed (yet)

I don't know if Daan has bidirectional-effects in mind, or if there is some other reason for adding explicit effects in the result type of an operation. Additionally I don't think we should necessarily refer to it as bidirectional effects, due to the fact that the paper is very specific in what it means by that. Koka could make some different choices since there is a whole design space in whether to treat 'bidirectional' effects as all effects in the operation handler being interpreted in the context of the operation call (get an implicit function value + call it), or to still have some operations interpreted in the context of the operation handler. Additionally, how that should be declared in the type system (either on an effect declaration for all effects, or specific to handlers), is another question that would need to be answered. Maybe we should call them deferred operations - deferring some effect handling to the operation site and potentially some to the handler site.