Just so you know, the problem Philip Wadler found when he tried to type erlang :
- message
- pid and process in particular
self ()
The other question is… how do you deal with distributed message. You can get a message from a node that do not follow the comtract you assigned. So your type checking is useless in that case…