Dialyzer and raise exception behavior

[Fl4m3Ph03n1x]

Background

I have a very minimalistic function that can return a boolean or blow up:

defmodule TestDialzer do

  @spec hello(integer) :: boolean
  def hello(n) do

    if n == 10 do
      true
    else
      raise "This is not a number!"
    end

  end
end

As you can see, this function can return a boolean. But it can also not return one. Dialyzer is not picking this up:

Starting Dialyzer
[
  check_plt: false,
  init_plt: '/home/pedro/Workplace/test_dialzer/_build/dev/dialyxir_erlang-23.3_elixir-1.12.0_deps-dev.plt',
  files: ['/home/pedro/Workplace/test_dialzer/_build/dev/lib/test_dialzer/ebin/Elixir.TestDialzer.beam'],
  warnings: [:unknown]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m0.77s
done (passed successfully)

My spec is incomplete and I expected dialyzer to fail with some kind of error / warning.

Questions

Why is dialyzer not complaining? (rare thing to ask, I know)

[kokolegorille]

I had a similar question…

Type and spec - Dialyzer not detecting error

Hello everyone, I have been reading this book [Functional Programming] Domain Modeling Made Functional (Pragprog) (F#) and liked it a lot. I am trying to mimic conditional type from F# to Elixir with the use of spec, type and dyalixir defmodule Ddd.OrderTaking do @type result :: :ok | :error @spec create_unit_quantity(integer) :: result def create_unit_quantity(qty) when is_integer(qty) do cond do qty < 0 -> :error qty > 1_000 -> :error true -> :ok end end end If …

[al2o3cr]

A function can be specced as no_return, but that’s only applicable if it never returns a value.

Otherwise the “can fail” is implied for all functions - for instance, :math.sqrt/1 has a spec of sqrt(number) :: float, but it gives an ArithmeticError when called with a negative input.

[Fl4m3Ph03n1x]

@peerreynders did find a solution for the issue in your thread right?
However I was not able to understand it quite well …

@al2o3cr I am confused, then what is the point of having ! (bang) functions, if all of them can simply explode whenever they feel like?

[kokolegorille]

The solution proposed was to have smaller functions with correct type…

For example, hello_success and hello_error, of type boolean.

[Fl4m3Ph03n1x]

The solution was to “not raise” at all, correct ?

[kokolegorille]

Whatever You choose to return from an error will be catched if it does not specify the right type for the error return, in the smaller function. While your hello function could not, because dialyzer assume it is correctly typed as boolean in case of success, and does not care about the error path.

[Fl4m3Ph03n1x]

I am sorry but I still dont quite understand.

defmodule TestDialzer do
  @moduledoc """
  Documentation for `TestDialzer`.
  """

  @spec hello(integer) :: boolean
  def hello(n) do

    if n == 10 do
      true
    else
      raise "This is not a number!"
    end

  end

  @spec test_hello_1 :: boolean
  def test_hello_1, do: hello(10)

  @spec test_hello_2 :: boolean
  def test_hello_2, do: hello(1)
end

In this example, test_hello_2 will clearly fail. Dialyzer should be able to prove this is wrong. Yet it passes.
I don’t understand how this can be fixed…

[michallepicki]

Dialyzer should be able to prove this is wrong

Should, based on what exactly?

Dialyzer doesn’t do dependent typing. And it only does a limited amount of data flow analysis, since it is highly computationally and memory intensive. Maybe in this particular case it seems easy and intuitive, but a generalized algorithm that would perform these kinds of checks is not trivial.

AFAIK individual integers (like 10, 1) are not distinguishable by Dialyzer.

[michallepicki]

If you let dialyzer infer specs for your functions, it will tell you that the hello (and other functions) return true. You can enable checking of your provided specs against those by using the overspecs, underspecs or the combinded specdiffs options. But beware that this may introduce a lot of noise: warnings when you don’t want them, where dialyzer hits his limits and simplifies types, or you intentionally simplify types, e.g. for documentation purposes.

[Fl4m3Ph03n1x]

Should based on the fact that I have a public function with a direct flow that causes a spec error.

I understand finding paths is computationally intensive, I am not discussing that here.

Perhaps my question can be better rephrased as: How can I make dialyzer detect there is an issue? What code changes would I need to perform?

[kokolegorille]

@Fl4m3Ph03n1x

  def hello(n) do

    if n == 10 do
      true
    else
      raise "This is not a number!"
    end

  end

The solution @peerreynders proposed in the similar question I had was to do something like this…

  def hello(n) do

    if n == 10 do
      hello_success()
    else
      hello_error()
    end

  end

This way You can detect type error in the smaller functions.

Here is the solution he provided in my question…

   cond do
     qty < 0     ->
       create_unit_quantity_error("unit_quantity can not be negative")
     qty > 1_000 ->
       create_unit_quantity_error("unit_quantity can not be more than 1000")
     true        ->
       create_unit_quantity_success(qty)
    end

[Fl4m3Ph03n1x]

defmodule TestDialzer do

  @spec hello(integer) :: boolean
  def hello(n) do

    if n == 10 do
      hello_success()
    else
      hello_error()
    end

  end

  @spec test_hello_1 :: boolean
  def test_hello_1, do: hello(10)

  @spec test_hello_2 :: boolean
  def test_hello_2, do: hello(1)

  @spec hello_success :: true
  defp hello_success, do: true

  # This is clearly wrong, yet no complaining =(
  @spec hello_error :: boolean
  defp hello_error, do: raise "This is not a number!"

end

I am quite lost here. Dialyzer is not picking up that hello_error has an wrong spec.