[erlang-questions] dialyzer and behaviours

[Richard A. O'Keefe]

On 17/07/2014, at 12:56 AM, Daniil Churikov wrote:
> Is there any way to write a spec for dialyzer that will tell that I expect module of certain behaviour?

The types that the Dialyzer works with have no connection
with the *state* of the Erlang system; it can only describe
the shape of a term in and of itself.  Types do not vary
with time.

You cannot have "registered process name" as a type.
You cannot have "defined key in the process dictionary" as a type.
You cannot have "loaded module" as a type.
You cannot have "open port" as a type.

Whether a module conforms to a behaviour is something that
can change either way when a new version of the module is
loaded.  Being time-dependent, it can't be part of a type.

This is not to say that *some* verification tool not utterly
unlike a type checker might not be possible that could get
closer to what you want.  It's just that time-dependent
properties are not commonly thought of as 'types'.  Even in
the languages I know about with dependent types, it's
value dependency not time dependency that's in question.