erlang / eep

Erlang Enhancement Proposals
http://www.erlang.org/erlang-enhancement-proposals/
264 stars 67 forks source link

EEP 71: clarification of type specs & generics #63

Closed kikofernandez closed 2 months ago

kikofernandez commented 3 months ago

Type variables are an often-used yet very misunderstood part of the type language. As dialyzer has been lax in enforcing their defined semantics owing to a few bugs, many users have been led to believe that they are simple generics as in most other languages. As a significant amount of code has been written with this in mind, OTP cannot fix the bugs that made dialyzer lax by accident without breaking the analysis of a lot of code.

While that would be fine if dialyzer were the only tool out there, all the other code analyzers we know of interpret type variables as generics which would fragment the ecosystem should we elect to fix the bugs. One application might have been written with eqWAlizer in mind and another with dialyzer, preventing either tool from being applied to the whole release.

As dialyzer is simply broken in this regard, this EEP aims to solve the problem by changing the definition of type variables from equality constraints to generics (parametric polymorphism). We also propose several other changes to make the type language more useful and less ambiguous.

This EEP was created by @jhogberg and @ilya-klyuchnikov

NAR commented 3 months ago

What would be these dialyzer bugs mentioned in the EEP?

jhogberg commented 3 months ago

What would be these dialyzer bugs mentioned in the EEP?

In brief, equality constraints entered by the user are lost. This is relatively easy to fix, but would break analysis of tons of projects as no one has written their specs that way.

hcs42 commented 2 months ago

Thank you for this EEP. I have always thought the current behaviour to be what you described as the proposed one.

However, there seems to be a small rendering problem with the last line of the first footnote on the website: https://www.erlang.org/eeps/eep-0071.

Source text:

This makes sense in `dialyzer` as values and types are the same thing in its
paradigm[^1], but restricts what other type checkers can do; while the
documentation states that the "extra information" given by type variables may be
ignored, it leaves no room for other interpretations when they are taken into
account.

[^1]: In an untyped language we cannot simply say that the type of `1` is
    `integer()` since `1 | foo` is just as much of a superset of `1` as
    `integer()` is. The type of `1` is simply `1`.

Screenshots from the rendered page:

image

image