Type and spec - Dialyzer not detecting error

Questions / Help
1

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 I run mix dialyxir, everything is fine.

But if I change :ok to :okidoki, dyalizer does not detect any error.

If I change the 3 values to be invalid result, like :erroryo, and :okidoki then dialyxir detect the error, but not if one choice is valid.

I read documentation about spec, and type, but did not find any conditional example.

I saw this code in Sasa Juric Blackjack example here https://github.com/sasa1977/erlangelist/blob/dc7cd1d2c77e52fa0a3a90f269c0f4ca8cca908b/examples/blackjack/lib/blackjack/deck.ex that is using multiple choice

@type suit :: :spades | :hearts | :diamonds | :clubs
@type rank :: 2..10 | :jack | :queen | :king | :ace

But could not make it work with dialyxir. My expectation is to catch any invalid value.

Thanks for taking time

BTW I don’t want to start a tabs vs spaces troll, but it is obvious spaces are more precise

2

Dialyzer will report errors only if they will always happen, not if they might happen. This is what the slogan “Dialyzer is never wrong” means in practice.

It might be that you only call the function with values that cause a legal return - it doesn’t know, so it assumes that’s the case until it can prove otherwise.

8 Likes
3

@michalmuskala Thanks for your reply.

So I assume it is why dyalizer cannot prove you are right, but can only prove you are wrong

4

Dialyzer assumes you are right until it can prove you wrong.

See Learn You Some Erlang: Success Typing.

4 Likes
5

@peerreynders Thank You for your reply. The link is really nice.

6 
defmodule Lima do

  @type unit_quantity_t :: 0..1000
  @type unit_quantity_error :: {:error, String.t()}
  @type unit_quantity_success :: {:ok, unit_quantity_t()}
  @type unit_quantity_result :: unit_quantity_success() | unit_quantity_error()

  @spec create_unit_quantity_error(s) :: r when s: String.t, r: unit_quantity_error()
  defp create_unit_quantity_error(msg),
    do: {:error, msg}
  @spec create_unit_quantity_success(n) :: r when n: unit_quantity_t(), r: unit_quantity_success()
  defp create_unit_quantity_success(qty),
    do: {:okidoki, qty}

 @spec create_unit_quantity(n) :: r when n: integer(), r: unit_quantity_result()
 def create_unit_quantity(qty) when is_integer(qty) do
   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
  end

end

.

$ mix dialyzer
...
Compiling 1 file (.ex)
Checking PLT...
[:compiler, :elixir, :kernel, :logger, :stdlib]
PLT is up to date!
Starting Dialyzer
dialyzer args: [check_plt: false,
 init_plt: '/Users/wheatley/sbox/elx/trial/lima/_build/dev/dialyxir_erlang-19.3_elixir-1.4.4_deps-dev.plt',
 files_rec: ['/Users/wheatley/sbox/elx/trial/lima/_build/dev/lib/lima/ebin'],
 warnings: [:unknown]]
done in 0m1.34s
lib/lima.ex:11: Invalid type specification for function 'Elixir.Lima':create_unit_quantity_success/1. The success typing is (integer()) -> {'okidoki',integer()}
done (warnings were emitted)
$

Alternately

defmodule Lima do

  @type result_error_t :: {:error, String.t()}
  @type result_success_t(t) :: {:ok, t}
  @type result_t(t) :: result_success_t(t) | result_error_t()

  @type unit_quantity_t :: 0..1000

  @spec unit_quantity_error(s) :: r when s: String.t, r: result_error_t()
  defp unit_quantity_error(msg),
    do: {:error, msg}

  @spec unit_quantity_success(v) :: r when v: unit_quantity_t(), r: result_success_t(unit_quantity_t())
  defp unit_quantity_success(qty),
    do: {:ok, qty}

  @spec create_unit_quantity(n) :: r when n: integer(), r: result_t(unit_quantity_t())
  def create_unit_quantity(qty) when is_integer(qty) do
    cond do
      qty < 0     ->
        unit_quantity_error("unit_quantity can not be negative")
      qty > 1_000 ->
        unit_quantity_error("unit_quantity can not be more than 1000")
      true        ->
        unit_quantity_success(qty)
    end
  end

end
4 Likes
7

@peerreynders That is perfect, Thanks!

It took me a little time to read the link on Learn You some Erlang, but it is very deep and informative. I will put this book on top of my reading list.

The key point is to have those private functions that can be tested individually.

8

This is a nice example. It highlights that it is (at least sometimes) very helpful to have proper functions to produce rather simple values. It is again one place where the data construction is concentrated making refactoring much easier, showing the power of abstractions.

However, using the ubiquitous Erlangish/Elixirish version of the Maybe-Type {:ok, any} | {:error, any} consequently in that style would require to do the pattern matching on the receiving side in a similar functional style (i.e. properly abstracted) to be able to change the internal representation. Has anybody an idea how to do this elegantly (and checkable)? What comes into my mind is to use pipelining in a monadic fashion, but this moves the problem only to the local functions:

defp do_inc({:ok, val}) do
    {:ok, val + 1 } 
end
defp do_inc(other), do: other

def inc_quantity(q) do
    create_unit_quantity(qty)
    |> do_inc()
end

Any suggestions?

9

This post mentions exceptional (Exceptional: Freedom from {:error}s: An error handling library (and philosophy) for Elixir) for smoother handling of tagged tuples - though I haven’t myself looked into it yet.

2 Likes
10

Yeah I am quite the proponant of exceptional. It is such a great mix of monadic handling but in an entirely elixir and backwards-compatible way. :slight_smile:

1 Like
11

Thanks for the hint. Exceptional looks like a promising approach, even with the new operators ~> and >>>, where I am always be a little reluctant. They make the code concise and more difficult to read at the same time, depending on how much these operators are in the main stream and properly understood by most of us.

12

Hmm, just read the linked forum post. It seems that the operators ~> and >>> are used more often in monadic inspired libraries. This reduces my concerns about incomprehensible code a bit.

13

Plus those operators are optional, you could always have it override the normal pipe |> operator too so you just use it everywhere instead of mixing it and ~> depending. But overall ~> is just like pipe but it calls the thing being piped into if the value is not an error or it skips it if it is an error.

The >>> operator is just a ‘throw if error’, it is the same as doing |> ensure!() |> blah() when you do >>> blah(), it just ‘cleans’ the pipe at that point of any errors (raising them) and passing along only good values. I tend to use ensure!() myself as I like explicitness. :slight_smile:

1 Like