r/ocaml • u/TomosLeggett • 7d ago
Why can't we have side effect annotations?
One of the things I like about OCaml is that it doesn't force you to write purely functional code. You can mutate values, throw exceptions, perform I/O, and generally use imperative features when they're appropriate.
I also like that OCaml is fairly explicit about this. If you're passing a reference around or mutating a value, it's usually apparent from the code.
One thing I don't particularly like, though, is that there's no indication in a function's type of whether it performs side effects. There's no equivalent of a ! suffix or an effect annotation, so you can call a function without knowing that it might throw an exception, mutate some state, perform I/O, etc.
The only real way to find this out is to inspect the implementation or rely on the documentation, assuming the author has actually documented it.
I'm wondering whether this is primarily a technical limitation or simply a design decision by the OCaml team. What prevents the compiler from analysing a function's body and determining that it uses things such as raise, :=, ref, I/O operations, and other effectful constructs, then incorporating that information into its type? For example:
val foo : unit -> int ![IO, State]
Obviously, there are complications around higher-order functions, modules, abstractions, user-defined effects, and so on, but could some form of effect inference make it possible to distinguish pure functions from effectful ones?
I'd be interested to know whether this has been considered for OCaml, and whether there are fundamental reasons why it doesn't work well, or whether it's simply a deliberate trade-off in the language's design.
3
u/BluddyCurry 7d ago
This stuff quickly results in heavy mental and syntactic overhead. You start out with an idea that seems simple but then the annotations and complications multiply very quickly. The art is in finding a compromise that doesn't make the language too cumbersome to use, and is still backwards compatible and compatible with all the other features OCaml already has.
5
u/EpochVanquisher 6d ago
I would describe it as kind of an open research problem—to come up with was to express these properties in the type system without inflicting a lot of heavy mental / syntactic overhead.
The research takes a long time… you make a language, get a lot of people to use it, and find out what the implications are like 10 years later.
1
u/AvaJMM-or-AJ 6d ago
I think that the ways languages like Verse and Unison handle it are pretty good. And the Kyo framework in Scala has a pretty ergonomic system ass well.
6
u/kitaz0s_ 7d ago
very new to OCaml, but I believe OxCaml (Jane Street's fork) kinda approaches this through modalities rather than traditional effect rows (which is what you described in your example)
You can't really tag a function with arbitrary effects, but there's a built-in set of modal axes that you can use (e.g. tracking whether a closure is stateless vs stateful, or whether a reference is @ local vs @ global).
So your example might look more like:
val foo : IoHandler.t @ local -> (unit -> int) @ stateful
1
u/Vegetable_Bank4981 6d ago edited 6d ago
It’s cool but basically completely unrelated.
It is an example of how to add new opt in axes to the type system. But it can’t model effects and there’s no proposal to. Also no inference on these and again no plans for it.
2
u/forciblycreated 6d ago
It can model effects. Taking an `Io.t @ local` is equivalent to tracking that the function performs some `Io` effect. The effects are tracked as capabilities.
I agree you don’t get this for free with the built-in effect syntax, but the handled_effect library is a wrapper around the effect system which turns effects into local capabilities.
1
u/Vegetable_Bank4981 6d ago
Ok I hadn’t seen that, that’s extremely cool.
Means I need to give locality another look. It’s the part of oxcaml least obviously useful to me so I guess I underestimated it. Thanks for the correction!
2
u/spermBankBoi 6d ago
OP (and commenters) might find [this paper](https://dl.acm.org/doi/pdf/10.1145/3371116) interesting; I did at least. imo this approach is more sensible than a lot of the more popular ones (Eff, Koka) and still not all that verbose (thanks to implicit effect parameters)
2
u/mister_drgn 6d ago
OCaml has algebraic effects, which in several new, experimental languages (Koka, Unison, etc) do exactly what you're asking for. A function signature has to indicate when it produces unhandled effects, which include side effects. It's very cool, but also a lot more cumbersome for the coder.
Unlike in those languages, the algebraic effect implementation in OCaml doesn't touch the type system. There's no way to know whether a function produces such effects (I mean, no way from looking at the function's signature). And OCaml's existing functions that produce side effects aren't tied to the algebraic effect system at all. I think that's kind of a shame, but to be honest there's no way you could force all that on people. At the barest minimum, you'd need to release a new version of the language, while continuing to support the old version.
2
u/TomosLeggett 6d ago
It's very cool, but also a lot more cumbersome for the coder.
I wonder how Koka and Unison do it? I know the new "Roc" language that's just exited beta does it with predefined effects (as in you can't define your own effects I think) although I'm not too sure if I've got that right.
It's a shame really cause there must be an extraordinary balance between Haskell's "wrap everything in a monadic plumbing" approach which is ideologically pure but a pain for the developer and "let the developer do what they want" which is OCaml's practical but slightly loose solution.
2
u/mister_drgn 6d ago
Roc's new approach is actually a lot simpler than full algebraic effects. You mark a function with "!" to indicate that it either performs an effect or calls some other function that performs an effect. Whereas with Koka, etc, you mark a function with the particular effect that it performs (and the effect type system itself is rich, with polymorphic effects).
Beyond that, the meaning of an effect is different. In Roc, an effect is some side effect that's performed by your platform. For example, if you're using the terminal platform, it might be writing to or reading from the terminal. Whereas if you're using the web platform, it could be some web-based operation. In contrast, in Koka you can create custom effects to do just about anything, and you can write one function that performs the effect, and then call that from another function that handles the effect in whatever way you want to handle it (this idea is modeled after error handling, where a function can either handle an error in whatever way it wants, or pass it up the call stack). So effects are a useful tool for abstracting away complex code operations, similar to monads in languages like Haskell. In fact they are pitched as a monad replacement.
If you're interested in learning more about algebraic effects, I'd suggest reading the Koka language tour. It's not too long, and it's quite interesting I think. You could start here, and then follow the links that interest you: https://koka-lang.github.io/koka/doc/index.html
1
u/Tomus 7d ago
Drive by non ocaml user here but I believe this is what algebraic effects give you right?
6
u/Nearby_Couple_3244 7d ago
No. It kind of could if you had a typing system for them but for now there is none. Even then you would have to make sure you are never using regular effects
3
u/mister_drgn 6d ago
I just posted a response about this. This is one thing algebraic effects give you in some new, experimental languages like Koka and Unison. But algebraic effects in OCaml aren't tied to the type system, so basically they're just optional.
10
u/Vegetable_Bank4981 6d ago edited 6d ago
Effect typing is at the frontier of type systems research these days.
There are a few known ways to do it but they all have big drawbacks. Mostly it just doesn’t work well with the HM inference as is so you either need to annotate every effect or give up on all type inference across function boundaries. Both of which aren’t acceptable for ocaml.
Adapting HM to infer effect types without changes to module level inference is an open CS problem, there’s a phd in it if you’ve got an idea and a few years. Making it fast enough to use in a production compiler would be a second one.
Haskell does it with monads but it needs a runtime built for that, with pervasive lazy evaluation, also not gonna work for us.
Koka has shown how to do it with row polymorphism, which is probably where ocaml is headed. OCaml already has row polymorphism for objects so you can get a sense of it if you want. But it ends up being an axis on the type (actually on the arrow if that makes sense) of every function. Async is a kind of effect so if you’ve run into “function coloring” in terms of async rust or js it’s the same thing but with a “color” for every effect.
So the theory is there! But there is a ton of design work to get it into ocaml in a way that doesn’t break what’s good about ocaml. And then a lot of engineering to make inference performant which I’m not qualified to get into but I understand has some open questions of its own.