type system in erlang?

[Rachwal Waldemar-AWR001]

Type system, loose set of modest wishes:

1) Usefull, not academic

It has to catch type errors as much as possible, thus relieving a
developer of tedious unit tests of thing which should do a compiler.
The type system hasn't to claim a right to be "complete" strict system
(like in Haskell or OCaml) to be usefull, I think. On the other hand
maybe the complete type system make a compiler's analysis easier, I
guess.

2) Minimalistic, or incremental

I'd want to define types mainly for exported functions, and not for all,
at least not at once.

3) Some notion to encompass heterogenous lists. [any()] ?

any() would mean potentially different type, from element to element,
and [any()] is different than [A], which means any type A, but all list
elements of the same type.
Some form of relaxation for type system, but expressable.

4) Record types and recursive data types.

5) Intuitive, reflecting how thing are used in practice

A function type for example is usually introduced first, before its
definition. This reflects how the function is to be used, not how it
will be implemented, although a library writer (producer) has always a
rough vision how to do it. Next he implemets the function and the final
effect may have types wider than specified. I'll reuse an example from
Wadler's paper:

  and(true,true) -> true;
  and(false,X)   -> false;
  and(X,false)   -> false.

I'd expect this implementation to be *compilable* after intuitive type
definition introduced earlier:

  -type and(bool(),bool()) -> bool().

But in turn, a client's (consumer) call of that function would be
checked if both args are exactly of type bool()!

Couldn't be these two facts described as:
  Tu <= Th <= Te
  where: Tu - type of client's call
         Th - type declared
         Te - type resulting from implementation

I wonder how much these wishes are contradictory in terms of
feasibility... ;)

Regards,
WR.

-----Original Message-----
From: Kostis Sagonas [mailto:kostis@REDACTED] 
Sent: Wednesday, December 14, 2005 3:32 PM
To: Rachwal Waldemar-AWR001
Cc: erlang-questions@REDACTED
Subject: Re: type system in erlang?

Waldemar Rachwal wrote:

 > What's happened with a type system? I've noticed a few papers and
even  > someone's claim that "we got a type system". I realized it was
premature  > but undoubtedly optimistic. Have opinions changed on the
type system in  > erlang since that time? I know there is Dialyzer, but
it's not the same.

You are right that it is not the same, but Dialyzer does get most of the
benefits of catching type errors, both simple and quite involved ones,
even some type errors that statically typed languages will not catch.
Do you have a case that it does not do what you want?

The basic problem with type systems is that there is no single one that
will satisfly all wishes.  What sort of type system would you want to
see?

Best,
Kostis

PS. FYI, we are currently working on the following two directions:
     1. Getting Dialyzer into Erlang/OTP.
     2. Developing Typer, a tool that will automatically annotate
        Erlang source code with Edoc-compatible type information.