[erlang-questions] Specifying Type Contracts in Erlang

[G Bulmer]

I've been reading the paper "A language for specifying type contracts  
in Erlang and its interaction with success typing' that was presented  
at the Erlang workshop. I think this is a good, useful and valuable  
piece of work.

As far as I can see, there are only 2 pieces which are not covered by  
existing Erlang syntax:
1. a range of values, like (0..255), and (0..), and
2. "..." which seems to be interpreted as 0 or more.

IMHO, it would be a good idea to stay within Erlangs existing syntax,  
and avoid extensions.
Case one, could be dealt with using a sequence, seq(0,255) with a  
reserved value for infinity, maybe inf(). I'd be happy inventing a  
new function, it doesn't have to be seq().
Case two appears to be the same as _. The example was [char(), ...]  
for non-empty string, which could also be written [char()|_]. I'm  
happy to use other alternatives like a 'magic' function, e.g. tail().

What benefits do I think we'd get by staying within Erlang syntax?
1. There is little new to learn.
2. The parser for type contracts (type annotations) is already  
written. This lowers the bar for others to reuse the type annotation  
information. I believe there is already a well defined representation  
for parsed Erlang which may reduce the amount of work to reuse  
annotations even more.
3. I believe there is already a well-defined mechanism for saving  
parsed Erlang in Beam files, so a tool needn't deal with Erlang  
source at all.
4. Erlang syntax could be extended in the future, without having any  
syntax 'stolen' by type annotations.

It was pointed out in the workshop that the syntax was proposed by  
Philip Wadler and Simon Peyton Jones. I accept these guys understand  
more about types than I ever will. But, I don't think they are likely  
to confuse surface syntax with underlying semantics. The underlying  
semantics seem to be clear. I am willing to believe I have missed  
some subtlety, but otherwise staying within Erlangs existing syntax  
seems to have the most benefits.

If there is a lot of work which has been expended on building  
annotations with the original annotation syntax, then it would be  
worth building a tool to translate the ... and 1..n syntax. I assume  
it should be relatively straightforward to develop a pretty printer  
based on the existing type contract parser.

So that is my main point, but I started to think, if the type  
contract/annotation syntax is cast within the syntax of normal  
Erlang, then we can consider using it within normal Erlang code. I  
don't think it gives any more power than guards, but it would be a  
pretty unification.

So, we might consider taking a type annotation and using it directly,  
for example in patterns:
receive X when [char()|tail()], pos_integer() -> fun(X) end.
Or even:
Pid ! [char()|tail()], pos_integer().

Also, assuming type-name functions yielded well defined values,  
storing type annotations in ETS/DETS should be straightforward. That  
might be a nice base for nifty tools which would like to check type  
annotations, maybe between versions of code.

Summary: I think here are some genuine benefits for type contracts to  
stay within Erlang syntax.
G Bulmer