RFC: Labelling implicit effects into explicit capabilities

[jiribenes]

[!NOTE] This is a request for comments in very early stages, feel free to comment/nitpick below.

Allow explicitly naming capabilities in effect sets in order to recover summon-style functionality, for example:

def foo(): Unit / {out: emit[Int], in: read[Byte], log, Exception[WrongFormat]} = {
  val n: Int = in.read().toInt
  do log(s"Saw: ${n}, emitting both it, and its square")
  do emit(n)
  out.emit(n * n)
}

then gets translated to

def foo() {out: emit[Int]} {in: read[Byte]} {$log: log} {$exc: Exception[WrongFormat]}: Unit = {
  val n: Int = in.read().toInt {$exc}
  $log.log(s"Saw: ${n}, emitting both it, and its square")
  out.emit(n)
  out.emit(n * n)
}

I think it's somewhat straightforward change in Parser, Namer, and ExplicitCapabilities, no changes at all from Core onwards, but I have no clue how big of a change this would be for Typer (I hope it's easy, but I can't really tell for sure).

As a bonus, this allows the LSP to come up with names, show them as inlay hints, and then we can even mention them in error messages.

[kyay10]

This would be rather nice to have! To clarify, would captures to such named effects be possible?

def foo(): Unit / {out: emit[Int], in: read[Byte], log, Exception[WrongFormat]} = {
  val n: Int = in.read().toInt
  do log(s"Saw: ${n}, emitting both it, and its square")
  do emit(n)
  val f: => Unit at {out} = box { out.emit(n*n) }
  f()
}

In fact, would this be compatible with higher-order effects, i.e. would this be possible:

def foo(): (Bar at t) / {t: Bar} = box t

just like this is possible:

def foo {t: Bar}: (Bar at t) = box t

I think there's a bigger discussion here to be had about captures to effects not existing. It'd be nice to be able to have defs that capture some effects from the outside.

def foo(): Unit / {out: emit[Int], in: read[Byte], log, Exception[WrongFormat]} = {
  val n: Int = in.read().toInt
  def f(): Unit / {} = do emit(n*n) // inferred to capture `out` automatically.
  val f2: => Unit / {} at {out} = box f
  val f3: => Unit / {} at {out} = box { do emit(n*n) } // maybe it should even work with lambdas
  f()
  f2()
  f3()
}

Kotlin has a similar feature to effect sets in the form of context parameters. They allow explicit naming too, but also provide a function contextOf in the stdlib to allow summoning. As far as I understand, contextOf is simply impossible to write in Effekt currently. I don't think this RFC is enough to be able to write it, though. I think this fails because type parameters can't range over computation types:

def contextOf[T](): (T at t) / {t: T} = t

So perhaps such a summoning construct should be added as syntactic sugar, for use primarily inside lambdas