Elixir / Erlang Dialyzer：为什么行为回调的参数类型应该是子类型而不是超类型？

Question

我有一个行为X和一个参数类型的回调函数：

%{a: any}

模块 Y 实现行为 X，实现模块 Y 中的回调函数具有参数类型：

%{a: any, b: any}

透析器不喜欢这样，并抱怨：

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

这意味着透析器尝试确定实现模块 Y 中的回调参数类型是否是行为 X 中参数类型的超类型。换句话说，它问：

行为 X 的回调参数类型%{a: any}实现模块 Y 的参数类型%{a: any, b: any}？

为什么透析器期望行为回调的参数类型是子类型而不是超类型？

在编程语言类型理论的上下文中，子类型定义为：

类型 S

是类型 T 的子类型，写为 S <：T，如果表达式为 S 类型可用于需要 T 类型元素的任何上下文。 另一种说法是，任何 S 类型的表达式都可以 伪装成 T 型表达。

根据上面的定义，如果行为回调的参数类型T并且实现模块的参数类型S，对我来说是有意义的。因为实现模块仍然保留行为契约。然而，我不知道为什么透析器期望相反。

请帮助我理解这一点。

注意：这个问题是后续问题，但独立于另一个SO问题Erlang(Elixir)透析器 - 令人困惑的超型错误。

Answer 1

透析器是正确的。如果存在带有%{a: any}类型回调的行为X，用户应该能够调用任何声称实现此行为的模块的函数，例如%{a: 1}.你的模块的函数采用%{a: any, b: any}，这是%{a: any}的子类型，这意味着该函数不能再与不符合行为的%{a: 1}一起调用。

另一方面，如果行为的回调具有%{a: any, b: any}类型，并且模块的函数具有%{a: any}类型，那就没问题%{a: any}因为%{a: any, b: any}的超类型并且您的模块可以使用%{a: 1, b: 2}调用 - 它可以忽略额外的字段。