otp
otp copied to clipboard
dialyzer is wrong about `[none()]`
Describe the bug
TL;DR - an empty list can be seen as a list of none()
. This is important for implementing different "opaque" types backed by lists in a type-safe manner. Unfortunately, dialyzer is not able to see it.
To Reproduce Steps to reproduce the behavior.
A simplistic example:
-module(stack).
-export([new/0, push/2, pop/1]).
-export_type([stack/1]).
-opaque stack(A) :: [A].
-spec new() -> stack(none()).
new() -> [].
-spec push(stack(A), A) -> stack(A).
push(T, H) -> [H | T].
-spec pop(stack(A)) -> {A, stack(A)}.
pop([H | T]) -> {H, T}.
dialyzer stack.erl
stack.erl:9:2: Invalid type specification for function stack:new/0. The success typing is
() -> []
Note that dialyzer has been launched WITHOUT -Wspecdiffs
option, - it's unclear why it complains about success typing here.
Note that in this example stack(none())
is the best return type for new/0
if we want to keep the implementation details "hidden" through the use of an "opaque" type.
Expected behavior
No complaints as none()
is the bottom type. - This is the standard way to give the most precise type to collections.
(like List[Nothing]
in Scala, never[]
in TypeScript and so on)
Affected versions 25.1
fwiw, it looks like sets
takes the view that it would be a stack(any())
, since, if we expand the spec:
-spec new() -> set(). % spec given in the source code
-spec new() -> set(_). % expand the definition of the 0-arity set() type
-spec new() -> set(any()). % rewrite _ alias to any()
Of course, that's not ideal, since we of course know that you can't get anything at all out of it, but you can put anything you want into it; plus you probably want to later add an element and have the resulting type be a union of the element types, which will always be any()
if we start with set(any())
. In the case of set(none())
for set:add_element/2
, we get:
% spec definition
-spec add_element(Element, Set1) -> Set2 when
Set1 :: set(Element),
Set2 :: set(Element).
% smallest type which would satisfy an application (acceptable, because none() is a subtype of all types)
-spec add_element("some string", set(none())) -> Set2 when
Set1 :: set(string()),
Set2 :: set(string()).
This suggests to me that the proposal to use none()
is appropriate, but it makes me wonder how exactly this is being interpreted at the moment for cases such as set()
. I suspect you can shed some light on how this is already handled in eqwalizer, @ilya-klyuchnikov?
The logic above is according a "classical" typing model, but of course, Dialyzer follows its own unique path, so in some sense it is right w.r.t itself, but perhaps the argument here is that rejecting [none()]
makes Dialyzer awkwardly incompatible with other typing approaches.
fwiw, it looks like
sets
takes the view that it would be astack(any())
, since, if we expand the spec:
which is not great from the point of view of good API. This is why we have to rewrite it in eqwalizer:
https://github.com/WhatsApp/eqwalizer/blob/65535e856c5cdfb188a482abe18b3452729875c4/eqwalizer_support/src/eqwalizer_specs.erl#L717-L721
TL;DR - an empty list can be seen as a list of
none()
.
I was very much tempted to stop reading here because this IMO does not make any sense, not only as a Dialyzer designer, but also as an Erlang programmer.
Even in all (static) type systems I know of, []
has type 'a list
. E.g.
Standard ML of New Jersey v110.76 [built: Sun Jun 29 03:29:51 2014]
- [];
val it = [] : 'a list
GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help
Prelude> :t []
[] :: [a]
And it's implicit that the 'a there is some type that may be instantiated later (i.e., _
- see also #6289), not no type
(i.e., none()
).
So, the -spec
should really read -> stack(_)
as it currently does (or stack(A)
, if you prefer, as in the rest of the functions of your example), not stack(none())
.
Dialyzer is never wrong (TM).
Even in all (static) type systems I know of
There are many different type systems with different approaches and different flavours - you may be interested to read an introductory book - like TAPL - https://www.cis.upenn.edu/~bcpierce/tapl/ - especially the section 15.4 "The Top and Bottom Types" or to consult a more lightweight source: https://en.wikipedia.org/wiki/Bottom_type
See https://www.erlang.org/doc/reference_manual/typespec.html - where any()
and none()
are defined as Top and Bottom correspondingly:
Because of subtype relations that exist between types, types form a lattice where the top-most element,
any()
, denotes the set of all Erlang terms and the bottom-most element,none()
, denotes the empty set of terms.
Standard ML GHCi
ML and Haskell have very different type systems, - in this context the main difference would be NO subtyping in the mentioned languages. - And, correspondingly, - the comparison would be of little relevance here.
(One of the obvious technical points would be that they do not have explicit bottom type).
If we look at type systems with subtyping and explicit bottom type - say Scala or Type Racket - they allow to see empty lists both as a dedicated singleton type (Nil) or a list of nothing (a list of value of bottom types).
Scala:
scala> Nil : List[Nothing]
val res1: List[Nothing] = List()
Typed Racket:
> (: x (Listof Nothing))
> (define x '())
Of course, - it's a matter of design choices in the end, - and not supporting seeing empty lists as a list of nothing (none()
s) may be a design choice as well - if it's applied consistently and user-friendly, - see the next section.
But then (in the light of your answer) I am wondering about how dialyzer behaves for a little bit modified example. Let's just add an empty list explicitly to stack(A)
:
-module(stack).
-export([new/0]).
-export_type([stack/1]).
-opaque stack(A) :: [A] | [].
-spec new() -> stack(none()).
new() -> [].
No complaints from dialyzer! Even with -Wspecdiffs
.
Or yet another example:
-module(result).
-export([mk_err/0, mk_ok/1]).
-export_type([result/1]).
-opaque result(A) :: {ok, A} | err.
-spec mk_err() -> result(none()).
mk_err() -> err.
-spec mk_ok(A) -> result(A).
mk_ok(A) -> {ok, A}.
Again, - dialyzer is happy here, - seeing err
as result(none())
.
So, a dialyzer complaint about []
and [none()]
from the original report is an inconsistent one-off one way or another.
I have re-classified this issue as a feature request.
Dialyzer uses none()
as the bottom type in the sense described in "Computer science applications" mentioned in the Wikipedia article, not in the second sense mentioned in the article.
To change none()
to also work in the second sense might be possible, but that is a feature request and not a bug fix. Before doing that change, we will have to answer these questions:
- Is this a useful and desirable feature?
- Is it backwards compatible?
- How technically difficult would it be to do the change in Dialyzer, that is, how much code would have to be rewritten/updated and how long time would it take?
- Would it better to perhaps introduce another name, such a
nothing()
ornever()
? Would that be easier to implement? Would it be less confusing?
@bjorng, that seems like a good framing to me
Hi there! I fail to see how dialyzer does not work as expected in the examples provided. I will comment on them and please, let me know how this is not the expected result.
First example
-module(stack).
-export([new/0]).
-export_type([stack/1]).
-opaque stack(A) :: [A] | [].
-spec new() -> stack(none()).
new() -> [].
I see that you wrote: "No complaints from dialyzer!"
As I see, stack(A) :: [A] | []
. The function returns []
and this is part of the return type stack(A) | []
. So all good there.
Second example
-module(result).
-export([mk_err/0, mk_ok/1]).
-export_type([result/1]).
-opaque result(A) :: {ok, A} | err.
-spec mk_err() -> result(none()).
mk_err() -> err.
-spec mk_ok(A) -> result(A).
mk_ok(A) -> {ok, A}.
This follows the same reasoning as before. result(A)
is a type synonym to {ok, A} | err
.
Lets go function by function:
-
If we look at the typing
mk_err :: () -> {ok, none()} | err
(where I have simply performed type substitution of the type synonym) themk_err
implementation returnserr
. Since the valueerr
is part of the set of possible return values, i.e.,{ok, none()} | err
, then dialyzer accepts it. -
if we look at
mk_ok(A) :: A -> {ok, A} | err
, the implementation returns{ok, A}
, for someA
. Since the return type is also{ok, A}
for some valueA
, then dialyzer will not complain.
Next steps
Regardless of whether the behaviour from above is what one expected or not, if someone would like to move this forward, my recommendation is that someone creates an EEP where the semantics of the desired behaviour are clearly specified. If that means introducing a new type! Go wild with the idea but make sure that it makes sense in the ecosystem and that it does not break anything. Apart from this, the team would require a prototype implementation where we can test the effect of the new semantics.
I am going to close the issue but feel free to re-open / write in this issue if there is something that is not clear.
Thanks.
@kikofernandez
I fail to see how dialyzer does not work as expected in the examples provided. ...
In these examples - the behaviour is OK.
The inconsistency IMHO can be seen in the example from the very first comment post:
-module(stack).
-export([new/0, push/2, pop/1]).
-export_type([stack/1]).
-opaque stack(A) :: [A].
-spec new() -> stack(none()).
new() -> [].
dialyzer stack.erl
stack.erl:9:2: Invalid type specification for function stack:new/0. The success typing is
() -> []
I see that you wrote: "No complaints from dialyzer!"
As I see,
stack(A) :: [A] | []
. The function returns[]
and this is part of the return typestack(A) | []
. So all good there.
The union with []
is redundant as [A]
is the same as [A,...] | []
. It should not make a difference, yet it does.
As far as I can tell this issue is caused by a bug in erl_types:t_list/1
which returns ?none
when the element type is impossible. This would be correct for known non-empty lists but not potentially empty ones. It should return ?nil
instead.
@jhogberg The code very explicitly returns ?nil
when given impossible contents:
t_list(?none) -> ?nil;
t_list(?unit) -> ?nil;
t_list(Contents) ->
?list(Contents, ?nil, ?unknown_qual).
Is that an oversight by the original authors or deliberate?
Running the Dialyzer test suite after changing erl_types:t_list/1
to return ?nil
when given ?none
or ?unit
, there were no failed test cases. Perhaps we can dare to do this change in master
if no other problems turns up.
@bjorng I think you quoted the wrong code in your message.
The current one returns ?none
and reads:
t_list(?none) -> ?none;
t_list(?unit) -> ?none;
t_list(Contents) ->
?list(Contents, ?nil, ?unknown_qual).
Changing the first clause to return ?nil
is, most likely, the wrong thing to do. [No time to explain why.]
The right thing to do to solve the (very minor, IMO) issue of stack(A) :: [A] | []
being handled differently from stack(A) :: [A]
is to add a preprocessing pass that:
- warns the user that such type declarations (where there is a union of a type with one or more of its subtypes) are redundant and confusing (for both programmers and tools), and
- automatically cleans up such type declarations by removing all subtypes from them.
My .02.
@kostis Yes, I quoted the wrong code. I quoted the code that I had updated.
It would be useful for us if you could find time later to explain why the change would be wrong. We want to do or not do things based on known reasons.
Changing the first clause to return
?nil
is, most likely, the wrong thing to do. [No time to explain why.]
I would very much like to hear why that's wrong. To the best of my understanding:
Since [A]
is [A,...] | []
, []
is a strict subset of all [A]
and therefore [A] | [] = [A]
[0] must be true for all A
. Hence, [none()]
must be []
or else we'll break the type lattice.
That also happens to be how the rest of dialyzer
sees it. t_list/1
is the odd one out, and making everything else follow it leads to trouble one way or the other. Consider:
-compile(export_all).
foo([H | T]) when is_integer(H) -> [H | foo(T)];
foo([]) -> [].
bar([H | T]) when is_atom(H) -> [H | bar(T)];
bar([]) -> [].
quux(L) -> foo(bar(L)).
Since lists are covariant on their element type, [A :: B] = [A] :: [B]
[1] must be true for all A
and B
. Edit: apologies for the sloppy use of ::
but using ∧
and ∨
felt a bit too cryptic. I mean it in the sense of "infimum of LHS and RHS" here, not "LHS is a subtype of RHS."
If we say that [integer()] :: [atom()]
[2] is []
, we correctly infer that quux/1
returns []
, but we've broken the above property since [integer() :: atom()]
[3] is none()
. It may not be a problem here, but breaking the lattice inevitably leads to super-mysterious bugs at some point.
If we say that [integer()] :: [atom()]
is none()
, then we've maintained the property but quux/1
cannot return, which is wrong because it works just fine when passing []
.
Either way there's a problem, so I consider the current behavior of t_list/1
buggy as it acts contrary to how everything else does, and things would break if we changed the rest to match its behavior. I'd be more than happy to hear why I'm wrong though.
[0]: t_sup(t_list(A), t_nil()) = t_list(A)
[1]: t_list(t_inf(A, B)) = t_inf(t_list(A), t_list(B))
[2]: t_inf(t_list(t_integer()), t_list(t_atom()))
[3]: t_list(t_inf(t_integer(), t_atom()))
Hi! Just giving my opinion and summarize why I agree that this is a bug:
In these fundamental discussions it's better to keep the example as minimal as possible. Opaqueness doesn't really matter here, the core issue is the bottom type:
-module(none).
-spec new() -> list(none()).
new() -> [].
Dialyzer output:
Invalid type specification for function none:new/0. The success typing is
() -> []
- As per the "computer science applications" interpretation of
none()
:-
List(Bot)
is a good type fornil
(see Wikipedia, Pierce;nil
is the empty list[]
in Erlang) - Erlang can denote the empty type explicity:
none()
-
list(none())
has exactly one value that inhibits the type:[]
- See Erlang reference manual, informally defined
The only difference between the two shorthands is that [T] can be an empty list
- See Erlang reference manual, informally defined
- The type specification is valid, because
[]
is a subtype oflist(none())
(which is itself equivalent to just[]
) -
list(none())
should be equivalent tolist(none()) | []
, but it is not
-
Changing the first clause to return ?nil is, most likely, the wrong thing to do. [No time to explain why.]
It's the right thing to do, as the list type of none()
elements is ?nil
(i.e. []
).
The arguments given in this discussion thread have convinced that this behaviour is indeed a bug. The fix is in the linked pull request.
If the proper way of being convinced about something technical and doing changes these days is for people to voice (naive or uneducated) opinions (like those in the issue's title "Dialyzer is wrong about ..." or in @albsch's post above) and up-voting reactions, then so be it.
However, let me ask a question: what do you think should be the return (success) type of the following Erlang function?
foo () -> [throw(42)].
Pick your favorite:
-
list(integer())
-
list(bananas())
-
[]
(a.k.a.[none()]
, according to the initial post) -
none()
The return type of foo()
is none()
.
The pull request does not change that. Dialyzer is able to distinguish the the two differenct senses for the bottom type. I initially thought that Dialyzer would not. It turns out that Dialyzer is always very careful to handle the none()
type directly and will not try to incorporate it into an Erlang term.
As far am I aware, the pull request removes an inconsistency and it causes no harm. I am still willing to withdraw the pull request if someone could give me a good reason why the change would make Dialyzer worse or cause other harm.
The return type of foo()
is none()
because the expression value [throw(42)]
is diverging, i.e. equivalent to the bottom type.
If the proper way of being convinced about something technical and doing changes these days is for people to voice (naive or uneducated) opinions (like those in the issue's title "Dialyzer is wrong about ..." or in @albsch's post above) and up-voting reactions, then so be it.
I'd have no problem being called naive/uneducated if you had taken the time to tell me why I'm wrong, but right now I find it difficult not to take offense. I politely asked you to point out any errors in my reasoning and a month later I get called naive/uneducated with no further elaboration. What gives?
Again, to keep the lattice consistent, we need to...
- Maintain that
[A] ∨ [] = [A]
for allA
because[A] = [A,...] ∨ []
. - Maintain that
[A ^ B] = [A] ^ [B]
for allA
andB
.
(Where ∨
is supremum and ^
is infimum.)
Neither of these hold if you say that [none()]
is none()
. (Remember that saying that [A] ^ [B] = none()
when A ^ B = none()
keeps the lattice consistent, but means that we're wrong about not successfully returning []
in the example in my previous post.)
Can you please explain where I've gone wrong here?
However, let me ask a question: what do you think should be the return (success) type of the following Erlang function?
none()
obviously. Like I said in my first post in this thread, this is correct for non-empty lists.
However, we are not talking about non-empty lists here, but possibly empty ones and [A]
says that we either have a non-empty list of A
or the empty list. If the former is impossible then we're left with the latter.
OK, (some of us) at least, we are agreeing on something. Namely, that the return type should be none()
.
Let's try to agree on another thing. The proposed PR changes/affects the behavior of the list type constructor. In particular, this change has nothing to do with supremums, infimums, or any other binary operators, right?
If we agree on the above, I would argue that independently of whatever (magic / internal / very careful) way dialyzer might be using to handle the none()
type, the constructor of lists in the type representation cannot return something different. In other words, one should get the same result independently of whether one uses Dialyzer's internal magic or the interface of the type language to construct the return type of foo/0
given the return type of throw/1
(or some other function that does not return), which is none()
, being encountered inside some list. This is what the current code in erl_types
is doing:
-spec t_list(erl_type()) -> erl_type().
t_list(?none) -> ?none;
t_list(?unit) -> ?none;
t_list(Contents) ->
?list(Contents, ?nil, ?unknown_qual).
It takes (the representation of) a type as argument and returns the representation of that type when wrapped inside a list. The first clause handles exactly the case of foo/0
's return type above. The second clause, if I remember correctly, handles the return type of functions like the following:
bar() -> [bar()].
which should also return none()
.
These cannot be changed to return ?nil
, or else the list type constructor becomes inconsistent. We cannot possibly have the function that returns the type representation of a list with none()
as type argument return []
instead of none()
.
Also, note (although, admittedly, this is a very weak argument), that in the current type language []
is a primitive type; it's not an alias for [none()]
. This would also need to change.
@jhogberg : I did not refer to your post in any explicit way; I only referred to posts that (in my view, at least) express opinions, so I do not really see why you would (or would not) take any offense. I think your post is about a different subject that what (I think) the proposed change is about. You are concerned about (what you perceive as problems in) the "consistency of the lattice", and I am concerned about the "consistency of the list type constructor". I am not sure I quite follow the arguments about empty vs non-empty lists. Is the type of a [throw(42)]
term an empty or a non-empty list (of something)? In my view, the distinction does not make sense since its type is none()
.
@jhogberg : I did not refer to your post in any explicit way; I only referred to posts that (in my view, at least) express opinions, so I do not really see why you would (or would not) take any offense.
Ah, but the OTP team was convinced on the basis of naive/uneducated opinions. If my post was not counted among those, am I then to assume that my colleagues ignored me?
I would much prefer it if all further discussion, here and otherwise, stuck to constructive arguments.
In other words, one should get the same result independently of whether one uses Dialyzer's internal magic or the interface of the type language to construct the return type of foo/0 given the return type of throw/1 (or some other function that does not return), which is none(), being encountered inside some list.
This is the core of my argument, there should be no difference between the two!
If we change the rest of dialyzer
to follow how t_list/1
works right now, we either end up with an inconsistent lattice or reject valid code (as in my example).
If we change t_list/1
to work the way the rest of dialyzer
does, everything is fine.
It takes (the representation of) a type as argument and returns the representation of that type when wrapped inside a list. The first clause handles exactly the case of
foo/0
's return type above. The second clause, if I remember correctly, handles the return type of functions like the following:
No, what you're looking for is t_nonempty_list/1
([A,...]
in the type lang). It covers the case where the list is never empty, such as the Erlang expression [42]
, and if the type argument to the constructor is impossible then the result is of course none()
(as in [throw(42)]
).
t_list/1
([A]
aka [A,...] | []
in the type lang) explicitly includes the empty list as a possible value. If we determine that such a list cannot contain any elements, then we're left with []
and not none()
.
No, what you're looking for is
t_nonempty_list/1
([A,...]
in the type lang).
Thank you for pointing this out! Now I (finally!) see what you are/were referring to (were concerned with), and also how to possibly cleanly resolve this.
How about the following proposal for t_list/1
then, which IMO is a better (much less confusing) way of writing what this constructor does:
t_list(Contents) ->
t_sup(t_nonempty_list(Contents), t_nil()).
I think this will (indirectly) achieve the properties you want to ensure, won't it?
WARNING: Untested code.
No, what you're looking for is
t_nonempty_list/1
([A,...]
in the type lang).Thank you for pointing this out! Now I (finally!) see what you are/were referring to (were concerned with), and also how to possibly cleanly resolve this.
How about the following proposal for
t_list/1
then, which IMO is a better (much less confusing) way of writing what this constructor does:t_list(Contents) -> t_sup(t_nonempty_list(Contents), t_nil()).
I think this will (indirectly) achieve the properties you want to ensure, won't it?
WARNING: Untested code.
Sure, that's equivalent to the linked PR and a bit easier to follow. :-)
I have updated the PR.
If the proper way of being convinced about something technical and doing changes these days is for people to voice (naive or uneducated) opinions (like those in the issue's title "Dialyzer is wrong about ..." or in @albsch's post above) and up-voting reactions, then so be it.
I have been considering to ignore this, but I consider such a statement in direct violation of the Erlang.org's Code of Conduct. It creates a toxic environment and is harmful on so many levels. You don't know each others' background. I read neither naive nor uneducated view points here.
Please be respectful, especially to persons new to the community, but also to each other.