The use-case for typestate or session types is very compelling to me, as it makes it possible to encode the correct order of a protocol in the type-system. What changes would be required to the OCaml type system to make session types (or some kind of typestate) idiomatic enough to be included in the standard library?
There are a lot of papers available on OCaml and session types. They all rely on either passing the session around manually and explicitly, or wrapping it in a monad (lenses etc) with some light syntax extension. The key point being to check everything during compilation and not runtime. From a quick glance, this all seems quite laborious, and prevent the technique to be widely used.
Is there any low-hanging fruit available to change to OCaml type system, to make typestate or session types more idiomatic and
Then there is Affe, an ambitious exploration into adding affine kinds to OCaml by Gabriel Radanne and Peter Thiemann, with session types as an explicit motivation: https://arxiv.org/abs/1908.09681. (It has just been updated recently.) One stumbling block is that it requires a lot of work to refactor/rewrite the OCaml typechecker (@Drup can correct me if I am mistaken or provide additional details).
Then there is my own survey and exploratory design on resource management for OCaml: https://arxiv.org/abs/1803.02796. One possibility is the expression of RAII-based typestate in the very idiomatic form found in the Rust language: http://cliffle.com/blog/rust-typestate/. First it assumes the existence of an affine kind system to build upon in the style of Affe (though it advocates against kind inference with hopes that this makes the work on the type system simpler). To that, it adds a notion of destructor that is guaranteed to be run even in cases of failure (it describes language abstractions and runtime implementation techniques, and leave questions about a type system open). Compared to Affe, it adds the ability to express something similar to Mostrous and Vasconcelos’s Affine sessions, whereby “sessions never get stuck” due to correct error-handling.
So there is a spectrum between “low-hanging fruits” and “idiomatic” as discovered and used in practice in Rust.
I’m pretty sure you can format the links as code (with backticks) to get around that restriction. They won’t be hyperlinked, but will be at least copyable.
About the changes to the type system, it would need to become “linear” or “affine”. I won’t write an unsolicited technical analysis, but I don’t think typing environments in OCaml can support this out of the box. One would need to control some structural rules, at least the so called “contraction” rule, which allows one to make “copies” of some x: T so that it can appear in multiple places in a typing derivation. This rule is implicit now: anything can be used zero or more times. It would have to be made explicit. And probably some syntax would be needed to distinguish linear or affine and unrestricted (the default, I’d guess).
Then there is the question of HM type inference. I don’t know the answer. Hopefully doable. But any adaptation to OCaml would need an inference algorithm…
It would definitely be an interesting extension. As for sessions, if you have the above stuff, they become easy to implement without some explicit encoding (chaining).
