<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body>
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Arial,Helvetica,sans-serif;" dir="ltr">
<p>> <span style="color: rgb(33, 33, 33); font-size: 15px;">There is no way to specify the "cross" of the two options as of now I think. </span></p>
<p><br>
</p>
<p>How realistic do you think it would be to add this functionality to Dialyzer?</p>
<p><br>
</p>
<div id="Signature">Thank you, Dmitry.</div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Jesper Louis Andersen <jesper.louis.andersen@gmail.com><br>
<b>Sent:</b> Tuesday, March 28, 2017 4:20:47 PM<br>
<b>To:</b> Dmitry Kakurin; erlang-questions@erlang.org<br>
<b>Subject:</b> Re: [erlang-questions] Dialyzer underspecs and overspecs options</font>
<div> </div>
</div>
<div>
<div dir="ltr">On Tue, Mar 28, 2017 at 9:03 PM Dmitry Kakurin <<a href="mailto:dima_kakurin@hotmail.com">dima_kakurin@hotmail.com</a>> wrote:<br>
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="gmail_msg">
<div id="m_-123184262507949923divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Arial,Helvetica,sans-serif" dir="ltr" class="gmail_msg">
These are pretty-much <i class="gmail_msg">c</i><span class="gmail_msg"><i class="gmail_msg">ovariance</i> and
<i class="gmail_msg">contravariance</i></span> rules: you <b class="gmail_msg">cannot
</b><b class="gmail_msg">accept less </b>than you claim and you <b class="gmail_msg">
cannot </b><b class="gmail_msg">produce more</b> than you claim.
<p class="gmail_msg"><br class="gmail_msg">
</p>
</div>
</div>
</blockquote>
Ah of course.<br>
<br>
</div>
<div class="gmail_quote">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<br>
<br>
</div>
<div class="gmail_quote"> S1 -> T1 <: S2 -> T2<br>
<br>
</div>
<div class="gmail_quote">Given that<br>
<br>
</div>
<div class="gmail_quote"> T1 <: T2 (covariance)<br>
</div>
<div class="gmail_quote"> S2 <: S1 (contravariance)<br>
<br>
</div>
<div class="gmail_quote">Do note that the dialyzer is an approximate analysis however. Consider these functions:<br>
<br>
f(a) -> true;<br>
f(b) -> false;<br>
f(c) -> true.<br>
<br>
g(a) -> true;<br>
g(b) -> true;<br>
g(c) -> false;<br>
g(d) -> true;<br>
g(e) -> false;<br>
g(f) -> true;<br>
g(g) -> true;<br>
g(h) -> true;<br>
g(i) -> false;<br>
g(j) -> false;<br>
g(k) -> true;<br>
g(l) -> true;<br>
g(m) -> false;<br>
g(n) -> true;<br>
g(o) -> false.<br>
<br>
</div>
<div class="gmail_quote">The dialyzer infers the following types for these:<br>
<br>
-spec f('a' | 'b' | 'c') -> boolean().<br>
-spec g(atom()) -> boolean().<br>
<br>
</div>
<div class="gmail_quote">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().<br>
<br>
</div>
<div class="gmail_quote">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.<br>
<br>
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.<br>
<br>
</div>
<div class="gmail_quote">It may also be worth mentioning that a success type f : A -> B is defined in a specific manner:<br>
<br>
</div>
<div class="gmail_quote"> Suppose f(X) reduces to a value V. Then V is among type B and X is among type A.<br>
<br>
</div>
<div class="gmail_quote">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.<br>
<br>
</div>
<div class="gmail_quote">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!<br>
</div>
<div class="gmail_quote"><br>
</div>
<div class="gmail_quote">If you are interested, Lindahl and Sagonas has a paper on the implementation, and its exposition is better than mine given here:<br>
<br>
<a href="https://it.uu.se/research/group/hipe/papers/succ_types.pdf">https://it.uu.se/research/group/hipe/papers/succ_types.pdf</a><br>
</div>
</div>
</div>
</body>
</html>