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

bsek43
Hello everyone, I’ve started learning Elixir and Phoenix few months ago and while I mostly grasped Elixir’s functional concepts and Phoe...
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 I am trying to encode a structure into json format using the Jason library. However, this is not working as expected. Code L...
New
GermaVinsmoke
Does anyone know beginner friendly Elixir/Phoenix Open source projects? For learning purpose :slightly_smiling_face:
New
Ora2pgnewbie
Wanted to check if there is a UI available to use Ora2pg tool.
New
AstonJ
If when trying to create (or recreate) your dev db with rails db:create you are getting: PG::ConnectionBad: connection to server on soc...
New
sona11
In Java, if I try to do.equals() on a null string, a null pointer error is issued. I’m wondering whether I can perform the following if I...
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
Fl4m3Ph03n1x
Background As I often do, I read books to learn and improve myself. I also enjoy teaching and helping others when I can, so this is somet...
New
Shiny
Hey community, this is my first post here so I will try to be as concise as possible and I appreciate any feedback. I’ve been writing Ro...
New

Other popular topics Top

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
New
AstonJ
poll poll Be sure to check out @Dusty’s article posted here: An Introduction to Alternative Keyboard Layouts It’s one of the best write-...
New
AstonJ
I’ve been hearing quite a lot of comments relating to the sound of a keyboard, with one of the most desirable of these called ‘thock’, he...
New
AstonJ
Seems like a lot of people caught it - just wondered whether any of you did? As far as I know I didn’t, but it wouldn’t surprise me if I...
New
PragmaticBookshelf
Build efficient applications that exploit the unique benefits of a pure functional language, learning from an engineer who uses Haskell t...
New
PragmaticBookshelf
Author Spotlight Jamis Buck @jamis This month, we have the pleasure of spotlighting author Jamis Buck, who has written Mazes for Prog...
New
New
First poster: bot
zig/http.zig at 7cf2cbb33ef34c1d211135f56d30fe23b6cacd42 · ziglang/zig. General-purpose programming language and toolchain for maintaini...
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