Elixir / Erlang Dialyzer : Why behaviour callback's param type should be subtype instead of supertype?

Question

I have a behaviour X and a callback function with parameter type:

%{a: any}

Module Y implements behaviour X and the callback function in implementing module Y has parameter type:

%{a: any, b: any}

Dialyzer doesn't like that and complains:

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

This implies dialyzer attempts to determine if callback parameter's type in implementing module Y is a supertype of param type in behaviour X. In other words, it asks:

Is behaviour X's callback param type %{a: any} a subtype of implementing module Y's param type %{a: any, b: any}?

Why does dialyzer expect behaviour callback's param type to be a subtype instead of a supertype?

In the context of programming language type theory, subtype is defined as:

type S is a subtype of a type T, written S <: T, if an expression of type S can be used in any context that expects an element of type T. Another way of putting this is that any expression of type S can masquerade as an expression of type T.

In light of the definition above, it makes sense to me if parameter type of behaviour callback is T and that of implementing module is S. Because implementing module still keeps the behaviour contract. However, I'm clueless as to why dialyzer expects the other way around.

Please help me understand this.

Note: This question is a follow-up but independent of another SO question Erlang (Elixir) Dialyzer - confusing supertype error.

Protrusile

Because implementing module still keeps the behaviour contract. I don't think it does. Now you have a module that you say implements X but no one can actually call the function with %{a: any} as the behavior says because your implementation also requires b: any in the map. – Campinas

Even though implementing module Y requires additional b: any in the map, it's good to allow any operation that can be performed on the original type specified by behaviour X. It respects width subtyping rule: en.wikipedia.org/wiki/Subtyping#Width_and_depth_subtyping – Protrusile

"it still allows all operations on the original type specified by behaviour X" According to the behaviour I should be able to pass %{a: 1} to all the implementors of X but I can't do that to Y because it requires an additional field :b. The reverse is fine -- if X requires %{a: any, b: any} and Y requires %{a: any}, that's fine because I can call it like the behaviour says and b will be ignored by Y. – Campinas

Just had an aha moment! Didn't think from that angle. Thanks a lot. This is very useful. Can you please put that in an answer so I can accept it? We're more likely to read an accepted answer than to read comments. – Protrusile

Answer 1

Dialyzer is correct. If there is a behaviour X with a callback of type %{a: any}, the user should be able to call that function of any module that claims to implement this behaviour with e.g. %{a: 1}. Your module's function takes %{a: any, b: any} which is a subtype of %{a: any}, which means that function cannot be called with %{a: 1} anymore which does not comply with the behaviour.

On the other hand, if the behaviour's callback had the type %{a: any, b: any} and your module's function had the type %{a: any}, that would have been fine because %{a: any} is a supertype of %{a: any, b: any} and your module can be called with %{a: 1, b: 2} -- it can just ignore the extra field.

Campinas