Hacker News Reader

Comment by Zalastax | Hacker News Reader

The problem of static types for the communicating parts of the actor model is not really solved yet. In the meantime there's Alpaca-lang and Simon Fowler did a run-time monitor for Erlang with behavioral types from Scribble. I think we'll see some nice progress in this area in a few years.

View on HN

By coincidence The Morning Paper has this today:

A static verification framework for message passing in Go using behavioural types, Lange et al., ICSE 18

http://blog.acolyer.org/2018/01/25/a-static-verification-fra...

Akka has solved them already. Just pattern match on the object you receive.

Before I send you an object, I’d like a static guarantee that you can process it. Typed channels is one approach used in Cloud Haskell - I think Akka tried and abandoned it.

I think a protocol type system like Scribble is a really good solution to the problem. It's very tricky to verify it statically though, so it will take time to get there.

The guarantee you can process it only works when your compiler has access to both sender and receiver.

When you connect to a cluster to send to something on another node, it’s no different than making an API call to a service that you don’t control. The compiler can’t make any guarantees there without contracts in hand, which can change at a whim on a deploy or when new nodes are added.

For message passing across a cluster, setting up Dialyzer is probably the most realistic approach. Function calls on the BEAM are more like request routing I think.

Node -> Module -> Function -> Arity -> Pattern

Akka clusters, like Erlang clusters, are completely trusted. This is not an integration technology, it’s for distributed processing by a single owner.

It is, but code updates still happen. Nodes aren't all identical.

As these things change, the contracts have to be exchanged with every member of the cluster which would not only add significant communication overhead, it would also bypass those compile time guarantees.

That's before even considering things like hot deploys where the code is updated live, while running, mid-execution.

The contract enforcement becomes akin to the goals of WSDL, which added a ton of overhead with minimal benefit aside from making consuming APIs easier for statically typed languages because of generators.

Is the overhead worth the difference from...

Client (this message will fail on this server) -> don't send

to...

Client -> (this message failed)

Especially when talking about a cluster which you own...that benefit is questionable at best.

The feature I'm talking about is a compile-time constraint. The sole purpose of it is to make development and refactoring easier by providing immediate feedback to the developer when they change code in a way incompatible with its interface. It is not really about providing global run-time guarantees. Solving evolving messages through deployment is really a separate topic, and something you have to do whether you have compile time checks or not.

In that case, I'm not following where Dialyzer doesn't already address the problem?

It doesn't cover every case, but it covers enough of them to provide a very watchful eye without getting in your way.

https://speakerdeck.com/jvoegele/elixirconf-2016-dialyzer-op...

I wrote and maintain Dialyxir. I'm familiar with Dialyzer. What it can't do, is tell me whether any given pid can actually accept and process a message of a particular type. You can write a module interface to your actor that does this, which is what most people do. But it is not quite the same as typed channels. And whoever started this thread was complaining about the "issue" in Akka. Messages are inherently dynamic in this style of communication. Its not the only possible style in either language, but its a valid criticism of this particular approach.

This requirement is incompatible with the actor model. Use channels (Go, Rust) if this is what you want. The lines of communication between actors are untyped because real life networks are untyped. When you receive a packet over the network you always have to look at it before you use it. Typed channels are fine for single machine use, but untyped is necessary for distributed computation.

I think if you have an evolved enough type system, then there isn't such a problem. I have written an Elixir backend for Idris and given some examples of well-typed actor communication here:

https://github.com/jameshaydon/idris-elixir

Reply on news.ycombinator.com