[erlang-questions] Specifying Type Contracts in Erlang

Tobias Lindahl tobias.lindahl@REDACTED
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.

Tobias





More information about the erlang-questions mailing list