[erlang-questions] Fwd: Must and May convention

[zxq9]

On 2017年09月28日 木曜日 10:49:21 Karlo Kuna wrote:
> > > -pure([f/1, g/0, h/3]).
> >
> > So, you declare f/1 is pure, but how do you really know it is pure?
> > Meaning it should be a way to prove f/1 is pure, at least with some tool
> > like dialyzer
> >
> 
> if f/1 is NIF there is little hope of proving that
> so in general i think ti should be either provable (meaning it is not NIF
> and uses only pure functions) or declared as such
> 
> i think we should go with "trust" here. If function is NIF it should be
> declared as pure, otherwise tool is to assume it is not

Right. This is actually the core issue with Dialyzer in general, because
it is a permissive typer that assumes anything is acceptable unless it
can prove by inference that something is impossible OR the user has
written a typespec to guide it and specify the wrongness. Those
specifications are essentially arbitrary in most cases.

This is the exact opposite approach used by GHC, for example. But for
the way Erlang and OTP work at their core it is necessary to have
permissive type checks guided by annotations.

NOTHING SAYS THOSE ANNOTATIONS MIGHT NOT BE WRONG.

This is also true of -pure declarations.

What you CAN prove, however, is that no definitely IMPURE functions
are called from within a function marked as -pure.

Which means Dialyzer would emit an error on any -pure function calling
a function not also considered -pure.

As noted before, much of the stdlib is pure, so quite a lot of code
could become provably pure quite quickly.

No messaging, no external resource calls, no ets, no nifs, certain
functions in io and io_lib are out, etc.

There may be a way to sneak a side effect in despite this, but I think
you could get CLOSE to having a provable graph of pure function calls.

BUT

That is true ONLY IF they are all actually fully qualified calls.
And this is also the problem with trying to make Dialyzer more strict.
(Also, dynamic upgrades are another impossible case to prove.)

Any time you do something like call apply(M, F, A) or Module:foo() you
suddenly can't know for sure what just happened. That module could have
come in dynamically. The only thing Dialyzer can know about it is, outside
of the runtime, the module itself is checked and it has a declaration.
But that's not the same thing as proving what the return type or external
effects of the ambiguous call site might be, so its return handler has
to be specced also. This is pretty much what happens throughout every
gen_server you ever write: the dispatching handle_* functions are quite
ambiguous, but the implementation functions below can be specified and
the interface functions that make the gen_*:call or gen_*:cast calls
can be specified as accepting and returning specific types -- so you
constrain the possibilities tremendously.

This happens every time you write a set of callbacks.
Part of what -callback declarations in behavior defining modules do for
you is typespec a callback -- but you can write callbacks without any
of that (and lots of people do) and that leaves Dialyzer blind. And
consider, of course, that the generic callback declarations for things
like gen_server are deliberately and arbitrarily broad. So to constrain
those you have to guard against type explosions in the interface and
implementation functions.

Nothing is going to fix that but hints like -pure and -spec and -callback.

And that means Dialyzer must continue to be permissive by default and
trust the programmer to be accurate about typespecs in their code.

So "proofing" is not attainable, no matter what, if you mean it in the
strict sense. But seriously, this is an industrial language hellbent on
getting code out the door that solves human problems. So forget about
silly notions of type completeness. That's for academia. In the real world
we have confusing problems and convoluted tools -- this one is
dramatically less convoluted than MOST tools in this domain of solutions
and it can AT LEAST give us a warning when it can prove that you've done
something that is clearly in error.

The kind of super late binding that dynamic module loading and dynamic
call sites imply prohibit proving much about them -- at least in Erlang.
Yet they still work quite well.

-Craig