[erlang-questions] Fwd: Must and May convention

[Karlo Kuna]

for me benefit would be to narrow down on what IS pure and what developer
THINKS is is pure
just with that IMHO lot of common errors could be detected

developers should be then guided during debugging on parts that are not
pure, also big help!


On Thu, Sep 28, 2017 at 11:38 AM, Roman Galeev <jamhedd@REDACTED> wrote:

> > 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 <+420%20702%20817%20968>
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20170928/0849dbf6/attachment.htm>