<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>Hi Jesper,</p>
<p><br>
</p>
<p>We need to separate what constitutes a specified contract violation for function
<b>inputs </b>and function <b>outputs</b>.</p>
<p>I have reworked my demo example (below) and produced warnings (also below) to make it absolutely clear.</p>
<p><br>
</p>
<p>Let <b>SpecIn </b>be a set of @spec <b>inputs </b>and <b>RealIn </b>be a set of inputs as inferred by Dialyzer from real code, then:</p>
<p>* The <b>Input </b>Contract is <b>satisfied </b>when <span style="font-size: 12pt;"><b>SpecIn <= RealIn</b> (where <= is a non-strict
<b>subset </b>operation). <b>See </b><i><b>over_in</b></i> in demo code below.</span></p>
<p><span style="font-size: 12pt;">* The <b>Input </b>Contract </span><b>violation</b><span style="font-size: 12pt;"><b> </b>is detected by -W<b>underspecs </b>option when
<b>SpecIn > RealIn</b>. See <i><b>under_in</b></i> below.</span></p>
<p><span style="font-size: 12pt;">It is easy to see in the code: </span><br>
</p>
<p><span style="font-size: 12pt;">* It's <b>OK</b> for <i><b>over_in</b></i> to declare that it only accepts
<b>:a and :b</b> while it also happens to accept <b>:c</b>. Maybe suboptimal, but fine.</span></p>
<p><span style="font-size: 12pt;">* It's <b>NOT OK</b> for <i><b>under_in</b></i> to claim that it accepts
<b>:a, :b and :c</b> and break if <b>:c</b> is passed. <b>Rejecting </b><b>:c </b>
would break the caller.</span></p>
<p><span style="font-size: 12pt;"><br>
</span></p>
<p><span style="font-size: 12pt;">Let <b>SpecOut </b>be a set of @spec <b>outputs
</b>and <b>RealOut </b>be a set of outputs as inferred by Dialyzer from real code, then:</span></p>
<p><span style="font-size: 12pt;">* The <b>Output </b>Contract is <b>satisfied </b>
when <b>SpecOut >= RealOut</b> (where >= is a non-strict <b>superset </b>operation). See
<i><b>under_out</b></i> below.</span></p>
<p><span style="font-size: 12pt;">* The <b>Output </b>Contract <b>violation </b>is detected by -W<b>overspecs</b> option when
<b>SpecOut < RealOut</b>. See <i><b>over_out</b></i> below.</span></p>
<p></p>
<p style="font-family: Calibri, Arial, Helvetica, sans-serif, "Apple Color Emoji", "Segoe UI Emoji", NotoColorEmoji, "Segoe UI Symbol", "Android Emoji", EmojiSymbols; font-size: 16px;">
<span style="font-size: 12pt;">It is easy to see in the code:</span><br>
</p>
<div><span style="font-size: 12pt;">* It's <b>OK</b> for <b><i>under_out</i></b> to declare that it returns <b>:a, :b and :c</b>, while currently it only returns
<b>:a and :b</b>. Maybe future implementations will return <b>:c </b>as well.</span></div>
<div><span style="font-size: 12pt;">* It's </span><b style="font-size: 12pt;">NOT OK</b><span style="font-size: 12pt;"> for
</span><i style="font-size: 12pt; font-weight: bold;">over_out</i><span style="font-size: 12pt;"> to declare that it returns
</span><b style="font-size: 12pt;">:a and :b</b><span style="font-size: 12pt;">, but to also return
</span><b style="font-size: 12pt;">:c</b><span style="font-size: 12pt;"> sometimes.
<b>Returning </b></span><b style="font-size: 12pt;">:c</b><span style="font-size: 12pt;"> </span>would<span style="font-size: 12pt;"> break the caller.</span></div>
<br>
<p></p>
<p>We can see the perfect <b>asymmetry </b>for inputs and outputs.</p>
<p>These are pretty-much <i>c</i><span><i>ovariance</i> and <i>contravariance</i></span> rules: you
<b>cannot </b><b>accept less </b>than you claim and you <b>cannot </b><b>produce more</b> than you claim.</p>
<p><br>
</p>
<p>Also we see how:</p>
<p>* -W<b>underspecs</b> option <b>detects </b><b>Input</b> Contract violations and produces
<b>false positives</b> for acceptable <b>Output</b> contracts</p>
<p>* -W<b>overspecs</b> option <b>detects </b><b>Output</b> Contract violations and produces<b> false positives</b> for acceptable<b> Input</b> contracts</p>
<p><br>
</p>
<p>That's why I'd like to enable <b>underspec_in</b> and <b>overspec_out</b> options (if they existed), as they are the 2 options detecting real problems (out of 4 possible combinations).</p>
<p><br>
</p>
<p></p>
<div style="color: rgb(212, 212, 212); background-color: rgb(30, 30, 30); font-family: Consolas, "Courier New", monospace; font-size: 14px; line-height: 19px;">
<div>
<div style="color: rgb(212, 212, 212); background-color: rgb(30, 30, 30); font-family: Consolas, "Courier New", monospace; font-size: 14px; line-height: 19px;">
<div>
<div style="color: rgb(212, 212, 212); background-color: rgb(30, 30, 30); font-family: Consolas, "Courier New", monospace; font-size: 14px; line-height: 19px;">
<div> <span style="color: #608b4e;"># suboptimal implementation, fine for caller</span></div>
<div> <span style="color: #9cdcfe;">@spec</span> over_in(x :: :a | :b) :: <span style="color: #569cd6;">nil</span></div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">over_in</span>(x) <span style="color: #c586c0;">when</span> x == :a or x == :b or x == :c <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #569cd6;">nil</span></div>
<div> <span style="color: #c586c0;">end</span></div>
<br>
<div> <span style="color: #608b4e;"># BROKEN caller contract, rejects input allowed by the spec</span></div>
<div> <span style="color: #9cdcfe;">@spec</span> under_in(x :: :a | :b | :c) :: <span style="color: #569cd6;">nil</span></div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">under_in</span>(x) <span style="color: #c586c0;">when</span> x == :a or x == :b <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #569cd6;">nil</span></div>
<div> <span style="color: #c586c0;">end</span></div>
<br>
<div> <span style="color: #608b4e;"># current implementation detail, does not concern caller</span></div>
<div> <span style="color: #9cdcfe;">@spec</span> under_out() :: :a | :b | :c</div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">under_out</span>() <span style="color: #c586c0;">do</span></div>
<div> produce_ab()</div>
<div> <span style="color: #c586c0;">end</span></div>
<br>
<div> <span style="color: #608b4e;"># BROKEN caller contract, could return unexpected value</span></div>
<div> <span style="color: #9cdcfe;">@spec</span> over_out() :: :a | :b</div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">over_out</span>() <span style="color: #c586c0;">do</span></div>
<div> produce_abc()</div>
<div> <span style="color: #c586c0;">end</span></div>
</div>
</div>
<br>
<div> <span style="color: #608b4e;"># helpers</span></div>
<div> </div>
<div> <span style="color: #9cdcfe;">@spec</span> produce_ab() :: :a | :b</div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">produce_ab</span>() <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #c586c0;">case</span> :rand.uniform(<span style="color: #b5cea8;">2</span>) <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #b5cea8;">1</span> -> :a</div>
<div> _ -> :b</div>
<div> <span style="color: #c586c0;">end</span></div>
<div> <span style="color: #c586c0;">end</span></div>
<br>
<div> <span style="color: #9cdcfe;">@spec</span> produce_abc() :: :a | :b | :c</div>
<div> <span style="color: #c586c0;">def</span> <span style="color: #dcdcaa;">produce_abc</span>() <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #c586c0;">case</span> :rand.uniform(<span style="color: #b5cea8;">3</span>) <span style="color: #c586c0;">do</span></div>
<div> <span style="color: #b5cea8;">1</span> -> :a</div>
<div> <span style="color: #b5cea8;">2</span> -> :b</div>
<div> _ -> :c</div>
<div> <span style="color: #c586c0;">end</span></div>
<div> <span style="color: #c586c0;">end</span></div>
</div>
</div>
</div>
<br>
<p></p>
<p>and the warnings are:</p>
<p><br>
</p>
<p></p>
<div style="color: rgb(212, 212, 212); background-color: rgb(30, 30, 30); font-family: Consolas, "Courier New", monospace; font-size: 14px; line-height: 19px;">
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);">
<div style="color: rgb(212, 212, 212); background-color: rgb(30, 30, 30); font-family: Consolas, "Courier New", monospace; font-size: 14px; line-height: 19px;">
<div>demo.ex:6: Type specification</div>
<div>'Elixir.Virt':over_in('a' | 'b') -> 'nil' is a subtype of the success typing:</div>
<div>'Elixir.Virt':over_in('a' | 'b' | 'c') -> 'nil'</div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);"><br>
</span></div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);">demo</span>.ex:12: Type specification</div>
<div>'Elixir.Virt':under_in('a' | 'b' | 'c') -> 'nil' is a supertype of the success typing:</div>
<div>'Elixir.Virt':under_in('a' | 'b') -> 'nil'</div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);"><br>
</span></div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);">demo</span>.ex:18: The specification for</div>
<div>'Elixir.Virt':under_out/0 states that the function might also return</div>
<div>'c' but the inferred return is</div>
<div>'a' | 'b'</div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);"><br>
</span></div>
<div><span style="color: rgb(212, 212, 212); font-family: Consolas, "Courier New", monospace; font-size: 14px; background-color: rgb(30, 30, 30);">demo</span>.ex:24: Type specification</div>
<div>'Elixir.Virt':over_out() -> 'a' | 'b' is a subtype of the success typing:</div>
<div>'Elixir.Virt':over_out() -> 'a' | 'b' | 'c'</div>
<div></div>
</div>
</span></div>
</div>
<br>
<p></p>
<p><span style="font-size: 12pt;">Thank you, Dmitry</span><br>
</p>
</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 8:46:00 AM<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 Fri, Mar 24, 2017 at 11:37 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 dir="ltr" class="gmail_msg">
<div id="m_1104362636394224897divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Arial,Helvetica,sans-serif" dir="ltr" class="gmail_msg">
Two of them that seem especially useful are <span class="gmail_msg"><i class="gmail_msg">underspecs
</i>and <i class="gmail_msg">overspecs</i>.</span>
<p class="gmail_msg"><span class="gmail_msg"></span></p>
</div>
</div>
</blockquote>
If you think about it, an overspecification is not really a problem with the code. The dialyzer uses inference analysis and makes a best effort at determining the type of a given function. Your contract specifies your usage of the function. When a overspec
happens, it is because your contract is more restrictive than the inference. This is usually not a problem. A small change in your function body might change the inferred type entirely. But unless you want to go change your contract all the time, it may be
better to keep it more restrictive. Lots of functions are more general than their intended use. Another problem is when the dialyzer fails to make a precise inference, so falls back to type any(). Enabling overspecs will make the system complain all the time
in this situation, but it may not be a problem.<br>
<br>
</div>
<div class="gmail_quote">Underspecs, on the other hand, could spell trouble. Here the inference is more restrictive, and thus there are inputs to the function which is within the contract, but won't make the code terminate as expected according to the inference
scheme. If your code never makes use of the extended contract, there is no problem, but as soon as some user tries to do so, things will go bad. The dialyzer will usually catch such a use quickly, but it is nicer to be strict in the contract if possible.<br>
<br>
</div>
<div class="gmail_quote">There are, however, situations where underspecs isn't that desirable as a property either. Suppose you are returning a map, such as #{ a => 37 }. The dialyzer can infer its success type to be #{ a := pos_integer() }[0]. But you may
have written a specification where you say a map() is returned. This is more general than the inferred type, and as such it is an underspec violation. Your contract isn't wrong, but on the other hand, it isn't precise either. A common problem that also hits
a lot are when you are declaring a binary(), but the dialyzer is able to figure out a more precise type scheme, for instance <<_:64, _:_*24>>. You will perhaps be more happy with just saying "this is a binary".<br>
<br>
</div>
<div class="gmail_quote">My usual recommendation is to start with the default set of warnings. Remove every error there, because the slogan is<br>
<br>
</div>
<div class="gmail_quote"> The dialyzer is never wrong!<br>
<br>
</div>
<div class="gmail_quote">and this is absolutely true. Once you have a dialyzer clean piece of code with the default warnings, you start turning on underspecs, no_return, and so on. But often this is more for understanding if there is anything that sticks out
as being too general.<br>
</div>
<div class="gmail_quote"><br>
<br>
</div>
<div class="gmail_quote">[0] This is strictly not true. If you *always* return 37, then it figures out the type is exactly the same response every time and tags its type as #{ a := 37 }. But for this exposition, I'm assuming your code returns "some positive
integer" where 37 is an example.<br>
<br>
</div>
</div>
</div>
</body>
</html>