1

背景

在使用透析器、typespecs 和 currying 时，我能够在透析器中创建一个误报示例。

出于本MWE的目的，我正在使用diallyxir（包括版本），因为它让我的生活更轻松。dialyxir 的作者证实这对他们来说不是问题，因此目前排除了这种可能性。

环境

$ elixir -v
Erlang/OTP 24 [erts-12.2.1] [source] [64-bit] [smp:12:12] [ds:12:12:10] [async-threads:1] [jit]
Elixir 1.13.2 (compiled with Erlang/OTP 24)
  • 您使用的是哪个版本的 Dialyxir？（猫 mix.lock | grep 透析器）：
"dialyxir": {:hex, :dialyxir, "1.1.0", "c5aab0d6e71e5522e77beff7ba9e08f8e02bad90dfbeffae60eaf0cb47e29488", [:mix], [{:erlex, ">= 0.2.6", [hex: :erlex, repo: "hexpm", optional: false]}], "hexpm", "07ea8e49c45f15264ebe6d5b93799d4dd56a44036cf42d0ad9c960bc266c0b9a"},
"erlex": {:hex, :erlex, "0.2.6", "c7987d15e899c7a2f34f5420d2a2ea0d659682c06ac607572df55a43753aa12e", [:mix], [], "hexpm", "2ed2e25711feb44d52b17d2780eabf998452f6efda104877a3881c2f8c0c0c75"},

当前行为

给定以下代码示例：

defmodule PracticingCurrying do

  @spec greater_than(integer()) :: (integer() -> String.t())
  def greater_than(min) do
    fn number -> number > min end
  end

end

显然输入错误，我收到一条成功消息：

$ mix dialyzer
Compiling 1 file (.ex)
Generated grokking_fp app
Finding suitable PLTs
Checking PLT...
[:compiler, :currying, :elixir, :gradient, :gradualizer, :kernel, :logger, :stdlib, :syntax_tools]
Looking up modules in dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt
Finding applications for dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt
Finding modules for dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt
Checking 518 modules in dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt
Adding 44 modules to dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt
done in 0m24.18s
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.ImmutableValues.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.PracticingCurrying.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.TipCalculator.beam'],
  warnings: [:unknown]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m1.02s
done (passed successfully)

预期行为

我希望透析器告诉我正确的规格是 @spec greater_than(integer()) :: (integer() -> bool()).

作为旁注（和比较，如果你愿意的话）梯度确实会发现错误。我知道比较这些工具就像比较橘子和苹果，但我认为还是值得一提。

问题

  1. 透析器不打算捕捉这种类型的错误吗？
  2. 如果它应该捕获错误，那么可能会失败吗？（是我的例子不正确，还是透析器内部的东西？）

我个人很难相信这可能是 Dialyzer 中的错误，该工具已被很多人广泛使用，我是第一个发现此错误的人。但是，我无法解释发生了什么。

帮助表示赞赏。

4

1 回答 1

1

Dialyzer 的分析相当乐观，忽略了某些类别的错误。 本文提供了一些关于其方法和局限性的高级解释。

在匿名函数的特殊情况下，dialyzer 似乎在声明它们时执行了非常小的检查：它将忽略其参数的类型和返回类型，例如，即使明显错误，以下内容也不会导致任何错误：

# no error
@spec add(integer()) :: (String.t() -> String.t())
def add(x) do
  fn y -> x + y end
end

然而，它会指出数量不匹配，例如

# invalid_contract
# The @spec for the function does not match the success typing of the function.

@spec add2(integer()) :: (integer(), integer() -> integer())
def add2(x) do
  fn y -> x + y end
end

在尝试使用匿名函数时，Dialyzer 可能能够检测到类型冲突，但这不能保证（参见上面的文章），并且错误消息可能没有帮助：

# Function main/0 has no local return.

def main do
  positive? = greater_than(0)
  positive?.(2)
end

我们不知道究竟是什么问题，甚至不知道导致错误的行。但至少我们知道有一个并且可以调试它。

在以下示例中，错误信息更丰富（使用:lists.map/2而不是Enum.map/2因为透析器不理解可枚举协议）：

# Function main2/0 has no local return.

def main2 do
  positive? = greater_than(0)

  # The function call will not succeed.
  # :lists.map(_positive? :: (integer() -> none()), [-2 | 0 | 1, ...])
  # will never return since the success typing arguments are
  # ((_ -> any()), [any()])

  :lists.map(positive?, [1, 0, -2])
end

这告诉我们，dialyzer 推断出返回类型greater_than/1为 be (integer() -> none())。 none在上面的文章中描述为：

这是一种特殊类型，意味着没有任何术语或类型是有效的。通常，当 Dialyzer 将函数的可能返回值归结为 时none()，这意味着该函数应该崩溃。它是“这东西行不通”的同义词。

所以dialyzer知道这个函数不能被成功调用，但是在实际调用之前不会认为是类型冲突，所以它会允许声明（同样的方式你可以完美地创建一个只有raises的函数）。

免责声明：官方没有找到关于dialyzer如何处理匿名函数的详细解释，所以上面的解释是基于我的观察和解释

于 2022-02-22T10:06:53.543 回答