-
Notifications
You must be signed in to change notification settings - Fork 29
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
Handler runtime improvements #282
base: hkmc2
Are you sure you want to change the base?
Conversation
0af878c
to
3808175
Compare
:re
handle h = Object with
fun write(x)(k) =
if x < 10 do write(10)
[x, k(())]
h.write(1)
h.write(2)
//│ ═══[RUNTIME ERROR] Error: Unhandled effects
handle h = Object with
fun write(x)(k) =
if x < 10 do runtime.enterHandleBlock(this, () => write(10))
[x, k(())]
h.write(1)
h.write(2)
//│ = [1, [2, ()]] |
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very good improvements! But let's please remove the Prelude hack.
hkmc2/shared/src/main/scala/hkmc2/codegen/StackSafeTransform.scala
Outdated
Show resolved
Hide resolved
fun enqueue(k) = | ||
tasks.push(k) | ||
fun enqueue(k, x) = | ||
tasks.push(k.bind(null, x)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this bind
needed, here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this is essentially () => k(x)
, I guess it is confusing so I'm gonna change it to a explicit lambda.
hkmc2/shared/src/main/scala/hkmc2/codegen/HandlerLowering.scala
Outdated
Show resolved
Hide resolved
Thanks for writing your thoughts and suggestions! Some more thoughts on this: eventually, we'll probably want to make the effect handler and type class/contextual parameters features work in synergy. This will allow programmers to pass handlers around implicitly instead of having to manually thread them everywhere. Adapting an example from https://effekt-lang.org/tour/effects, we could have: // Interface definition
abstract class Yield[A] with
fun yield(x: A): Unit
// Interface use
fun fib(using Yield[Int]) =
fun inner(a, b) =
use[Yield].yield(a)
inner(b, a + b)
inner(0, 1)
// Handler creation (as a type class)
fun genFibs(limit: Int): Array[Int] =
let
count = 0
fibs = []
handle Yield[Int] with // Define a type class instance AND handle it
effect yield(x) =
if count < limit do
count += 1
fibs.push(x)
resume(()) // <- we resume the computation where yield was invoked
in fib()
fibs Of course, type classes would not be necessary to use effect handlers. We could also just use normal classes and plain // Handler creation (as a normal class)
class YieldUntil(n: Int) extends Yield[Int] with
val results = []
effect done() =
results
effect yield(x) =
if x === 42 do done()
results.push(x)
resume(())
print of
let h = YieldUntil(42)
handle h
// or just: `handle h = YieldUntil(42)`
y.yield(1)
y.yield(2)
y.done()
??? // never reached The type system can keep track of the fact that effect methods are not used outside of corresponding handlers. Note that for effect hygiene, it's critical that the effect be attached to a specific object instance and not just a label. What do you think? |
hkmc2/shared/src/main/scala/hkmc2/codegen/StackSafeTransform.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Lionel Parreaux <lionel.parreaux@gmail.com>
I think type classes should work quite well with handlers. Does I think it would be good to implement the explicit syntax first as the next step from here. P.S. On the other hand, // Handler creation (as a normal class)
class YieldUntil(n: Int) extends Yield[Int] with
val results = []
effect done() =
results
effect yield(x) =
if x === 42 do done() // this makes effect call, which doesn't work now
results.push(x)
resume(()) For this type of recursive binding, I think the semantics for this can be:
But I'm unaware of other implementation of algebraic effect doing this, raising effect in a handler body means raising an effect in the outer context. |
Wait, in fact I remember precisely why I proposed the original coupled design in the first place. It was not accidental. The problem is that we want to prevent programmers from being tempted to write code like this: // In some place:
object Foo(p) with
effect raise(x) = ... resume ...
// In another place:
fun test(f) =
handle Foo(...)
xs map(x => if x < 0 then Foo.raise(x) else f(x)) The problem is that if a user calls handle Foo(arg)
test(x => ... Foo.raise ...) Then there is an unhygienic interaction that may be surprising: the person who wrote So I think it's better to ensure that a fresh, unique object instance is generated whenever an effect is handled in some scope.
So actually I don't think the general
Yeah, it's probably better to follow the standard practice, and we could allow |
Right, but I think the problem here lies in how the contextual parameter is handled. Suppose in |
The suggested scheme doesn't involve much change for handler lowering; during lowering everything involving contextual parameter should be resolved already. Again for the example above:
The type of f can be required to be free of implicit contextual parameter, then
The reason for introducing this type of binding was due to usage of recursive handlers in the old UserThread test. We can go without this syntax while still allowing a special syntax for the semantics of the recursive binding ( But the test at handle h = Object with
fun write(x)(k) =
if x < 10 do
print(enterHandleBlock(this, () => write(10)))
[x, k(())] showed that it is possible to create many surprising patterns, including rebinding the same handler at different levels, which may result in surprising behaviour if a function rebinds a given handler. So I agree that it should probably not be introduced. On the other hand, recursive binding seems fine for now and the usage pattern seems rather restricted and cannot cause such rebinding problem, except the |
Sorry, I realize I messed up the example. I meant to make // In some place:
object Foo with
effect raise(x) = ... resume ...
// In another place:
fun test(f) =
handle Foo
xs map(x => if x < 0 then Foo.raise(x) else f(x))
handle Foo
test(x => ... Foo.raise ...) I can see where your remark is coming from: by using type classes like fun test(f) =
handle Yield[Int] with ...
xs map(x => if x < 0 then use[Yield].yield(x) else f(x)) it would seem like we would lose the hygienic property I was talking about. But that's not the case. Contextual parameters are resolved and expanded statically, at compile time. They're just as if the programmer had manually passed the parameters manually. They're not dynamic and require an explicit type annotation. With To make fun test(f: (Int)(using y: Yield[Int]) ->{y} Int) =
handle Yield[Int] with ...
xs map(x => if x < 0 then use[Yield].yield(x) else f(x)) and then it would be completely clear that this capture is the intended semantics. (Notice the
Not sure what you are referring to. Which kind of binding specifically, and how was it used in the old UserThread test?
I guess that's as expected though because we don't bind handlers dynamically. |
Oh the type of binding I refer to is exactly the one you wrote (equivalent to arbitrary usage of |
Changes:
Runtime.mls
I have some further improvement in mind which should allow some program that cannot be run currently to work fine.(Update: done)Problem:
I added Runtime module in
decl/Prelude.mls
just to get the class symbols. I think this is not correct as it causeRuntime
to pass elab but I don't know how to get the class symbols otherwise. (Runtime.mls has dependence on these classes, and Predef.mls imports Runtime.mls, so I don't think these classes can go to Predef?)TODO:
MLsCompiler.scala
. It should not use full path.enterHandleBlock
toPredef
(as it's intended to be used by programmers directly) and document its semantics thereTest diffs:
UserThreads*.mls
: these tests are malformed, and the new implementation throws Error on themLeakingEffects.mls
: the new test output matches with intended semanticsZCombinator.mls
: the stack depth changes because ofRuntime.stackDepth
is a selection which gets sanity checks. The sanity check moves the selection before the stack depth is increased for the function callconsole.log
.Follow-up:
enterHandleBlock
(...handlerArgs) => return mkEffect(h, (k) => handlerMtdBody);
enterHandleBlock(h, () => handlerBody)
h
andk
is clear in the handler method, i.e. we can even have standalone handlers likeh
is a value, butk
is binded as param, so it is kind of awkward. Also for type checking this means you retroactively add behaviour toh
which is not great and probably won't work.while awkward, Object are not essential for codegen to work,
h
can be anything that can be equality checked, i.e. everything in JS is technically fine (but this is kind of awkward and might not work well with type checking).It might be worthwhile to add yet another keyword for
handler fun
for clarity and conciseness.