为什么透析器没有检测到这种不良类型？答案

【问题标题】：Why doesn't dialyzer detect this bad type?为什么透析器没有检测到这种不良类型？
【发布时间】：2017-11-05 15:08:27
【问题描述】：

在这种情况下，Dialyzer 的行为对我来说相当奇怪，我还没有找到任何可以更好地理解它的东西。

这不是错误：

defmodule Blog.UserResolver do
  @type one_user :: ( {:error, String.t} )

  @spec find(%{id: String.t}, any()) :: one_user

  def find(%{id: id}, _info) do
    age = :rand.uniform(99)
    if (age < 100) do
      # This doesn't trigger a type error, even though it's wrong
      {:ok, %{email: "dw@1g.io", name: "Deedub"}}      
    else 
    {:error, "Age isn't in the right range"}
    end
  end
end

请注意，可能的返回分支之一肯定与类型签名不匹配。

然而这确实有一个错误：

defmodule Blog.UserResolver do
  @type one_user :: ( {:error, String.t} )

  @spec find(%{id: String.t}, any()) :: one_user

  # Throws an error since no return path matches the type spec
  def find(%{id: id}, _info) do
    age = :rand.uniform(99)
    if (age < 100) do
      {:ok, %{email: "dw@1g.io", name: "Deedub"}}      
    else 
     10
    end
  end
end

在这种情况下，没有个可能的分支与 typespec 匹配，并且透析器说有以下错误消息：

web/blog/user_resolver.ex:4: Invalid type specification for function 'Elixir.Blog.UserResolver':find/2. The success typing is (#{'id':=_, _=>_},_) -> 10 | {'ok',#{'email':=<<_:64>>, 'name':=<<_:48>>}}

我不明白的部分是透析器清楚地识别了分支可能返回的两种不同类型（(#{'id':=_, _=>_},_) -> 10 | {'ok',#{'email':=<<_:64>>, 'name':=<<_:48>>}），所以这不是推理问题。那么为什么它不承认其中一个分支不符合类型规范（如果只有一个分支符合，这似乎很高兴，这根本不是我想要的）

【问题讨论】：

我认为这里的“成功输入”部分解释了这一点：learnyousomeerlang.com/dialyzer。 “请记住，Dialyzer 是乐观的。它对您的代码具有象征性的信心，并且由于对 convert/1 的函数调用有可能在某些时候成功，因此 Dialyzer 将保持沉默。在这种情况下不会报告类型错误。”
但这似乎不直观 - 在错误消息中它清楚地 可以检测到所有可能的返回类型。也许这只是我可以设置的一个标志，上面写着“如果其中一个分支与类型规范不匹配，请告诉我”？如果可能的话，我正在寻找一个更严格的类型检查器，如果有必要，我很乐意通过额外的挑战。
可以这样看：如果类型指定成功，Dialyzer不会报错，因为不完整的定义是故意的。在您的第一个示例中，您可以想象您的函数的正常（和记录）行为是返回 {:error, String.t}（不是很奇怪），而其他情况不应发生

标签： erlang elixir dialyzer

【解决方案1】：

通过 Dogbert 提供的 LearnYou 链接，dialyzer 将：

只抱怨会导致崩溃的类型错误。

在您的第一个示例中，如果年龄始终大于或等于 100，则您的函数将返回声明的类型。在第二个示例中，您的函数无法返回声明的类型。

dialyzer 创建一组约束方程。如果这些方程有任何解，那么透析器就不会抱怨。 Erlang 是作为一种动态类型语言创建的。 dialyzer 只是有人事后编写的程序。出于我确信他们深思、讨论和理论化的原因，dialyzer 的设计者选择了该功能。

如果可能的话，我正在寻找更严格的类型检查器。

目前不可能：

Erlang 类型系统

没有更精细的类型系统的原因是没有一个 Erlang 的发明者知道如何编写一个，所以它从未完成。这静态类型系统的优点是可以在编译时而不是运行时，因此允许出现错误更早发现并以更低的成本修复。许多人有试图为 Erlang 构建一个静态类型系统。不幸的是，由于发明 Erlang 时做出的设计决策，还没有任何项目能够编写一个全面的类型系统，因为使用热代码加载，这本质上是困难的。引用乔·阿姆斯特朗的话许多类型系统的火焰战争之一，“看起来应该是 “简单”——事实上，几个星期的编程就可以创建一个类型系统，处理 95% 的语言。几个人年的工作[由一些计算机科学领域最聪明的人]已经开始尝试修复剩下的 5%——但这真的很难。”

来自“Erlang Programming (Francesco Cesarini & Simon Thompson)”。

需要test suite 来控制动态类型的程序。 Elixir 只是 Erlang 的 Rubified 版本。 Ruby 也是一种动态类型语言——但它没有透析器。 Ruby 唯一的功能就是测试。您使用测试套件来控制计算机编程语言的狂野西部——而不是编译器。如果您需要静态类型语言，那么 Erlang 的 Rubified 版本不是一个好选择——请参阅 Haskell。

【讨论】：