While playing around with dialyzer, typespecs and currying, I was able to create an example of a false positive in dialyzer.
For the purposes of this MWE, I am using diallyxir (versions included) because it makes my life easier. The author of dialyxir confirmed this was not a problem on their side, so that possibility is excluded for now.
$ 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": {: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"},
Given the following code sample:
defmodule PracticingCurrying do
@spec greater_than(integer()) :: (integer() -> String.t())
def greater_than(min) do
fn number -> number > min end
end
end
Which clearly has a wrong typing, I get a success message:
$ 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)
I expected dialyzer to tell me the correct spec is @spec greater_than(integer()) :: (integer() -> bool())
.
As a side note (and comparison, if you will) gradient does pick up the error. I know that comparing these tools is like comparing oranges and apples, but I think it is still worth mentioning.
I personally find it hard to believe this could be a bug in Dialyzer, the tool has been used rather extensively by a lot of people for me to be the first to discover this error. However, I cannot explain what is happening.
Help is appreciated.
Dialyzer is pretty optimistic in its analysis and ignores some categories of errors. This article provides some advanced explanations about its approach and limitations.
In the particular case of anonymous functions, dialyzer seems to perform a very minimal check when they are being declared: it will ignore both the types of its arguments and return type, e.g. the following doesn't lead any error even if is clearly wrong:
# no error
@spec add(integer()) :: (String.t() -> String.t())
def add(x) do
fn y -> x + y end
end
It will however point out a mismatch in arity, e.g.
# 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 might be able to detect a type conflict when trying to use the anonymous function, but this isn't guaranteed (see article above), and the error message might not be helpful:
# Function main/0 has no local return.
def main do
positive? = greater_than(0)
positive?.(2)
end
We don't know what is the problem exactly, not even the line causing the error. But at least we know there is one and can debug it.
In the following example, the error is a bit more informative (using :lists.map/2
instead of Enum.map/2
because
dialyzer doesn't understand the enumerable protocol):
# 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
This tells us that dialyzer inferred the return type of greater_than/1
to be (integer() -> none())
.
none
is described in the article above as:
This is a special type that means that no term or type is valid. Usually, when Dialyzer boils down the possible return values of a function to
none()
, it means the function should crash. It is synonymous with "this stuff won't work."
So dialyzer knows that this function cannot be called successfully, but doesn't consider it to be a type clash until actually called, so it will allow the declaration (in the same way you can perfectly create a function that just raise
s).
Disclaimer: I couldn't find an official explanation regarding how dialyzer handles anonymous functions in detail, so the explanations above are based on my observations and interpretation