Impure arity types

[thwfhk]

I tried to define some effects with impure arities / coarities (i.e., impure parameter and result types) but I failed. I wonder if this is possible in Effekt without using the special syntax for bidirectional effects.

For example, I want to define an operation Get : () => (() ->{Exc} String) which takes a unit and returns an impure function that takes a unit, returns a string, and might invoke the effect Exc. At the first attempt, I wrote down the following Effekt code

effect Exc[A](msg: String): A
effect Get(): => Int at { Exc }

which gave me the following error

[error] ./issue.effekt:4:27: Could not resolve capture Exc
effect Get(): => Int at { Exc }

I had no idea why this error appeared, because Exc is defined just before Get. To figure out the reason, I wrote down some testing code with different combinations of blocks, boxed blocks, capability types, and capability instances as follows.

interface Greeter {
  def sayHello(): Unit
}

def hand1{f: => Unit / { Greeter }} = try f() with Greeter {
  def sayHello() = { println("hi"); resume(()) }
}

def hand2{f: => Unit / { greeter }} = try f() with greeter: Greeter {
  def sayHello() = { println("hi"); resume(()) }
}

def hand3(f: => Unit at { Greeter }) = try f() with Greeter {
  def sayHello() = { println("hi"); resume(()) }
}

def hand4(f: => Unit at { greeter }) = try f() with greeter: Greeter {
  def sayHello() = { println("hi"); resume(()) }
}

Only hand1 is well-typed. The hand2 is ill-typed with the error Could not resolve type greeter. The hand3 is ill-typed with the error Could not resolve capture Greeter. The hand4 is ill-typed with the error Could not resolve capture greeter.

Looking at hand3 and hand4, I guessed the reason is that there is a lexical scoping condition for the appearance of capabilities on types. The following well-typed code verified my guess.

def wrapper() = {
  try {
    def hand2( f: => Unit at { greeter } ) = 42
    42
  } with greeter: Greeter { def sayHello() = { println("hello"); resume(()) } }
}

Also, I came up with the following assumptions about how Effekt works:

1. For block type A => B / {E}, E can only contain capability types, e.g., Greeter.
2. For boxed block type A => B at {E}, E can only contain capability instances, e.g., greeter.
3. Capability types have their globally unique names, and can appear flexibly in types with no scoping condition. (hand1 is well-typed)
4. Capability instances must be well-scoped (i.e., used in the scope that they are introduced such as the scope of their handlers), even though they only appear in types. (hand4 is ill-typed but wrapper is well-typed)

These assumptions seem to be different from the formalisation of the "Effects, Capabilities, and Boxes" paper, because in the paper there is no lexical scoping condition on capabilities at all when they appear on types after at. If there is indeed such lexical scoping condition, it would be restrictive without explicit abstraction over capability instances, evidenced by the fact that I failed to define effects with impure arities.

I wonder if my assumptions are correct and if there is a good reference to look at.

Back to the initial question of having impure arities / coarities, it seems that it is indeed impossible because of the lexical scoping condition. I'd like to know whether this is correct since I'm very unfamiliar with Effekt and probably just made some stupid mistakes.

[thwfhk]

I realised that Effekt does have explicit abstraction of capabilities which is the same as the abstraction of blocks. With that, I finally defined a version of the Get operation with an impure arity by explicitly abstracting the capability instance of Exc as follows.

interface Exc {
  def raise(msg: String): Int
}
effect Get(): {f: Exc} => (Unit => Int at { f }) at {}

def test() = {
  try {
    try {
      (do Get()){exc}(())
    } with Get { resume (box {{f: Exc} => box {(x: Unit) => f.raise("no")}}) }
  } with exc: Exc { def raise(msg:String) = {println(msg); 42} }
}

[b-studios]

Hey, thanks for your questions; sorry that I only just saw them. Actually, what you are asking for will be supported by #361.

I'll go into detail later, when I am out of my meetings :)

[thwfhk]

Thank you, Jonathan! Yes, it indeed looks quite similar to what I want. This pull request seems to add supports for several different things. If I understand it correctly, what you meant is the ability to have block parameters when defining effects. Thus, I guess we could potentially have things like

effect Get2(){f: Exc}: Unit => Int at { f }

This is similar to the code I wrote above and I kind of believe that they have similar expressiveness

effect Get(): {f: Exc} => (Unit => Int at { f }) at {}

Back to my previous questions, now I understood that the lexical scoping condition is indeed discussed in the "Effects, Capabilities, and Boxes" paper. My confusion mostly came from the relations and differences between capability types and capability instances as they were introduced by different papers. It would be great if you could tell me whether my assumptions above are correct.

[b-studios]

I wonder if this is possible in Effekt without using the special syntax for bidirectional effects.

What do you mean with "special syntax for bidirectional effects"?

[error] ./issue.effekt:4:27: Could not resolve capture Exc
effect Get(): => Int at { Exc }

I think there is a confusion between effects and captures (understandably, so).

The type

=> Int at { Exc }

is shorthand for

(() => Int / {})    at    { Exc }

which says: it is a pure function from unit to unit, not using any effects, but closing over the term-level capability Exc.

Now there is no term-level capability Exc in scope, hence the error. Term-level capabilities scope like every other term-level name. So in

def hand2{f: => Unit / { greeter }} = try f() with greeter: Greeter {
  def sayHello() = { println("hi"); resume(()) }
}

greeter is not in scope in the type signature; only in the handled block (e.g. f()) it would be bound/

For block type A => B / {E}, E can only contain capability types, e.g., Greeter.

Yes, exactly. Effects are on the type level (it is a set of types).

For boxed block type A => B at {C}, C can only contain capability instances, e.g., greeter.

Yes, exactly. Note that I changed from E to C since these are really two completely different things. The only commonality is that both are sets.

Capability types have their globally unique names, and can appear flexibly in types with no scoping condition.

Yes, exactly. At some point we allowed local type definitions like

def foo() = {
  effect Bar { ... }
  ...
}

where Bar was only allowed in foo. If I remember correctly, for simplicity, we deprecated that.

Capability instances must be well-scoped Yes, that is also completely correct. It is this well-scoped-ness that we heavily rely on for effect safety.

in the paper there is no lexical scoping condition on capabilities at all when they appear on types after This is not correct, we just did not write down the rules for well-formedness. :) Capability variables are just block variables and they are lexically scoped. This is of course made explicit in the Coq artifact.

Back to the initial question of having impure arities / coarities, it seems that it is indeed impossible because of the lexical scoping condition. It is not impossible but a lot of programs will be ruled out, if one proceeds without care. This is the reason, why in our first paper (OOPSLA 2020) we excluded "higher-order effects" (or as you call them impure argument arities).

effect Get2(){f: Exc}: Unit => Int at { f }

Exactly, with the PR it is now possible to write these. Actually, the effect syntax is somewhat deprecated and I typically use the full syntax (which looks closer to OOP):

interface Get2 {
  def get(){f: Exc}: Unit => Int at { f }
}

This also makes it a little bit more clear that Get2 is a type and not a term.

Relation between Bidirectional and Higher-order effects

There is an intimate relationship between "bidirectional effects" and "higher-order effects" visible through capability-passing. Let us assume the following interface type

record User(name: String)
interface DB {
  def getUser(id: Int): User / { Exc }
  //                           ^^^^^^^
  //                   A "bidirectional" effect
}

which is very similar to the OOP way of doing things. It is clear that getUser returns a User and potentially uses the Exc effect, right? At a call-site this means getUser receives a capability for Exc:

def printUser {db: DB} = 
  try {
    println(db.getUser(42))
  } with exc:Exc {  def raise(msg:String) = println("ERROR") }

(is translated to)

def printUser {db: DB} = 
  try {
    println(db.getUser(42) {exc})
  } with exc:Exc {  def raise(msg:String) = println("ERROR") }

That is, after translation, getUser receives an exception capability:

interface DB {
  def getUser(id: Int){exc: Exc}: User
  //                  ^^^^^^^^^^
  //            A higher-order effect 
}

So, after translation, both are the same. Since we already (conceptually, and technically modulo bugs) supported bidirectional effects, it wasn't too difficult to also add support for higher-order effects in PR #361.

In Effekt, there are two ways to implement interfaces like DB, (1) as an object and (2) as a handler.

// an object
def myDB = new DB {
  def getUser(id: Int) = 
    if (id == 0) User("Jonathan") 
    else do raise("Not found")
}

def withDB[R] { p : => R / { DB } }: R = 
  try { p() } with DB {
  def getUser(id: Int) = 
    if (id == 0) resume { User("Jonathan") } 
    else resume { do raise("Not found") }
}

Now note that in the second case, we resume and THEN raise. This is important to be truthful to the types. We raise the exception at the call-site of getUser, not at the definition site of the DB instance.

The same holds for higher-order effects:

// an object
def myDB = new DB {
  def getUser(id: Int) {exc: Exc} = 
    if (id == 0) User("Jonathan") 
    else exc.raise("Not found")
}

def withDB[R] { p : => R / { DB } }: R = 
  try { p() } with DB {
  def getUser(id: Int) = 
    if (id == 0) resume { {exc:Exc} => User("Jonathan") } 
    else resume { {exc:Exc} => exc.raise("Not found") }
}

In the second case, the impure arity (block argument) is only available in the scope of the call-site which we make super explicit by passing it as argument to resume.

---

I hope this addresses a few of your points. Please let me know if you have more questions and I can help clarify things. We are still in the process of writing a paper on the relation between higher-order effects and bidirectional effects. But the answer should give you a gist of it.

[thwfhk]

Thanks a lot! Your answers are very clear and helpful! I think my confusion is all resolved now.

What do you mean with "special syntax for bidirectional effects"?

I just meant syntax like

interface DB {
  def getUser(id: Int): User / { Exc }
  //                           ^^^^^^^
  //                   A "bidirectional" effect
}

I call it "special" because it is not included in the OOPSLA'20 paper and does not correspond to any operation which takes a first-class value and returns a first-class value from the point of view of conventional algebraic effects. It is more like giving a block type to an operation. Of course this makes sense in Effekt especially using this OOP-like syntax.

This is not correct, we just did not write down the rules for well-formedness.

Yes, I realised my error the next day I asked. This is mostly because I didn't read the paper carefully enough :)

Also thanks for your explanation on the ongoing work. The connection is shown clearly. I have some further questions:

1. I can already encode

   interface Get2 {
    def get(){f: Exc}: Unit => Int at { f }
   }

   in Effekt with

   interface Get2 {
    def get(): {f: Exc} => (Unit => Int at { f }) at {}
   }

   I believe this kind of encoding easily generalises to other cases of bidirectional effects and "higher-order effects". Is there anything that I cannot do with this encoding but this new PR can?

2. I wouldn't treat higher-order effects and algebraic effects with impure arities / coarities as the same thing. There has been a lot of work on different variations of higher-order effects [1,2,3,4,5,6] and I think one common point is that we need special semantics / algebras / handlers to interpret higher-order effects instead of just use the handlers for algebraic effects. Otherwise, we gain nothing more interesting than what we can already do with algebraic effects and handlers.

3. I'm suspicious of the expressiveness of the support for "higher-order effects" here since I don't think there are many things we can do when the block argument is some function just by looking at the syntax. (This is probably just because I don't know the full new things.) For example, is it possible to implement the classical catch example [1] in Effekt using the feature introduced by this new PR? Intuitively, there is an algebraic operation raise s which takes an error string s and raises this error, and a scoped operation catch m n which takes two computations, runs m, and switches to n if m raises an error.

[b-studios]

Thanks for your questions, pointers, and fruitful discussion. I'll try to address the questions as best as I can.

1. Encoding

In the following example failingGet1 will type check, whereas failingGet2 will not. The reason is a bit subtle, but basically the at {} and at {f} are very limiting in the encoding. The don't allow the use of exceptions which are handled at the definition site of the Get capability.

interface Exc { def raise[A](): A }
interface Amb { def flip(): Boolean }

interface Get1 {
  def get1() {f: Amb}: Int
}

interface Get2 {
  def get2(): {f: Amb} => (() => Int at { f }) at {}
}

def failingGet1[R] { p: => R / Get1 } : R / Exc = 
 try { p() } with Get1 {
  def get1() = resume { {amb: Amb} => if (amb.flip()) 0 else do raise() }
}

def failingGet2[R] { p: => R / Get2 } : R / Exc = 
 try { p() } with Get2 {
  def get2() = resume(box { {amb: Amb} => box { () => if (amb.flip()) 0 else do raise() }  })
}

2. Higher-order vs. Impure arities

I do agree that there might be additional expressivity to be gained by scoped/proper higher-order effects. However, I think many use-cases of scoped effects can actually be expressed with impure arities, already. Do you have a good intuition about when this is not the case?

3. The Catch

If I am not completely mistaken it can:

interface Exc { 
  def raise[A](msg: String): A
}
interface Handler {
  def catch[R] { p: => R / Exc } { h: String => R }: R
}

def ex(n: Int) = do catch {
  if (n == 0) do raise("Zero") else n + 1
} { msg => println("caught"); 0 }

def main() = try {
  println(ex(42))
  println(ex(0))
} with Handler {
  def catch[R]() = resume { { p: => R / Exc } { h: String => R } =>
    try { p() } with Exc {
      def raise[A](msg) = h(msg)
    }
  }
}

Running main prints

43
caught
0
()

Here, ex has the inferred type ex(n: Int): Int / { Handler }, since the handler removes the exception.

I am sorry for the very noisy syntax. It is easy to make the type annotations on block parameters optional, but we just haven't done so, yet. :)

Since the Handler implementation is tail resumptive in this case, it is easy to also express it as an object:

def handler = new Handler {
  def catch[R]{ p: => R / Exc } { h: String => R } =
    try { p() } with Exc {
      def raise[A](msg) = h(msg)
    }
}

However, we didn't implement binding objects like handler, like

try { p() } with handler;

but it is on our bucket list of low-hanging fruit.

[thwfhk]

Thanks for your clear and patient answers! Now I think I have a better understanding of higher-order effects in Effekt. Actually, I find that the support for higher-order effects in Effekt is quite similar to the (unpublished) work by van der Rest et al. I'll explain why in the following discussions.

1. Encoding

I see! Yes, this is a good example.

3. The Catch

(I'll go back to the second item later.)

Your implementation is different from what I thought initially but makes sense to me. What I thought initially is that raise and catch are two operations in one interface and are handled by the same handler. I tried to implement it as follows using a sum type for the carrier and it seems to work well.

interface Exc {
  def raise[A](msg: String): A
  def catch[R] { p: => R / Exc } { h: String => R }: R
}

type Sum[A,B] {
  Left(x: A);
  Right(x: B)
}

def hexc[R]{ f: => R / Exc }: Sum[String, R] = try {
  Right(f())
} with Exc {
  def raise[A](msg) = Left(msg)
  def catch[R]() = resume { { p: => R / Exc } { h: String => R } =>
    hexc{p()} match {
      case Left(s) => h(s)
      case Right(x) => x
    }
  }
}

I'm glad that it is possible to use recursive functions to use a deep handler inside its handler clauses (this is an important feature needed for simulating higher-order effects with algebraic effects). This is cool and resolves (most of) my suspicion before.

Now I guess my main concern is that we can only use the block parameters (representing the scoped computations) inside the scope of the block that is passed to resume. For example, consider another classical scoped operation once {p} which takes the first result from a non-deterministic program p that uses the choose operation. Let's extend it with another scoped operation twice {p} which takes the first two results from p. I implemented them as follows.

interface Nd {
  def choose(): Boolean
  def once[R](default: R){ p : => R / Nd } : R
  def twice[R](default: R){ p : => R / Nd } : R
}

def hnd[R]{ f: => R / Nd }: List[R] = try {
  [f()]
} with Nd {
  def choose() = resume(true).append(resume(false))
  def once[R](default: R) = resume { { p: => R / Nd } =>
    hnd{p()} match {
      case Nil() => default // this should never happen
      case Cons(head, tail) => head
    }
  }
  def twice[R](default: R) =
  // duplicating p is not what we always want
  resume { { p: => R / Nd } =>
    hnd{p()} match {
      case Nil() => default // this should never happen
      case Cons(head, tail) => head
    }
  }.append(
  resume { { p: => R / Nd } =>
    hnd{p()} match {
      case Nil() => default // this should never happen
      case Cons(head, tail) => tail match {
        case Nil() => default
        case Cons(head, tail) => head
      }
    }
  })
}

To handle once, we just need to take the first element of handled p and then resume. However, to handle twice, the only way I can come up with is to write some slightly wired code which destructs p individually in two different invocations of resume. However, in this way we are forced to duplicate p, which may not be what we want. For example, consider the following program

def nd3() = do twice(0){ if (do choose()) {println("A"); 1}
                         else {println("B"); 2} }

We get the following result

> hnd{nd3()}
A
B
A
B
Cons(1, Cons(2, Nil()))

Both A and B are printed twice! I would consider this as an unexpected behaviour. I wonder if there is any other way to implement twice which avoids this problem?

2. Higher-order vs. Impure arities

Yes, without considering the composition of handlers (i.e., there is only one handler which handles all effects), they indeed have the same expressive power at least for the case of scoped effects. This is formally proved by Yang et al..

However, when we want to compose different handlers in the presence of scoped effects, we need to be careful. For example, consider the following computation which uses Exc and Nd as we have defined above

def mix1() = do catch {
  if (do choose()) 1 else do raise("False!")
} { msg => println("caught"); 2 }

What should we expect when we execute hexc{hnd{mix1()}}? From my point of view, I would argue that

1. the choose inside the scope of catch should be handled by hnd
2. the semantics of effect interaction should follow the case when hnd is closer to the computation than hexc

For point 1, this is a classical problem when we want to simulate higher-order effects with algebraic effects; the handler hnd just does not know it needs to handle some operations inside the parameter of other operations. I'm glad to see that Effekt solved this problem by restricting where the block parameter (representing the scoped computation) can appear. If I understand it correctly, in the example of hexc{hnd{mix1()}}, the resume below has hnd installed, so the choose operation in p does not escape from the scope of hnd.

  def catch[R]() = resume { { p: => R / Exc } { h: String => R } =>
    hexc{p()} match {
      case Left(s) => h(s)
      case Right(x) => x
    }
  }

This is the same technique used by van der Rest et al. I think the better part of Effekt is that capabilities make this very clear!

However, Effekt still does not achieve point 2, because the catch clause of hexc installs a new hexc handler which is closer to the computation inside the scope than hnd. As we know reordering handlers could result in different semantics. For example, here, we essentially get the same result by running either hexc{hnd{mix1()}} or hnd{hexc{mix1()}}. Running

def main() = {
  val x = hexc{hnd{mix1()}};
  println(show(x))
  println("----")
  hnd{hexc{mix1()}};
}

gives

> main()
caught
Right(Cons(1, Cons(2, Nil())))
----
caught
Cons(Right(1), Cons(Right(2), Nil()))

Both 1 and 2 are in the result lists in both cases. This is because the order of the two handlers is fixed to be hnd{hexc{...}} for the computation in scope. However, when running hexc{hnd{mix1()}}, I would only expect 2 to be in the result list. I think this is the expected behaviour when hnd is the closest handler: the whole program crashes by raising an error, so 1 is discarded and only 2 is left. To see it more clearly, we can look at the following two programs.

def mix2() = hnd{hexc{
  if (do choose()) 1 else do raise("False!")
}}

def mix3() = hexc{hnd{
  if (do choose()) 1 else do raise("False!")
}}

Running them gives

> mix2()
Cons(Right(1), Cons(Left(False!), Nil()))
> mix3()
Left(False!)

It is clear that when hnd is closer than hexc, the result 1 is discarded.

I solved this problem for scoped effects in Bosman et al. by introducing an explicit forwarding clause to handlers. We get the expected behaviour in our calculus. Yang and Wu give a more general way to compose handlers for higher-order effects. (Btw, this problem is discussed in Section 7.1 and 7.2 in Bosman et al. using the state effect. However, I had trouble implementing the state effect using a parameter-passing handler without using mutable states. I wonder if it is possible to do this.)

To summarise, my main intuition when proper higher-order effects are more expressive than algebraic effects with impure arities is when composing different handlers with a preferred order / semantics.

Again, I'm not familiar with Effekt and please correct me if I made some stupid mistakes.

[b-studios]

Regarding 3)

I agree that it is not always desirable to duplicate p. Especially, since it will always be the same value. We chose this particular syntax / implementation, since it is very close to what we already had with bidirectional effects.

But maybe you are right and we should switch to something like

def twice[R](default: R) { p: => R / Nd } =
  resume { p() /* can only be called under resume */ }

where p can only be called under the resume. While this complicates the implementation of the type checker it might be easier to understand and reason about.

BTW I would write your example using yet another effect Yield, which gives us a bit more flexibility. However, the semantics here is different to your implementation since I do not (want to) invoke resume twice. Calling it twice duplicates the continuation, which I would assume is not desired here.

interface Yield[R] {
  def yield(value: R): Unit
}

def first[R](default: R) { p: => Unit / Yield[R] }: R = 
  try { p(); default } with Yield[R] {
    def yield(value) = value
  }

def all[R] { p: => Unit / Yield[R] }: List[R] = 
  try { p(); [] } with Yield[R] {
    def yield(value) = Cons(value, resume(()))
  }

interface Nd {
  def choose(): Boolean
  def once[R](default: R){ p : => R / Nd } : R
  def twice[R](default: R){ p : => R / Nd } : R
}

def hnd[R]{ f: => R / Nd }: Unit / Yield[R] = try {
  do yield(f())
} with Nd {
  def choose() = { resume(true); resume(false) }
  def once[R](default: R) = resume { { p: => R / Nd } =>
    first(default) { hnd { p() } }
  }
  def twice[R](default: R) = resume { { p: => R / Nd } =>
    first(default) { hnd { p(); p() } }
  }
}

def main() = all[Int] {
  var x = 0
  hnd {
    if (do choose()) { println("hi"); x = 0 }
    else { do twice(()) { println("hey"); x = x + 1 } };
    println("common continuation");
    x
  }
}

Regarding: 2) Higher-order vs. Impure arities

I see why you would expect 2 to be in the result list, since this is the behavior of dynamic (or traditional / algebraic / however you want to call them) effects and handlers.

However, in Effekt, in the example mix1 if you hover over catch you will see its signature is:

def catch[R] { p: () => R / { Exc } } { h: String => R }: R / {}
//                          ^^^^^^^                           ^^

This means it will handle the exception effect. This is no accident but fully intentional. In Effekt, we want to enable programmers to lexically reason about where an effect is handled (using type information). Since do catch is the lexically closest surrounding handler for Exc, we know that it will handle the do raise. We can reason about this locally and no reordering of handlers or any other change of the context will invalidate this.

We sometimes use the slogan: WYSIWYG. There should be no surprises about where something is handled. It should all be explicit from the types and the nesting of lexical scopes.

If you really want to raise the exception in the outer scope, you need to change the implementation of mix1:

def mix1() = {
  def outer[A](): A / {} = do raise("False!")
  //                  ^^
  //  makes sure it is not handled at the CALLSITE of outer
  do catch {
    if (do choose()) 1 else outer()
  } { msg => println("caught"); 2 }
}

Again, this choice is independent of the order of handlers, so in both cases it will abort and 2 will never be emitted.

Left(False!)
Cons(Right(1), Cons(Left(False!), Nil()))
()

Summary

So, I fully agree with you that the current design of effect operations taking block parameters can improved significantly (for instance by moving the block parameters from resume to the operation).

However, I would argue that the behavior you observe when reordering handlers is exactly the right one in the context of Effekt. The types truthfully tell you what handler will handle an effect and we should not break this promise.

[thwfhk]

Thank you for your patient answers again!

To disambiguate, I'll use the word "algebraic effects with impure parameters" to refer to the style of higher-order effects in Effekt, and use the word "higher-order effects" to refer to the style of higher-order effects following the line of work [1,2,3,4,5,6,7].

3

Probably I didn't explain what I wanted to do clear enough. For twice{p}, what I really want is to run p only once, and then resumes twice with the first two results of p. The intuition is that the twice operation is used in together with choose to cut the search space, so that we only keep the first two results from the nondeterministic program in a scope, instead of searching for all results. Resuming twice is expected; this is how we implement nondeterminism with effect handlers.

If I understand it correctly, your implementation did something different where the meaning of twice{p} is to run p twice but then only keep the first result.

I don't think the proposed new syntax can really solve this problem. Even though p is not duplicated here, we still need to execute p twice, which would lead to the same problem. I think the real restriction here is that p can only be called under resume. I agree that this restriction is totally desired in Effekt, because capabilities tell us to do this. However, I would say that this is a case where algebraic effects with impure parameters are less expressive than higher-order effects; with the latter we don't have this restriction and can easily implement twice.

2

This means it will handle the exception effect. ... Since do catch is the lexically closest surrounding handler for Exc, we know that it will handle the do raise.

I see. With this understanding in mind, it makes sense that both hexc{hnd{mix1()}} and hnd{hexc{mix1()}} give the same result, because it is not the handler hexc written here but the hexc introduced by catch that handles the raise operation inside catch.

We can reason about this locally and no reordering of handlers or any other change of the context will invalidate this.

I guess there might be some misunderstanding. Reordering handlers of different effects (usually) does not change which handlers handle which effects. Instead, it changes the semantics of effect interaction. It is still true in Effekt that reordering handlers would give different semantics. For example, just look at the mix2 and mix3 I gave before.

def mix2() = hnd{hexc{
  if (do choose()) 1 else do raise("False!")
}}

def mix3() = hexc{hnd{
  if (do choose()) 1 else do raise("False!")
}}

They give different results:

> mix2()
Cons(Right(1), Cons(Left(False!), Nil()))
> mix3()
Left(False!)

Also, running your implementation of mix1() with different handler orders also give different results.

Your implementation of mix1() also doesn't give me the semantics I want. What I really want (and what higher-order effects do) is to treat catch purely syntactically. That is to say, when executing hexc{hnd{mix1()}}, I would expect the both two things: (1) raise is caught by catch, and (2) the effect interaction follows the case when the handler order is hexc hnd.

I agree that this is the expected behaviour in Effect. This is also the expected behaviour when we simulate higher-order effects using algebraic effects with impure parameters in other languages. However, again, I would say that this is another case where algebraic effects with impure parameters are less expressive than higher-order effects; with the latter we can have both semantics of effect interaction easily by reordering, but with the former we can only have one of them (as the order is fixed to be hnd hexc).

Summary

However, I would argue that the behavior you observe when reordering handlers is exactly the right one in the context of Effekt. The types truthfully tell you what handler will handle an effect and we should not break this promise.

I fully agree that this is the expected behaviour in Effekt. I think capabilities work quite well in this setting since it makes things very clear! Moreover, I think it is a really nice observation that algebraic effects with impure parameters are related to bidirectional effects when we want to restrict where we can use these impure parameters. I'm looking forward to seeing the formalisation in your (ongoing) paper one day!

However, from my understanding, I would still argue that the higher-order effects in Effekt are not higher-order effects in the sense of [1,2,3,4,5,6,7]. Instead, they are algebraic effects with impure parameters. (To some extent, they are more similar to higher-order effects in the sense of 8 and 9.) Strictly speaking, they technically do not give us anything beyond the expressiveness of algebraic effects and handlers. By this, I mean

1. As shown by the previous two cases, it is less expressive than higher-order effects.
2. It seems not to be more expressive than the classical way of treating scoped effects as handlers as proposed in the very first work on algebraic effects by Plotkin and Power.
3. I understand that before this new feature it is impossible to have block parameters for algebraic effects in Effekt. It is very cool to support this and the type system looks quite nice! However, we can already encode all these things (both bidirectional effects and algebraic effects with impure parameters) in other languages with algebraic effects and handlers. For example, I implement the mix1 example in Koka as follows. Similar to Effekt, it gives the same result with different orders of handlers.

   
   rec effect aexc
   ctl raise(msg : string) : a
   ctl acatch(p : () -> <aexc, nd, div> a, q : string -> <aexc, nd, div> a) : (() -> <aexc, nd, div> a)

effect nd ctl choose() : bool

pub fun mix1() acatch(fn(){if (choose()) then 1 else raise("False!")}, fn(msg){2})()

val hnd = handler return(x) [x] ctl choose() resume(True) ++ resume(False)

fun haexc(f: () -> <aexc|e> a) : <|e> either<string, a> with handler return (x) Right(x) ctl raise(msg) Left(msg) ctl acatch(p, q) resume(fn(){ match (haexc(p)) Left(s) -> q(s) Right(x) -> x }) f()

pub fun main1() with haexc with hnd mix1() // output: Right([1,2])

pub fun main2() with hnd with haexc mix1() // output: [Right(1),Right(2)]

fun show( x : either <string, list> ) : string match x Left(a) -> "Left(" ++ a ++ ")" Right(b) -> "Right(" ++ b.show() ++ ")"

fun show( x : either <string, int> ) : string match x Left(a) -> "Left(" ++ a ++ ")" Right(b) -> "Right(" ++ b.show() ++ ")"

fun show( x : list<either <string, int>> ) : string x.show-list fn(x x.show()

I think the main advantage of algebraic effects with impure parameters in Effekt than other languages like Koka is that the types and capabilities are more clear. To properly encode everything in languages like Koka, we may need more features like more expressive effect subtyping than what Koka alreay has, and have to work with more complicated types.

On the other hand, I also don't think capabilities make Effekt incompatible with higher-order effects in the sense of [1,2,3,4,5,6,7]. It is a design choice whether to have them or not.

[b-studios]

Thank you for all your valuable comments and references.

3

Wow, that's a tricky one. We can only hack this together using mutable state, I guess:

```scala interface Nd { def choose(): Boolean def once[R](default: R){ p : => R / Nd } : R def twice[R](default: R){ p : => R / Nd } : R } def hnd[R]{ f: => R / Nd }: List[R] = try { [ f() ] } with Nd { def choose() = { resume(true).append(resume(false)) } def once[R](default: R) = resume { { p: => R / Nd } => hnd { p() } match { case Cons(el, _) => el case Nil() => default } } def twice[R](default: R) = { var other: Option[R] = None() resume { { p: => R / Nd } => hnd { p() } match { case Cons(el1, Cons(el2, _)) => other = Some(el2); el1 case Nil() => default } } resume { {p: => R / Nd} => other match { case Some(v) => v case None() => default } } } } def main() = { hnd { val res = do twice(0) { if (do choose()) { 1 } else { 2 } }; println(res) } } ```

which will output

1
2
Cons((), Nil())

You are right in that the proposed syntax will not really change this. Do you have an implementation in a language / calculus that does support higher-order effects?

2

What I want is to treat catch purely syntactically

Thanks, I understand now. I am just not sure I want this, though ;)

To be clear, I didn't mean to claim that the implementation in Effekt is more expressive (or even as expressive as existing calculi) -- this is rarely our motivation. Sometimes this happens by accident, but most of the time we purposefully restrict expressiveness. However, it is very important to be aware of the restrictions, so I am very grateful for all your explanations.

I am now convinced that we maybe should not call them higher-order effects. However, looking at the interface declaration they really are higher-order "operations".

Maybe "higher-order operations" is slightly less confusing...

[thwfhk]

3

I see! Yes, the implementation using mutable state indeed gives the semantics I want.

Do you have an implementation in a language / calculus that does support higher-order effects?

Yes, but it is just a simple prototype implementation used to show the main idea of Bosman et al. (The paper itself is also still under revision.)

I added the twice example to it which can be found at: https://github.com/thwfhk/lambdaSC/blob/main/test/twice.sc

2

I agree that it can be useful to restrict expressiveness in order to have clear types, semantics, or make it easier to reason about. I think blocks and capabilities do a good job on it in your setting of higher-order effects.

However, looking at the interface declaration they really are higher-order "operations".

Yes, I think people also use higher-order effects / operations to mean different things. I just personally prefer to follow the terminologies used the in the existing line of work on scoped / higher-order effects; otherwise it is unclear what's the essential difference between higher-order effects and algebraic effects (with impure parameters).