Resume both bidirectional and normal handlers with both either a block or a value

[phischu]

Consider the following program which works fine in Effekt:

effect stop(): Unit

effect yield(): Unit / stop

def main() = {
  try {
    do yield()
  } with stop {
    resume(())
  } with yield {
    resume { () }
  }
}

Indeed, stop is a normal effect and we resume it with resume(()), and yield is a bidirectional effect and we resume it with resume { () }.

I would like the following program to be accepted too and be the same as the previous one:

effect stop(): Unit

effect yield(): Unit / stop

def main() = {
  try {
    do yield()
  } with stop {
    resume { () }
  } with yield {
    resume(())
  }
}

We should be able to resume both kinds of effects with both kinds of syntax. resume(v) should be syntactic sugar for resume { v }.

[b-studios]

Quick question: what do we do in the following case?

val k = box resume

a. nothing: just forbid it; users should eta-expand b. eta-expand: but to what? the bidirectional one because it is more general?

By now I strongly tend towards a. This simplifies the implementation and will help us provide better error messages at the cost of a few eta expansions (that might even make it clearer...)

[b-studios]

Requiring eta expansion destroys demos, since we cannot simply write resume unless we already know it.

One solution would be to have a better type on hover on the operation that mentions the type of resume. Another option would be to error in Typer and provide some better feedback to the user that tries to call resume.