Fl4m3Ph03n1x

Dialyzer does not catch errors on returned functions

Background

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.

Environment

$ 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)

Which version of Dialyxir are you using? (cat mix.lock | grep dialyxir):

"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"},

Current behavior

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)

Expected behavior

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.

Questions

Is dialyzer not intended to catch this type of error?
If it should catch the error, what can possibly be failing? (is it my example that is incorrect, or something inside dialyzer?)

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.

6 comments

/elixir

13 1232 6

2022-02-22 12:25:37 UTC

Marked As Solved

Fl4m3Ph03n1x

Answer

As far as I can understand, Dialyzer wont perform checks on input and output types of returned anonymous functions. The following example, much like mine, is incorrect, but the tool won’t complain:

# 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

If however, we try to call the function, Dialzyer might detect that the input and output types are incorrect, but if it does so there is a good chance it will default to the "Function has no local return" error message.

There is an excellent reply in StackOverflow (which I have quickly summarized here) that explains this behavior in more detail and even though we (I and the person replying) were not able to find a specific reason to the “why” of this happening, the empirical tests and samples are still of considerable value.

Upon skimming through the Dialyzer paper I found I was still unable to understand why the algorithm behaves this way, but I will leave it here in case someone else has a different take on it and is able to better understand this specific case:

Post #8

Also Liked

Fl4m3Ph03n1x

So, in this case, Dialyzer only check that greater_than returns a Function. It does not check what that Function returns (it assumes I know what I am doing), correct?

Post #4

Fl4m3Ph03n1x

I deeply respect your participation in this thread, but please forgive me if I am not yet convinced.
I am somewhat familiar with success typing:

From Type Specifications and Erlang:

The other option is then to have a type system that will not prove the absence of errors, but will do a best effort at detecting whatever it can. You can make such detection really good, but it will never be perfect. It’s a tradeoff to be made.

I understand dialyzer is not meant to be perfect. I am not after that here. I am trying to understand what classes of issues I can trust dialyzer.

If I understand (please forgive me if I don’t) you are defending the claim that dialyzer does not check function bodies. This is a falsifiable claim. Let’s see if I can falsify it:

defmodule Test do @type option(t) :: some(t) | nothing @type some(t) :: [t] @type nothing :: [] @spec validate_name(String.t()) :: option(String.t()) def validate_name(name) do if String.length(name) > 0 do [name] else nil end end end

Will return an error if run with mix dialyzer --overspecs.
A very good one also:

Total errors: 1, Skipped: 0, Unnecessary Skips: 0 done in 0m0.88s lib/test.ex:6:missing_range The type specification is missing types returned by function. Function: Test.validate_name/1 Type specification return types: [{:some, binary()}] Missing from spec: nil

This class of error would only be possible if dialyzer analyses the body of my functions, which is happening (it is checking my function returns nil and my spec does not cover that).

Now, I claim by no means to be an expert in dialzyer, and it may very well be that using different flags completely and totally changes the default algorithm in unimaginable ways.

But running this thread’s original sample with either --underspecs or --overspecs won’t make a difference.

If I can’t understand what I can trust Dialzyer with, my trust in this tool will be very limited. While gradient is a good idea, it is still, IMHO, very green and needs more time in the oven.

That is why I created this thread. I can’t understand what is happening. I need help.

Post #6

OvermindDL1

It’s just something to get used to with dialyzer. I do not, emphasis on NOT trust it to catch even most typing errors, it helps catch some things, but it still won’t catch most. If you are used to static typing systems it will not do well to compare it to those. It’s just another tool to catch some obvious type failures, just a linter essentially, but it’s not going to catch actual “Typing Issues” like a static type system would, there are many things its not capable of no matter how much information you give it.

Post #7