[erlang-questions] A subtyping system for Erlang

[Sven-Olof Nystrom]

Hello,

I would like to announce a type system for Erlang.

This type system offers guarantees for safety; a program that types
should not fail (at least, it should not fail with a type
error). Typing a program requires specifications and declarations of
visible functions and visible data types.

As Erlang data structures such as lists and tuples cannot be modified
at run-time it is a good fit to base the type system on
*subtyping*. Among other advantages, subtyping allows some values to
be typed as the universal type.

The implementation is written in Erlang. It uses a modified Erlang
parser to process Erlang modules extended with function specifications
and type declarations. The type system can type itself, of course.


Below follows two examples of modules that type:

-module(example1).

-compile(export_all).

%: +type list(X) = [] + [X|list(X)].

%: +func append :: list(X) * list(X) -> !list(X).
append([A | B], C) -> 
    [A | append(B, C)];
append([], C) -> C.


%: +func dup :: list(integer()) -> !list(!integer()).
dup(S) ->
    append(S, S).

The module starts with a declaration of the recursive parametric data
type "list". This is followed by a specification and a definition of
the recursive function append. The function "dup" is only specified
for lists of integers (but that can be changed). The exclamation marks
force the type system to check that something interested is returned
by the functions.

Let's take a look at a less orthodox example. This example gives a
hint of what the type system can express, even though it is perhaps
not very practical:

-module(tsil).

-compile(export_all).

%: +type tsil(X) = [tsil(X)|X] + [].
%: +func dneppa :: tsil(X) * tsil(X) -> tsil(X).

dneppa([], L) ->
    L;
dneppa([L1|X], L2) ->
    [ dneppa(L1, L2) | X].

%: +type list(X) = [X|list(X)] + [].
%: +func from_list :: list(X) -> tsil(X).
from_list([]) ->
    [];
from_list([X|L]) ->
    [from_list(L)|X].


%: +func to_list :: tsil(X) -> list(X).
to_list([]) ->
    [];
to_list([L|X]) ->
    [X|to_list(L)].

"tsil" is of course "list" backwards. "dneppa" concatenates two
"tsil"s. Included are also functions that convert between "tsil"s and
lists, just to show that the type system can reason about combinations
of types that use the same data type constructors in different ways.


Currently there is not much documentation of the system available,
beside what I have written here and the README file that comes with
the source. The download page also contains some paper that describe
the theory.

Download: 
http://user.it.uu.se/~svenolof/scfa/


yours,

Sven-Olof Nyström



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