Skip to content

EEP 82: Align with the implementation - #86

Open
williamthome wants to merge 2 commits into
erlang:masterfrom
williamthome:eep-0082-amendments
Open

williamthome wants to merge 2 commits into
erlang:masterfrom
williamthome:eep-0082-amendments

Conversation

@williamthome

Copy link
Copy Markdown
Contributor

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.

Value sets may hold binaries of different sizes, and only fall back
to a structural type when they overflow. Describe how intersection
and subtraction combine value sets with structural binary types, and
that the empty binary is represented structurally.

Also list adjacent string concatenation and byte order specifiers
among the unsupported forms.
The bare form example <<"café">> is valid, since é is 233; use a
character above 255 instead. Clarify that the bare form is Latin-1
and that no latin1_binary warning is emitted, describe how printers
render the node, and target OTP 30.
@josevalim

Copy link
Copy Markdown
Contributor

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants