[erlang-questions] Specifying Type Contracts in Erlang

[Kirill Zaborski]

Is this paper publicly available somewhere? I think it would be interesting
to read.

Best regards,
Kirill.

On 10/7/07, G Bulmer <gbulmer@REDACTED> wrote:
>
> 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
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://www.erlang.org/mailman/listinfo/erlang-questions
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20071007/9ee12ebb/attachment.htm>