"while there have been attempts to graft a more versatile type system onto the Erlang base language, the cleanest way forward seems to be a language purpose-built for the task."
Are you sure that's even possible? Erlang is fundamentally a dynamic system, with hot code (re)loading, processes starting and stopping (possibly crashing), and nodes attaching and detaching.
Moreover, the idea that a message can be sent to any PID seems fundamentally at odds with type checking at compile time. You'd probably need to do something more like channels.
Perhaps an ML-like type system can work with all of that, but it sounds like a research problem.
Simon Marlow and Philip Wadler tried to make a type system for Erlang and couldn't do it [1]. And if they couldn't do it... well, it's a very hard problem, for many of the reasons you cited.
From what I understand, the general consensus is that Erlang's dynamic types are a small price to pay for the flexibility and features afforded by the runtime. To be fair, what makes Erlang/OTP awesome is how the system works as a cohesive whole, rather than any particular feature of the language itself.
I don't believe that one should attempt to copy the Erlang model in a typed language (and this is one reason I don't particularly like Akka). There are many facilities, some noted in other comments, that make statically typing Erlang difficult but I don't believe most of these are necessary.
Can send any message to any actor? Probably a bug.
Hot code swapping? Never had a need for this. Restarts are fine. Any distributed system is supposed to be crash resistant. A restart is just another crash.
I much prefer the CSP model to the Actor model in any case (with asynchronous channels available), and it is much easier to type CSP.
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.
So, maybe that's an interesting thing you've got there, right?
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?
Typing a the message-passing part of a language like Erlang is very much an open research problem. I spoke about this at length with the session type community. They are thinking about this, but it's at least a decade away.
From a superficial reading I think what they are doing is quite simplistic. Basically they want to provide typed channels, e.g. ActorRef[T] that only accepts T messages. That's the easy part. What you really want is something like type-based guarantees that a the interaction between actors cannot get stuck. Achieving this is fraught with difficulties.
no true scottsman? This reminds me of arguments against STM, which efforts previously failed because they tried to enforce it across the whole system. The way forward was to demarcate clearly which vars were in STM and which weren't, and it is very useful - note doesn't solve the "hard theory cs" formulation of STM.
Just because typed ActorRef aren't as hard as implementing this other property which has some other "hard cs" property, does that really devaule the utility of typed ActorRefs?
I admit I'm not sure exactly if 'the interaction between actors cannot get stuck' property is something that is an existing pain point, or something that would be introduced as a result of typed ActorRefs
I didn't say it wasn't useful. It is. But it's checking essentially a sequential property: a sequential actor is using a channel in a consistent way. What e.g. the session type community is aiming at are properties of concurrent computation, such as linear channel usage which depends on the behaviour of multiple processes.
Cloud haskell is interesting but doesn't even approach the level of the same capabilities as Erlang w/ OTP and BEAM, and the creator of Elm has described it as a language primarily oriented for responding to UI concerns, not a systems language
Are you sure that's even possible? Erlang is fundamentally a dynamic system, with hot code (re)loading, processes starting and stopping (possibly crashing), and nodes attaching and detaching.
Moreover, the idea that a message can be sent to any PID seems fundamentally at odds with type checking at compile time. You'd probably need to do something more like channels.
Perhaps an ML-like type system can work with all of that, but it sounds like a research problem.