爲什麼不透析器檢測到這種不良類型？

在這種情況下，透析器對我來說表現得很奇怪，我還沒有找到任何可以更好地理解它的東西。爲什麼不透析器檢測到這種不良類型？

這是不是一個錯誤：

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>>}），所以它不是推論的問題。那麼，爲什麼它不認識到其中一個分支不符合類型規範（它似乎很高興，如果只是一個的分支符合，這不是我想要的）

來源

2017-06-04 sgrove

我認爲這裏的「成功打字」部分解釋了這一點：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。

來源

2017-06-05 01:51:05 7stud

爲什麼不透析器檢測到這種不良類型？

回答

相關問題