I'm impressed, but how on earth did Dialyzer figure this out?

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

I'm impressed, but how on earth did Dialyzer figure this out?

Yestin L Harrison
Right, so, I have a module with a big important central function that takes a
proplist of options, and I have a product type annotated representing valid
options, opt(). Then, I've got:

-type opts() :: [opt()].

I've got functions:

-spec default_options() -> opts().
%% you can imagine what this looks like

-spec options(opts()) -> opts().
options(Options) ->
        Default = maps:from_list(proplists:unfold(default_options())),
        New = maps:from_list(proplists:unfold(Options)),
        proplists:compact(maps:to_list(maps:merge(Default, New))).

I run Dialyzer on my project, and... this typechecks just fine?

It was my understanding that Dialyzer spits errors on a potential violation of
stated success typing, and I figured that after going through all the
functions in the maps and proplists module, that static analysis would only
be able to determine that the output of maps:to_list/1 would be
{term(), term()}? Or am I not giving Dialyzer enough credit? Is this what the
PLT is for, statically stepping through the modules it contains?

Really, in any case,
a) This is amazing,
b) I would love any resources anyone is aware of on the workings of Dialyzer,
   besides the obvious look through the source code, which I might attempt
   after getting a bit of a better feel for what it does.
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: I'm impressed, but how on earth did Dialyzer figure this out?

Kostis Sagonas-2
On 10/08/2018 05:29 AM, Yestin L Harrison wrote:

> Right, so, I have a module with a big important central function that takes a
> proplist of options, and I have a product type annotated representing valid
> options, opt(). Then, I've got:
>
> -type opts() :: [opt()].
>
> I've got functions:
>
> -spec default_options() -> opts().
> %% you can imagine what this looks like
>
> -spec options(opts()) -> opts().
> options(Options) ->
> Default = maps:from_list(proplists:unfold(default_options())),
> New = maps:from_list(proplists:unfold(Options)),
> proplists:compact(maps:to_list(maps:merge(Default, New))).
>
> I run Dialyzer on my project, and... this typechecks just fine?

I am not sure what your point is, but note that Dialyzer (Discrepancy
Analyzer of Erlang programs) is NOT a static type checker (i.e., a tool
that is sound for correctness), but is a tool that is sound for defect
detection.  As the slogan goes "a tool whose warnings are never wrong".

So, what you write below is not accurate:

> It was my understanding that Dialyzer spits errors on a potential violation of
> stated success typing,

Dialyzer spits warnings on *definite* (not potential!) violations of
success typings.

> and I figured that after going through all the
> functions in the maps and proplists module, that static analysis would only
> be able to determine that the output of maps:to_list/1 would be
> {term(), term()}?

Well, no.  It should be able to determine that the output of
maps:to_list/1 would be at least [{term(), term()}], i.e., that it is a
list of 2-tuples.

> Or am I not giving Dialyzer enough credit? Is this what the
> PLT is for, statically stepping through the modules it contains?
>
> Really, in any case,
> a) This is amazing,
> b) I would love any resources anyone is aware of on the workings of Dialyzer,
>     besides the obvious look through the source code, which I might attempt
>     after getting a bit of a better feel for what it does.

I suggest you start from reading the Dialyzer description in the Learn
You Some Erlang book

   https://learnyousomeerlang.com/dialyzer

and then, if you want to find out more, read the "success typings" paper

   Practical Type Inference Based on Success Typings
   https://it.uu.se/research/group/hipe/papers/succ_types.pdf


Kostis
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions