Static typechecking in erlang

Question

I'm slowly falling in love with Erlang, and only have one big, BIG problem.

I'm a big fan of languages like Standart ML and ocaml with their strong static typechecking.

is there a nice and clean way to introduce somesort of static typechecking in erlang. I'm looking at the -type and -spec annotations.

Does anyone have a nice solution?

Answer 1

I've been there! I love both OCaml and Erlang and use them regularly.

By the time I started using Erlang I had years of experience with OCaml. It took me several weeks to adjust to the fact that there's no static typechecker in the compiler. But after that, the pain was completely gone.

To a certain extent, going without the typechecker is a worthwhile exercise. For me, it was enlightening experience and really made me a better programmer.

There's is, however, an external static typechecker for Erlang called Dializer. I find it very useful. The problem with it is that you need to call it separately and it is slow. Running it once in a while (e.g. before committing code or as a part automated builds) works great. I've never tried running it after each compilation as it would be too much of a distraction to wait until it completes.

Answer 2

check the Dialyzer tool

The Dialyzer is a static analysis tool that identifies software discrepancies such as definite type errors, code which has become dead or unreachable due to some programming error, unnecessary tests, etc. in single Erlang modules or entire (sets of) applications.

Answer 3

Through the years, there were some attempts to build type systems on top of Erlang. One such attempt happened back in 1997, conducted by Simon Marlow, one of the lead developers of the Glasgow Haskell Compiler, and Philip Wadler, who worked on Haskell's design and has contributed to the theory behind monads (Read the paper on said type system). Joe Armstrong later commented on the paper:

One day Phil phoned me up and announced that a) Erlang needed a type system, b) he had written a small prototype of a type system and c) he had a one year’s sabbatical and was going to write a type system for Erlang and “were we interested?” Answer —“Yes.”

Phil Wadler and Simon Marlow worked on a type system for over a year and the results were published in [20]. The results of the project were somewhat disappointing. To start with, only a subset of the language was type-checkable, the major omission being the lack of process types and of type checking inter-process messages.

http://learnyousomeerlang.com/types-or-lack-thereof

Answer 4

I mostly use -spec and -type for documentation purposes: you write spec with -spec, then check it with TypEr and then (after add some additional info in edoc format) generate documentation