[erlang-questions] A subtyping system for Erlang

[Sven-Olof Nystrom]

Ł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 
lists module:

-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.



Sven-Olof



Sven-Olof Nystrom 
Comp Sci Dept, Uppsala University, Box 337, S-751 05 Uppsala SWEDEN
svenolof@REDACTED