[williamthome]

Follow-up to #84, which accepted EEP 82. Reviewing the implementation (erlang/otp#10816) showed a few places where the EEP text no longer matches the code or is wrong:

Dialyzer section

• A set of values can contain binaries of different sizes, for example <<"ping">> | <<"start">>. It only falls back to the structural t_bitstr/2 type when the set grows past the size limit. The previous text said that combining different sizes also caused the fallback, which would make most sets of commands useless.
• Describes how value sets combine with structural binary types: union gives the structural type, while intersection and subtraction filter the values.
• States that <<>> is always the structural type, so that each type has a single representation.

Examples and restrictions

• <<"café">> was listed as invalid, but é is 233, so it is accepted. It is replaced by <<"😀">>.
• Clarifies that the bare form is Latin-1: <<"é">> is the one-byte binary <<233>>. No latin1_binary warning is emitted for types, because the encoding is not kept in the abstract form.
• Adds <<"a" "b">> (string concatenation) and <<"hello"/utf16-little>> (byte-order specifiers) to the unsupported forms.

Other

• Describes how printers render the node: <<"..."/utf8>> when the value is valid UTF-8 with non-ASCII characters, otherwise <<"...">>.
• Changes Erlang-Version to OTP-30.0, since the implementation targets the next major release.

[josevalim]

Hi everyone, I missed the original EEP discussion, but I'd like to bring up some concerns about how this feature could affect future type systems on the BEAM.

For example, imagine we have a function with this signature:

-spec handle(<<"cont">> | <<"halt">>) -> ok.

Now imagine that you call this function like this:

Leading = binary_part(Binary, 0, 4),
handle(Leading)

This approach would be completely fine with Dialyzer, because there is a chance that the first four bytes of the binary will be either "cont" or "halt". However, for a sound static type system, you need to guarantee that Leading is either "cont" or "halt"! So you will most likely need to write code similar to this:

case binary_part(Binary, 0, 4) of
  <<"cont">> -> handle(<<"cont">>);
  <<"halt">> -> handle(<<"halt">>)
end

Which I'd argue that, at this point, you might as well use an atom.

It can also introduce false positives and/or type system complexity in code samples like this:

Binary = case Halt of
  true -> <<"halt:reason">>;
  false -> <<"cont">>
end,
%% ...
Leading = binary_part(Binary, 0, 4),
handle(Leading)

We can clearly see the code above will never fail (assuming Halt is a boolean)! However, a type system would only be able to prove it if it understands how binary_part transforms singleton binary types. Otherwise, you get false positives.

Similarly, consider this code:

handle_upper(Bin) when Bin == <<"HALT">>; Bin == <<"CONT">> ->
  handle(string:lowercase(Bin)).

It can clearly never fail, but unless the type system can determine that lowercasing <<"HALT">> produces <<"halt">>, it is another false positive. So you'd have to write it as:

handle_upper(<<"HALT">>) -> handle(<<"halt">>);
handle_upper(<<"CONT">>) -> handle(<<"cont">>).

If I could summarize it, I'd say a static type system would partly force binaries in typespecs to be treated very similarly to atoms, or require significantly more complex type-level reasoning about common binary operations. Since binaries are frequently sliced, concatenated, and transformed, this could reduce the usefulness of the feature for such systems, or require programmers to repeatedly reestablish type information that is already evident from their code.

This concern does not apply in the same way to Dialyzer, though. If folks are interested in digging deeper, I give a talk on this topic at ElixirConf: https://youtu.be/Ay-gnCqDw9o?t=105