YATT (Yet Another Typing Thread)

[Luke Gorrie]

Hello,

This is probably a bad time to start a different thread about typing
in Erlang. But I'm doing it anyway :-). In my playing around I have
found a nice type system, and would like to put it on the radar of
Erlang hackers and hear what people doing static-typing for Erlang
think of it.

I refer to CMU Common Lisp (CMUCL). This is a free Lisp system that
has been actively developed since early in the 1980s and continues
today. http://www.cons.org/cmucl/

They have a very interesting approach to typing which is both static
and dynamic. They don't make the language fully statically typed, but
instead do as much as possible with what type information they have
available. The type information available in a Common Lisp program is
very similar to what's available in an Erlang program, mostly from
type-checking guards. This makes me think the CMUCL approach may work
well for Erlang too.

CMUCL is interesting because they do a _lot_ with the type information
available. For example:

  * Compiler optimizations. e.g. if some variables are declared to be
  floats, you can generate more efficient code for doing arithmetic on
  them. Erlang/BEAM does this too - that's why there are so many
  'float(X)' type declarations in the Wings3D code that Ulf quoted
  (excerpted down below). This is safe because before the
  float-specific code is executed the arguments are runtime-checked to
  actually be floats -- like in Erlang, type guards/declarations are
  not blindly trusted, they are treated as assertions to be checked.

  * Type inference. If some variables have specified types, this is
  used to figure out the types of more variables. For example, with:

     foo(X, Y) when float(X) ->
         Z = X * Y,
         ...

  You can figure out that Z is also a float. You also know that Y has
  to be a number in any of the "..." code, because otherwise it would
  have crashed with badarg on the the first line before getting that
  far.

  * Efficiency notes. If you want a function to be fast, you can tell
  the compiler so. It will then report every optimization opportunity
  that was missed because of insufficient type information.

  Take the Wings3d example again: they have added float(X)
  declarations in strategic places to generate fast code. Exactly
  which declarations they add are, I believe, based on deep knowledge
  of the compiler and BEAM.

  In CMUCL it is easier for mortals. You write the function with no
  type declarations, and say "this has to be fast". Then the compiler
  will print notes to the effect that "Hey, I could generate faster
  code if I knew that X, Y, and Z were floats". Then, if you know that
  they really should be floats, you add the type guards and get the
  good code. Thus you can do effective low-level optimization without
  intimate knowledge of the compiler.

  * Conservative static type error detection. If the compiler sees
  that you will cause a type error, it will give you a warning. It
  does this when it can prove that your code _will_ lead to a type
  error, not just that it might. For example, this code would generate
  a warning:

      X + length(X)

  because it could never work correctly: X has to be both a list and
  an integer, which is impossible. Note that it's a warning and not an
  error: maybe you want to test some other parts of the program before
  you fix this.

Overall you get a lot of benefits and none of the drawbacks usually
associated (by us Erlang programmers at least) with static typing -
i.e. it makes no restrictions on how you write code and you can ignore
the warnings if you want. In practice you do not ignore the warnings,
because the compiler only bothers to warn you when you've almost
certainly made a mistake.

So what does this mean to us Erlang programmers? Is this something
we'd like? Are recent compiler/BEAM developments already leading us in
this direction? Are there some fundamental reasons that this would not
work as well for Erlang that the type-theorists can tell us? Should I
shut the hell up about Lisp already? :-)

In any case, there are worse ways to spend a lazy afternoon than
reading the CMU Common Lisp user manual -- particularly the section on
advanced compiler usage. It is a seriously excellent work of
programming language implementation, even if you aren't interested in
Lisp per se. The URL is:

  http://www.cons.org/cmucl/doc/index.html

Also -- I don't like playing the luddite, but I never understand
conference talks about type systems. I'm not familiar with the
formalism(s) that people use and just see a lot of greek letters. Can
someone explain what formalisms people are using (e.g. is it
declarative semantics, or..?), and perhaps point to a book or two that
one could read to appreciate what's going on?

Here's the Wings3D code that Ulf quoted:

    twist_fun(y, {Cx,_,Cz}) ->
        fun(U, Min, {X0,Y,Z0})
           when float(U), float(Min), float(X0), float(Y), float(Z0) ->
                Angle = U*(Y-Min),
                Cos = math:cos(Angle),
                Sin = math:sin(Angle),
                X = X0 - Cx,
                Z = Z0 - Cz,
                {X*Cos+Z*Sin+Cx,Y,Z*Cos-X*Sin+Cz}
        end;

(BTW, comparison to CL also suggests another possible notation for
writing type guards: "when float(U, Min, X0, Y, Z0) ->", i.e. to make
the type guards n-ary.)

Cheers,
Luke