A few years ago when OCaml 5.0 landed with effects, there was a lot of discussion about making them typed in a way that prevents unhandled-effect runtime errors. Back then, there seemed to be an impression that typed effects were coming soon and they would be a necessary improvement. If you look back at old discussions, there’s a lot of advice saying to avoid using effects until the typed version arrives.
In the years since then, a lot of new features have come to OCaml, but I haven’t heard any news about typed effects. At the same time, people don’t seem to have reservations about using untyped effects anymore (or if they do, they don’t express them as publicly as they used to).
I’m curious: is this still on the timeline somewhere? I’m also curious if there’s still a demand for typed effects now, since untyped effects seem to have gained traction on their own.
Was there really an impression that typed effects were ‘coming soon’? My understanding was always that they were mostly conceptual at that point and a lot of theoretical and academic work needed to be done for them to even reached POC stage. I don’t think anyone has so much as shown a demo?
Back when effects were first getting released, there was a lot of discussion where people said things like “wait to use effects until they’re typed,” “we don’t want to add a syntax for effects until they’re typed,” or “let’s wait for typed effects before we add features X Y and Z.” I don’t want to go dig up all of the exact quotes, but people then seemed to believe that typed effects were on the timeline. They certainly gave me the impression that typed effects were actively being worked on.
I’m fairly sure the messaging was more along the lines of ‘don’t use untyped effects directly in application code yet, use them indirectly via libraries like Eio that wrap their functionality’.
Maybe there was a communication gap that made people think that meant typed effects were on the way, but the way I see it, there are a lot of design issues to solve before that, not the least of which is that it would basically be ’checked exceptions’, and everybody hates those…
The only thing I would add to this discussion is that Jane Street is making progress on the related front of statically guaranteeing that effects are handled in OxCaml with modes. It’s not fully typed effects, but it is an interesting way of making effects much more usable in application code. They even have a library codifying the concept: GitHub - janestreet/handled_effect: Typed effects API for OxCaml · GitHub (where they call it “typed effects,” but I’m not sure that’s what most people would mean by it).
A couple years ago I tried to get people to work on typed effects specifically for OCaml, but I failed to gather steam and actually do it (apologies!). There are plenty of people in academia working on type systems for effects, but most of it is not directly applicable to OCaml. I don’t know of active projects to retrofit effects into OCaml (there is comparatively a lot more on effect via capability control in Scala, and also some energy going into Koka, Effekt, Lexa etc.), except of course for the work on modes in OxCaml.
I feel bad about this because I think that typed effects would be much more usable than untyped effects, but this is not a consensus position (some people say that because effects are more pervasives than exceptions in libraries that use them, we catch mistakes earlier in normal testing). And no one believes that retrofitting an effect system into OCaml would be easy.
Hmm… as a semi-official position, this is disappointing. I also thought untyped effects were sold as a springboard to typed effects somewhere down the line, but it seems like that’s not in the works. That makes me want to avoid effects even more outside of concurrency. In a world where every library utilizes its own effects all over the place, OCaml becomes a far less safe language.
I appreciate the insight. It’s slightly disappointing that the work doesn’t seem to be going anywhere (for OCaml at least) since typed effects always seemed like an intriguing feature to me.
I’m personally happy using the untyped effects we have now, but sometimes wonder about what effects could become in the future.
Sorry for the sarcasm, but this is to me the same as saying the same sentence, but where “effects” are replaced with “bugs”. Yes, let’s have more bugs so we can catch them early
Your response is tongue in cheek I guess - but the answer is that it’s possible to write a pure core logic in your programs and keep effects at the edges; OCaml has in my experience been excellent for this - and now much less so.
Interestingly, typed effects would in some ways enable this program structure even more than was the case before untyped effects.
I suspect for that purpose it would suffice to be able to mark functions as pure with an attribute. Whether it’s helpful to type functions with a polymorphic row type of the effects they demand seems like an open research problem to me.
I try to keep with the latest research on it, but if there’s been something conclusive published about that specific question yet then I would like to know.
I don’t think this is true. For example something like bytesrw which can be used to write what you’d call “pure core logic” and “keep effects at the edge” would be significantly less useful without effects regardless of whether they are typed or not. Without them it couldn’t be made to accommodate with non-blocking IO.
I’ve idly wondered what it would be like to use a standard library that’s exactly the same as the existing stdlib except all of the side-effects are replaced with algebraic effects. While that’s probably impractical, it might be nice to be able to write a custom effect handler for things like print_endline and take control over how those functions work. Then, in a fantasy world where we get typed effects, the whole language suddenly looks every different when every side-effect built on top of the stdlib is typed.
I have no idea if I want that hypothetical version of OCaml, but it’s interesting to think about.
Yeah this is an interesting difference of effects vs monads. In monads, you have to color effectful code. If you want code that’s polymorphic over monads, you have to explicitly make it so, and even then it’s not trivial to compose multiple effects. In an effect system, there’s no color. This means that you can have code that uses any number of effects or is polymorphic over effects - it’s all the same. So for maximum usability you’d want code that is permissive with regard to effects, rather than the default being purity. The code then gets structured a different way from how monads are. The root of the call graph is pure, and handlers introduce the scope of effectful code, much of which is polymorphic. At the edges, any effect can be added. The job of the effect system is to make sure no effect leaks out.
However, this is a very different paradigm from traditional purity, and we lose the nice properties of purity, such as optimization potential. If all code is effect-polymorphic by default, how much optimization can we even do? How many nice properties do we lose? And why would anyone ever want to deliberately lock down their code’s effects, thus making the code less versatile?
I don’t think these questions have different answers from what happens when you abstract behaviour with user provided functions, something that has always been in the language.
If you take the bytesrw example effects are only potentially done when you read/write a new byte slice which is just a function call. All the number crunching you do on the slices remain optimized as always.