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.

Popular Backend topics Top

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
gagan7995
API 4 Path: /user/following/ Method: GET Description: Returns the list of all names of people whom the user follows Response [ { ...
New
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
sampu
I have a use case where a client is invoking a Rest endpoint via a load balancer, which in turn invokes a third party endpoint which is r...
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
JimmyCarterSon
I am confused about the Schema setup, I am setting up a new application and I want to seed files in it as well. I tried to mix to create...
New
Fl4m3Ph03n1x
Background I have recently been delving into more functional code. My objective right now is to get something similar to the IO Monad (in...
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
harwind
I received this error for a binary search programme in C, despite the fact that it requested for inputs and produced the right output. Th...
/c
New
Fl4m3Ph03n1x
Background I have an umbrella project, where I run mix test from the root. In one of the apps, I am mocking the File module using the Mo...
New

Other popular topics Top

Rainer
My first contact with Erlang was about 2 years ago when I used RabbitMQ, which is written in Erlang, for my job. This made me curious and...
New
AstonJ
We have a thread about the keyboards we have, but what about nice keyboards we come across that we want? If you have seen any that look n...
New
AstonJ
Inspired by this post from @Carter, which languages, frameworks or other tech or tools do you think is killing it right now? :upside_down...
New
AstonJ
I have seen the keycaps I want - they are due for a group-buy this week but won’t be delivered until October next year!!! :rofl: The Ser...
New
PragmaticBookshelf
Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
New
wmnnd
Here’s the story how one of the world’s first production deployments of LiveView came to be - and how trying to improve it almost caused ...
New
gagan7995
API 4 Path: /user/following/ Method: GET Description: Returns the list of all names of people whom the user follows Response [ { ...
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
PragmaticBookshelf
Author Spotlight: Bruce Tate @redrapids Programming languages always emerge out of need, and if that’s not always true, they’re defin...
New
AstonJ
If you’re getting errors like this: psql: error: connection to server on socket “/tmp/.s.PGSQL.5432” failed: No such file or directory ...
New

Latest in Questions

View all threads ❯