Typed processes

[NicolasT]

Currently, a Process is not typed, as in, any (Typeable) message can be sent to it, and it can check for any type of messages in receive.

It may make sense (not sure, though!) to have a concept of "typed" processes as well. Basically, there'd be a TypedProcess r msg wrapping Process r, and with it a TypedProcessId msg, and all utility functions lifted to TypedProcess r msg. Then, receive would be something like [TypedMatch msg a] with, e.g., MatchMessage (Message msg -> TypedProcess r msg a (or something along those lines), and send :: TypedProcessId msg -> msg -> m ().

Of course, we should be able to deliver Down, Exit and other "system" messages, hence the Message wrapper in receive. A TypedProcess r msg doesn't actually receive msg messages, but Message msg where data Message = Exit | Down | UserMessage msg (with Exit and Down and others more elaborate of course). Alternatively, Message could be SystemMessage _ | UserMessage msg or similar, of course.

Then, receive will use the untyped API and select on system messages or the user message type, wrapping things up accordingly.

A wide design space, and as said, not sure this is a good idea. Thoughts welcome.

[alt-romes]

For typed processes we could consider leveraging the existing literature on session types, whose scope is exactly typed concurrent processes (even more so since Linear Haskell, which makes the encoding of session types more convenient: https://arxiv.org/pdf/2103.14481.pdf)

(I'm not an expert on session types!)

[NicolasT]

That definitely makes sense! Thanks for the suggestion.

I wonder whether a notion of typed processes (without session types) layered on top of the untyped processes core could then be used to provide what's needed to layer session typed interactions on top.