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

Kostis Sagonas kostis@REDACTED
Mon Oct 8 10:30:52 CEST 2018

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


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

   Practical Type Inference Based on Success Typings


More information about the erlang-questions mailing list