I'm trying to understand how the dialyzer works with polymorphic/parametrized types. I understand that it is optimistic and will succeed if there is any path through the code that does not cause a crash; what I don't understand is how to use type variables, given this fact.
I have a simple recursive binary search tree type specification that is intended to produce a BST with values of only one type. I know that (for instance) atoms and integers are comparable in Erlang, but I don't want my BST to allow those comparisons. I wrote and exported a function b/0 that builds a BST with an integer and an atom, and the dialyzer isn't compaining.
-module(bst).
-export([add/2, b/0, new/1]).
-type bst(T) :: {T, bst(T), bst(T)} | nil.
-spec new(T) -> bst(T).
-spec add(T, bst(T)) -> bst(T).
new(Root) -> {Root, nil, nil}.
add(Val, nil) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) ->
case Val =< Root of
true -> {Root, add(Val, Left), Right};
false -> {Root, Left, add(Val, Right)}
end.
% Why no type error here? Adding atom to bst(integer()),
% but type spec allows only same type.
b() -> N = new(8), add(why_no_type_error, N).
Running the dialyzer gives the following success result:
dialyzer-tests ❯ dialyzer bst.erl
Checking whether the PLT /home/.../.dialyzer_plt is up-to-date... yes
Proceeding with analysis... done in 0m0.12s
done (passed successfully)
I was able to make this example fail by editing my add/2 spec as below:
-spec new(integer()) -> bst(integer());
(atom()) -> bst(atom()).
-spec add(integer(), bst(integer())) -> bst(integer());
(atom(), bst(atom())) -> bst(atom()).
Is this in any way idiomatic, or is there a better way to do this? I would not necessarily want to elaborate each possible type for each possible operation on my tree.
The reason you get no warning is the fact that unconstrained type variables in specs (i.e. those that have no when clause) are generalized and treated as term().
Notice that in your example, even without maximal generalization, there is the possibility of the type atom() | integer() for instances of T in your code which would give no warnings.
I can't think of an example where use of a type variable leads to an error, as I don't fully understand what you are looking for.