[erlang-questions] dialyzer and behaviours

[Siraaj Khandkar]

On 07/17/2014 03:46 AM, Daniil Churikov wrote:> (Sorry, initially
replied directly)
>
> Replying inline
>
>> Whether a module conforms to a behaviour is something that
>> can change either way when a new version of the module is
>> loaded.  Being time-dependent, it can't be part of a type.
>
> Whether a function returns an iolist or an atom can change with
> a next version of code too. But you expect that dialyzer run will
> reveal this spec incompatibility. So if next version of the module
> will not implement behaviour it used to, why not to notify about
> this?

It isn't so much about runtime possibilities but more about a lack of
static capabilities given the semantics. The difference is in
constructing a reference to a module (or function) statically or
dynamically.

The bellow reference to the module is not constructed statically, but
dynamically, so at the time of analysis it does not actually exist:

    -spec create(Mod :: atom(), Vals :: [iolist(), ...]) -> iolist().
    create(Mod, Vals) ->
        Table = Mod:table(),
        ... .

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


> I understand that this will not guarantee anything in runtime, you
> still could load anything you want, but at least it could guarantee
> me certain level of safety at dialyzer-run time.
>

It isn't just about guarantees, it is just that Dialyzer has no concrete
path to follow at the time it sees `Foo:bar()`.


> 2014-07-17 5:03 GMT+04:00 Richard A. O'Keefe <ok@REDACTED>:
>
>>
>> On 17/07/2014, at 12:56 AM, Daniil Churikov wrote:
>>> Is there any way to write a spec for dialyzer that will tell that I
>> expect module of certain behaviour?
>>
>> The types that the Dialyzer works with have no connection
>> with the *state* of the Erlang system; it can only describe
>> the shape of a term in and of itself.  Types do not vary
>> with time.
>>
>> You cannot have "registered process name" as a type.
>> You cannot have "defined key in the process dictionary" as a type.
>> You cannot have "loaded module" as a type.
>> You cannot have "open port" as a type.
>>
>> Whether a module conforms to a behaviour is something that
>> can change either way when a new version of the module is
>> loaded.  Being time-dependent, it can't be part of a type.
>>
>> This is not to say that *some* verification tool not utterly
>> unlike a type checker might not be possible that could get
>> closer to what you want.  It's just that time-dependent
>> properties are not commonly thought of as 'types'.  Even in
>> the languages I know about with dependent types, it's
>> value dependency not time dependency that's in question.
>>