[erlang-questions] Why isn't erlang strongly typed?

[Jesper Louis Andersen]

2008/10/23 Stuart Bailey <sbailey@REDACTED>:
> There is a very enjoyable and rigorous treatment of many of the issues
> raised on this thread in the book:
>
> Types and Programming Languages by Benjamin C. Pierce.

TAPL is a wonderful book indeed. However, I feel it is a bit misplaced
in this discussion. The problem is not the fact that you can (simply
type) the lambda calculus, but you need some more heavyweight
machinery to incorporate the message passing. The hard thing in type
theory is when you begin to combine the different ideas from TAPL into
one language. It is exactly this strain which makes Haskell and ML
impressive.

The hardest thing to get a good type system for will be the message
passing semantics. Just building a big sum-type of all messages that
can be received is probably not enough: the type system will catch far
too few errors to be interesting. On the other hand, I've toyed with
the idea of using substructural types to prove that a message can be
passed by pointer rather than copied between 2 processes. That is, the
type of the sender proves that once the message is sent, it is the
last use.

Food for thought: You can augment any language with a type system.
There is one type, TET (The Erlang Type), and all expressions have
type TET. It works, but the system is trivial. You can't *use* it for
anything. If you want the type system to provide you any help, it must
be designed cleverly. The design must be such that whenever you do
something wrong, there is a high chance of tripping the type system.