Effect type appears twice in expected type

[osa1]

effect ctl-flow
  ctl continue_(): ()
  ctl break_(): ()

fun for<a, item, cb-fx>(
    iterator: a,
    next: a -> <div,console|cb-fx> maybe<item>,
    cb: (item) -> <ctl-flow,div,console|cb-fx>()
): <div,console|cb-fx>()
  match iterator.next()
    Nothing ->
      ()

    Just(item) ->
      handle ({ cb(item) })
        ctl continue_()
          println("  in continue handler")
          ()
        ctl break_()
          println("  in break handler")
          ()
      println("  recursing")
      test/for(iterator, next, cb)

value struct vector-iterator<a>
  vector: vector<a>
  idx: ref<global, int>

fun vector-iterator/next(iterator: vector-iterator<a>): <read<global>, write<global>> maybe<a>
  if !iterator.idx < iterator.vector.length then
    val value = iterator.vector.at(!iterator.idx)
    iterator.idx.set(!iterator.idx + 1)
    value
  else
    Nothing

fun vector/iterator(vector: vector<a>): <alloc<global>> vector-iterator<a>
  Vector-iterator(vector = vector, idx = ref(0))

fun main()
  [1, 2, 3].vector.iterator.for(vector-iterator/next, fn(item) {
    println("item = " ++ item.show())
    if item % 2 == 0 then
      println("  stopping")
      break_()
  })

This program is not right (break effect is not handled properly), but it type checks.

To fix the break effect handling I introduce a local variable:

fun for<a, item, cb-fx>(
    iterator: a,
    next: a -> <div,console|cb-fx> maybe<item>,
    cb: (item) -> <ctl-flow,div,console|cb-fx>()
): <div,console|cb-fx>()
  var recurse := True

  match iterator.next()
    Nothing ->
      ()

    Just(item) ->
      handle ({ cb(item) })
        ctl continue_()
          println("  in continue handler")
          ()
        ctl break_()
          println("  in break handler")
          recurse := False
          ()
      println("  recursing")
      if recurse then
        test/for(iterator, next, cb)

Which fails to type check, apparently this uses an effect called local now. I can't find any documentation on it, but from the definition of it in the standard library it looks identical to Haskell's ST. So I add it to the type sig:

fun for<a, item, cb-fx, h>(
    iterator: a,
    next: a -> <div,console,local<h>|cb-fx> maybe<item>,
    cb: (item) -> <ctl-flow,div,console,local<h>|cb-fx>()
): <div,console,local<h>|cb-fx>()

But it fails with:

test.kk(57, 7): type error: effects do not match
  context        :       handle ({ cb(item) })
                   ...
                             ()
  term           :       handle ({ cb(item) })
                   ...
                             ()
  inferred effect: <local<$h>,console/console,div|$e>
  expected effect: <console/console,div,local<$h>,local<$h>|$e>

How can local<$h> appear twice in an effect type?

[TimWhiting]

It doesn't answer your question about local, but I would probably use a non-mutable variable for this.

fun for<a, item, cb-fx>(
    iterator: a,
    next: a -> <div,console|cb-fx> maybe<item>,
    cb: (item) -> <ctl-flow,div,console|cb-fx>()
): <div,console|cb-fx>()
  match iterator.next()
    Nothing ->
      ()

    Just(item) ->
      val result = 
        handle({cb(item); True})
          ctl continue_()
            println("  in continue handler")
            True
          ctl break_()
            println("  in break handler")
            False
      if result then
        println("  recursing")
        for(iterator, next, cb)
      else ()

As far as using a mutable variable what you want to do is actually mask the local:

  Just(item) ->
      var recurse := True
      handle ({ cb(item) })
        ctl continue_()
          println("  in continue handler")
          ()
        ctl break_()
          println("  in break handler")
          recurse := False
          ()
      println("  recursing")
      if recurse then
        mask<local>{for(iterator, next, cb)}

By masking the local you are telling the recursive call that it doesn't need to know about the handler for the local variable, even though you needed it to make a decision in the if expression. Otherwise it thinks that the recursive call needs access to the local above it in the stack and then because of the recursion it would be able to see all local variables recursively above it in the stack, not to mention you would need a local variable just to call the for expression in the first place. That is why you get two locals. You are basically unrolling the handler stack in the type, which turns out to be impossible because of recursion.

[osa1]

Thanks, this works:

fun for<a, item, cb-fx>(
    iterator: a,
    next: a -> <div,console|cb-fx> maybe<item>,
    cb: (item) -> <ctl-flow,div,console|cb-fx>()
): <div,console|cb-fx>()

  match iterator.next()
    Nothing ->
      ()

    Just(item) ->
      var recurse := True
      handle ({ cb(item) })
        ctl continue_()
          println("  in continue handler")
          ()
        ctl break_()
          println("  in break handler")
          recurse := False
          ()
      if recurse then
        println("  recursing")
        mask<local> { test/for(iterator, next, cb) }

Is there a way to make sure the call to test/for is tail recursion? I think it may not be, depending on what mask does.

[TimWhiting]

You should be able to mark the function definition as tail recursive using tail fun for().... It is supposed to warn if that is not the case, but I'm not sure if it actually does it. As far as mask goes, it does things prior to the call (adjusts a vector of handlers), so it shouldn't affect the tail recursive nature.

[osa1]

As far as mask goes, it does things prior to the call (adjusts a vector of handlers), so it shouldn't affect the tail recursive nature

But doesn't it restore the vector of handlers after the call? Or is the restoration part optimized away if it's in the tail call position?

[TimWhiting]

Ah yes it should restore, I'm not sure how it affects tail calls

[TimWhiting]

I do not think that this function is in fact tail-call optimized. It must need to clean up the local variable after returning. This is why the non-mutable variable is likely a better design choice here, though hopefully the compiler can be smart enough in the future to optimize away some mutable variables.