<div dir="ltr">Thanks Siraaj, this is pretty close to what I meant.</div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-07-17 9:12 GMT+04:00 Siraaj Khandkar <span dir="ltr"><<a href="mailto:siraaj@khandkar.net" target="_blank">siraaj@khandkar.net</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><br>
<br>
On 07/16/2014 09:03 PM, Richard A. O'Keefe wrote:<br>
><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>
> 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>
</div></div>Richard, what I think Daniil is asking for is only time-depended in a<br>
language like Erlang. In a statically typed language with a module<br>
system it'd be something like:<br>
<br>
    signature MY_DB =<br>
        sig<br>
            val table : unit -> iolist<br>
        end<br>
<br>
    functor Foo (Db_impl : MY_DB) =<br>
        struct<br>
            ...<br>
        end<br>
<br>
Daniil, is that what you had in mind? Unfortunately this is not possible<br>
in Erlang, because, as Richard said, calls to module names in Erlang are<br>
like calls to mutable, global reference cells. The only thing statically<br>
checkable is that the module name is of type atom(), while the<br>
implementation of a named module is always swappable at runtime.<br>
</blockquote></div><br></div>