Dialyzer 无法识别使用多态类型的函数中的错误

Question

背景

我正在尝试使用透析器进行多态输入。作为一个例子，我使用了著名的Option 类型（又名，Maybe Monad），它现在在许多其他语言中很流行。

defmodule Test do
  @type option(t) :: some(t) | nothing
  @type some(t) :: [{:some, t}]
  @type nothing :: []

  @spec validate_name(String.t()) :: option(String.t())
  def validate_name(name) do
    if String.length(name) > 0 do
      [{:some, name}]
    else
      nil
    end
  end
end

如您所见，函数 validate_name 应该返回（根据规范定义）[{:some, String.t}] | []。

这里的问题是，实际上，该函数返回[{:some, String.t}] | nil。 nil 与空列表[] 不同。

问题

考虑到这个问题，我希望透析器会抱怨。但是它很乐意接受这个错误的规范：

$ mix dialyzer
Compiling 1 file (.ex)
Finding suitable PLTs
Checking PLT...
[:compiler, :currying, :elixir, :gradient, :gradualizer, :kernel, :logger, :stdlib, :syntax_tools]
PLT is up to date!
No :ignore_warnings opt specified in mix.exs and default does not exist.

Starting Dialyzer
[
  check_plt: false,
  init_plt: '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt',
  files: ['/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.Book.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.DealingWithListsOfLists.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.Event.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.FlatMapsVSForComprehensions.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.ImmutableValues.beam',
   ...],
  warnings: [:unknown]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m1.09s
done (passed successfully)

此外，无论我在else 分支中放什么，结果始终是“快乐的透析器”。

问题

此时，我能想到的唯一合乎逻辑的解决方案是透析器仅关注幸福路径。意思是，它将忽略我的else 分支。

如果 dialzyer 只关心快乐路径，那么这可以解释问题（毕竟它被称为成功输入），但这也意味着它会完全错过我的代码中的一堆错误。

• 我对透析器的假设是否正确？
• 有没有办法让它更精确地发现错误，或者这是透析器使用的算法的限制？ （因此无法修复）

Answer 1

也意味着它会完全错过我的代码中的一堆错误。

您的理解是正确的，dialyzer 不是静态类型系统，它只能检测到会导致确认类型冲突的错误子集。这个detailed article 解释了透析器背后的设计和权衡。

虽然有一些警告标志，例如underspecs / overspecs / specdiffs，但可以启用以检测更多类别的错误：可以找到列表here，dialyxir 支持它们为command line options .

如果运行mix dialyzer --overspecs（或--specdiffs），你应该得到：

your_file.ex:6:missing_range
The type specification is missing types returned by function.

Function:
Test.validate_name/1

Type specification return types:
[{:some, binary()}]

Missing from spec:
nil

运行mix dialyzer.explain missing_range:

Function spec declares a list of types, but function returns value
outside stated range.

This error only appears with the :overspecs flag.

编辑：自 OTP 25 起，Dialyzer 将引入 two new flags：missing_return 和 extra_return，分别类似于 overspecs 和 underspecs，但误报更少，在实践中更有用。

missing_return 将捕获上面的 missing_range 示例，但不会返回很多您可能并不真正关心的嘈杂的 contract_subtype 警告，就像 overspecs 一样。

Answer 2

总结

免责声明：这是我寻找这个问题的答案的冒险总结。短版请查看@sabiwara的response。

在与许多人交谈后，我了解到只要我的代码中的 1 条路径能够成功执行并且与我提供的规范兼容，dialyzer 就不会抱怨。

可能有很多路径会中断，但只要 1 有效，Dialzyer 就很高兴。

在我的具体情况下，因为我有一个返回 [{:some, String.t}] 的分支，所以透析器不会抱怨，因为我有 1 个分支成功。

这可以在Type Specifications and Eralng的引用中得到更好的总结：

另一个选择是拥有一个类型系统，它不会证明没有错误，但会尽最大努力检测它可以检测到的任何东西。你可以使这种检测非常好，但它永远不会是完美的。这是一个权衡。

其实上面提到的那篇文章，有一个和我自己很相似的例子：

main() ->
    X = case fetch() of
        1 -> some_atom;
        2 -> 3.14
    end,
    convert(X).

convert(X) when is_atom(X) -> {atom, X}.

这也不会触发透析器。根据文章：

从我们的角度来看，似乎在某个时间点，对convert/1 的调用将失败。 (...) 透析器不这么认为。 (...) 因为对convert/1 的函数调用有可能在某个时候成功，所以Dialyzer 将保持沉默。这种情况下不会报类型错误。

这很有启发性，我相信这就是我的情况。

透析器会知道发生了什么吗？

公平地说，如果我们使用一些标志，即--overspecs（对于这种情况）及其姊妹--underspecs（对于这种情况，我们不需要），透析器可以捕获此错误。

经过一番研究，我找到了一个邮件列表，以数学格式详细说明了这些标志的行为：

• [erlang-questions] Dialyzer underspecs and overspecs options

来自它：

令 SpecIn 为一组@spec 输入，RealIn 为一组输入，如 Dialyzer 从真实代码中推断出的，那么：

• 当 SpecIn
• 当 SpecIn > RealIn 时，-Wunderspecs 选项检测到输入合同违规。请参阅下面的 under_in。

在代码中很容易看出：

• over_in 可以声明它只接受 :a 和 :b 而它也恰好接受 :c。也许不是最理想的，但很好。
• under_in 不能声称它接受 :a、:b 和 :c 并在 :c 被传递时中断。拒绝 :c 会破坏调用者。

令 SpecOut 为一组 @spec 输出，RealOut 为一组输出，如 Dialyzer 从真实代码中推断出的，那么：

• 当 SpecOut >= RealOut（其中 >= 是非严格的超集操作）时，输出协定得到满足。请参阅下面的 under_out。
• 当 SpecOut

在代码中很容易看出：

• under_out 可以声明它返回:a、:b 和:c，而目前它只返回:a 和:b。也许未来的实现也会返回 :c。
• over_out 不能声明它返回 :a 和 :b，但有时也返回 :c。返回 :c 会破坏调用者。

事实上，如果我用这个样本运行mix dialyzer --overspecs，Dialzyer 确实会抱怨，因为：

当 SpecOut

其中 RealOut 是 [] | [t] | nil 而 SpecOut 是 [] | [t]。 因此，检测到违反合同。

显示错误：

lib/test.ex:6:missing_range
The type specification is missing types returned by function.

Function:
Test.validate_name/1

Type specification return types:
[{:some, binary()}]

Missing from spec:
nil

这是一次通过 Dialyzer 的疯狂之旅，而且我确实需要一个修订版。在整个磨难过程中，我了解了一些透析器标志，并在成功打字时刷新了我的记忆（我绝对需要这样做）。

感谢大家的参与！