[erlang-questions] Unions of Cardinality > 13

[AJ Foster]

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:

    -module(atom_widening).

    -export([example1/1, example2/1, main/0]).

    % Cardinality above 13 -> not checked as expected.

    -type value1() :: 1..14.

    -spec example1(value1()) -> ok | error.

    example1(A) when A >= 1, A =< 10 -> ok;

    example1(_) -> error.

    % Cardinality not above 13 -> checked as expected.

    -type value2() :: 1..13.

    -spec example2(value2()) -> ok | error.

    example2(A) when A >= 1, A =< 10 -> ok;

    example2(_) -> error.

    main() ->

      error = example1(15), % Passes successfully.

      error = example2(15). % Warning: breaks the contract.

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

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?

Thank you for your time,

- AJ

[zx...@zxq9.com]

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
_______________________________________________
erlang-questions mailing list
erlang-q...@erlang.org
http://erlang.org/mailman/listinfo/erlang-questions

[Kostis Sagonas]

On 02/19/2018 06:27 AM, AJ Foster wrote:
> 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:
>

>     <SNIP>

Yes, this is correct.

> My questions: where is this threshold defined, and can it be configured?

This threshold is defined here:

https://github.com/erlang/otp/blob/fe1df7fc6bf050cb6c9bbd99eb9393c426b62f67/lib/hipe/cerl/erl_types.erl#L257

It can easily be changed, and in fact perhaps it should have been
increased by now. I think I have been running my own version of
dialyzer with 21 (or 23?) for a number of years now and I have not
experienced any memory issues. On the other hand, all the machines I
use have at least 8 GB of RAM.

However, no matter what number is chosen, with the current code there
will always be a point where the analysis collapses (loses) information
and thus becomes approximate. But this is OK. Dialyzer is NOT a type
checker; it's a _discrepancy analyzer_, meaning that it only guarantees
that the issues it reports are indeed issues (this is the "Dialyzer is
never wrong" slogan), not that it finds all type errors.

> 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?

Perhaps there is. Feel free to experiment.

Kostis