[erlang-questions] Specifying Type Contracts in Erlang
Sun Oct 7 21:08:15 CEST 2007
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
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.
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.
More information about the erlang-questions