[erlang-questions] dialyzer and behaviours

[Siraaj Khandkar]

On 07/16/2014 09:03 PM, Richard A. O'Keefe wrote:
> 
> 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.
>

Richard, what I think Daniil is asking for is only time-depended in a
language like Erlang. In a statically typed language with a module
system it'd be something like:

    signature MY_DB =
        sig
            val table : unit -> iolist
        end

    functor Foo (Db_impl : MY_DB) =
        struct
            ...
        end

Daniil, is that what you had in mind? Unfortunately this is not possible
in Erlang, because, as Richard said, calls to module names in Erlang are
like calls to mutable, global reference cells. The only thing statically
checkable is that the module name is of type atom(), while the
implementation of a named module is always swappable at runtime.