So let's say you restart, and the process comes up with new code, including new type signatures for the messages that the process is expecting to receive. How (and when) does the compiler check those new type signatures against already-running processes on another node?

Maybe there's some very sophisticated way of managing versions using subtyping to ensure that a new version always accepts a superset of the messages that the old version accepted. That sounds like a mess, and I doubt it would actually work.

Even if it did, it's solving the wrong problem. In a massively distributed system, message types are just one small part of a larger problem: protocol integrity. If you send the right message type at the wrong time, or are waiting for a message that never comes, a type system won't do you any good.

So to make this all actually work, you need to incorporate some high-level declarative protocol specification into your distributed versioning static type system (with subtypes). Perhaps not impossible, but wow, that would be some serious research effort; and then a lot of engineering effort to make it practical.

I could sum this up by saying that all static type systems seem to revolve around one very simple protocol: the function call. The erlang type system can handle that just fine. But erlang also brings a lot of other protocols to the forefront, and we don't know how to typecheck them all. Other languages punt on these problems so that they can call the type system "sound", but that doesn't make the problems go away.

Time-dependent type systems--and that kind of makes me think of state machines. Not sure if there's anything there, but maybe there is. Maybe we can prove that type systems that are time-dependent have certain computability properties?