[erlang-questions] [Dialyser] Type parametrized behaviours

Matthew Sackman matthew@REDACTED
Thu Apr 26 02:20:02 CEST 2012


On Thu, Apr 26, 2012 at 12:57:19AM +0200, Kostis Sagonas wrote:
> In the general case,
> the behaviour module needs to have a way to define what the callback
> module *can* have as implementation of callbacks, not what it
> *should* have as its implementation. For example, it's perfectly ok
> for the behaviour module to say that there needs to be a callback
> function f/1 which can return 'foo' and 'bar' and for the callback
> module to implement a function that just returns 'bar'.

Absolutely. So we agree that 'foo' is a subtype of 'foo' | 'bar'. Just
so that we're on the same page, let us also define subtyping to be
symmetric - i.e. A is a subtype of A. Let us also define supertype to be
"if A is a subtype of B then B is a supertype of A".

> So, we do
> need both these attributes since they serve different purposes. This
> also means that the "header file approach" does not work / is not
> flexible enough in general.

In general, yes, I agree. I would add the following though:

If type inference on the callback module's function definition yields a
type that wider in the parameters and narrower in the result type, then
that is an acceptable implementation of the callback.

I.e. if the callback says :: (number()) -> (boolean() | 'undefined')
and the function is :: (number() | atom()) -> 'undefined' then that is
fine, as the callback spec is a subtype of the function in parameter and
a supertype in the result. As per the usual covariance/contravariance
methods.

Consequently, the only purpose of a spec in the module itself is for
clarity of documentation, or to explicitly provide a type that dialyzer
cannot infer.

> If I understand what you are sketching correctly, the problem I see
> is that since there will be no definition for state() in the
> behaviour module, that module will impose no constraints on what
> state() can be. Thus, your example is semantically equivalent to:
> 
> 	-callback step(X) -> Y.
> 
> for some arbitrary types X and Y. (Just take state() to be their union.)
> 
> The point is that the callback module is allowed to provide the
> following implementation of step/1
> 
> step(foo) -> 42.
> 
> and dialyzer (*) is obliged to keep silent in this case. As I wrote
> this case is actually fine. The callback module is allowed to
> implement only a portion of what the callback spec specifies. How is
> that different than what currently takes place other than perhaps
> requiring that the callback module contains a definition for
> state()? (Perhaps as liberal as -type state() :: 'foo' | 42.)

If I understand you correctly, the answer to your question is purely to
do with scoping of the type parameters. Rather than just leaving
individual functions as polymorphic, we wish to express that the
instantiation of the type parameter is the same across the callback.

The problem we wish to solve is that

-callback init() -> A.
-callback step(A) -> A.
-callback unstep(A) -> A.

would allow me to implement a module in which it is unsafe to write
unstep(step(init())), because those As may not be the same thing. For
example:

$ cat behave.erl 
-module(behave).
-export([behaviour_info/1]).
behaviour_info(callbacks) ->
    [{init, 0},
     {step, 1},
     {unstep, 1}];
behaviour_info(_Other) ->
    undefined.

$ cat foo.erl
-module(foo).
-export([init/0, step/1, unstep/1]).
-behaviour(behave).
init() ->
    5.
step(true) ->
    false.
unstep(wibble) ->
    wobble.

$ rm *.beam ; erlc behave.erl ; erlc -I . -pa . -Wall foo.erl
$ dialyzer foo.erl
  Checking whether the PLT /home/matthew/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.99s
done (passed successfully)


I want to prevent this as I choose to judge it illegal and I would like
dialyzer to help enforce this.

Thus the current solution is:

$ cat behave.erl
-module(behave).
-export([behaviour_info/1]).
behaviour_info(callbacks) ->
    [{init, 0},
     {step, 1},
     {unstep, 1}];
behaviour_info(_Other) ->
    undefined.

$ cat behave_specs.hrl
-spec init() -> state().
-spec step(state()) -> state().
-spec unstep(state()) -> state().

$ cat foo.erl
-module(foo).
-export([init/0, step/1, unstep/1]).
-behaviour(behave).
-type state() :: boolean().
-include("behave_specs.hrl").
init() ->
    5.
step(true) ->
    false.
unstep(wibble) ->
    wobble.

This will now be rejected, which is what I want.

As a user of modules which implement this behaviour, I want to know that
it is always safe to write M:unstep(M:step(M:init())). I don't care what
the ground type is, but I want dialyzer to be able to enforce this for
me. To do that, I can't use *just* the -callback attribute, because 1)
they do not allow the scope of polymorphic type parameters to be wider
than the callback attribute itself; and 2) they do not allow type
parameters to be defined in the callback modules themselves.

As you said, -callback and -spec do serve different roles. In our case,
it would seem of greater use to us for the -callback attributes to be
treated as templates for the -specs which can be further refined in the
module, thus achieving the same avoidance of duplication as we currently
do.

In short, the method we use with headers allows us to express more
accurate constraints with less duplication than the -callback attributes
alone would allow. If the -callback attributes are not designed to help
us achieve the sorts of abstractions and constraints that I've
described, then it becomes very unclear what additional functionality
the -callback attribute mechanism is providing.

I hope that's clearer.

Matthew



More information about the erlang-questions mailing list