[erlang-questions] dialyzer and behaviours

[Thomas Lindgren]

"This is a somewhat controversial view that will probably upset somepeople, but _statistically_ creating and enforcing axiomatic
abstractions is the only thing that qualifies as a type system. Dynamic
typing just isn't typing (going even further, which is even more
controversial (but accurate IMO), it is uni-typing)."



Static typing people as a rule want to reject dynamic typing from consideration, usually reserving "typing" for their own work. (Do I detect a hint of Bob Harper in your text above?) But dynamic typing does however, for example, work well in Milner's sense of "does not go wrong", which is sufficient to many of us. There are other advantages too, like trivially handling incomplete or changing programs. Or for that matter allowing programs that are correct and do not go wrong, yet still are rejected by the type inference algorithm.

In the larger scheme of things, we also have to consider other issues than typing purity tests. While there are many aspects to this, two points have remained with me. First, it's a family of restrictive disciplines combined with various inference algorithms that buys you some assurances of correctness, but utterly ignores other potentially important issues, including partial correctness. Do the gains outweigh the costs? It's a trade off. Second, in some sense, the preference for static vs dynamic seems more than anything else to be an issue of personality (perhaps reinforced by upbringing). For example, some love it that the type checker finds their "tons of errors" (as they often put it), while others prefer the shortcuts available when there are less restrictions, like having PIDs instead of typed channels.

And since this same discussion has been recurring for me since the early 90s, with no apparent progress, and since this is not the mailing list to rehash these old issues, with that I'll try to leave the bait and unhook myself ;-)

Best,
Thomas



On Saturday, July 19, 2014 8:16 PM, Siraaj Khandkar <siraaj@REDACTED> wrote:
 

>
>
>On 07/17/2014 10:29 AM, Fred Hebert wrote:
>> On 07/17, Siraaj Khandkar wrote:
>>> In the face of such ambiguities, Dialyzer really has no choice but to
>>> assume innocence until guilt can be proven with certainty.
>>>
>>> When you say `baz = foo:bar()`, Dialyzer can _try_ to follow the path
>>> and match the expressions, but when you say `baz = Foo:bar()` - the rug
>>> is swept from underneath Dialyzer's feet and (at that call site) it can
>>> go no further than _try_ to find a case where Foo does not result in
>>> being an atom.
>>>
>>> So in other words, Dialyzer is not a type checker - it only seeks
>>> _definite_ failure cases in the call graph and sometimes
>>> success-or-failure depends _only_ on runtime state (such as dynamic
>>> references).
>>>
>> 
>> Someone who knows better about types, type systems, and type checking
>> than me may correct me, but I believe that Dialyzer still is a type
>> checker.
>> 
>> The difference is that it checks a type system that isn't axiomatic
>> (such as Hindley-Milner) -- those that tend to *prove* that there is no
>> type errors in the program, sometimes at the cost of forbidding certain
>> otherwise valid programs.
>> 
>> The canonical example for this is is:
>> 
>>     'and'(true, true) -> true;
>>     'and'(_, _) -> false.
>> 
>> being called as:
>> 
>>     'and'(5,6)
>> 
>> A type inference for an axiomatic type system might decide that the
>> 'and'/2 function's signature is 
>> 
>>     -spec 'and'(boolean(), boolean()) -> boolean()'
>
>
>Very interesting point! To explore it, the key question to answer is:
>"What is a type?"
>
>I struggled with that question for sometime, because I noticed that I
>use similar reasoning, of creating building blocks, in languages with
>_and_ without static type enforcement. So one way to think about "type"
>is as a synonym for "abstraction".
>
>Going further, I think the most enlightening definition of "type" was
>given by John Reynolds as: "a syntactic discipline for maintaining
>levels of abstraction." [1]
>
>So, while related, a type is not the abstraction itself, but a tool for
>enforcing it. More specifically, a _syntactic_ tool, that is - static.
>
>The 'and' example, I think, perfectly demonstrates why the enforcement
>necessarily has to be static - the catch-all case breaks the abstraction
>and by the time it hits runtime - it is too late and there's no
>principled way to prevent it other than adding checks _syntactically_.
>
>This is a somewhat controversial view that will probably upset some
>people, but _statistically_ creating and enforcing axiomatic
>abstractions is the only thing that qualifies as a type system. Dynamic
>typing just isn't typing (going even further, which is even more
>controversial (but accurate IMO), it is uni-typing).
>
>
>[1]:
>http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf
>
>> 
>> and therefore ban the call. Dialyzer can in fact ban this one if you
>> explicitly write that signature down, but won't infer this. If you have
>> no signature and call `$ typer <mod>`, the output is:
>> 
>>     -spec 'and'(_,_) -> boolean().
>
>And this is the key point that makes me feel that Dialyzer is not quite
>a type checker. Except... it DOES give you a way to syntactically define
>and enforce abstraction, so it DOES do type checking, but _optionally_
>and _incompletely_ (as in the case of dynamic references discussed
>earlier). So what to do? :)
>
>IMO it is an awesome static analysis tool that I cannot imagine using
>Erlang without, but because of the unavoidable typing holes - it cannot
>be thought of as a full-blown type checker in my mind.
>
>
>> Erlang's semantics allow that call, and that is the correct type
>> signature that will correspond to its behavior at runtime.
>
>Yes, Dialyzer is true to Erlang semantics, but Erlang semantics is
>exactly what creates the abstraction holes in the first place.
>
>
>
>> So the reason for this is that Dialyzer type checks on a concept called
>> 'success typing'. To simplify a lot (maybe too much), an axiomatic type
>> checker will build its list of what is valid or not by starting with a
>> null set (nothing is valid), and expanding it as it finds more
>> information in your program. This leads to denying programs that are:
>> 
>> 1. wrong all of the time for an execution path
>> 2. wrong some of the time for an execution path (and therefore right
>>    some of the time)
>> 3. do not provide sufficient information to know something will always
>>    be right (false negative)
>> 
>> Success typing basically works the other way around. It starts assuming
>> that everything is good, and then restricts what it thinks is valid as
>> it finds more information. This leads to denying programs that are:
>> 
>> 1. wrong all the time for an execution path
>> 
>> Programs that may or may not fail, either due to lack of information or
>> succeeding some of the time (or a combination of both) will be accepted
>> by Dialyzer.
>> 
>> Dialyzer still definitely checks your types, does analysis, does
>> inference, etc. It just analyzes them differently to give you a
>> different diagnostic, but for all intents and purposes, it is a type
>> checker (on top of being able to find other discrepancies in your
>> programs).
>_______________________________________________
>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/20140720/b6496fce/attachment.htm>