[erlang-questions] Dialyzer underspecs and overspecs options

Jesper Louis Andersen jesper.louis.andersen@REDACTED
Wed Mar 29 01:20:47 CEST 2017


On Tue, Mar 28, 2017 at 9:03 PM Dmitry Kakurin <dima_kakurin@REDACTED>
wrote:

> These are pretty-much *c**ovariance* 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/20170328/51628280/attachment.htm>


More information about the erlang-questions mailing list