[erlang-questions] Fwd: Must and May convention

[Roman Galeev]

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

So each function sending a message out is impure by definition, therefore
all gen_server calls are impure too. Meaning -pure declarations are
applicable only to a narrow subset of all functions defined. I just wonder
how many paths are in a graph of calls not involving calls to gen_server:*
family in a typical Erlang application.


On Thu, Sep 28, 2017 at 11:16 AM, zxq9 <zxq9@REDACTED> wrote:

> 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
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>



-- 
With best regards,
     Roman Galeev,
     +420 702 817 968
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20170928/f6378813/attachment.htm>