-
Notifications
You must be signed in to change notification settings - Fork 56
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Caprese Alternative #211
Comments
One-page documentation about the dotty-cps-async compiler plugin here: https://rssh.github.io/dotty-cps-async/BasicUsage.html#direct-context-encoding-experimental. In short, when we see a method with implicit CpsDirect[F] parameters (can be with carrying, i.e., a method which returns context function), let's it Note that with an effect system, we can do better than dotty-cps-async: we can catch not application of Ok, not let's try to understand the approach described here as
Alternative encoding makes sense because using context functions for pure computations can be annoying, especially when we have many effects. I can imagine this as syntax sugar on top of Capreso's capabilities. Could this be semantically different from capabilities (?)—need to think. (Find an illustrative example.)
Interesting. I will think about this. A helpful step might be to write a few simple examples in such a hypothetical style and compare them with other approaches. |
also, after some thinking, I can't understand the example.
If the result type of
UPD 1: Now I understandAxx, things changes when you start thinking that pure should mean 'monadic' or
Ok, The difference is the result type. In dotty-cps-async compiler plugin returns the result type visible to the user as return type, therefore we receive
in proposed syntxt:
This solves the problem of (choosing a type of coloring), which appeared when using the cps-async-plugin: you always have two ways of writing a function, in the direct style or monadically. Result types are different; therefore, if you write a library, you should know what result types are preferable to the clients of these libraries. Proposed encoding solves this problem on the price of changing the function signatures and possibly changing the core typing rules for monadic. There exists yet one interesting way of interpretation (this can be a special case for a set of implicit conversions. enabled inside effect-gathering function). UPD 2I.e. if we have enabled implicit conversion from F[Int] to Int inside effect-gathering function (or for each operation on int write a wrapper operation over F[Int] with the same number of parameters), then this will become possible in the current scala after typing:
In such case this will be possible with macro-annotations. Upd 4(Sorry for the set of updates, it's reflect that I'm slow) Interesting, that this functionality was already implemented in the dotty-cps-async as automatic coloring. And later - dropped in the favor of direct context encoding. (some history is https://github.com/rssh/notes/blob/master/2021_06_27_automatic-coloring-for-effects.md and current state is here: https://rssh.github.io/dotty-cps-async/AutomaticColoring.html It's. was dropped for social reasons: people were afraid to use it, despite of existence of preliminary analysis which flags incorrect usage. Your idea is solving this too: when we have a Purifier[F] in the scope, then another usage (i.e., map, passing as parameters, etc.) is illegal, so probably fear of incorrect usage will be eliminated. |
Upd.5. (will switch to many-comment mode) If we want implement this in macros (i.e. after typing), we have two visible problems (except need for extra Purifier) clause:
Implicit conversions for satisfying typer will be inserted in
Macros can insert a call to effect here, but a compiler with enabled '-Wnounit-statement -Wno-value-discard' will produce warnings (Maybe in lucky way this warning are after inlining -- need to check). Hmm, maybe for lucky cases, we need even 'after typer' because of macros (but not annotation macros). can be transparent inline, which works inside typer. |
hey @rssh! Nice to see you here :) Thank you for your work on Yes, Caprese and Kyo are solutions in the same domain and thus share major similarities. For example, Caprese's Capabilities is equivalent to Kyo's pending effect set and both require a suspension mechanism. It's a bit difficult to form a complete picture of Caprese so I'm basing this reply on this recent talk. The fundamental issues I see with Caprese's design are how prescriptive and restrictive it is while still not addressing the two main challenges it sets out to solve: 1. Effect Composability Building an effect system where multiple effects can be composed in a safe and principled way is quite challenging. It's necessary to ensure handlers are pure and impure code doesn't introduce invalid control flow when effects are handled. Caprese's current design does not address that. Handlers are based on impure short circuiting via exceptions and mutable internal state. Examples from the talk: // Impure short circuiting via exceptions
object boundary:
final class Label[-T]
def break[T](value: T)(using label: Label[T]): Nothing =
throw Break(label, value)
inline def apply[T](inline body: Label[T] ?=> T): T = ...
end boundary
// Handlers rely on mutable internal state
trait Produce[-T]:
def produce(x: T): Unit
def generate[T](body: () => Unit) = new Generator[T]:
def nextOption: Option[T] = step()
var step: () => Option[T] = () =>
boundary:
given Produce[T] with // handler
def produce(x: T): Unit =
suspend[Unit, Option[T]]: k =>
step = () => k.resume(())
Some(x)
body
None This approach to effects does not compose. If both boundaries and generators are used in the same computation, the behavior seems undefined since Caprese doesn't even offer a way to handle the fact that the continuation itself might have other effects. The solution doesn't seem useful other than in non-nested and locally-scoped handlers. It also doesn't enable programming with values in the FP sense and relies on fragile control flow primitives instead. For comparison, here's the equivalent in Kyo: // a pure and composable boundary/break effect in Kyo
class Boundary[V]() extends Effect[Boundary[V]]:
opaque type Command[T] = Left[V, Nothing]
def break(value: V): Nothing < Boundary[V] =
suspend(this)(Left(value))
def run[T: Flat, S](v: T < (Boundary[V] & S)): Either[V, T] < S =
handle(handler, v)
private val handler =
new ResultHandler[Const[Left[V, Nothing]], [T] =>> Either[V, T], Boundary[V], Any]:
def pure[T](v: T) = Right(v)
def resume[T, U: Flat, S](
command: Left[V, Nothing],
k: T => U < (Boundary[V] & S) // notice the continuation as a pure function
) = command // short circuit by ignoring the continuation
// pure generators (borrowed from @kitlangton)
class Generators[Input: Tag, Output: Tag]() extends Effect[Generators[Input, Output]]:
opaque type Command[A] = Yield[Input, A]
case class Yield[Input, Output](value: Input)
def yield_(value: Input): Output < Generators[Input, Output] =
suspend(this)(Yield(value))
def run[Input: Tag, Output: Tag, T: Flat, S](
value: T < (Generators[Input, Output] & S)
)(
handler: Input => Output < S
): T < S =
val h = new Handler[[T] =>> Yield[Input, T], Generators[Input, Output], S]:
def resume[T, U: Flat, S2](
command: Yield[Input, T],
k: T => U < (Generators[Input, Output] & S2)
) =
handle(
handler(command.value)
.map(output => k(output.asInstanceOf[T]))
)
handle(h, value) Another important difference between Caprese and Kyo at the current phase of the projects is that both these implementations are already fully functional in Kyo without the need for any language changes and in a purely functional manner. 2. Effect Suspension Caprese's answer to how to introduce suspension is still unaddressed. Its design locks in to a significantly more limited form of suspension than Kyo's that can only be provided by an underlying runtime: // Caprese's runtime-based suspension API
class Suspension[-T, +R]:
def resume(arg: T): R = ???
def suspend[T, R](body: Suspension[T, R] => R)(using label: Label[R]): T Note how the methods return values directly, which means the suspension can only happen by pausing the execution in the runtime itself. In Kyo, suspensions use the typical building block to perform suspensions: monads. I believe other languages like Unison and Koka adopt a similar approach and model the execution of algebraic effects on top of a monadic runtime. Caprese's design seems to come from a misconception regarding the performance characteristics of monadic runtimes. Fine-grained effect suspensions like what Kyo and Caprese want to offer would have significantly worse performance using Loom's suspension for example. Although I'm a big fan of Loom and think it's one of the major improvements of the JVM in recent years, it seems only appropriate for coarse-grained effects like async, where its overhead is generally acceptable. In contrast, Kyo's suspensions are pure values: // Kyo's pure value-level suspension
def suspend[E <: Effect[E], T](e: E)(v: e.Command[T])(
using _tag: Tag[E]
): T < E =
new Root[e.Command, T, E]:
def command = v
def tag = _tag This characteristic enables a more powerful form of suspension. Handlers receive a regular function as the continuation, which provides a high degree of freedom. Essentially, it enables proper multi-shot continuations. In addition to the more flexible algebraic effect mechanism, Kyo's monadic encoding has significantly better performance than traditional effect systems. Conclusion Caprese's current work seems to prioritize defining APIs and abstractions over addressing the main challenges of the problem. While this approach may help iterate quickly and produce papers, it seems to be leading to major limitations. The work on this ticket is intended to provide an alternative that works seamlessly with Kyo and other effect systems rather than baking in an impure effect system in the language, which can't be reused by them. Addressing first-class support for purity is also a necessary step to make the transformation from direct to monadic in a principled way. |
I was thinking about your suggestions and I’m afraid it’d be too fragile to do that via macros and implicit conversions. The usability wouldn’t be great since it wouldn’t be able to prevent mistakes and macros can’t express the effectful type mechanism properly. Maybe we should aim for a plugin directly. The purity check would also be necessary. I’ve taught newcomers to use Kyo and one of the first things they normally do is mix impure code. The direct syntax seems to encourage that given the similarities with other languages. |
A purity check can be implemented in macros (we have all trees there, so it's relatively easy). Also, I forgot about the third problem, which is inferring function type via the last expression in the block. So yes, implementing on top of implicit conversion is more fighting with existing typing than developing. Thinking about finding another way of typing |
If we want to escape implicit conversion, we should change the primary representation of effect total values to be compatible by assignment with its result. (Also, the idea to have a type defined differently in different compile-time environments, but it look like this required a huge amount of boilerplate) Two possible variants of typing should be used instead of IOs[A]. I see now: |
I think we'd need to change the type inference of effectful types via a research plugin for the proposed solution to have a reasonable usability. I wonder if it's really very complicated since
Both options do not seem viable. The fundamental impedance mismatch between Kyo and Caprese/Capabilities is that Kyo uses suspended computations as pure values. A type like |
For the programmer. |
I.e. exists 3 options:
(can we find more ways to choose from ?) |
@rssh thank you for following up on this! I was taking a look at capabilities and, besides the issue with it not being designed to represent monadic effects, there are some important usage patterns of the pending effect set in Kyo that might not be possible to express with capabilities: 1. Restricting EffectsSome methods in Kyo require restricting the effects that are allowed to be present in a computation. This is an essential feature to have proper support for fibers for example since forking with effects requires special handling. The object Fibers {
def init[T, S](v: => T < (Fibers & S))(
using
@implicitNotFound(
"Fibers.init only accepts Fibers and IOs-based effects. Found: ${S}"
) ev: S => IOs,
f: Flat[T < (Fibers & S)]
): Fiber[T] < (IOs & S) = ...
} When this method is called with effects that aren't Something remarkable about this approach is how it offers a mechanism similar to Rust's borrow checking to ensure safe use of state but without the significant usability issues that comes with it. 2. Aliased Effect SetsSince Kyo's pending type leverages the type system itself, it's easy to refactor sets of effects using regular type aliases: type Databases = Envs[Database] & Aborts[DBException] & IOs
def countPeople: Int < Databases = Envs[Database].use(_.countPeople) This approach becomes even more powerful when paired with opaque types. For example, the opaque type Resources <: IOs = IOs
val a: Int < (Databases & Resources) = Resources.acquire(new Database).map(_.countPeople)
val b: Int < (Databases & IOs) = Resources.run(a) Note how 3. Parametrized EffectsKyo offers effects with a type parameter like def t1(v: Int < Envs[Int & String]): Int < Envs[String] =
Envs[Int].run(1)(v)
def t2(v: Int < (Envs[Int] & Envs[String])): Int < Envs[Int] =
Envs[String].run("s")(v) ConclusionI'm not convinced that Capabilities are reusable in Kyo and I think it's likely they'll require major redesigning to achieve reasonable usability. If we build the plugin on top of it, we risk degrading user experience and maintaining the plugin can become quite challenging as Capabilities will likely still have major changes. That said, capture checking would still be valuable in Kyo since it'd enable a safer |
I don't know the compiler's internals but wouldn't it be possible to treat |
The question - how we would know without typer, that we extract something from monad or we use plain values?
Is impossible, because Of course, we can reuse
And if we have syntax for extracting value from some monads, we don't need a { 'pure' , 'effect-gathering' } markers for functions: if we use Syntax-only way is cool ;). But how is it suitable for kyo goals is unclear. |
Yet one way - think that in effect-gathering function any non-constant value is wrapped in a monad (and use |
good point! I've been discussing this proposal with other people and a common concern is the lack of an It seems with this approach we wouldn't need |
I'm not sure what you mean by this but I don't foresee any performance issues with the translation. It'd be Kyo's regular monadic composition under the hood, which is efficiently executed. |
translation:
|
It's still not clear to me but I think you're assuming that the transformation would need to lift all parameters into the monad? That wouldn't be the case, declaring which effects each parameter can have is an important aspect of how Kyo provides effects. What I'd expect of the transformation: pure def calc1(x: Int < Fibers, y: Int): Int < Fibers =
await(x) + y
// translation
def calc1(x: Int < Fibers, y: Int): Int < Fibers =
x.map(v => v + y) pure def calc2(x: Int < Fibers, y: Int < IOs): Int < (Fibers & IOs) =
await(x) + await(y)
// translation
def calc1(x: Int < Fibers, y: Int < IOs): Int < (Fibers & IOs) =
x.map(v1 => y.map(v2 => v1 + v2)) // Kyo's map is equivalent to flatMap pure def otherFun(x: Int, y: Int): Int < Fibers = ...
pure def calc3(x:Int, y:Int, z:Int): Int < Fibers =
(x+y+z) * await(otherFun(x,y))
// translation
def calc3(x: Int, y: Int, z: Int): Int < Fibers =
otherFun(x, y).map(v => (x+y+z) + v)
I think we'd still need |
Ohh, in first comment (with askValue primer) I say, that some syntax form of monadic wrapping is needed.
If we use Fibers:
|
Type parameter is needed for case, when we want to call f form |
I think I understand now. Kyo is different from other effect systems because you don't need to lift pure values into the monad since any type |
Hmm, if we generate a copy of function, then we can do this after typing |
About variation of (1). [before typing]. Example with sum will be more verbose than I have wrote:
because before typing we don't know -- is '+' return us monadic value or not. |
So, among the options to most simple solutions that are very close to the original idea: Variant A: 4:
compiler after typing will generate
but we will fully remap it to normal 'virtual' representation in the near-generated method:
which eventually become
And old method will make compiletime-only. |
/bounty $2000 |
Bounty requirements:
|
@kitlangton I'm redistributing Kyo's bounties. Have you been able to work on this? If not, can you cancel the attempt? Thank you! |
Cancelling the bounty for now. This is still desirable but I don't think we'd be able to build something on time for 1.0. |
Caprese is a major risk for Kyo's progress. Its development has been happening with little involvement from effect system developers, the proposed abstractions don't seem principled in the FP sense of programming with values, nor are they reusable in Kyo, and it might end up baking in a concrete effect system into the language itself.
In order to provide a new avenue for Kyo's evolution that mitigates this risk, the goal of this ticket is to provide a research compiler plugin to enable seamless direct syntax. The plugin should be generic and reusable with other effect systems as an alternative to Caprese. Initial design idea:
First-class Purity
A key challenge when performing the transformation from direct syntax to monadic composition is the risk of impure code changing the execution control flow and making the transformation invalid. Kyo and other effect systems rely on the user's discipline to suspend any impure code in an
IO
effect, but that's an error-prone approach that requires a level of discipline newcomers are typically not accustomed to. The convenience of the direct syntax and similarities to solutions in languages like Python make misuse even more likely to happen.I've been thinking about the different ways we could introduce first-class support for expressing pure code in Scala to overcome this challenge. One alternative is introducing something like a
fun
keyword to be used in place ofdef
or defining a new kind of pure function likeT ~> U
instead ofT => U
(I think I saw something like that in Caprese some time ago). The main challenge of such approaches is being able to also express that a class constructor is pure.I'm leaning more towards introducing a new
pure
keyword to be used as a modifier for classes, constructors, and methods:It seems the rules for validating purity could be relatively straightforward:
pure
member can only invoke other members also marked aspure
, including constructors.pure
modifier, which includes standard library APIs, we could compile a static set of pure symbols and add it to the plugin.var
,try
,throw
, etc., would be disallowed in pure members.Effectful Types
Effectful types like Kyo’s pending type, ZIO, and IO would need to provide APIs the same way they do for for-comprehensions, with no need for an implicit
Monad
or specific interface. It's not clear to me what would be a good syntax to express them, but we'd need a way to mark the type parameter that specifies the "result" type of the computation:Effectful types would have special type-checking behaviors:
IOs(println(1))
for example.pure
by default, without the need for the modifier, although they may use impure code internally. The developers of effectful types would be responsible for ensuring their purity.With these building blocks, Kyo could be used in the following way:
Essentially, types like
Int < Fibers
,ZIO[Any, Throwable, Int]
, andIO[Int]
would behave asInt
in pure members. Any and every use of them implies a monadic bind by the syntax sugar transformation. An important imitation is that a pure member must use at most one effectful type, as it’s not possible to mix different monads like Kyo’s pending type and ZIO.Notes
dotty-cps-async
might have something similar. I saw a compiler plugin but I couldn't find documentation for it.The text was updated successfully, but these errors were encountered: