Dialyzer and List Type

classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Dialyzer and List Type

PhayTsukiming
Hi list, I am new to erlang and dialyzer. I have encounter a problem when I tried to fiddle with type specifications. 

Say, I have two functions:

-module(t).
-export([foo/1, bar/1]).

-spec foo([integer()])->[integer()].
foo(Arg)->
    [I+1||I<-Arg].

-spec bar(atom())->[integer()].
bar(_Arg)->
    foo(_Arg).

Then apply dialyzer to this module and dialyzer warns:

t.erl:8: Invalid type specification for function t:bar/1. The success typing is ([integer()]) -> [integer()]

But if I change the specification of bar to:

-spec bar([atom()])->[integer()].

dialyzer will show no warnings. My intention is to make sure the argument of bar is the same type of list as the argument of foo. 

Is this normal? Do I miss or misunderstand something about success typing or dialyzer?


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer and List Type

Stavros Aronis

Hi!

The most general type that foo can have is [number()] -> [number()]. The spec restricts both number() instances to just integer(). Then, since bar's only argument is given as is to foo, it should also be [integer()].

If you specify bar's argument as atom() then there is no way to make a successful call to foo and Dialyzer complains. If however bar's argument is a list of atoms, then there is a way, though a bit trivial, for a call to succeed: an empty list is both a valid list of atoms and a valid list of integers.

Dialyzer can see this, and does not complain. Perhaps a patch is needed, for a warning of type "only the empty list satisfies the given spec"...

Cheers,

Stavros


On Tue, 19 Apr 2016, 08:50 PhayTsukiming, <[hidden email]> wrote:
Hi list, I am new to erlang and dialyzer. I have encounter a problem when I tried to fiddle with type specifications. 

Say, I have two functions:

-module(t).
-export([foo/1, bar/1]).

-spec foo([integer()])->[integer()].
foo(Arg)->
    [I+1||I<-Arg].

-spec bar(atom())->[integer()].
bar(_Arg)->
    foo(_Arg).

Then apply dialyzer to this module and dialyzer warns:

t.erl:8: Invalid type specification for function t:bar/1. The success typing is ([integer()]) -> [integer()]

But if I change the specification of bar to:

-spec bar([atom()])->[integer()].

dialyzer will show no warnings. My intention is to make sure the argument of bar is the same type of list as the argument of foo. 

Is this normal? Do I miss or misunderstand something about success typing or dialyzer?

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer and List Type

Kostis Sagonas-2
In reply to this post by PhayTsukiming
On 04/19/2016 08:50 AM, PhayTsukiming wrote:

>
> Then apply dialyzer to this module and dialyzer warns:
>
> t.erl:8: Invalid type specification for function t:bar/1. The success
> typing is ([integer()]) -> [integer()]
>
> But if I change the specification of bar to:
>
> -spec bar([atom()])->[integer()].
>
> dialyzer will show no warnings. My intention is to make sure the
> argument of bar is the same type of list as the argument of foo.

OK, but then why don't you put the same spec there?  Is there any
problem in this case?

> Is this normal? Do I miss or misunderstand something about success
> typing or dialyzer?

Yes, you do.  All that dialyzer ever promised is that when it spits a
warning then this warning is correct.  (This is the "Dialyzer is never
wrong" slogan.)

On the other hand, it never promised to produce warnings in all cases
you may expect it to do so.

Kostis
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer and List Type

PhayTsukiming
On Tue, Apr 19, 2016 at 4:08 PM Kostis Sagonas <[hidden email]> wrote:
On 04/19/2016 08:50 AM, PhayTsukiming wrote:
>
> Then apply dialyzer to this module and dialyzer warns:
>
> t.erl:8: Invalid type specification for function t:bar/1. The success
> typing is ([integer()]) -> [integer()]
>
> But if I change the specification of bar to:
>
> -spec bar([atom()])->[integer()].
>
> dialyzer will show no warnings. My intention is to make sure the
> argument of bar is the same type of list as the argument of foo.

OK, but then why don't you put the same spec there?  Is there any
problem in this case?

Sorry, I forgot to mention that I was experimenting with my understanding of dialyzer. In the beginning, I thought type specification in erlang works as just the same as in other static type language.  

So I used -spec bar(atom())->[integer()] then dialyzer complained. This worked as expected. 

But when I used -spec bar([atom()])->[integer()], then dialyzer didn't say a word and in static type languages, similar specifications would cause the compiler to generate errors. 

> Is this normal? Do I miss or misunderstand something about success
> typing or dialyzer?

Yes, you do.  All that dialyzer ever promised is that when it spits a
warning then this warning is correct.  (This is the "Dialyzer is never
wrong" slogan.)

On the other hand, it never promised to produce warnings in all cases
you may expect it to do so.

Kostis

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer and List Type

PhayTsukiming
In reply to this post by Stavros Aronis
Thanks for you explanation. One more question: should I use non empty list specification to make dialyzer complain? 

On Tue, Apr 19, 2016 at 4:03 PM Stavros Aronis <[hidden email]> wrote:

Hi!

The most general type that foo can have is [number()] -> [number()]. The spec restricts both number() instances to just integer(). Then, since bar's only argument is given as is to foo, it should also be [integer()].

If you specify bar's argument as atom() then there is no way to make a successful call to foo and Dialyzer complains. If however bar's argument is a list of atoms, then there is a way, though a bit trivial, for a call to succeed: an empty list is both a valid list of atoms and a valid list of integers.

Dialyzer can see this, and does not complain. Perhaps a patch is needed, for a warning of type "only the empty list satisfies the given spec"...

Cheers,

Stavros


On Tue, 19 Apr 2016, 08:50 PhayTsukiming, <[hidden email]> wrote:
Hi list, I am new to erlang and dialyzer. I have encounter a problem when I tried to fiddle with type specifications. 

Say, I have two functions:

-module(t).
-export([foo/1, bar/1]).

-spec foo([integer()])->[integer()].
foo(Arg)->
    [I+1||I<-Arg].

-spec bar(atom())->[integer()].
bar(_Arg)->
    foo(_Arg).

Then apply dialyzer to this module and dialyzer warns:

t.erl:8: Invalid type specification for function t:bar/1. The success typing is ([integer()]) -> [integer()]

But if I change the specification of bar to:

-spec bar([atom()])->[integer()].

dialyzer will show no warnings. My intention is to make sure the argument of bar is the same type of list as the argument of foo. 

Is this normal? Do I miss or misunderstand something about success typing or dialyzer?

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer and List Type

Stavros Aronis
I would not phrase it like that... you are hopefully not writing specifications just for the sake of testing or being shouted at by Dialyzer! :-) If your function should work for the empty list, then your specification should include it.

It is true, however, that with an "[atom(),...]" spec (non-empty list of atoms), you will get an error, as this type has no values in common with the "[integer()]" (possibly empty list of integers).

Stavros

On Tue, Apr 19, 2016 at 10:32 AM PhayTsukiming <[hidden email]> wrote:
Thanks for you explanation. One more question: should I use non empty list specification to make dialyzer complain? 


On Tue, Apr 19, 2016 at 4:03 PM Stavros Aronis <[hidden email]> wrote:

Hi!

The most general type that foo can have is [number()] -> [number()]. The spec restricts both number() instances to just integer(). Then, since bar's only argument is given as is to foo, it should also be [integer()].

If you specify bar's argument as atom() then there is no way to make a successful call to foo and Dialyzer complains. If however bar's argument is a list of atoms, then there is a way, though a bit trivial, for a call to succeed: an empty list is both a valid list of atoms and a valid list of integers.

Dialyzer can see this, and does not complain. Perhaps a patch is needed, for a warning of type "only the empty list satisfies the given spec"...

Cheers,

Stavros


On Tue, 19 Apr 2016, 08:50 PhayTsukiming, <[hidden email]> wrote:
Hi list, I am new to erlang and dialyzer. I have encounter a problem when I tried to fiddle with type specifications. 

Say, I have two functions:

-module(t).
-export([foo/1, bar/1]).

-spec foo([integer()])->[integer()].
foo(Arg)->
    [I+1||I<-Arg].

-spec bar(atom())->[integer()].
bar(_Arg)->
    foo(_Arg).

Then apply dialyzer to this module and dialyzer warns:

t.erl:8: Invalid type specification for function t:bar/1. The success typing is ([integer()]) -> [integer()]

But if I change the specification of bar to:

-spec bar([atom()])->[integer()].

dialyzer will show no warnings. My intention is to make sure the argument of bar is the same type of list as the argument of foo. 

Is this normal? Do I miss or misunderstand something about success typing or dialyzer?

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions