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.

Obscenity

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.

Conditional

If I remove redis_url property, dialyzer is happy. So, binary vs any is not the problem. – Obscenity

What dialyzer attempts is to determine if param type of behaviour's callback is a subtype of implementing module's param type (or calling function's argument type). Why? Shouldn't it be: if callback's param type is a supertype or not? That way it could have been guaranteed that the behaviour contract won't fail. Now it's possible for the contract to fail and dialyzer won't report it. – Obscenity

Isn't the example in your original question exactly an example of where dialyzer does report a contract failure? The code implementing the behaviour declared callback with a subtype for the parameter (the additional redis_url key). This would cause calling code to fail. Dialyzer correctly reports the error. – Conditional

My confusion was cleared in a separate question: #46315201 My train of thought was in the wrong direction and I was corrected. – Obscenity

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.

Milk

Thanks for your answer. You said it's not the same supertype as in OOP. Then how would you define / determine if a type A is a supertype of type B? – Obscenity

The second question is worth a separate SO question. I'm gonna create one. I'll appreciate if you could answer that. – Obscenity

I changed my mind. Not gonna create a separate question. Looks like it's related to programming language subtyping: en.wikipedia.org/wiki/Subtyping – Obscenity

From paper Since these unions can become large or even infinite, in our analysis we impose a fixed size limit after which the union is widened to a supertype. [...] union type 1 ∪ 2 ∪ 3 ∪ 4 will be widened to integer(). – Milk