Fl4m3Ph03n1x

Fl4m3Ph03n1x

Dialyzer cannot recognize error in function using polymorphic types

Background

I am trying out polymorphic typing with dialyzer. As an example I am using the famous Option type (aka, Maybe Monad) that is now prevalent in many other languages these days.

defmodule Test do
  @type option(t) :: some(t) | nothing
  @type some(t) :: [{:some, t}]
  @type nothing :: []

  @spec validate_name(String.t()) :: option(String.t())
  def validate_name(name) do
    if String.length(name) > 0 do
      [{:some, name}]
    else
      nil
    end
  end
end

As you can see, the function validate_name should return (by spec definition) [{:some, String.t}] | [].

The issue here is that in reality, the function is returning [{:some, String.t}] | nil. nil is not the same as empty list [].

Problem

Given this issue, I would expect dialyzer to complain. However it gladly accepts this erroneous spec:

$ mix dialyzer
Compiling 1 file (.ex)
Finding suitable PLTs
Checking PLT...
[:compiler, :currying, :elixir, :gradient, :gradualizer, :kernel, :logger, :stdlib, :syntax_tools]
PLT is up to date!
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.Book.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.DealingWithListsOfLists.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.Event.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.FlatMapsVSForComprehensions.beam',
   '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/lib/grokking_fp/ebin/Elixir.ImmutableValues.beam',
   ...],
  warnings: [:unknown]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m1.09s
done (passed successfully)

Furthermore, no matter what I put in the else branch, the result is always a “happy dialyzer”.

Question

At this point, the only logical solution I can think of is that dialyzer is only concerned with the happy path. Meaning, it will ignore my else branch.

If dialzyer is only ever concerned with happy paths, then this would explain the issue (it is called success typing after all) but it also means it will totally miss a bunch of errors in my code.

  • Is my assumption about dialyzer correct?
  • Is there a way to make it more precise in finding errors, or is this a limitation of the algorithm used by dialyzer ? (and therefore no fix is possible)

Marked As Solved

Fl4m3Ph03n1x

Fl4m3Ph03n1x

Answer

After talking with many folks I have come to understand that as long as 1 path in my code leads to a successful execution that is compatible with the specs I provide, dialyzer will not complain.

There may be many paths that break, but as long as 1 works, dialzyer is happy.

In my specific case, because I have a branch that returns [{:some, String.t}] dialyzer does not complain, because I have 1 branch that succeeds.

This can be better summarized in the quote from Type Specifications and Eralng:

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.

In fact, the article mentioned above, has an example case very similar to my own:

main() ->
    X = case fetch() of
        1 -> some_atom;
        2 -> 3.14
    end,
    convert(X).

convert(X) when is_atom(X) -> {atom, X}.

Which also does not trigger dialyzer. According to the article:

From our point of view, it appears that at some point in time, the call to convert/1 will fail.
(…)
Dialyzer doesn’t think so. (…) because there is the possibility that the function call to convert/1 succeeds at some point, Dialyzer will keep silent. No type error is reported in this case.

This is quite enlightening and I am convinced this is what is happening in my case.

Will dialyzer ever understand what is going on?

To be fair, this error can be caught by dialyzer if we use some flags, namelly --overspecs (for this case) and its sister --underspecs (which we don’t need for this case).

After some research I was able to find a mailing list that details the behaviour of these flags in a mathematical format:

From it:

Let SpecIn be a set of @spec inputs and RealIn be a set of inputs as inferred by Dialyzer from real code, then:

  • The Input Contract is satisfied when SpecIn <= RealIn (where <= is a non-strict subset operation). See over_in in demo code below.
  • The Input Contract violation is detected by -Wunderspecs option when SpecIn > RealIn. See under_in below.

It is easy to see in the code:

  • It’s OK for over_in to declare that it only accepts :a and :b while it also happens to accept :c. Maybe suboptimal, but fine.
  • It’s NOT OK for under_in to claim that it accepts :a, :b and :c and break if :c is passed. Rejecting :c would break the caller.

Let SpecOut be a set of @spec outputs and RealOut be a set of outputs as inferred by Dialyzer from real code, then:

  • The Output Contract is satisfied when SpecOut >= RealOut (where >= is a non-strict superset operation). See under_out below.
  • The Output Contract violation is detected by -Woverspecs option when SpecOut < RealOut. See over_out below.

It is easy to see in the code:

  • It’s OK for under_out to declare that it returns :a, :b and :c, while currently it only returns :a and :b. Maybe future implementations will return :c as well.
  • It’s NOT OK for over_out to declare that it returns :a and :b, but to also return :c sometimes. Returning :c would break the caller.

And indeed if I run mix dialyzer --overspecs with this sample, dialzyer does complain becasue:

The Output Contract violation is detected by -Woverspecs option when SpecOut < RealOut. See over_out below.

Where RealOut is [] | [t] | nil and SpecOut is [] | [t].
Therefore, a contract violation is detected.

Error shown:

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 was a wild ride through Dialyzer, and a revision I quite honestly needed. During the whole ordeal I learned about a couple of dialyzer flags and I refreshed my memory on success typing (which I absolutely needed to).

Thank you everyone for participating !

Also Liked

dimitarvp

dimitarvp

There’s likely special behaviour around empty lists in Erlang is my best guess. And dialyzer is widely admitted to not be the best at the job even by Erlang maintainers.

If I were you I’d try going all the way on nested tuples and have an Option type with {:option, {:some, value}} and {:option, :none} and see if Dialyzer chokes on those. I’d guess it wouldn’t.

Fl4m3Ph03n1x

Fl4m3Ph03n1x

Polymorphic types are one of the most powerful constructs in any Typing system. This is not about Option type, this is about how Dialyzer’s behaviour does not seem to fit correct behaviour.

Instead of Option, I could have Fruit[Banana] or Deck[Cards] or any other thing. Going down tuple lane would be a mere workaround. I am not looking for that here :smiley:

dimitarvp

dimitarvp

We have to work with what we have, right? Just not sure that what you’re looking for is even existing in the BEAM ecosystem.

Where Next?

Popular Backend topics Top

dimitarvp
As a part of my new job I’ll have to learn to manage a local k8s cluster. The tools used are microk8s, tilt and helm. I’ll appreciate an...
New
DevotionGeo
I know that -t flag is used along with -i flag for getting an interactive shell. But I cannot digest what the man page for docker run com...
New
New
Ookma-Kyi
I am learning Elixir at the moment but am finding it difficult to learn. The issue is there aren’t any good tutorial sites out there when...
New
Fl4m3Ph03n1x
Background I am trying out polymorphic typing with dialyzer. As an example I am using the famous Option type (aka, Maybe Monad) that is n...
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
JimmyCarterSon
Hello, I am working on a new application with Elixir, Dish_out. I want to see Data I follow this tutorial with Elixir Casts. However, I ...
New
sona11
If isReachable throws an IOException in Java, what is the right step to do and why? The application, I believe, should halt the process ...
New
Fl4m3Ph03n1x
Background I have to queries that return a colossal amount of data on their own. I cannot use Repo.all as doing so would materialize thes...
New
yamuna
Hi everyone, I’m trying to run deepseek-coder:6.7b-instruct-q4_K_M in Docker using Ollama to create an LLM that will be used by CrewAI a...
New

Other popular topics Top

Devtalk
Reading something? Working on something? Planning something? Changing jobs even!? If you’re up for sharing, please let us know what you’...
1037 19435 386
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
PragmaticBookshelf
Design and develop sophisticated 2D games that are as much fun to make as they are to play. From particle effects and pathfinding to soci...
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
Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
New
mafinar
This is going to be a long an frequently posted thread. While talking to a friend of mine who has taken data structure and algorithm cou...
New
AstonJ
If you get Can't find emacs in your PATH when trying to install Doom Emacs on your Mac you… just… need to install Emacs first! :lol: bre...
New
PragmaticBookshelf
Build efficient applications that exploit the unique benefits of a pure functional language, learning from an engineer who uses Haskell t...
New
AstonJ
Was just curious to see if any were around, found this one: I got 51/100: Not sure if it was meant to buy I am sure at times the b...
New
First poster: bot
zig/http.zig at 7cf2cbb33ef34c1d211135f56d30fe23b6cacd42 · ziglang/zig. General-purpose programming language and toolchain for maintaini...
New