[erlang-questions] dialyzer and behaviours

Daniil Churikov ddosia@REDACTED
Thu Jul 17 09:47:53 CEST 2014


Thanks Siraaj, this is pretty close to what I meant.


2014-07-17 9:12 GMT+04:00 Siraaj Khandkar <siraaj@REDACTED>:

>
>
> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20140717/172642e5/attachment.htm>


More information about the erlang-questions mailing list