Continually experimenting with new ideas and techniques — Reconstructing, Developing, Modernising.
There’s a way to add useful types and helpful type checking to the eminently practical sensible language Erlang and other languages, like Elixir, which use the Beam virtual machine. As a practical chap who wants typing to help me rather than submit to typing bondage that’s exciting! If you’re looking for a bland, objectively reasoned & considered post then I suggest stopping now!
I like strongly typed dynamic languages, and I like the idea that type systems can help us think about our problem domain and save us from some of the errors we’re likely to make as humans when working on a system conceived by someone else or some time in the distant past — say more than a week ago. Recently I’ve been working with Elixir, and was interested in its integration of Erlang’s dialyzer tool.
I expect that most people who’ve been exposed to my thoughts about type systems would imagine me grinding my teeth and rolling my eyes when faced with a type checker. I think that dialyzer is a pleasant breath of pragmatic fresh air when compared to some of the more powerful and abstract type systems which seem to be the current fad or some of the clunky and impoverished type systems from decades ago.
The thing I find most attractive about dialyzer is its intent, as explained in Lindahl and Sagonas’ paper Practical Type Inference Based on Success Typings:
Our main goal is to make uncover the implicit type information in Erlang code and make it explicitly available in programs. Because of the sizes of typical Erlang applications, the type inference should be completely automatic and faithfully respect the operational semantics of the language. Moreover, it should impose no code rewrites of any kind. The reason for this is simple. Rewriting, often safety critical, applications consisting of hundreds of thousand lines of code just to satisfy a type inferencer is not an option which will enjoy much success. However, large software applications have to be maintained, and often not by their original authors. By automatically revealing the type information that is already present, we provide automatic documentation that can evolve together with the program and will not rot. We also think that it is important to achieve a balance between precision and readability. Last but not least, the inferred typings should never be wrong.
This post and its successors are intended to be an entertaining and enlightening record of my voyage of discovery adding dialyzer to a production Elixir application.
One way to incorporate dialyzer in your elixir project is to find it on hex.pm and add it as a dependency in an elixir project’s mix.exs.
Then if you run the following commands and no warnings are emitted, you’re done 😉:
mix dialyzer # this might take a while...
The interesting part is how to deal with warnings, and how to make the types you add useful to maintainers, and that’s another post…