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

New
Kurisu
Following on an old discussion I started on Elixir Forum here, I finally made my mind to learn Ruby on Rails in addition to Elixir/Phoen...
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
s2k
I have this code in a file that’s used to … render templates. require 'erb' require 'ostruct' MISSING_CONFIG_MARKER = :config_key_and_v...
New
JimmyCarterSon
Hello, I am. very new to Elixir lang I have only been doing it for about 2 weeks. I recently started following this tutorial todo list, ...
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
sona11
I’m having a difficulty. I want to modify an attribute’s data type from String to Array. { “id”: “trn:tarb:tradingpartner:uuid:00000...
New
Fl4m3Ph03n1x
Background When trying to execute mix release on a Windows 11 machine for a Phoenix project I get the following error: * assembling mark...
New
pillaiindu
Currently reading the book “Programming Phoenix LiveView”. At the end of the Chapter 1, I’m trying to solve the guess game. If the user ...
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

AstonJ
If it’s a mechanical keyboard, which switches do you have? Would you recommend it? Why? What will your next keyboard be? Pics always w...
New
axelson
I’ve been really enjoying obsidian.md: It is very snappy (even though it is based on Electron). I love that it is all local by defaul...
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
I ended up cancelling my Moonlander order as I think it’s just going to be a bit too bulky for me. I think the Planck and the Preonic (o...
New
dimitarvp
Small essay with thoughts on macOS vs. Linux: I know @Exadra37 is just waiting around the corner to scream at me “I TOLD YOU SO!!!” but I...
New
PragmaticBookshelf
Use WebRTC to build web applications that stream media and data in real time directly from one user to another, all in the browser. ...
New
AstonJ
Saw this on TikTok of all places! :lol: Anyone heard of them before? Lite:
New
PragmaticBookshelf
Author Spotlight Rebecca Skinner @RebeccaSkinner Welcome to our latest author spotlight, where we sit down with Rebecca Skinner, auth...
New
husaindevelop
Inside our android webview app, we are trying to paste the copied content from another app eg (notes) using navigator.clipboard.readtext ...
New
AnfaengerAlex
Hello, I’m a beginner in Android development and I’m facing an issue with my project setup. In my build.gradle.kts file, I have the foll...
New