[erlang-questions] Trouble with init/1 spec

[Kostis Sagonas]

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
http://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf

and

   A Language for Specifying Type Contracts in Erlang and its Interaction
	with Success Typings
http://user.it.uu.se/~kostis/Papers/contracts.pdf

which perhaps will shed more light to how type inference in Dialyzer 
takes place.

> I get no error for the following code:
> 
> -module(jay).
> -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 
> interpretation?

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 
such code.)

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 ;-)

Cheers,
Kostis

(*) 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.