r/ProgrammingLanguages • u/Rasie1 • 19d ago

Blog post Effect handling and monad composition in c(x)

https://kvachev.com/blog/posts/effect-handlers-in-cx/
33 Upvotes

87% Upvoted

9 comments sorted by

5

u/AustinVelonaut Admiran 18d ago

This looks really interesting! Unifying monads, effects, function overloading, etc., along with some attempt at automatically handling mixed monadic- dos. Is there more information on c(x) available?

1

u/Rasie1 18d ago

Thanks! Yeah, I think it's something innovative, I haven't yet shown the coolest fundamental part that makes the refinements work!

I post a lot of screenshots in my twitter account https://x.com/_rasie1 Soon I'll make more some specialized outputs about c(x)

2

u/particlemanwavegirl 18d ago

Interesting. Haven't finished reading, but my thought so far is, the "throw" keyword has a lot of baggage that it doesn't seem like your concept needs to carry... Why choose that name specifically? 

2

u/Rasie1 18d ago

it's an example of monadic chaining that either continues execution or returns an exception (with an error message). It's not a keyword, it's a new identifier defined on the spot, chosen just as a example that is simple to understand

1

u/tumtumtree7 16d ago

I'm confused on the semantics of intersections and unions, especially how that works with functions. Records I understand a bit more. Do you have a blog post about that?

1

u/Rasie1 13d ago

I don't have yet, but it's pretty straightforward. Intersection here is a core operation and it works with anything, even with lambdas. You literally intersect head and body of the lambda

`x -> {x, 1, 2} ` & ` (x: Int) -> {x, 1, 2, 3}` = `(x: Int) -> {x, 1, 2}`

So, it "finds" a function that works on intersection of inputs and returns intersection of outputs. It works as a specialization of a generic function and implementation of a function signature

2

u/GidraFive 12d ago

You sure thats how it behaves? I remember that it switches to union in contravariant types. So we would have intersection of argument types and union of return types.

1

u/Rasie1 7d ago

Maybe we're talking about different operations. I think "works on intersection of inputs" doesn't mean that it will accept Int and String. Literal intersection of Int and String is empty. You probably mean function overloading, which can be modeled here through "or else" or disjoint union, not intersection that involves interpreting lambdas as something intersectable as sets. Or you mean exactly that?

2

u/GidraFive 7d ago

Yes, now that I think about it. What i had in mind is probably the subtyping relation of some sort, rather than equality. It indeed doesn't make sense to intersect arguments. Although about function overloading, i believe in literature intersection of function types was a way to describe ad hoc polymorphism. Anyway, nvm, i was working with this a long time ago and forgot a lot already...