[erlang-questions] Specifying Type Contracts in Erlang
Mon Oct 8 12:02:41 CEST 2007
EDIT: After having written most of my answers in this mail I want to
make a general point. The types would be parsed by the Erlang parser,
and not some plug-in parser that understands types. The types will be
turned into parse forms that are Erlang terms, and then be used by any
Erlang tool. As long as you use the Erlang parser (which I guess most
tools are using) there is only the matter of defining how the parse
forms look like, and to provide an interface for interpreting them. I
think it must be clear from the context if you are talking about types
or erlang terms, so I think there should be a special parse form for types.
G Bulmer 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.
Thank you. However, if nobody uses it it will be worthless, so let us
try to find a syntax that pleases most erlangers.
It was pointed out to me that there are differences between our syntax
and the one used by Quick Check and possibly also with Edoc. I think it
is ok to have differences as long as the core of the language is the
same so it would be good if we can agree on some syntax, and pretty fast
at that since we would like to include the type specifications in R12B.
> 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().
We used to have ranges with the syntax range(1,42) which is more or less
what you suggest. I think that range is a slightly better keyword since
seq somewhat suggests that you really have a sequence including all
integers (which of course is more or less the same as range...).
> 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().
The "proper" description for this type is nonempty_list(char()), but as
this is a pretty common construction it is good to have syntactic sugar
for it. [char()|_] looks a bit to me as a list with a char as the first
element and then anything in the tail, which is not the meaning of the
type. The meaning of the type is better captured by [char()|[char()]],
but this is also a bit of a mouthful. The current representation
[char(),...] is quite handy in that respect.
There two more places where we do not have erlang syntax, and that is
the function types. Both as specifications, and as higher order
functions (funs). The specifications are a minor problem since it can
only appear at the top level of a -spec, but the funs are a bit more
problematic. In our current implementation they look as
fun((T1, T2, T3)-> T4)
and if we would use erlang fun syntax it would look as
fun(T1, T2, T3) -> T4 end
whith the end keyword having to be added to end the type.
> What benefits do I think we'd get by staying within Erlang syntax?
> 1. There is little new to learn.
You still need to understand that you are talking about types and not
about function calls and structured term construction, so I don't think
this is a major point.
> 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.
The parse format for types should probably recognize that the user
specified the type byte() rather than a call to the function byte(), but
this is of course an implementation issue.
> 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.
The mechanism is the same whatever the parser gives back.
> 4. Erlang syntax could be extended in the future, without having any
> syntax 'stolen' by type annotations.
Yes, this is a good point. We would still probably hog the '::' to
specify that you are talking about types rather than of Erlang terms.
> 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.
Yes, this is not a major problem.
> 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().
I will leave for others to debate how types can be used within normal
Erlang constructs, but it must be absolutely clear from the context that
the programmer is talking about types, since this would be a major shift
in the language. Having types and specifications given as attributes is
a minor shift since we are not altering the semantics of Erlang (unless
you specifically ask for it by using some tool).
> 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.
The types are of course represented as Erlang terms in my
implementation, and storing them in whatever form you like is
unproblematic. However, the types should be treated as an ADT and should
be handled by a module with a nice interface. This is somewhat
orthogonal to types having the same syntax as the rest of Erlang.
> Summary: I think here are some genuine benefits for type contracts to
> stay within Erlang syntax.
> G Bulmer
I can also see benefits with having types in Erlang syntax, but the
syntax still have to be extended to make it clear from the context that
the programmer is talking about types and not general Erlang terms. Any
tool that wants to use types would do so either directly on the parse
forms or on some abstract format that will be provided. Either way, the
types would have an Erlang representation that can be manipulated.
More information about the erlang-questions