Session Types in Elm

[d4hines]

Hi all,
I’m new to Elm, and relatively new to type theory. Has anyone played with session types in Elm? I.e, the stuff out of http://groups.inf.ed.ac.uk/abcd/index.html
Thanks,
Daniel Hines

[rupert]

Hi, welcome to Elm.

I never heard of session types before reading your post, but it certainly looks like an interesting idea. There is nothing built-in to Elm around this, so presumably you would be looking at taking a ‘session type’ and mapping it onto Elm code in some way that faithfully represents and enforces the type?

Elm is single threaded, due to how JS works on browsers, so communicating parallel processes is not a programming model Elm uses. That said, Elm clients may be talking to back-ends over HTTP or web sockets, or communicating with other Elm programs running as service workers running in parallel. And of course, a communicating processes model can sometimes still make sense even in single threaded programs, just as a conceptual system for structuring a program.

Now abandoned, but in an earlier version of the Elm compiler I had a little experiment with something along those lines: https://github.com/rupertlssmith/elmq

Perhaps if you could give a small example of a session type, we could try and turn it into Elm code and see what the result looks like?

[d4hines]

Unfortunately, I don’t yet know enough about them to provide useful examples. However, there is a Typescript example of using session types to achieve deadlock-free communication with web workers: https://github.com/ahuglajbclajep/session-typed-worker This Typescript example implements only a small subset of session types, but, since it only uses generics, that subset should be trivially implementable in Elm.

I think the main use case is for full stack code. If your front- and backend-end are both in Elm, then session types in Elm could enforce proper communication between them. In my particular case, I’ll be working on an Electron app, where Elm could be used both in the Main and Render process, and session types could validate the IPC messages between them.