Why Typing Erlang is Hard: Standard Erlang

Re:Why Typing Erlang is Hard: Standard Erlang by yellowapple on Friday November 06, 2020 @02:24PM (#25010328)

I'd imagine that in this context (i.e. one where a 1-arity function initializes a tail-recursive 2-arity function) the 1-arity function is the only one that'd be exposed outside of the module, in which case you can know with reasonable certainty that only things within the current module will ever call it.

If you really do need to export the 2-arity version, you could always do a meaningless addition to force it to typecheck to a number, like so:

    count([], C) -> C+0;
    count([_|T], C) -> count(T, C+1);

Which should then result in the following:

    erl> c(test_count).
    {ok,test_count}
    erl> test_count:count([], bang).
    ** exception error: an error occurred when evaluating an arithmetic expression
         in function  test_count:count/2 (test_count.erl, line 8)

Or alternately, use guards (though in the context of BEAM-level introspection I haven't the slightest idea if this would produce an equivalent check):

    count([],    C) when is_integer(C) -> C;
    count([_|T], C) when is_integer(C) -> count(T, C+1);

Which then gets you a somewhat clearer error message:

    10> c(test_count).
    {ok,test_count}
    11> test_count:count([], bang).
    ** exception error: no function clause matching test_count:count([],bang) (test_count.erl, line 8)

[ Parent | on HN ]

Re:Why Typing Erlang is Hard: Standard Erlang by Joker_vD on Friday November 06, 2020 @03:26PM (#25010793)

Yes, if you look at my reply to the sibling comment, you'll see that if count/2 is unexported, TypEr (apparently, that's the proper capitalization) infers the types with non_negative_integer().

In fact, I've just looked at the original TypEr paper [0], and wow, they use exactly this example in the section 6: "One might even jump to the conclusion that success typings are unnecessarily general and, as such, quite useless. However, notice that this success typing succinctly captures all possible applications of length_3 which will not result in a type error. [...] Still, we also find the situation sub-optimal and we will improve on it as explained below", and then they use exactly your proposal, recognizing that non-exported functions are only called from the exported functions, and perform dataflow analysis to constrain the types even further.

[0] Tobias Lindahl and Konstantinos Sagonas, "Practical type inference based on success typings", https://www.it.uu.se/research/group/hipe/dialyzer/publicatio...

[ Parent | on HN ]