Expressiveness of Effekt computations

[SystemFw]

Hey :)
I've been following Effekt for a while, nice to see all the progress!

I have a quick question about Effekt's current expressive power:
In Haskell-style FP, programs are values that need to be combined explicitly through functions, but are first class:

def 2p[A](p: Parser[A]): Parser[A] = p.andThen(p)

In Effekt, programs are computations that are mostly combined in direct style, using second-class blocks when you want to take a program as an input:

def 2p[A] { p: A } : A / Parser = p() ; p()

Now, am I correct to assume the following signature is not currently expressible in Effekt?

def alternatives[A](ps: List[Parser[A]]): Parser[A] = ... fold with `orElse` ....

and that you would have to write the equivalent of :

val ps: List[Parser[MyA]] = List(p1, p2, p3)
val p: Parser[MyA] = alternatives(ps)

as a series of direct calls to something like or? :

def p: MyA / Parser = or { p1() } { or { p2() } { p3() } }

I understand why second class blocks are important in Effekt's current design btw, I just want to make sure I get the full implications in code.

Thanks!
Fabio

[b-studios]

Hey Fabio, sorry for the late response (I need to figure out how to turn on notifications ;) )

First of all, very good question. Indeed, everything you said is 100% correct.

The limitation that Effekt (as described in our OOPSLA20 paper) does not have first-class functions means that computation cannot be thunked and treated first-class.

It can (of course) be thunked and treated second-class, but that excludes the list example.

We have been working on lifting this restriction, which resulted in a new core calculus "System-C". You can find an implementation and a copy of our paper here:

https://github.com/se-tuebingen/oopsla-2022-artifact

Our main motivation to bring back first-class functions was to

1. implement schedulers (https://se-tuebingen.github.io/oopsla-2022-artifact/casestudies/scheduler.html), that is treat continuations as first-class
2. being able to reason about purity. In your example above the argument block p can have arbitrary effects. Sometimes we want to express that a function argument should have no effects at all -- for instance for parallelisation.

We have not yet fully implemented all features of System C back in Effekt; but this is on our bucket list.

[SystemFw]

Oh wow, I was secretly hoping you were working on lifting those restrictions :) Thanks for the paper, I'll add it to my reading list