[erlang-questions] Inconsistent and incomprehensible handling of variables in spec's by compiler
Fri Feb 17 21:56:00 CET 2012
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
-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 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
(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
I hope it is clear now.
More information about the erlang-questions