Dialyzer behaves rather strangely to me in this case, and I haven't found anything to better understand it.
This is not an error:
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
Note that one of the possible return branches definitely does not match with the type signature.
This however does have an error:
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
In this case, none of the possible branches match the typespec, and dialyzer says has this error message:
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>>}}
The part I don't understand is that dialyzer clearly recognizes the two different types the branches may return ((#{'id':=_, _=>_},_) -> 10 | {'ok',#{'email':=<<_:64>>, 'name':=<<_:48>>}), so it's not a problem of inference. So why then does it not recognize that one of the branches does not conform to the type spec (it seems to be happy if just one of the branches conforms, which is not what I want at all)
From the LearnYou link that Dogbert provided, dialyzer will:
only complain on type errors that would guarantee a crash.
In your first example, if age is always greater than or equal to 100, your function will return the declared type. In the second example, there is no way for your function to return the declared type.
dialyzer creates a set of constraint equations. If there is any solution to those equations, then dialyzer won't complain. Erlang was created as a dynamically typed language. dialyzer is just a program someone wrote after the fact. For reasons I'm sure they pondered over and discussed and theorized about, the designers of dialyzer chose that functionality.
I'm looking for a more rigorous type checker if possible.
Not possible so far:
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."
From "Erlang Programming (Francesco Cesarini & Simon Thompson)".
A test suite is required to keep dynamically typed programs under control. Elixir is just a Rubified version of Erlang. Ruby is also a dynamically typed language--but it has no dialyzer. The only thing Ruby has is testing. You use test suites to keep the Wild West of computer programming languages under control--not a compiler. If you require a statically typed language, then a Rubified version of Erlang wasn't a great choice--see Haskell.