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