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?

Crandale

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.

Bacardi

Can you explain why going without a typechecker was enlightening? Do you became to think that typecheckers are useless in your experience? – Pentecost

There are plenty of applications where typecheckers are tremendously useful. And they work like magic in languages like OCaml. For me, a side effect of always relying on them was that the part of my brain wasn't paying attention to a significant high-level aspect of a program. It becomes something like a blindspot and I prefer to maintain full awareness and focus of the program I am writing. That said, I wish there was a better optional typechecker in Erlang. Can't beat typecheckers for refactoring and collaboration as it's impossible to maintain same focus with all the code at all times. – Bacardi

Answer 2

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

Cardin

Answer 3

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.

Hardbitten

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

Fungal

thats what I ended up doing as well :) – Crandale

Answer 5

For some time now there's also Gradualizer. Disclaimer: I'm one of the contributors.

Gradualizer is a static type checker for Erlang with support for gradual typing. It can infer some types, but mostly relies on function specs. It checks for consistency of a function body with its declared spec and for consistency of a callee's spec with passed in arguments. It supports equi-recursive types (user types which expand to user types), union types, a limited form of intersection types (multi-clause specs, i.e. overloaded functions).

Gradualizer is written in Erlang, so contributing by the community should be possible. Since recently, it can self-check without reporting any errors. It's a work in progress, but at an advanced stage with coverage of practically the entire Erlang syntax (tuples, records, maps, whatnot). Thanks to dogfooding it on itself, we know how convenient (or inconvenient) it already is in comparison with writing untyped Erlang and can focus on the most important things to improve next. It comes with a Rebar3 plugin and a CLI interface.

Check it out on GitHub or on HexDocs!

Cedric