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

[Michael Truog]

On 06/05/2017 03:42 PM, Richard A. O'Keefe wrote:
>> On 6/06/2017, at 5:35 AM, Michael Truog <mjtruog@REDACTED> wrote:
>> I believe it is more important to be able to mark functions impure or pure
> Actually that was something I was working on with SERC just before
> funs were introduced into Erlang and completely derailed my ideas.
>
> One issue is that 'pure' or 'impure' is far too coarse a classification.
It would be nice to have finer granularity than just 'pure' or 'impure', though it seems
very easy to make this purity concept complex enough that people don't use it.
Having the ability to distinguish between "operational purity" and
"mathematical purity" (as they were described in https://bugs.erlang.org/browse/ERL-373)
would be interesting, though it would go beyond the concept of purity that is
present in Haskell, which is already complex, and would require that people
care about the difference (I don't think most people would care, in practice,
since their concerns would be likely focused only on their logic they are
attempting to develop, while they assume the compilation platform remains
(generally) constant).  I would expect that Erlang, as a dynamically typed
language, would favor simplicity in the purity concept, instead of providing
more granularity, though I personally would like more granularity
(i.e., to keep the function types in any Erlang system simple, and able to
handle future changes more easily, even if the changes span separate
module versions and Erlang versions).

> For example, we might want to distinguish
>   - termination
>     - terminates in bounded time
>     - terminates in finite time
>     - not known to terminate
I would assume most analysis of normal source code wouldn't be able to say
anything too useful about termination (due to normal complexity), but I don't
know much about this.  I mainly just consider that dialyzer is already pushing
speed and memory limits which shouldn't be taxed much more (especially
if this would only ever work on toy examples).  I would rather that dialyzer is
always part of compilation (even if it always remains a separate executable)
to get similar lint-ing when compared to statically typed languages.

>   - process dictionary
>     - no dependency on process dictionary
>     - reads specified parts of process dictionary
>     - writes (and maybe reads) specified parts of process dictionary
I like the idea of being able to distinguish between local mutable data
(the process dictionary) and global mutable data (ets, etc.), to show the
scope of the mutability used in the function.  It is likely reasonable to say
global mutable data use permits local mutable data use, where global
mutable data use is considered "more impure" than local mutable data
use (i.e., using ets allows you to use the process dictionary, without
being specific about using the process dictionary).  Having separate
levels of impurity could convey an increasing potential for error
(more impurity requires more testing at a system level to ensure state
is being managed according to expectations).

>   - input/output
>     - does no I/O
>     - reads
>     - writes
>     - opens and closes
>   - inter-process communication
>     - does it create processes or not
>     - does it send messages or not
>     - does it receive messages (which?) or not
I think it is best to group I/O as it relates to the Erlang port type,
so sockets and Erlang port processes would be treated the same.
That I/O is separate from Erlang messages, which relates more to the
-protocol declaration idea.

> And that isn't meant to be a complete list.
>
> Another issue is higher-order functions.
>
> map(F, [X|Xs]) -> [F(X) | map(F, Xs)];
> map(_, [])     -> [].
>
> is itself pure, but if F has any effects, map(F, ...) may
> (but need not) have those effects too.  So we need a type
> like
> map/2 :: (A -> B effect E, list(A)) -> list(B) effect E+finite.
If dialyzer could infer the purity from the anonymous function,
then we should be able to avoid making the syntax for the type
specification more complex.  That may require that functions
never default to being "impure" and just stay ambiguous, until
it can be inferred from type specifications based on the call path
(or things like catching exceptions, local/global mutable state, etc.).
>
> Since then, Erlang has gone through at least three different
> type systems (the Wadler one, the Armstrong one, and the one
> it now has), and I never did get around to trying to adapt a
> proper "effect" system to the Dialyzer approach.