[erlang-questions] Unions of Cardinality > 13

[zxq9@REDACTED]

On 2018年2月19日月曜日 0時27分20秒 JST AJ Foster wrote:
> Hello,
> 
> I am new to the Erlang ecosystem, so please excuse / assist with my vocabulary. I’ve observed that Dialyzer behaves differently with union types of different cardinality, with a threshold of 13 items. An example is below:

I ran into this with numeric types a few months ago:

http://erlang.org/pipermail/erlang-questions/2017-November/094079.html

> Similar behavior occurs with unions of atoms; unions of up to 13 atoms are checked as I expect, but unions of 14 or more atoms are not. This behavior appears to be intentional according to this: https://github.com/erlang/otp/blob/master/lib/dialyzer/test/small_SUITE_data/src/atom_widen.erl <https://github.com/erlang/otp/blob/master/lib/dialyzer/test/small_SUITE_data/src/atom_widen.erl>
> 
> My questions: where is this threshold defined, and can it be configured? Alternatively, is there a better way of constructing large union types that will allow Dialyzer to check them as “strictly” as types with fewer items?


From what I understand this is a hacky optimization to make Dialyzer less memory hungry. Tobias Lindahl elaborates a little in this post (in that thread):
http://erlang.org/pipermail/erlang-questions/2017-November/094118.html

I did happen to locate a place in Dialyzer (under lib/hipe/cerl/erl_types.erl) where there is a distinction made between an "unsafe" too-large union and one that has been broadened by merging many types into a common type (like a large integer span becoming integer(), as in my case, or lots of atoms becoming atom(), etc).
https://github.com/erlang/otp/blob/fe1df7fc6bf050cb6c9bbd99eb9393c426b62f67/lib/hipe/cerl/erl_types.erl#L2018

I'm not sure if this is a temporary situation or what to expect in the future. It seems odd to me that a type checker would require enormous amounts of memory, but I don't really know much about how Dialyzer *works* internally as much as I know it has been super useful to me in nearly every case I've used it. The good news is that writing normal software I've only run into this with integer spans; the case of really broad unions tends to just not come up unless you try to enforce strict typechecks on things that are impossible to strictly type (like dynamically loaded modules, future upgrades that haven't been written yet, etc. that can't be known at build time for obvious reasons).

-Craig