[erlang-questions] I'm impressed, but how on earth did Dialyzer figure this out?

[Kostis Sagonas]

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