Open RyanBrewer317 opened 1 year ago
I'm running into the same or very similar issue. In my case it doesn't matter if I use unsafe-no-div or unsafe-total, both will crash.
Here is an example. We define a take
function which should turn a divergent iterator into a non-divergent one.
Furthermore, for some reason the to-list function also thinks it is divergent, requiring another unsafe-no-div there.
pub effect iter<a>
ctl yield(elem : a) : ()
pub fun to-list(it : () -> iter<a> ()) : list<a>
with unsafe-no-div()
var result := Nil
with fun yield(elem)
result := Cons(elem, result)
it()
reverse(result) // List was accumulated in reverse order
pub fun take(n : int, it : () -> <div,iter<a>> ()) : iter<a> ()
var count := 0
with ctl yield(elem)
if count < n then
yield(elem) // Forward the yield to our new iterator
count := count + 1
resume(())
else
()
with unsafe-no-div()
it()
And some test code
pub fun test-iter() : div list<int>
fun fib-iter(n1 : int, n2 : int) : <div,iter<int>> ()
val n3 = n1 + n2
yield(n3)
fib-iter(n2, n3)
to-list
take(100)
fib-iter(1,1)
See https://github.com/koka-lang/koka/pull/321 as well (I was running into seg faults too).
When I run the following code:
I get a segmentation fault, even though
test2
is of course not divergent at all. Replacingunsafe-no-div
withunsafe-no-ndet
also leads to a segfault, but replacing it withunsafe-total
results in printing "success," presumably because it gets rid of the parse effect. All three unsafe functions are of course implemented the same way, except for their typing.I of course understand that using these unsafe functions are, well, unsafe, but this behavior is so odd that I figured I'd make an issue about it just in case it's caused by an unknown compiler bug.
I also want to add that the reason I got into this experimentation to begin with was wanting to build a recursive parser using the parser combinator library, then realizing that I would have to add the "div" effect to everything I'd written even when I knew that the top-level function expr-parsing function (which was the only recursive one) wasn't divergent. I knew that in std, functions like
for
use the unsafe functions to get the looping they need without getting the "div" effect. I say all of this just to say that this didn't come out of mindless messing-around with koka but an actual project, hopefully to show that if this is a bug, it's not a too-remote edge case.