Has anyone considered the idea of using the contex...

# language-evolution

[Exerosis]

Has anyone considered the idea of using the context rewrite as an excuse to enable kotlin as an algebraic effects language.
it's ig a bit too late in the sense that it has invisible throws and suspend is a keyword but you could just make the use of those warnings.

[Youssef Shoaib [MOD]]

Checkout https://github.com/kyay10/KonTinuity (I'm the author)
It implements multishot delimited continuations, which famously are used to implement algebraic effects.
It then builds a lexical effect system on top of that. It's all based on effekt-lang.org, and so a lot of their research applies there, including the fact that, for most cases, context parameters will basically tell you what effects something does. My dream is to eventually use the rest of their research (especially their paper about scope-based reasoning to type-based reasoning and back) to add a checker on top that checks effect usage to prevent e.g. effects escaping the scope they're declared in.
Keep in mind though that for most cases such a system isn't strictly necessary, especially when dealing with these lexical effects because runtime errors happen very clearly if an effect instance escapes and is used then, and so runtime checks mostly suffice here.
suspend being a keyword isn't that big of a deal. It really just marks effectful functions, while non-suspend functions are pure and side-effecty ones.
throw really isn't that big of an issue either, it's really just an implicit effect given to all functions. Also, if you just restrict yourself from using it and instead use something like Arrow's Raise, then you get back effect safety.

[Youssef Shoaib [MOD]]

I think btw that effekt-lang has very similar design goals to Kotlin and hence it fits so well. Its usage of scopes, evidence/capability passing (which we do explicitly through context parameters), and generics makes it work pretty well. Especially because of generics I think lexical effect handlers are the only effect system that'd work for Kotlin (btw, just because they're lexical doesn't mean there's no dynamic nature to them. One can still intercept and rehandle effects if the effect itself allows you to do so, although I personally haven't found that to be very helpful vs just using parameterized handlers).
You should also have a look at the predecessor to effekt-lang, which was an implementation in Java using some bytecode instrumentation magic. That one survives just fine without checks for effect escaping.

[Youssef Shoaib [MOD]]

Just some final thoughts: I don't think that algebraic effects need official support from the language. In fact, the language already has most of the necessary things to implement them, including the necessary compiler plugin mechanisms to implement an extra checker for more effect safety. Context parameters, interfaces, and suspend are already enough for most of what you want to do. The only official support I'd really like to have is for continuation cloning. Currently in the library above, we use reflection to achieve that, but that limits us to JVM and JS for multishot use cases. A tiny API with just a couple of operations for cloning compiler-generated continuations is everything that's needed to make the library work the same across all Kotlin platforms.

Also, regarding the extra effect safety I keep harping on about. I believe this extra effect safety can be achieved with some mechanism for resource safety in the language. In other words, if Kotlin adds something in the type system that prevents resources escaping, then (I conjecture) that should solve all the issues with effect safety and guarantee that all programs are effect-safe (unless they use explicit escape hatches of course).
A resource safety mechanism like that is applicable to more than just algebraic effects though. My belief about this comes from the literature that explores effect safety (and delimited continuation safety). They all seem to end up implementing or using some form of resource safety (e.g. monadic regions in Haskell).

[Exerosis]

Wow sorry for the delay been a bit busy. I'll have to look through the source. I was playing around with multishot at one point while writing a networking library but didn't think it was actually possible (didn't try reflection or anything)
I figured that without "variadic generics" it would be hard to implement method that passes on it's effects.

[Youssef Shoaib [MOD]]

Absolutely fine on the delay! Would be excited to hear any feedback once you've played around with it! Variadic generics (i.e higher kinded types) end up not being needed because we don't explicitly use any free monad or anything. suspend is basically a built-in monad with direct-style monad comprehensions if you will. Delimited continuations is the technical term for this, and they're widely used to implement effects. A language that supports delimited continuations directly (like Kotlin) doesn't need HKTs or Monads or anything like that. Instead, "evidence" or "capability" passing is used through context parameters so that one can define an interface like:

fun interface Amb {
  suspend fun flip(): Boolean
}

and an effectful function that uses `Amb`is just:

suspend fun Amb.drunkFlip(): String {
  val caught = flip()
  val heads = if (caught) flip() else error("too drunk")
  return if (heads) "heads" else "tails" 
}

You could also use context parameters instead of an extension receiver here
An implementation of Amb can be defined as:

private suspend fun <R> selectAll(block: suspend Amb.() -> R): List<Result<R>> = buildList {
  handle {
    val amb = Amb {
      [e-mail] { resume ->
        resume(true)
        resume(false)
      }
    }
    add(runCatching { block(amb) })
  }
}

and running with that implementation produces [Success(heads), Success(tails), Failure(java.lang.IllegalStateException: too drunk)]
The effects are passed on implicitly because of context parameters and receivers. There is the issue of effects escaping, which I've talked about above, but in short it's currently a runtime exception, but it's doable to make a compiler plugin that reports errors when that happens (and doesn't modify any code at all, so it's just a linter really). It's easy enough to spot those errors usually, and so it's not a big problem (and other languages with effects like Ocaml for instance don't have it)

[Exerosis]

Hmm, okay, I'm somewhat new to the entire theory. Can you explain to me two things:
1. Do none of the DSL annotations help with escaping (since IIRC they limit calling "dsl functions" to the first scope right?)
2. Is there simply NEVER a need for anything like this? On paper I think I agree with you but I feel like there might be cases where expressing this matters because it's not "effectively inline"

context(Others...) fun <From, To> List<From>.map(
   mapper: context(Others...) (From) -> (To)
) = ...

https://gitlab.com/ballysta/architecture/-/tree/4.0.2/src/main/kotlin/com/gitlab/ballysta/architecture?ref_type=tags
I've been sort of refining this concept of a "component engine" for a long time. When I learned about algb effects and their relationships to continuations and context I started wondering if this idea of "Toggled" can be represented as an "effect" and what the pros and cons of that would be.
I'm still too new to the whole thought process (and traditional solutions) to provide effective feedback. But the scala discord has a lot of cool people including one of the guys behind https://www.unison-lang.org/ which explained alg effects to me 🙂
I plan to fork your repo and play around a bit over the weekend though, I certainly want to play with multishot in kotlin that's extremely cool tech 🙂

[Youssef Shoaib [MOD]]

1. Sadly no they don't help with escaping. I think arrow-analysis has some basic stuff to help with that with Raise, which can be adapted for this too, but it might have a lot of false negatives (since the whole point is to capture the HandlerPrompt inside of an object
2. There is never a need for that really, unless we're dealing with complicated usages of functions-as-values and such. Basically, right now no escape analysis happens, and so the mapper just has access to the contexts it already had. When such an escape checker is made, functions would have to explicitly say that they don't preserve the same context (although I have some ideas to do that automagically. For instance, the calls-in-place contract seems to specify exactly that, so the escape analyser can use that as a signal to consider that an escape. Again, the point ultimately is to build a resource escape checker). There is a paper about this from the effekt-lang people called something like "Effects as Capabilities", and another one called "From scope-based to type-based reasoning and back" which discuss this idea. Roman Elizarov, the previous language designer, said before that explicit effect polymorphism (that Others... thing you're talking about) isn't really a good fit for mainstream languages, and that paper expands on that by completely hiding away effect polymorphism, and instead letting you reason thru `context`s, until you need to e.g. store a lambda somewhere, then the lambda has an explicit type annotation as to what effects it needs

[Exerosis]

Ah okay that does make sense, I do see why it wouldn't be a good fit. That said I do feel like varadic generics WOULD be a good fit and I don't see why they wouldn't also resolve the problem. Do you have a link to the paper in question?

[Youssef Shoaib [MOD]]

https://dl.acm.org/doi/10.1145/3428194 and https://dl.acm.org/doi/10.1145/3527320

[Youssef Shoaib [MOD]]

Btw, I'm working on an alternative presentation of this system that uses @RestrictsSuspension to ensure effect safety, although it's a little annoying to use due to the type inference just giving up sometimes. I'm basically doing monadic regions, and so effectful operations have a type variable that refers to the region they need to operate in. Also note that there's unsoundness bugs with @RestricitsSuspension that allows one to escape such safety, but usually it's hard to just "stumble" on that, and they should be fixed eventually regardless.