[erlang-questions] Inconsistent and incomprehensible handling of variables in spec's by compiler

[Kostis Sagonas]

On 02/17/2012 10:54 AM, Robert Virding wrote:
> If in my file I add the sepc:
>
> -spec set_var(PrefixExp, Val, State) ->  State.
>
> I get the compiler errors, errors mind you, not warnings:
>
> src/luerl_eval.erl:332: type variable 'PrefixExp' is only used once (is unbound)
> src/luerl_eval.erl:332: type variable 'Val' is only used once (is unbound)
>
> but if I write it as:
>
> -spec set_var(_PrefixExp, _Val, State) ->  State.
>
> then the compiler is happy and is quiet. If I write it as:
>
> -spec set_var(Val, Val, State) ->  State.
>
> (which is wrongly from my point of view) or go all verbose and write:
>
> -spec set_var(PrefixExp::any(), Val::any(), State::any()) ->  State::any().
>
> (which doesn't really add any useful information) the compiler is again happy and silent.
>
> This is inconsistent and does not make sense for variables in a function spec. Either it is wrong, for some incomprehensible reason, to have singleton variables in a function spec, or it shouldn't matter what the variable names are. And why should adding a type, even the most general one, make a difference to the variable name usage. And why should the compiler be bothered with the function spec at all seeing it is doesn't use it and it is not part of the language.
>
> In my naive view of the the typing world my original spec says that set_var/3 takes three arguments of any type and returns a value of the same type as the third argument. Then why not just add type information and make the compiler happy? Well in my case it doesn't give me anything; it makes the spec much longer and there is nothing in a type which would give me more information than is in the variable names. Also dialyzer doesn't actually *need* the spec as it works it out by itself anyway. And the type of PrefixExp is a big hairy recursive type which I am happy to let dialyzer work out for me. Typer gives me a half-screen long type for it.
>
> I get the same behaviour when running dialyzer on the different versions. Again I don't understand why it behaves like that.

As others mentioned, in their most basic form, specs should contain 
*types*, not type variables. Continuing your example, the following is a 
valid spec:

   -spec set_var(exp(), val(), state()) -> state().

for some appropriate definitions of exp(), val() and state() types.
I recommend that you write such specs.  I would even go as far as say 
that you should stick to this kind of specs: specs that contain types 
and types alone.

Of course, the benefits of writing the above spec are dependent on the 
precision of your type declarations. If you are lazy and map all three 
types to any(), something that the type language allows you to do, then 
of course you cannot expect much from the tools that take these specs 
into account, can you? (In such a case the spec is there mostly (only?) 
for documentation purposes. Personally, I am not interested in this type 
of specs; they have very little purpose.)


Now, for convenience and for compatibility with what the edoc @spec 
language also allowed, we have retained the possibility that the user 
provides, perhaps selectively, *names* to argument positions and return 
results. So, you can write the above as:

   -spec set_var(PrefixExp::exp(), ImpValue::val(), state()) -> state().

Note that PrefixExp and ImpValue, i.e. whatever comes to the left of the 
:: symbol in the above, are *optional names* for arguments 1 and 2, not 
type variables.


Type variables in specs come into the picture when you want to express 
(subtype or equality) relations between different argument positions or 
return values. (And by definition to express a relation you need to 
somehow use the same variable twice; personally I cannot think of a case 
where a singleton type variable is interesting.) For example, you may 
want to state in a more emphatic way that the third argument and the 
return result of the set_var/3 function are of the same type. You can do 
that as follows:

   -spec set_var(PrefixExp::exp(), ImpValue::val(), InState::ST) ->
             OutState::ST when ST::state().

(Note that the only type variable in the above is ST.)


Another example of use of type variables is in functions like map/2. 
Since the type system is based on subtyping, you would need to write its 
spec as follows:

    -spec map(F::fun((X) -> Y), InL::[XE]) -> OutL::[YE]
        when X::term(), Y::term(), XE::term(), YE::term(), XL::X, YL::Y.

or, even stricter, as:

   -spec map(F::fun((X) -> Y), InL::[X]) -> OutL::[Y]
             when X::term(), Y::term().

but I guess most people would find the above two ways of giving a spec 
for map/2 probably too verbose so we also allowed them to write simply:

   -spec map(fun((X) -> Y), [X]) -> [Y].

with the implicit assumption that for all type variables T that are not 
qualified by a subtype constraint, there is a constraint T::term() which 
is implicit.

(Note that in this case, all type variables are not singletons.)


Also, because we had a hunch that there may be Erlang programmers who 
have hard time grasping the subtleties of the type language (for 
example, they might be confusing type variables with argument and 
position names) and might make typos in specs, we decided to never allow 
type variables that are singleton. As I explained, such variables are 
not just unconstrained, but they are really not needed because they 
serve no purpose; instead type names do.

I saw/see no reason for one to write a type variable just to name a 
position; if you think otherwise, please provide an example that makes 
sense. Till you do, you are not allowed to write MY_NAME for the type 
any(); if you want the type any() please write any(); if you want to 
name it appropriately, you are required to write MY_NAME::any() or its 
shorthand MY_NAME::_.

I hope it is clear now.

Kostis