Fl4m3Ph03n1x

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

  1. Is dialyzer not intended to catch this type of error?
  2. 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.

Marked As Solved

Fl4m3Ph03n1x

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:

Also Liked

Fl4m3Ph03n1x

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?

Fl4m3Ph03n1x

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.

OvermindDL1

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.

Where Next?

Popular Backend topics Top

Kurisu
Hello, Please, let’s say I have a website with user authentication made with Elixir/Phoenix, and now want to add a forum to it (using a ...
New
andrea
Can Phoenix LiveView be used in multi-page applications, unlike React/Vue/Blazor which seems to be targeted for SPA?
New
GermaVinsmoke
Reading Programming Elixir 1.6 book, I’ve completed part 1 of the book. Now I’m thinking of reading Elixir in Action. What do you all sug...
New
Fl4m3Ph03n1x
Background I am trying to get a Github Action working with Windows and Bakeware because I am trying to create a release using it. Howeve...
New
Fl4m3Ph03n1x
Background So, I am playing around with a concept named “NewType” and I am taking inspiration from languages like F# and Scala. My objec...
New
conradwt
Hi, I’m building an application that will have support for both the web and mobile. At this time, I’m using PhxGenAuth for authenticatio...
New
Ora2pgnewbie
Wanted to check if there is a UI available to use Ora2pg tool.
New
sona11
I wrote this code to calculate Fibonacci numbers by specifying the size. The results are correct, however the one thing that concerns me ...
New
Sumityadav
Hello all, I am new to learning Java Programming and want to learn java from scratch. I was writing a Java program to get the first and l...
New
Fl4m3Ph03n1x
Background I have a phoenix application in Windows 11. Unfortunately for me, I cannot compile the application because of a dependency err...
New

Other popular topics Top

AstonJ
What chair do you have while working… and why? Is there a ‘best’ type of chair or working position for developers?
New
siddhant3030
I’m thinking of buying a monitor that I can rotate to use as a vertical monitor? Also, I want to know if someone is using it for program...
New
AstonJ
There’s a whole world of custom keycaps out there that I didn’t know existed! Check out all of our Keycaps threads here: https://forum....
New
AstonJ
Thanks to @foxtrottwist’s and @Tomas’s posts in this thread: Poll: Which code editor do you use? I bought Onivim! :nerd_face: https://on...
New
Exadra37
I am asking for any distro that only has the bare-bones to be able to get a shell in the server and then just install the packages as we ...
New
New
PragmaticBookshelf
Author Spotlight Rebecca Skinner @RebeccaSkinner Welcome to our latest author spotlight, where we sit down with Rebecca Skinner, auth...
New
sir.laksmana_wenk
I’m able to do the “artistic” part of game-development; character designing/modeling, music, environment modeling, etc. However, I don’t...
New
AstonJ
This is cool! DEEPSEEK-V3 ON M4 MAC: BLAZING FAST INFERENCE ON APPLE SILICON We just witnessed something incredible: the largest open-s...
New
AstonJ
Curious what kind of results others are getting, I think actually prefer the 7B model to the 32B model, not only is it faster but the qua...
New