[erlang-questions] dialyzer and behaviours

[Fred Hebert]

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()'

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

Erlang's semantics allow that call, and that is the correct type
signature that will correspond to its behavior at runtime.

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

Regards,
Fred.