Do you use Dialyzer in your Erlang projects?

Do you use Dialyzer in your Erlang projects?

Do you use Dialyzer in your projects?
  • Yes - all of them
  • Yes - some of them
  • No

0 voters

  • If you only use it in some of them, which ones?
  • If you don’t use it, why not?
  • If you do, any thoughts or experiences you’d like to share?
5 Likes

https://twitter.com/lauramcastro/status/1526593536648429568

Tell us more @lauramcastro :003:

4 Likes

Yes that a part of you dies everytime you battle with the errors.

5 Likes

I love the functionality of Dialyzer, catching lots of issues before merging, now that we have added Dialyzer to the Zotonic CI (using GitHub actions).

The Dialyzer errors are a bit interesting… but after a while you start to understand how to chase down those errors and fix the issues.

5 Likes

I don’t want to get too technical (and also don’t want to spoil it for the authors, which were encouraged by 4 out of 5 members of the panel to get in touch with Kostis and his team, and also to disseminate their work within this community), but here’s a (very!) simplified summary:

Dialyzer/typer right now allow us to specify/infer things like

-spec function(integer() | atom()) -> float() | atom().

thus giving us a somewhat ilusion of working with polymorphic types. However, under the hood, this polimorphysm is not actually “fine-grain traced”, meaning the signature above matches different implementations, for instance:

function(A) when is_atom(A) ->
    "Unsupported";
function(B) ->
    B * 1.0.

and also:

function(A) when is_integer(A) ->
    "Unsupported";
function(other) ->
    1.0.

So the thesis proposal (which was formalized, and proved correct!) is to actually exploit polymorphic inference for success types, so that we could distinguish:

-spec function(integer()) -> float() U (atom()) -> string().
from
-spec function(integer()) -> string() U (atom()) -> float().

A side effect of this is that we now have to deal with any() many times precisely because we cannot express that “U” in a more precise way, but if we could, the whole typechecking process would get more fine-grained, thus catching things that might currently slip through.

I hope I managed to convey the idea!

11 Likes

I’m trying to see how Gradualizer handles the example you provide here, but I’m missing some (likely assumed) information. Should the provided functions type check with the provided spec? Specifically, the spec doesn’t declare string() in the return value, whereas both of them return "Unsupported".

2 Likes

Well, I’d argue that “Unsupported” is a particular instance of string(), so actually

-spec function(integer()) -> float() U (atom()) -> "Unsupported".
-spec function(integer()) -> "Unsupported" U (atom()) -> float().

would be an even more precise inference, given that “Unsupported” is the only instance of string() that is actually returned in this simple example.

6 Likes

Very want to use, but haven’t managed to adopt it during last 13 years =(

2 Likes

I love dialyzer and have used in everywhere since it’s first release. I’ve been using types since before there were types (@spec) and wouldn’t work any other way.

Understanding what it’s telling you can be a challenge, reports can be misleading, but it never cries wolf.

That is until you confuse it with esoterics. Right at the moment I’m flummoxed by portability macros triggering it, but I’ll just add a directive to the code to squelch it just for that one function.

4 Likes