effekt-lang / effekt-lang/effekt

Proposal: Expanded lightweight capture polymorphism

Open
#1,207 3 comments 0 reactions 0 assignees View on GitHub
Dominant language
Scala
Stars
469
Forks
41
Avg merge
1d 16h
Merged PRs (30d)
23

Description

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:
```effekt
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:
```effekt
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:
```effekt
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:
```effekt
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 `launch`ed 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:
```effekt
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:
```effekt
def scheduler{block: {s: Scheduler[=> Unit at {block, s}]} => Unit}
```
Which is beautiful IMO.
The usage becomes incredibly simple as well:
```effekt
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 `def`s 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.

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.