Erlang (Elixir) Dialyzer - confusing supertype error

Question

I have defined an Elixir behaviour X. A callback start_link is spec'ed as:

@callback start_link(
  args :: producer_args,
  opts :: GenServer.options
) :: GenServer.on_start

where producer_args type is defined as:

@type producer_args :: %{job_queue_name: String.t}

In the client code Y that implements the behaviour, start_link is defined as:

def start_link(args = %{job_queue_name: _job_queue_name, redis_url: _redis_url}, opts) do
  GenStage.start_link(__MODULE__, args, opts)
end

Dialyzer doesn't like it. It says,

(#{'job_queue_name':=_, 'redis_url':=_, _=>_}) 
is not a supertype of 
#{'job_queue_name':=binary()}

Question #1:

In terms of inheritance, subtypes extend supertypes. Therefore, the defined behaviour(X) should be considered supertype. Module implementing the behaviour(Y) should be considered subtype. Apparently Dialyzer should have asked the question:

Is #{'job_queue_name':=binary()} a supertype of (#{'job_queue_name':=_, 'redis_url':=_, _=>_})?

Rather it asks the question the other way around. Why?

Question #2:

Is the definition of supertype in dialyzer the same as in discussion of OOP inheritance? If not, what is it then? I tried to find definition of supertype in the context of dialyzer but found none.

Answer 1

The error message is basically saying: You cannot require the additional redis_url key, since it was not declared in the type spec of the behaviour.

Dialyzer doesn't treat the behaviour and implementing module as types. It is specifically looking at the parameter to the callback.

The set of values that will match against #{'job_queue_name':=_, 'redis_url':=_, _=>_} is a subset of the values that will match against #{'job_queue_name':=_}.

So #{'job_queue_name':=_, 'redis_url':=_, _=>_} is a subtype of #{'job_queue_name':=_}.

Dialyzer will permit you to implement a callback with parameters that are supertypes of what was declared in the callback, since that ensures any code relying on the behaviour contract won't fail with a match error at runtime.

Answer 2

Regarding your second question:

The short answer is NO.

The long answer is a little bit more complicated. Erlang/Elixir are dynamic languages by nature (mostly due to the fact that ! and receive must handle any type) and it would be extremely hard to introduce any static type checking into the language. So new solution was proposed and implemented in form of Succes Types and Dialyzer.

You can find an introduction to the tool here and formal definition in original paper. And I could recommend recent talk on the matter.

It is not so straightforward approach as in other languages and in my experience, it's hard to find any experts in it. Error messages are cryptic, and even those who use it for quite some time more often guess what is wrong that actually know how he came to it. That said it is a very useful tool and any messages he spue out are worth investigating.

Few things worth notice are:

• Errors are not generated from mismatched specs in function definitions, but rather from function calls with concrete arguments. That's where you should be looking for bugs.
• Adding specs does not always help. A great example is add function presented in the talk. Where most people would use (bool(), bool()) the correct type is (any(), any()) or even (false, any()) | (any(), false) | (true, true). Sometimes all you need to do is fix your specification.
• If you can use typer to find out to what function specs dialazer derived to.