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

[ok@REDACTED]

One of the things I've wanted for a long time in Erlang is
a way to check message passing.  Now that we have the
Dialyzer, it occurred to me that there's a simple thing we
could do that wouldn't achieve everything we might want
(it's not UBF) but might be useful in catching typos at least.

Before writing it up as an EEP, I thought I'm check with the
mailing list whether it makes sense to other people.  It seems
like the kind of thing that must have been thought of before,
so maybe there is some flaw in it that I'm not seeing.

-protocol(<type>).
says that the following function and the functions it calls
may only receive messages that conform to the <type>.
Taking the <type> as a union type (counting a type that is
not a union type as a union of one element), each element
of the union must have at least one corresponding receive.
[I know 'corresponding' is vague; this is one of the things
the EEP would spell out.]

What if a function calls another that is not known until
run time?  That requires a change to the type language:

Fun :: fun( OptRcv)                    %% any function
       | fun((...) -> Type OptRcv)     %% any arity, returning Type
       | fun(() -> Type OptRcv)
       | fun((TList) -> Type OptRcv)


OptRcv :: /* empty */
        | receive Type

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.

-spec could be extended too.
  -spec Module:Function(ArgType1, ..., ArgTypeN) -> ReturnType OptRcv.

This would not let us check that sends and receives matched up
properly, although part 2 of the EEP would address that.  But
it would provide
(1) a place to document the programmer's intentions
    about the messages a process should receive
(2) a way to check that patterns in receives were supposed to
    be there, catching typos
(3) a way to check that everything that is supposed to be
    received might be received somewhere; this would have
    false negatives, but it's still better than what we have.