Interestingly enough, the article doesn't say anything about propagation of types, which is the crux of the type checking and what makes any typing system useful or useless, obnoxious or helpful. Consider the example from the article:
% a good old list length counter
count(A=[_|_]) -> count(A, 0).
count([], C) -> C;
count([_|T], C) -> count(T, C+1).
What is the type of count/2? Arguably, it's "(list, any | number) -> any | number", which means that count/1 has type "list -> any | number". Well, that's bloody pointless, isn't it? What you probably want is "(list, any) -> any | (list, number) -> number" for count/2, so you could give count/1 its useful type "list -> number", but intersection function types are notoriously difficult to infer or typecheck, even with manual annotations.
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)
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.
Yeah, I mean that it will properly identify that the only time you can do that is when you have an empty list. The final spec will be (in elixir syntax):
(nonempty_list, number -> number) | ([], any -> any)
It should also be able to correctly infer that the count/1 function must be
I did say "should be able to" without regard to any of the existing type inference engines =D I'll be sure to make this as explicit test in Mavis Inference, which is the one I'm working on. https://github.com/ityonemo/mavis_inference/issues/47
