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

问题描述：

在这种情况下，透析器对我来说表现得很奇怪，我还没有找到任何可以更好地理解它的东西。为什么不透析器检测到这种不良类型？

这是不是一个错误：

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: "[email protected]", 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: "[email protected]", name: "Deedub"}}  
    else 
    10 
    end 
    end 
end

在这种情况下，没有可能的分支的的类型指定匹配，并且透析说有此错误消息：

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>>}），所以它不是推论的问题。那么，为什么它不认识到其中一个分支不符合类型规范（它似乎很高兴，如果只是一个的分支符合，这不是我想要的）

我认为这里的“成功打字”部分解释了这一点：http://learnyousomeerlang.com/dialyzer。 “请记住，Dialyzer是乐观的，它对代码具有比喻性的信念，并且因为在某个时候调用convert/1函数成功的可能性，Dialyzer将保持沉默，在这种情况下没有报告类型错误。 – Dogbert

但这看起来不直观 - 在错误消息中*清楚*可以检测到每种可能的返回类型。也许这只是一个我可以设置的标志，说：“告诉我，如果其中一个分支不符合类型规格”？如果可能，我正在寻找更严格的类型检查程序，并且如果有必要，很乐意通过额外的挑战来解决问题。 – sgrove

你可以这样看：如果型号规格可以成功，Dialyzer不会报告任何错误，因为不完整的定义是有意的。在你的第一个例子中，你可以想象你的函数的正常（和记录）行为是返回'{：error，String.t}'（怪异不是它），而其他情况不应该发生 – Pascal

答

从LearnYou链接Dogbert提供，dialyzer会：

only complain on type errors that would guarantee a crash.

在你的第一个例子，如果年龄总是大于或等于100，你的函数将返回声明的类型。在第二个示例中，函数无法返回声明的类型。

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

I'm looking for a more rigorous type checker if possible.

不可能至今：

The Erlang Type System

The reason for not having a more elaborate type system is that none of the Erlang inventors knew how to write one, so it never got done. The advantage of a static type system is that errors can be predicted at compile time rather than at runtime, therefore allowing faults to be detected earlier and fixed at a lower cost. A number of people have tried to build a static type system for Erlang. Unfortunately, due to design decisions taken when Erlang was invented, no project has been able to write a comprehensive type system, since with hot code loading, this is intrinsically difficult. To quote Joe Armstrong in one of the many type system flame wars, "It seems like it should be 'easy'—and indeed, a few weeks programming can make a type system that handles 95% of the language. Several man-years of work [by some of the brightest minds in computer science] have gone into trying to fix up the other 5%—but this is really difficult."

从 “Erlang编程（弗朗西斯利尼&西蒙·汤普森）”。

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

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

相关推荐