Why Dialyzer tells me that this fun contract has overlapping domains?

Question

I am reading with interest the online book "learn you some erlang" and trying some exercises to check my understanding.

I made some modification on the fifo example, in the chapter Type Specifications and Erlang, trying to define a "typed_fifo(T)" (a fifo where all elements must be of the same type T)

my type specification are:

-type typed_empty_fifo() :: {fifo, [], []}.

-type typed_nonempty_fifo(A) :: {fifo, nonempty_list(A), list(A)} | {fifo, [],nonempty_list(A) }.

-type typed_fifo(A) :: typed_empty_fifo() | typed_nonempty_fifo(A).

and when I use it in the following function spec:

-spec empty (typed_empty_fifo()) -> true;

  (typed_nonempty_fifo(_)) -> false.

empty({fifo, [], []}) -> true;

empty({fifo, A, B}) when is_list(A), is_list(B) -> false.

Dialyzer tells that it will ignore the specification because of overlapping domain.

Can somebody tells me where I make a mistake?

I have another point, before trying to define typed fifo I had a version that worked nicely, An Dialyzer show me that nothing prevent the usage of improper lists. Surprizingly, I do not find a simple way (that I can use in a guard) to test for proper/improper character of a list.

It is really strange, because when I use the bif length/1, it is able to fail with the reason badarg!

23> L=[1,2|3]. ==> [1,2|3]

24> is_list(L). ==> true

25> length(L). ==> exception error: bad argument

 in function  length/1

    called as length([1,2|3])

Thanks

Wifeless

Answer 1

Nothing is wrong with your types and spec. The problem is that the datatype which is used in Dialyzer for the representation of types does not keep as much precision as you are providing. Specifically, the union: {fifo, nonempty_list(A), list(A)} | {fifo, [], nonempty_list(A)} is "crushed" into {fifo, list(A), list(A)}, as the tuples have the same arity (3) and first atom element (fifo). Dialyzer generally does over-approximations (as you can also see here) to make the type analysis more efficient. You can safely ignore this warning.

For your second question, is_list/1 only checks whether the first constructor of the term that is passed as its argument is a cons cell. Even is_list([1|2]) returns true.

If you want to ensure that an argument is a proper list you can use a custom function in a case expression like this:

case is_proper_list(L) of
  true -> ...;
  false -> ...
end

is_proper_list([]) -> true;
is_proper_list([_|L]) -> is_proper_list(L);
is_proper_list(_) -> false.

This can't be placed in a guard however. In guards you can use the one that you suggest in your comment below (length(L) >= 0).

Superheat

Thank you Aronis. I think I am asking more than Dialyzer intends to provide. I am trying to figure out what could be the benefit of using those spec definitions, what dialyzer can do, and what is the effort for me. At least I discover this issue with improper list. By the way, I am still looking a solution to my second question. I have fount that a test in fun guard like: is_list(X) andalso length(X) > -1 works. But it crashes inside a function. – Wifeless

I have edited the answer with a possible solution. Oh and my first name is Stavros! :-) – Superheat

Answer 2

Regarding to your second question, the right way to work with list is:

1> L = [1,2|[3]].
[1,2,3]
2> is_list(L).
true
3> length(L).
3

Note, that [Head|Tail] notation requires from you Tail to be list (not int).

Duplicate

Thank you for answer. I knew that, but I wrote the end of question maybe too fast. I did this assignment on purpose, in order to create an improper list. The fact is that my fifo module will create only valid fifo, but nothing prevents that another module creates a fifo built on improper list, and I would like to check it (for the sake of the exercise of course, in real life I use the sdlib one ...) – Wifeless