[erlang-questions] dialyzer and behaviours

[Siraaj Khandkar]

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).