Handling without control

[phischu]

It would be great if objects could be passed implicitly without introducing an effect handler.

interface State {
  def get(): Int
  def set(x: Int): Unit
}

def myComputation(): Int / State = do get()

def main() = {
  var s = 0;
  with State {
    def get() = s
    def set(x: Int) = s = x
  };
  myComputation()
}

The typing rule for with should be like

Γ |- b : F    Γ |- s : 𝜏 / ε
――――――――――――――――――――――――――――――
Γ |- with b; s : 𝜏 / (ε - F)

[b-studios]

Yes, this is on our map for quite some time. I have thought a bit about it: most of it should be fairly straight forward. There are a few things that need to be sorted out:

• what syntactic category (in source) is with? Can be a Stmt, or a Def, or a Term -- all would make sense. Maybe Def is the most appropriate one.
• much more important: how does this interact with capture tracking (System C). I would assume the outer context captures whatever b and s capture, but the inferred capability would probably need to be transparent. This is a problem, since in Typer associates effect types with tracked block parameters: https://github.com/effekt-lang/effekt/blob/13af16fc1215814905cba9d0839af862d8bd00a1/effekt/shared/src/main/scala/effekt/Typer.scala#L1289