[erlang-questions] Type def and spec syntax

[Robert Virding]

I have done some more checking and the problem still remains. These
following type specifications are all legal in the sense that compiler does
not complain about them or it gives a strange error:

-spec f5(_) -> integer() when atom(integer()).
-spec f6(Y) -> integer() when atom(Y :: integer()).

The first is passed by the compiler without any warnings or errors while
the second you get the error "type variable 'Y' is only used once (is
unbound)". So if the first is legal then what does it mean? And why is the
second illegal because Y occurs more than once?

Does this mean I should strictly only accept exactly what is in the manual
and not what lint accepts?

Robert


On 3 October 2016 at 19:16, Fred Hebert <mononcqc@REDACTED> wrote:

> On 10/03, Robert Virding wrote:
>
>> And it if can be used in a
>> meaningful way why isn't it documented? I think that having syntax which
>> can never legal is a great way to complicate things. Which we don't need.
>>
>
> The three samples for syntax were:
>
> -type atom(X) :: list(X).
> -spec foo(Y) -> integer() when atom(Y).
> -spec foo(Y) -> integer() when atom(Y :: integer()).
>
> So here's a valid way to use them that is useful, at the very least in
> some cases:
>
>    -module(mod).
>    -export([main/0]).
>       -type collection(K, V) :: #{K => V}
>                            | dict:dict(K, V)
>                            | gb_trees:tree(K, V).
>       -spec lookup(K,F,C) -> V when
>                  C :: collection(K, V),
>                  F :: fun((K, C) -> V).
>    lookup(K, F, C) -> F(K, C).
>       main() ->
>        C = maps:from_list([{a,1},{b,2},{c,3}]),
>        lookup(b, fun maps:get/2, C),
>        lookup("bad ignored type", fun maps:get/2, C),
>        lookup(b, C, fun maps:get/2).
>
> This module defines an accessor function using the parametrized types and
> 'when' parts of typespecs syntax. Sadly the analysis is currently not good
> enough to figure out that "bad ignored type" is not an acceptable value of
> `K' for the lookup (it appears dialyzer does not do the parametrized
> inference this deep), but in the third call, it can definitely infer that I
> swapped the collection and the accessor function:
>
>    mod.erl:13: Function main/0 has no local return
>    mod.erl:17: The call mod:lookup('b',C::#{'a'=>1, 'b'=>2,
> 'c'=>3},fun((_,_) -> any())) does not have a term of type    dict:dict(_,_)
> | gb_trees:tree(_,_) | map() (with opaque subterms)    as 3rd argument
>
> Had I otherwise defined my spec as:
>
>    -spec lookup(K,F,C) -> V when
>                  K :: atom(),
>                  C :: collection(K, V),
>                  F :: fun((K, C) -> V).
>
> Which adds a constraint that keys must be atoms, Then dialyzer would have
> caught my error:
>
>    mod.erl:17: The call mod:lookup("bad ignored type",fun((_,_) ->
> any()),C::#{'a'=>1, 'b'=>2, 'c'=>3}) breaks the contract (K,F,C) ->    V
> when K :: atom(), C :: collection(K,V), F ::    fun((K,collection(K,V)) ->
> V)
>
> If you're using rebar3, you should also be getting colored rebar3 output,
> which does make the error a lot easier to see by putting the bad value in
> red and the piece of contract it breaks in green*:
> http://i.imgur.com/AjNgVCB.png
>
> Regards,
> Fred.
>
> * we should find a way to somehow parametrize the colors to help *
> colorblind users I guess.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20161018/15d96240/attachment.htm>