I am calling it now - algebraic effects are the “next big thing.” The syntax for it in OCaml 5 is a little clunky, precisely because there’s actually not much syntactic support for it yet and it’s just implemented as a library. But, if you look at languages like Eff or Koka where the syntax is more integrated, the whole concept is very lightweight and solves a ton of problems.
Nitpick: I call them “effect handlers” rather than “algebraic effects”. “handlers” emphasizes the key property of effects, which is that you define their behavior (in the handler) separately from where you use them (in the handlee). And it suggests that they generalize exceptions (exceptions handlers), which is correct. On the other hand, the “algebraic” in “algebraic effect” comes from looking at equations expected to be satisfied by handlers, it is an idea that is important/influential in the theoretical circles that invented effect handlers, but it is in fact completely absent from the realization in practical programming languages, that generally cannot check that equations/laws actually hold.
(For monads, the community has realized that laws are important and that checking them, even on the nose, is useful. Maybe such a time will come with effect handlers as well. Note that non-free monads also quotient over some equations, so we don’t actually need explicit reasoning to enforce equations.)
I hear your point. I like to minimize the division between theory and practice, because I don’t really see them as different things. Algebraic effects are so useful exactly because of their algebraic properties, not in spite of them. The fact that those properties aren’t checked for in implementations is only relevant to me in the sense that implementations should make sure to follow the theory.
So coming up with a different name is an admission that they are separate things, which I don’t think they should be.
The fact that those properties aren’t checked for in implementations is only relevant to me in the sense that implementations should make sure to follow the theory.
It’s arguably worse than not checking the equations. There is no way to specify in the language what the equations should be. For monads and applicative functors (or other standard algebraic structures), the set of expected laws is fixed once and forall by the structure. For algebraic effects, each effect signature will naturally come with its own equations. Some signatures (Get,Set for example; or free monads) have a standard set of equations that would be expected, but many use of effect handlers in language that support them are for bespoke effect signatures where no one has tried to think about the expected equations.
Dependently-typed languages with a notion of quotient (or higher inductive types, etc.) give a natural way for the user to express equations – and to prove that they hold. Combined with effect handlers, you can work with “algebraic” effects. But without those… We could do with in-language support for equivalence assertions, that we could try to check dynamically for example. But OCaml, Koka don’t have those either.
This is a great nit to pick and I learned a lot from your comment. Eff wasn’t familiar to me before now so thanks for exposing me to that as well. Regarding your remark about integrated syntax, are there any examples of syntax which make writing effect handlers particularly ergonomic?
What would be the advantages of multi core ocaml over say rust?
OCaml’s compile speed blows Rust out of the water. Incremental development and edit-compile cycles are way shorter. Makes it much easier to try out code changes. Oh, and OCaml actually has a pretty good REPL which can conveniently load your working project and let you interactively explore it.
I don’t see them as incompatible or only currently slightly competing because of implementation details. Rust has a solid enough footing that other languages should start to have a Rust runtime or core. OCaml on Rust would get you the best of both worlds.
Many proof assistants support extraction, often to OCaml. Extraction is pretty much never a verified process though, mostly because OCaml doesn’t have a formal semantics, so it can’t be verified. So I wouldn’t say that OCaml has a “formal methods ecosystem.”
I agree that OCaml’s formal methods tools could be improved (languages like C or Ada have a better story), but I think you are unfair. WhyML was explicitly designed as a subset/dialect of OCaml amenable to formal verification, and feels very close to (imperative) OCaml programming – see Camleer as a tool to bridge the gap, without strong formal guarantees but it works nice in practice. So yeah, I would say that they are “strongly related”.
This being said, I also expect the verification tools for Rust to improve quickly, for example Creusot which is itself built on top of Why3 is rather impressive. Unfortunately the elephant in the room is unsafe: some Rust codebases will be amenable to formal verification, but I would suspect that a lot of Rust code in practice depends on unsafe to deeply for this to really work on everyday programs. In practice people that have verification in mind may end up designing projects from the start in “safe Rust” with, say, a non-standard library ecosystem.
I agree that they’re related, but I guess my point is that the whole ML family of languages is related in that sense. OCaml can surely be part of a formal ecosystm - in fact I intend on using a verified interpreter in OCaml for my own language project that I’m working on. So I’m being a bit pedantic - the verification isn’t done on OCaml itself, but rather OCaml is the final result of a verified project.
I have nothing against extraction. My point was that there is no real formal methods ecosystem for OCaml, and that verification is done in other languages.
Extraction works well enough in practice. I mentioned this elsewhere in the thread, but I’m planning on using extraction to create a verified interpreter for a language project I’m working on.
As far was what my preferred alternative is, I am partial to model-based test case generation. At least at some point in the workflow, because there is always a point past which there are no formal semantics so you can’t even do true verification. And even if there were, testing is a lower-cost investment.
Could somebody explain what specifically effects are? I am a little out of practice but understand the idea of monads as a concept, and I have read that effects are a generalization of exceptions - I took a look at the ocaml documentation for it but it isn’t exactly easy reading.
I am calling it now - algebraic effects are the “next big thing.” The syntax for it in OCaml 5 is a little clunky, precisely because there’s actually not much syntactic support for it yet and it’s just implemented as a library. But, if you look at languages like Eff or Koka where the syntax is more integrated, the whole concept is very lightweight and solves a ton of problems.
Nitpick: I call them “effect handlers” rather than “algebraic effects”. “handlers” emphasizes the key property of effects, which is that you define their behavior (in the handler) separately from where you use them (in the handlee). And it suggests that they generalize exceptions (exceptions handlers), which is correct. On the other hand, the “algebraic” in “algebraic effect” comes from looking at equations expected to be satisfied by handlers, it is an idea that is important/influential in the theoretical circles that invented effect handlers, but it is in fact completely absent from the realization in practical programming languages, that generally cannot check that equations/laws actually hold.
(For monads, the community has realized that laws are important and that checking them, even on the nose, is useful. Maybe such a time will come with effect handlers as well. Note that non-free monads also quotient over some equations, so we don’t actually need explicit reasoning to enforce equations.)
I hear your point. I like to minimize the division between theory and practice, because I don’t really see them as different things. Algebraic effects are so useful exactly because of their algebraic properties, not in spite of them. The fact that those properties aren’t checked for in implementations is only relevant to me in the sense that implementations should make sure to follow the theory.
So coming up with a different name is an admission that they are separate things, which I don’t think they should be.
It’s arguably worse than not checking the equations. There is no way to specify in the language what the equations should be. For monads and applicative functors (or other standard algebraic structures), the set of expected laws is fixed once and forall by the structure. For algebraic effects, each effect signature will naturally come with its own equations. Some signatures (Get,Set for example; or free monads) have a standard set of equations that would be expected, but many use of effect handlers in language that support them are for bespoke effect signatures where no one has tried to think about the expected equations.
Dependently-typed languages with a notion of quotient (or higher inductive types, etc.) give a natural way for the user to express equations – and to prove that they hold. Combined with effect handlers, you can work with “algebraic” effects. But without those… We could do with in-language support for equivalence assertions, that we could try to check dynamically for example. But OCaml, Koka don’t have those either.
This is a great nit to pick and I learned a lot from your comment. Eff wasn’t familiar to me before now so thanks for exposing me to that as well. Regarding your remark about integrated syntax, are there any examples of syntax which make writing effect handlers particularly ergonomic?
I think Eff has the most minimal syntax. Here’s an example with printing, which for example would be done using Monads in Haskell:
You can see more examples here: https://www.eff-lang.org/try/
I think people have been saying algebraic effects are the “next big thing” for a number of years now.
Yes but during that time, I didn’t believe it. Now I do!
Maybe it + multicore will be enough to mainstream OCaml so we can Go out of the Rust we’re in?
What would be the advantages of multi core ocaml over say rust? Does ocaml have a non-garbage collected lifetimes based form of memory management?
OCaml’s compile speed blows Rust out of the water. Incremental development and edit-compile cycles are way shorter. Makes it much easier to try out code changes. Oh, and OCaml actually has a pretty good REPL which can conveniently load your working project and let you interactively explore it.
I don’t see them as incompatible or only currently slightly competing because of implementation details. Rust has a solid enough footing that other languages should start to have a Rust runtime or core. OCaml on Rust would get you the best of both worlds.
It would also require a hard dependency on the LLVM and Rust toolchains to bootstrap, which would add a huge amount of complexity.
Which is why Rust needs to have a non-LLVM bootstrap path. LLVM is too big to fail at this point, or too big to compile, or both.
I’d like to see a boostrap path that goes through Wasm where we could bootstrap the whole ecosystem in under 1MLOC.
No. But there’s, of course, no silver bullet. So non-garbage collected lifetimes as a memory management is not for everyone.
That you don’t have to use Rust, and you get effects handlers, and OCaml’s type system.
OCaml has a fantastic formal methods ecosystem, e.g. WhyML.
Since it’s more of a high-level language, verified code is simpler to achieve.
In what way is Ocaml directly related to WhyML?
Stating the obvious: Drop the “Why” and the “Oca” and you have “ML” in both.
But, re-stating some info from the Why3 page:
Many proof assistants support extraction, often to OCaml. Extraction is pretty much never a verified process though, mostly because OCaml doesn’t have a formal semantics, so it can’t be verified. So I wouldn’t say that OCaml has a “formal methods ecosystem.”
I agree that OCaml’s formal methods tools could be improved (languages like C or Ada have a better story), but I think you are unfair. WhyML was explicitly designed as a subset/dialect of OCaml amenable to formal verification, and feels very close to (imperative) OCaml programming – see Camleer as a tool to bridge the gap, without strong formal guarantees but it works nice in practice. So yeah, I would say that they are “strongly related”.
This being said, I also expect the verification tools for Rust to improve quickly, for example Creusot which is itself built on top of Why3 is rather impressive. Unfortunately the elephant in the room is
unsafe: some Rust codebases will be amenable to formal verification, but I would suspect that a lot of Rust code in practice depends on unsafe to deeply for this to really work on everyday programs. In practice people that have verification in mind may end up designing projects from the start in “safe Rust” with, say, a non-standard library ecosystem.I agree that they’re related, but I guess my point is that the whole ML family of languages is related in that sense. OCaml can surely be part of a formal ecosystm - in fact I intend on using a verified interpreter in OCaml for my own language project that I’m working on. So I’m being a bit pedantic - the verification isn’t done on OCaml itself, but rather OCaml is the final result of a verified project.
One can extract correct-by-construction OCaml programs from WhyML.
Yes but the verification is done in WhyML, and there is no formal verification of the extraction process.
That’s correct, I’m afraid. What’s your preferred alternative?
I have nothing against extraction. My point was that there is no real formal methods ecosystem for OCaml, and that verification is done in other languages.
Extraction works well enough in practice. I mentioned this elsewhere in the thread, but I’m planning on using extraction to create a verified interpreter for a language project I’m working on.
As far was what my preferred alternative is, I am partial to model-based test case generation. At least at some point in the workflow, because there is always a point past which there are no formal semantics so you can’t even do true verification. And even if there were, testing is a lower-cost investment.
Could somebody explain what specifically effects are? I am a little out of practice but understand the idea of monads as a concept, and I have read that effects are a generalization of exceptions - I took a look at the ocaml documentation for it but it isn’t exactly easy reading.
I was wondering the same thing and found this article and the Koka Book helpful.
If you are familiar with Common Lisp conditions they seem similar.