What changes would be required to the OCaml type system to make session types (or some kind of typestate) idiomatic?

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

Edit: Also a previous discussion on this forum: Is there a good way to encode linear types in OCaml?

Could you put links on these papers in your post for folks (like me) how are not familiar with the topic?

Nope! Not allowed to post more than 2 links, so better to not pick and choose. Search for “ocaml linear types” and “ocaml session types”.

Among what is available, it is worth checking out https://github.com/keigoi/ocaml-mpst and https://github.com/keigoi/linocaml — I think you are alluding to them in your message.

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.

2 Likes

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.

I should have lifted this restriction just now.

1 Like

FuSe approach is quite lightweight http://www.di.unito.it/~padovani/fuse.html

You can use this polymorphic variants trick for a variety of simple uses: https://kcsrk.info/ocaml/types/2016/06/30/behavioural-types/

Linearity encoded dynamically though.

4 Likes

great links, thank you!