[erlang-questions] Type def and spec syntax

[Jesper Louis Andersen]

>
>
>
> -spec foo(Y) -> integer() when atom(Y).
> -spec foo(Y) -> integer() when atom(Y :: integer()).
>
>
Hi Robert,

Putting this in the limestone spotlight, we can muse over why this can
happen:

A language consists of 3 things: A grammar of accepted syntax, a static
semantics ("statics"), run on the grammar before execution, and a dynamic
 semantics which tells how the program executes ("dynamics"). Almost
*every* language has all three. The reason is that the grammar often
accepts more input than what are valid programs. One example would be in
common lisp, where

(defun x)

is a valid s-expression, but it isn't a valid program. In fact, SBCL
rejects this program. One could argue it is within the valid syntax of a
Lisp (S-exp) but isn't valid according to the statics. Another, better,
example is the following Erlang module:

-module(z).
-export([t/1, u/1]).
t(X) ->
    t(X, a).

u(X) -> X + Y.

which is valid from a parsing perspective, but isn't a valid erlang program
due to an arity mismatch on t/2 which is undefined. And u/1 uses the
unbound variable Y. What erlang uses is a linting step as part of its
statics to rule out such a module as valid. It is very nice to allow for
being lax in the notation of the grammar and then tighten up the valid
programs later on. In fact, type checking/inference is often part of the
statics in order to constrain the valid programs and simplify the later
compiler parts. Most notably the dynamic semantics of the program.

The key part is that Erlang *does* have a type checker, but it is rather
weak since it is really the linting step + more correctness steps inside
the compiler. It verifies structurality of your expressions, but it doesn't
verify that the types you pass around are valid. You cannot avoid it if you
have any kind of way to exit the compiler with some kind of structural
error, like an undefined variable. The alternative is to postpone these
kinds of errors until the dynamics at runtime, but only very insane
programming languages do this. One such example is Guido in which you can
write:

def foo():
    return y

which is accepted as a program, but once you run it, it fails
spectacularly[0]:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 2, in foo
NameError: name 'y' is not defined

The TL;DR is that you can't judge the valid programs by the grammar and
syntax alone. You have to know the statics of a program as well to be able
to define what constitutes a valid program.

And what does this have to do with types? Well, types are just languages
with grammar rules as well. So it is likely that you have grammar-valid
syntax which isn't a valid type because there is a statics which encode
what the valid types are. This is often called a kind-system, and it
encodes certain rules for what to check to rule out the invalid programs at
the type level.

If you think about it, this is also why BNF is a lousy way to document what
are the valid programs. What you really need are operational semantics so
you can properly encode what the valid programs are. Preferably in machine
verifiable form (Agda, Coq, Twelf, ...)

[0] To be very polite: HOW THE HELL DO PEOPLE PROGRAM LARGE SOFTWARE
SYSTEMS WITH THIS????
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20161003/21ddc106/attachment.htm>