-
Notifications
You must be signed in to change notification settings - Fork 158
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Plan to support "explicit effect in result type of an operation"? #548
Comments
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 ( 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 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. |
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 The caller would understand |
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 It is the same with named effects, though the dynamic lookup for the closest handler doesn't happen. It might look like 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 |
I see, so among many design choices we could have, |
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 As far as bidirectional-effects.
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. |
koka/samples/handlers/named/file.kk
Line 14 in 9f400dd
I'd expect the signature of
fun read-line()
here to beario
(or similar) effect, i.e.: io string
, but currently it errs out: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"?
The text was updated successfully, but these errors were encountered: