[erlang-questions] Trouble with init/1 spec
Thu Mar 25 13:10:36 CET 2010
Jay Nelson wrote:
> On Mar 24, 2010, at 1:34 PM, Kostis Sagonas wrote:
>> The type any() means "anything goes". It's possible that you are not
>> fully aware of what specs and type declarations in records do. They
>> put extra constraints that have to be compatible with the types that
>> dialyzer infers (the so called "success typings"). An inferred type of
>> any() for some record field is compatible with a user declaration that
>> the field is of type string(). If compatible, the strongest of the
>> two -- in this case string() -- is used from then on.
> Yes, I have this backwards. I thought any() meant the code may try to
> put any type of value, so no constraints can be applied. In my example,
> I thought I had declared the field 'port' to accept only integer()
> values, but the value of the arg being supplied could be any term. That
> was why I thought it failed.
> Rather than restricting the types, the arguments of a function declare
> the widest acceptable range and if by inference the type can be
> restricted after the binding, the restriction is used as the inferred
> type. Does this only apply to the special case of records?
Sorry, but either I do not understand what you've written or you have
this backwards again. Rather than continuing this, I suggest you read
the following papers:
Practical type inference based on success typings
A Language for Specifying Type Contracts in Erlang and its Interaction
with Success Typings
which perhaps will shed more light to how type inference in Dialyzer
> I get no error for the following code:
> -export([init/1, foo/1]).
> -spec init(any()) -> integer().
> init(Val) -> Val.
> -spec foo(string()) -> integer().
> foo(Val) -> init(Val).
> Should dialyzer complain about this code? If not, what is the
Once again you have this backwards. Dialyzer does not _have_ to complain
about this code. In fact, dialyzer does nowhere promised to find all
errors in a program or check that all its specifications are indeed
possible or make sense. Instead, all that dialyzer promises is that when
it does report a discrepancy then there is indeed something wrong in
your code. (Of course, this does not mean that some future dialyzer
version will not be able to detect more discrepancies and complain about
What happens in your program is that dialyzer initially infers the
following types for its functions:
init(any()) -> any() and foo(any()) -> any() (*)
Note that the types nowhere have dependencies between the type(s) of
input arguments and the return. The specs you have written are not in
violation with these inferred types so these are considered ok and are
trusted. There is only one call in the program and this call is to a
function (init/1) which does not constrain its input argument in any
way, so there are no discrepancies in call sites either. Moreover, the
spec of init/1 specifies that the return of this call is of type
integer() which is consistent with the return in the spec of foo/1.
So that's what's happening here.
Is it possible to do better than that you may ask? Of course it's
possible! In fact, dialyzer's code is open source, so be my guest ;-)
(*) I lied on purpose here to simplify the presentation.
In fact dialyzer infers the following types
init(any()) -> any() and foo(any()) -> integer()
because the -spec for the init/1 function is trusted before the
analysis of foo/1 starts.
More information about the erlang-questions