Proposal: Expanded lightweight capture polymorphism

[kyay10]

This proposes an extension of the pre-existing lightweight capture polymorphism, but without going all the way to #271. Even with #271 implemented, this proposal would still be a QoL improvement.

(The examples in the current Effekt are hopefully of use to the practical programmer who wishes #271 exists. It's my belief, now, that, if you accept some syntactic noise, #271 is not necessary)

Effekt already has lightweight capture polymorphism. If I take in a computation type, I can refer to it in my return type. This allows me to, e.g. expose delimited control:

interface Prompt[R] {
  def shift[T](block: (T => R at {}) => R at {}): T
}

interface CapSet {}

def resetAnnoying[R]{cap: CapSet}: (=> R / Prompt[=> R at cap] at cap) => R at cap = box { block =>
  try block() with Prompt[=> R at cap] {
    def shift[T](block) = block(box { t => box{resume(t)} })()
  }
}

def reset[R]{cap: CapSet}: ({[T] ((T => R at cap) => R at cap) => T} => R at cap) => R at cap = box { block => 
  resetAnnoying{cap}(box {
    block { [T] (handler) => do shift[=> R at cap, T](box { resume => box{handler(box { t => resume(t)()})} }) }
  })
}

def main() = {
  def cap at io = new CapSet {}
  val x = reset{cap}(box { {shift} =>
    shift(box { k => 
      println("hi")
      k(())
    })
    println("hello")
    42
  })
  println(x)
}

Lightweight capture polymorphism is motivated by the observation that "capture sets are usually associated with a passed-in computation". It has one fatal flaw, though. Take cap from above. It would be nice if, instead of currying, I could refer to cap in the inputs to the function. I.e. it'd be nice to do this:

def reset[R]({[T] ((T => R at cap) => R at cap) => T} => R at cap){cap: CapSet}:  R = <>

Yes, this has a forward reference, so I can see that maybe it'd be hard to support; there's an even better incarnation of this signature:

def reset[R]{block: {[T] ((T => R at block) => R at block) => T} => R}:  R = <>

That'd be amazing to have! It means that the user-defined reset can feel just as native and idiomatic as try-with:

val x = reset { {shift} =>
  shift(box { k =>
    println("hi")
    k(())
  }
  println("hello")
  42
}

Here's another motivating example: imagine I want to have a scheduler/event-loop that allows me to launch blocks with a limited capture set. Specifically, I want them to have the same allowed captures as the call to the scheduler handler. Importantly, the launched blocks should be allowed to launch further blocks. With some effort, you can write this:

import option
import dequeue

interface Scheduler[C] {
  def launch(c: C): Unit
}

def scheduler{reg: Region}: {(Scheduler[=> Unit at reg] at reg) => Unit} => Unit at reg = box { {block} =>
  var queue: Dequeue[=> Unit at reg] in reg = emptyQueue()
  def run(): Unit = queue.popBack match {
    case None() => ()
    case Some((k, q)) =>
      queue = q
      k()
      run()
  }
  def s = new Scheduler[=> Unit at reg] {
    def launch(c) = queue = queue.pushFront(c)
  }
  block(box s)
  run()
}

def main() = region r {
  def r at {r, io}: Region = r
  with val s = scheduler{r}()
  println("hi")
  s.launch(box {
    println("hi")
    s.launch(box {
      println("hi")
    })
  })
}

But this has 2 issues. For one, it exposes the implementation detail that scheduler is defined using a Region. More importantly, Scheduler can actually escape the scope where run() would be called, and so you can have launched blocks that don't end up running. Limiting the escape of effects is exactly what captures are for! With some magic, you can force this:

import option
import dequeue

interface Scheduler[C] {
  def launch(c: C): Unit
}
interface CapSet {}
def scheduler{cap: CapSet}: {{cap2: CapSet} => ((Scheduler[=> Unit at {cap, cap2}] at cap2) => Unit at {cap, cap2})} => Unit at cap = box { {block} =>
  region reg {
    var queue: Dequeue[=> Unit at {cap, reg}] in reg = emptyQueue()
    def run(): Unit = queue.popBack match {
      case None() => ()
      case Some((k, q)) =>
        queue = q
        k()
        run()
    }
    def s = new Scheduler[=> Unit at {cap, reg}] {
      def launch(c) = queue = queue.pushFront(c)
    }
    def cap2 at reg = new CapSet {}
    block{cap2}(box s)
    run()
  }
}

def myBox[T, R]{block: T => R} = box block

def main() =  {
  def cap at io = new CapSet {}
  with def _ = scheduler{cap}()
  with val s = myBox
  println("hi")
  s.launch(box {
    println("hi")
    s.launch(box {
      println("hi")
    })
  })
}

The trick being that the block itself is curried, so that we may introduce a cap2: CapSet. With this proposal, the signature would be more like:

def scheduler{block: {s: Scheduler[=> Unit at {block, s}]} => Unit}

Which is beautiful IMO. The usage becomes incredibly simple as well:

with def s = scheduler
println("hi")
s.launch(box {
  println("hi")
  s.launch(box {
    println("hi")
  })
})

This covers a ton of use cases of #271. The only missing ones are that interfaces cannot be easily capture-polymorphic. You can see in the initial Prompt example that I had to use => Unit at blah to represent a capture set of blah. Note also that, if I use function types instead of an interface, the problem completely disappears. Thus, an extension to this proposal would be to add capture type parameters in some fashion to interface types only. This'd also cover #1155. Importantly, this extension would not add capture set type parameters to defs in any way. This would thus put interfaces on par with function types.

I can't speak to how easy or difficult this would be to implement in the compiler, and whether formalization would be necessary. My hunch is that the compiler might already be able to handle this (because it needs such analysis for try-with, and for the pre-existing lightweight capture polymorphism). Theory-wise, I think this is on par with the lightweight capture polymorphism, so I don't think it breaks anything. There's probably a mechanical translation between the 2 languages, even.

The very first step to implementing this would be to support such self-references in capture sets. Currently, something like block: {Prompt[=> Unit at block]} => Unit fails since block can't be resolved. With that supported, there's some chance that the compiler can already magically handle the rest.

[jiribenes]

Hi, thanks for the write-up.

I've been thinking about allowing value params refer to block param captures for a few years now 😅 I still haven't convinced myself about the design and usability of such a proposal, but it's somewhat straightforward to try and implement it (IMO easier than the self-referential one).

Here's a patch I quickly put together for Namer that allows that: (Some changes in Typer might likely be needed too, no idea)

--- i/effekt/shared/src/main/scala/effekt/Namer.scala
+++ w/effekt/shared/src/main/scala/effekt/Namer.scala
@@ -150,10 +150,14 @@ object Namer extends Phase[Parsed, NameResolved] {
       // we create a new scope, since resolving type params introduces them in this scope
       val sym = Context scoped {
         val tps = tparams map resolve
-        // TODO resolve(ParamSection) loses structural information about value params and block params.
-        //   we should refactor!
-        val vps = vparams map resolve
+
+        // FIX: Resolve block params first, then bind their captures
         val bps = bparams map resolve
+        bps.foreach { bp => Context.bind(bp.capture) }
+
+        // Now value params can reference block param captures in their types
+        val vps = vparams map resolve
+
         val ret = Context scoped {
           Context.bindValues(vps)
           Context.bindBlocks(bps)

Here's your program working, notice the reset:

interface Prompt[R] {
  def shift[T](block: (T => R at {}) => R at {}): T
}

interface CapSet {
  def hi(): Unit
}

def resetAnnoying[R]{cap: CapSet}: (=> R / Prompt[=> R at cap] at cap) => R at cap = box { block =>
  try block() with Prompt[=> R at cap] {
    def shift[T](block) = block(box { t => box{resume(t)} })()
  }
}

def reset[R](block: {[T] ((T => R at cap) => R at cap) => T} => R at cap){cap: CapSet}: R = {
  resetAnnoying{cap}(box {
    block { [T] (handler) => do shift[=> R at {cap}, T](box { resume => box{handler(box { t => resume(t)()})} }) }
  })
}

def main() = {
  def makeCap(): CapSet at io =
    box new CapSet {
      def hi() = println("") // making sure that the `io` is inferred, not just an annotation
    }
  def cap: CapSet = makeCap()
  val x = reset(box { {shift: [T]((T => Int at {io}) => Int at {io}) => T} =>
    shift(box { k =>
      println("hi") // ❗️error: capture {io} not allowed, unless I annotate the type of `shift` above
      k(())         // ... which otherwise gets inferred as only `[T]((T => Int at {}) => Int at {}) => T`
    })
    println("hello")
    42
  }){cap}
  println(x)
}

// $ effekt repro.effekt
// hi
// hello
// 42

I'm not quite sure why the io capture should work automagically in shift, but I'm neither versed in capture calculi, nor familiar enough with the codebase (and certainly not the greatest fan of captures around). I can't guarantee we'll get to this issue any time soon, and I also cannot guarantee this works at all the way it should, though adding a second k(()) does show me a second hello printed out.

---

EDIT:

Thus, an extension to this proposal would be to add capture type parameters in some fashion to interface types only. This'd also cover https://github.com/effekt-lang/effekt/issues/1155. Importantly, this extension would not add capture set type parameters to defs in any way. This would thus put interfaces on par with function types.

I think this would be feasible, yes, esp. with the reasoning that interfaces should be on par with Effekt's builtin function type.

---

EDIT 2: Don't take this message as a final answer from the team, I'm just trying to give a quick "I guess this works" answer with a few details on how to get this running in case you'd want to investigate further. :)

[kyay10]

Thanks for having a look at this!

This is plenty useful! A lot of the examples I have in mind would gain a few extra CapSets passed around, which is alright.

(IMO easier than the self-referential one)

Is the self-referential one that much harder? I thought it could just work by making sure that inside {block: {...} => ...} block is visible as a capture set. I'm not familiar with your compiler that well (I'm very tempted to go in and start trying things tbh), but it doesn't seem insurmountable to me. Not sure how Context operates exactly, but I'm imagining that you could add in "delayed" bindings that have the param names and fake types, and then rebind them after resolve.

I'm not quite sure why the io capture should work automagically in shift

Well, because capture set {cap} gets expanded to {io} and reset has shift mentioning at cap everywhere.

It seems to be a typing issue, then. My guess would be that it uses block first to infer what {cap} should be, thus inferring it to the empty capture set, and then erroring out inside (an easy way to test this would be that reset(box { _ => 42}){cap} should error out).

I wonder if the self-referential one may fare better at typing because there's no value parameter to trip it up and make it infer a bad/empty capture set.

[kyay10]

FWIW, the compiler already accepts this:

effect Foo[C]: Unit
def bar{this: Region}: Unit / Foo[=> Unit at this] = do Foo[=> Unit at this]

but, it's very unhappy when it's called (#1208). It might be an accident that the compiler allows that, but if it isn't accidental, then, with a Namer patch, the compiler should already have all the facilities to implement this proposal (modulo bugs, of course).