Closed hflsmax closed 1 month ago
Looks like there is an error in type inference / checking. Change this:
fun driver(): <st<global>, pure> ()
with handler
final ctl throw-exn(err) ()
val res = (!q).popFront()
q := snd(res)
fst(res)()
driver()
to this:
fun driver(): <st<global>, pure|e> () // The function can have more than the effects listed
with handler
final ctl throw-exn(err) ()
val res = (!q).popFront()
q := snd(res)
mask<exn> // Since we are calling driver in a loop, and it introduces a new handler at each loop, we need to mask `exn`, additionally, we don't really want to catch exceptions raised in the job either, so mask it for that as well.
fst(res)()
driver()
Alternatively you can just introduce the exception handler later above the entire driver loop, and just mask the exn
for the user function.
fun spawn(f)
...
fun driver(): <st<global>, pure|e> ()
val res = (!q).popFront()
q := snd(res)
mask<exn>{fst(res)()}
driver()
spawn(f)
with handler
final ctl throw-exn(err) ()
driver()
At the start of the scheduler
function, you can find this line (with forall<e>
added for clarity):
val q: forall<e> ref<global, dequeue<() -> <div, st<global>|e> ()>> = ref(emptyQueue())
I am surprised that Koka accepts this, since it seems to violate the value restriction and is explicitly disallowed by the Gen
rule in Figure 3 of Type Directed Compilation of Row-Typed Algebraic Effects.
Looks like there is an error in type inference / checking. Change this: ............ to this:
fun driver(): <st<global>, pure|e> () // The function can have more than the effects listed .....
Thanks for the suggestion. It works. But why is it necessary to make driver
effect polymorphic?
Apologies for the late reply but it is fixed now -- the bug was in two place, a missing substitution and a missing check for polymorphic values due to annotations. Thanks!
Apologize for not able to narrow down the issue. I implemented a scheduler using
raw ctl
handler, and stores the resumption in a queue. The program type checks but it segfaults. Can someone help me diagnose whether it's a compiler bug or a program bug? Or point me to the direction of how to debug.The scheduler uses a custom dequeue data structure, which is not included in the code below. An compilable file is here: scheduler.txt
Thanks!