Combining callback effects in the return type?

[osa1]

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

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

    Just(item) ->
      handle ({ cb(item) })
        ctl continue_()
          ()
        ctl break_()
          return ()
      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.vector.length < !iterator.idx 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())
  })
  ()

Output:

test.kk(74,33): type error: effects do not match
  context        :   [1, 2, 3].vector.iterator.for(vector-iterator/next, fn(item) {
                       println("item = " ++ item.show())
                     })
  term           :                                 vector-iterator/next
  inferred effect: <read<global>,write<global>|_e>
  expected effect: total

Shouldn't main handle read<global> and write<global> effects? If not, how do I handle them myself?

I'm also not sure why I need a div effect in the cb parameter of for. If I remove it I get

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

Is this expected?

[osa1]

I realized that the error is actually that vector-iterator/next has effects so can't be passed as pure next argument.

I'm trying to update the for function to allow effets in next and cb but I can't figure out the syntax. So far I have this:

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

    Just(item) ->
      handle ({ cb(item) })
        ctl continue_()
          ()
        ctl break_()
          return ()
      test/for(iterator, next, cb)

Which is not right, as the return type should include effects of both next and cb, but it causes a compiler crash instead of a type error:

test(1, 1): internal error: Type.Type.labelNameEx: label is not a constant
CallStack (from HasCallStack):
  error, called at src/Common/Failure.hs:46:12 in koka-3.1.2-2NpoSf9Uv2JEsgjfT7jQ0Q:Common.Failure
  raise, called at src/Common/Failure.hs:32:5 in koka-3.1.2-2NpoSf9Uv2JEsgjfT7jQ0Q:Common.Failure
  failure, called at src/Type/Type.hs:602:13 in koka-3.1.2-2NpoSf9Uv2JEsgjfT7jQ0Q:Type.Type

What is the syntax for "div + next-fx + cb-fx" in the return type of for?

[TimWhiting]

These are the changes to get it working.

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

// By the way, it looks like your length comparison was inverted. 
fun vector-iterator/next(iterator: vector-iterator<a>): <read<global>, write<global>> maybe<a>
  if iterator.vector.length > !iterator.idx then
  ...

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

The effect variable after the vertical bar needs to be the same in all callbacks and the return type. Also <extra-fx> treats it as a label (specific effect), and not an effect variable. You can use <<>|extra-fx> or just plain extra-fx if you want a effect variable with no other effects.

The reason it needs to be the same in all is that it needs to unify to the least upper bound of both callback's extra effects. For example if cb requires a state handler above it, and next requires an exception handler above it, then the function as a whole needs to have both state and exception handlers above it. It doesn't mean that next or cb has to use both.

Due to similar reasoning the same goes for all the explicit effects in the callback type signatures when they have an effect variable. In this case this is only div but in general the rule is that if you have an effect variable all unhandled effects need to be the same in all callbacks. Let's consider the situation with state and exception handlers again. If the signatures were next: a -> <div,st<global>|extra-fx> maybe<item> and cb: (item) -> <ctl-flow,exn,div|extra-fx> (), with the result effect as <exn,st<global>,div|extra-fx>, we would have an error. This is because lets consider the case where we have two exception handlers above us on the stack. Which should be the one next uses if the concrete function passed to next has the exn effect and extra-fx unifies with that? Should it be the inner one (the same as the exn from cb), or the outer one. Well since extra-fx also occurs above cb it seems like it would skip the inner exception effect and reach the outer. However in most cases that is not what you want. Koka requires us to make our intentions explicit. If it should be the same one, then we need to add exn to the effect row for next, and similarly for state and cb's effect row. If however we want the exn handler for the outer then we should mask / hide the exn effect in our result effect from next using mask<exn>{iterator.next()}. Usually you want the former though and not to use mask. Note that adding extra effects to these first class function parameters doesn't require that those functions use those effects, it just tells what the maximum allowed shape of the callback function should be.

For functions that are not polymorphic in the effect type, you can have different types in the callback functions because koka already knows that next / cb will not use any additional effects, so it doesn't need to worry about a cb being passed in that uses a state effect and whether it is the same state effect that next uses:

fun for<item>(iterator: a, next: a -> <write<global>,read<global>> maybe<item>, cb: (item) -> <ctl-flow> ()): <st<global>,div> ()
// By the way st<h> is an alias for <read<h>,write<h>,alloc<h>>

I haven't really encountered any situations where I need one function parameter to be polymorphic in effect and the other not.

As far as the reason for div being needed, the function is not guaranteed to terminate. A poorly coded or intentionally infinite iterator could end up diverging. However, if you want to assert to the compiler that that will not happen you can import std/core/undiv
and tell Koka which argument is going to eventually decrease in size.

fun for<item,extra-fx>(iterator: a, next: a -> extra-fx maybe<item>, cb: (item) -> <ctl-flow|extra-fx> ()): extra-fx ()
  ...
      test/for(iterator.pretend-decreasing, next, cb)