[erlang-questions] Dialyzer underspecs and overspecs options

[Dmitry Kakurin]

> There is no way to specify the "cross" of the two options as of now I think.


How realistic do you think it would be to add this functionality to Dialyzer?


Thank you, Dmitry.
________________________________
From: Jesper Louis Andersen <jesper.louis.andersen@REDACTED>
Sent: Tuesday, March 28, 2017 4:20:47 PM
To: Dmitry Kakurin; erlang-questions@REDACTED
Subject: Re: [erlang-questions] Dialyzer underspecs and overspecs options

On Tue, Mar 28, 2017 at 9:03 PM Dmitry Kakurin <dima_kakurin@REDACTED<mailto:dima_kakurin@REDACTED>> wrote:
These are pretty-much covariance and contravariance rules: you cannot accept less than you claim and you cannot produce more than you claim.


Ah of course.

There is no way to specify the "cross" of the two options as of now I think. What you want is basically to check for contravariance in inputs and covariance in outputs if I read what you say correctly. This is normal errors for a subtype hierarchy where you have functions as first class values. That is the relation is that

    S1 -> T1 <: S2 -> T2

Given that

    T1 <: T2 (covariance)
    S2 <: S1 (contravariance)

Do note that the dialyzer is an approximate analysis however. Consider these functions:

f(a) -> true;
f(b) -> false;
f(c) -> true.

g(a) -> true;
g(b) -> true;
g(c) -> false;
g(d) -> true;
g(e) -> false;
g(f) -> true;
g(g) -> true;
g(h) -> true;
g(i) -> false;
g(j) -> false;
g(k) -> true;
g(l) -> true;
g(m) -> false;
g(n) -> true;
g(o) -> false.

The dialyzer infers the following types for these:

-spec f('a' | 'b' | 'c') -> boolean().
-spec g(atom()) -> boolean().

The point is that 'g' contains "too much" information so the dialyzer just moves one up in the type lattice rather than running with a precise specification. Clearly g/1 fails if called as 'g(x)' for instance, but this is not represented in the type specification. Rather, the dialyzer has approximated that the function is probably from atom() to boolean().

This is what usually makes underspecs/overspecs a bit like a false positive in the system. As long as you travel along a subtyping chain in the lattice, you may be witnessing an approximation.

Where we are sure of a mistake is if you suddenly have an input that doesn't match the type lattice at all. Say we called 'g(<<>>)' which would obviously be wrong since g doesn't accept binary() as input.

It may also be worth mentioning that a success type f : A -> B is defined in a specific manner:

  Suppose f(X) reduces to a value V. Then V is among type B and X is among type A.

It is subtly different from a standard static type system. Note that 'g/1' above fulfills this notion: if it terminates with a boolean() value, then its input was definitely an atom(). Also note that the succes type any() -> any is valid for 'g/1'. But it doesn't establish a relation of being well-typed and thus having certain desirable meta-theoretic properties.

On the other hand, the key aspect is that while it over-approximates, we can say something about a function application such as g(<<>>) because we know a priori it will fail. This is program defect and we better report such defects!

If you are interested, Lindahl and Sagonas has a paper on the implementation, and its exposition is better than mine given here:

https://it.uu.se/research/group/hipe/papers/succ_types.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20170330/027b396f/attachment.htm>