[erlang-questions] A subtyping system for Erlang
Fri Oct 11 11:40:25 CEST 2019
Łukasz Niemier writes:
> Out of curiosity, why this is using custom type specification
> format? What are type specs lacking to work with that type checker?
> Łukasz Niemier lukasz@REDACTED
The short answer is that the Dialyzer specifications did not contain
the information I needed.
Consider for example the specification of the foldl function in the
-spec foldl(Fun, Acc0, List) -> Acc1 when
Fun :: fun((Elem :: T, AccIn) -> AccOut),
Acc0 :: term(),
Acc1 :: term(),
AccIn :: term(),
AccOut :: term(),
List :: [T],
T :: term().
foldl(F, Accu, [Hd|Tail]) ->
foldl(F, F(Hd, Accu), Tail);
foldl(F, Accu, ) when is_function(F, 2) -> Accu.
Note that the type of Acc0 (second argument) is set to any term. I
wanted (and needed) a more specific specification so that I could give
a warning for programs that would have a type error at run:
+func foldl :: (X*V -> V)*V*list(X) -> V.
According to this specification, the accumulator must be the of the
same type as the second argument as the function parameter.
There are also other reasons. I wanted to have user-defined recursive
data types. Since the one you see everywhere is the list type I wanted
to make that one user-defined.
Comp Sci Dept, Uppsala University, Box 337, S-751 05 Uppsala SWEDEN
More information about the erlang-questions