<div dir="ltr">(Sorry, initially replied directly)<br><br>Replying <span>inline</span><div class="im"><br>> Whether a module conforms to a behaviour is something that<br>
> can change either way when a new version of the module is<br>
> loaded. Being time-dependent, it can't be part of a type.<br><br></div>Whether a function returns an iolist or an atom can change with<br>a next version of code too. But you expect that dialyzer run will<br>reveal this spec incompatibility. So if next version of the module<br>
will not implement behaviour it used to, why not to notify about<br>this?<br>I understand that this will not guarantee anything in runtime, you<br>still could load anything you want, but at least it could guarantee<br>me certain level of safety at dialyzer-run time.<div class="gmail_extra">
<br><br><div class="gmail_quote">2014-07-17 5:03 GMT+04:00 Richard A. O'Keefe <span dir="ltr"><<a href="mailto:ok@cs.otago.ac.nz" target="_blank">ok@cs.otago.ac.nz</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class=""><br>
On 17/07/2014, at 12:56 AM, Daniil Churikov wrote:<br>
> Is there any way to write a spec for dialyzer that will tell that I expect module of certain behaviour?<br>
<br>
</div>The types that the Dialyzer works with have no connection<br>
with the *state* of the Erlang system; it can only describe<br>
the shape of a term in and of itself. Types do not vary<br>
with time.<br>
<br>
You cannot have "registered process name" as a type.<br>
You cannot have "defined key in the process dictionary" as a type.<br>
You cannot have "loaded module" as a type.<br>
You cannot have "open port" as a type.<br>
<br>
Whether a module conforms to a behaviour is something that<br>
can change either way when a new version of the module is<br>
loaded. Being time-dependent, it can't be part of a type.<br>
<br>
This is not to say that *some* verification tool not utterly<br>
unlike a type checker might not be possible that could get<br>
closer to what you want. It's just that time-dependent<br>
properties are not commonly thought of as 'types'. Even in<br>
the languages I know about with dependent types, it's<br>
value dependency not time dependency that's in question.<br>
<br>
<br>
<br>
<br>
</blockquote></div><br></div></div>