<div dir="ltr">for me benefit would be to narrow down on what IS pure and what developer THINKS is is pure <div>just with that IMHO lot of common errors could be detected </div><div><br></div><div>developers should be then guided during debugging on parts that are not pure, also big help! </div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 28, 2017 at 11:38 AM, Roman Galeev <span dir="ltr"><<a href="mailto:jamhedd@gmail.com" target="_blank">jamhedd@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span class=""><div>> No messaging, no external resource calls, no ets, no nifs, certain functions in io and io_lib are out, etc.</div><div><br></div></span><div>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. </div><div><br></div><img src="https://mltrk.io/pixel/C2hkvhyILoGhWY99nVL4?rid=C2hkvhyILoGhWY99nVL4" width="1" height="1" border="0"></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">On Thu, Sep 28, 2017 at 11:16 AM, zxq9 <span dir="ltr"><<a href="mailto:zxq9@zxq9.com" target="_blank">zxq9@zxq9.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2017年09月28日 木曜日 10:49:21 Karlo Kuna wrote:<br>
> > > -pure([f/1, g/0, h/3]).<br>
> ><br>
> > So, you declare f/1 is pure, but how do you really know it is pure?<br>
> > Meaning it should be a way to prove f/1 is pure, at least with some tool<br>
</span><span>> > like dialyzer<br>
> ><br>
><br>
> if f/1 is NIF there is little hope of proving that<br>
> so in general i think ti should be either provable (meaning it is not NIF<br>
> and uses only pure functions) or declared as such<br>
><br>
> i think we should go with "trust" here. If function is NIF it should be<br>
> declared as pure, otherwise tool is to assume it is not<br>
<br>
</span>Right. This is actually the core issue with Dialyzer in general, because<br>
it is a permissive typer that assumes anything is acceptable unless it<br>
can prove by inference that something is impossible OR the user has<br>
written a typespec to guide it and specify the wrongness. Those<br>
specifications are essentially arbitrary in most cases.<br>
<br>
This is the exact opposite approach used by GHC, for example. But for<br>
the way Erlang and OTP work at their core it is necessary to have<br>
permissive type checks guided by annotations.<br>
<br>
NOTHING SAYS THOSE ANNOTATIONS MIGHT NOT BE WRONG.<br>
<br>
This is also true of -pure declarations.<br>
<br>
What you CAN prove, however, is that no definitely IMPURE functions<br>
are called from within a function marked as -pure.<br>
<br>
Which means Dialyzer would emit an error on any -pure function calling<br>
a function not also considered -pure.<br>
<br>
As noted before, much of the stdlib is pure, so quite a lot of code<br>
could become provably pure quite quickly.<br>
<br>
No messaging, no external resource calls, no ets, no nifs, certain<br>
functions in io and io_lib are out, etc.<br>
<br>
There may be a way to sneak a side effect in despite this, but I think<br>
you could get CLOSE to having a provable graph of pure function calls.<br>
<br>
BUT<br>
<br>
That is true ONLY IF they are all actually fully qualified calls.<br>
And this is also the problem with trying to make Dialyzer more strict.<br>
(Also, dynamic upgrades are another impossible case to prove.)<br>
<br>
Any time you do something like call apply(M, F, A) or Module:foo() you<br>
suddenly can't know for sure what just happened. That module could have<br>
come in dynamically. The only thing Dialyzer can know about it is, outside<br>
of the runtime, the module itself is checked and it has a declaration.<br>
But that's not the same thing as proving what the return type or external<br>
effects of the ambiguous call site might be, so its return handler has<br>
to be specced also. This is pretty much what happens throughout every<br>
gen_server you ever write: the dispatching handle_* functions are quite<br>
ambiguous, but the implementation functions below can be specified and<br>
the interface functions that make the gen_*:call or gen_*:cast calls<br>
can be specified as accepting and returning specific types -- so you<br>
constrain the possibilities tremendously.<br>
<br>
This happens every time you write a set of callbacks.<br>
Part of what -callback declarations in behavior defining modules do for<br>
you is typespec a callback -- but you can write callbacks without any<br>
of that (and lots of people do) and that leaves Dialyzer blind. And<br>
consider, of course, that the generic callback declarations for things<br>
like gen_server are deliberately and arbitrarily broad. So to constrain<br>
those you have to guard against type explosions in the interface and<br>
implementation functions.<br>
<br>
Nothing is going to fix that but hints like -pure and -spec and -callback.<br>
<br>
And that means Dialyzer must continue to be permissive by default and<br>
trust the programmer to be accurate about typespecs in their code.<br>
<br>
So "proofing" is not attainable, no matter what, if you mean it in the<br>
strict sense. But seriously, this is an industrial language hellbent on<br>
getting code out the door that solves human problems. So forget about<br>
silly notions of type completeness. That's for academia. In the real world<br>
we have confusing problems and convoluted tools -- this one is<br>
dramatically less convoluted than MOST tools in this domain of solutions<br>
and it can AT LEAST give us a warning when it can prove that you've done<br>
something that is clearly in error.<br>
<br>
The kind of super late binding that dynamic module loading and dynamic<br>
call sites imply prohibit proving much about them -- at least in Erlang.<br>
Yet they still work quite well.<br>
<div class="m_3476666464207707730HOEnZb"><div class="m_3476666464207707730h5"><br>
-Craig<br>
______________________________<wbr>_________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/list<wbr>info/erlang-questions</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div></div></div><span class="">-- <br><div class="m_3476666464207707730gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">With best regards,<div>     Roman Galeev,</div><div>     <a href="tel:+420%20702%20817%20968" value="+420702817968" target="_blank">+420 702 817 968</a></div></div></div>
</span></div>
<br>______________________________<wbr>_________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/<wbr>listinfo/erlang-questions</a><br>
<br></blockquote></div><br></div>