<div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><div class="gmail_msg"><br class="gmail_msg"><br class="gmail_msg">-spec foo(Y) -> integer() when atom(Y).<br class="gmail_msg">-spec foo(Y) -> integer() when atom(Y :: integer()).<br class="gmail_msg"><br class="gmail_msg"></div></div></div></div></div></div></blockquote><div><br></div><div>Hi Robert,</div><div><br></div><div>Putting this in the limestone spotlight, we can muse over why this can happen:</div><div><br></div><div>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</div><div><br></div><div>(defun x)</div><div><br></div><div>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:</div><div><br></div><div><div>-module(z).</div><div>-export([t/1, u/1]).<br></div><div>t(X) -><br></div><div>    t(X, a).</div><div><br></div></div><div>u(X) -> X + Y.</div><div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div>def foo():</div><div>    return y</div><div><br></div><div>which is accepted as a program, but once you run it, it fails spectacularly[0]:</div><div><br></div><div><div>Traceback (most recent call last):</div><div>  File "<stdin>", line 1, in <module></div><div>  File "<stdin>", line 2, in foo</div><div>NameError: name 'y' is not defined</div></div><div><br></div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>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, ...)</div><div><br></div><div>[0] To be very polite: HOW THE HELL DO PEOPLE PROGRAM LARGE SOFTWARE SYSTEMS WITH THIS????</div></div></div>