[erlang-questions] -protocol declartion idea, worth an EEP?

[zxq9]

On 2017年06月05日 月曜日 10:35:40 Michael Truog wrote:
> On 06/05/2017 06:16 AM, ok@REDACTED wrote:
> >>> If you want to specify that a function doesn't receive
> >>> anything, use 'receive none()'; any empty OptRcv says nothing
> >>> about the function's protocol.
> >> I disagree. This would mean that all "pure" functions require
> >> annotations. This seems pretty tedious.
> > The problem is that right now fun() and -spec say *nothing*
> > about reception.  Backwards compatibility seems to require
> > not changing that.
> >
> > The idea was that a checker should *infer* 'receive none()'
> > for pure functions, and that this should *refine* a given
> > -spec.
> >
> > One thing I was after was that you should normally require
> > just one -protocol declaration per process, with the
> > receive part of the functions it calls being inferred.
> 
> I believe it is more important to be able to mark functions impure or pure within the Erlang type specification as described at https://bugs.erlang.org/browse/ERL-373 than to clarify the received messages, though it would be nice to have both.  In practice, the code paths taken with a receive won't benefit clearly with the -protocol addition, when considering how receives are normally buried in an Erlang behaviour (it is considered beneficial to use Erlang behaviours in practice, and often explicit receives are typical in academic exercises which may refer back to Erlang in earlier days before OTP existed).  If we could mark functions as impure or pure and have it inferred/checked with dialyzer, there would always be a clear benefit at any level of abstraction.

I totally agree, to the point that I often annotate pure functions:
https://github.com/zxq9/zuuid/blob/master/src/zuuid.erl#L34-L39

BUT

These are two very different issues. What ROK is getting at is having a way to declare a message protocol (as a verifiable contract) by which a certain process is going to live and abide by (at the "living objects" level of the system), whereas declaring functional purity is strictly functional annotation. These are entirely orthogonal issues, but both absolutely critical to providing a way for a programmer to formally declare the intent of some code and have that intent checked by a tool like Dialyzer.

That said...

OTP and extension of generic behaviors (OTP or otherwise) is an interesting issue because while it is often useful to have one module in src/ equate to one type of process that will be spawned, leveraging gen_server with another layer of abstraction is not uncommon (consider wx) -- and neither is writing OTP-compliant pure Erlang processes that contain their own naked 'receive' clauses when dealing with code that needs to have extremely low latency (tight socket handling code comes to mind). That means that the parts of a process' definition that might include informal declarations of valid incoming and outgoing message forms may be spread across several code modules and shared across processes -- and this gets tricky to determine how to define. Even a good syntax for how to write this is not easy to pull out of a hat.

The traditional way to sort of wish the protocol message adherence issue away has been to use behaviors and abstract all message passing behind public interface functions that are as explicitly typed as one can manage -- and yet this still fails to really give us a solid contract by which processes have to live in a way that dialyzer can check for us, as it forces side-effecty message-involved functions to be conflated with any other functions. (This approach is also one that seems to be heavily used and almost never discussed in these terms.)

Hmmm...

Anyway, I certainly think a -pure declaration in Dialyzer would be much easier to implement in the short-term than a process-level message protocol declaration. But I deeply wish we had both already -- and always have.

-Craig