4 ms·

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.

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.

platz 12y ago
Isn't Akka planning to add types w/ typed akka? If they can pull that off some subset of Erlang should be doable as well
- saryant 12y ago
  That's their plan for Akka 3.0. I believe this is the current status: https://github.com/akka/akka/pull/16665 https://github.com/akka/akka/pull/16665
- mafribe 12y ago
  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.
  - platz 12y ago
    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
    - mafribe 12y ago
      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.
jacques_chester 12y ago
In practice you have to check messages as they arrive because you cannot control what others will send you.

platz 12y ago

Isn't Akka planning to add types w/ typed akka? If they can pull that off some subset of Erlang should be doable as well

saryant 12y ago
That's their plan for Akka 3.0. I believe this is the current status: https://github.com/akka/akka/pull/16665 https://github.com/akka/akka/pull/16665
mafribe 12y ago
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.
- platz 12y ago
  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
  - mafribe 12y ago
    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.

jacques_chester 12y ago

In practice you have to check messages as they arrive because you cannot control what others will send you.