From dynamic to static, Elixir begins its transformation
The open-source programming language Elixir has found a lot of success for web applications and distributed systems, but the current lack of a static type system is a limitation for finding a series of bugs at compile time. Elixir’s latest version kickstarts its transition towards a safer and more ergonomic approach thanks to the theoretical work of Giuseppe Castagna and his PhD student Guillaume Duboc, both working at Institut de Recherche en Informatique Fondamentale (IRIF - CNRS/Université Paris Cité).
Created in 2012 by José Valim, currently chief adoption officer at Dashbit, Elixir is an open-source programming language tailor-made for the Erlang Virtual Machine. Erlang was developed in the late ’80s by the Swedish company Ericsson with the ability to run 24/7 for years without needing to be closed or risking crashing, to deal with an enormous number of simultaneous users and to exchange with various other software. Started as a tool to manage telephone lines networks, Erlang is now used for numerous online applications. For instance, WhatsApp is built on Erlang.
Elixir builds on top of Erlang with new abstractions and a rich ecosystem, powered by many libraries that are both easy to use and very stable. It also enables to fully develop an application without the need to know other programming languages. ‘Developers often praise Elixir because it allows a small team to create from the ground up a prototype, and then upscale it for millions of users with the same people, says Guillaume Duboc, PhD student at IRIF. Otherwise, you’d have to hire dozens of engineers to do that.’
With his doctoral advisor Giuseppe Castagna, CNRS senior researcher at IRIF, Guillaume Duboc has been contributing since 2021 to Elixir’s development. Their work has been central in its next release. ‘One of the main features of Elixir’s new version is that we introduce a gradual set-theoretic type system, explains José Valim. This will allow us to start moving from a dynamic language to also a static one.’
Coding implies using a lot of different types of data, like numbers, words, strings or lists, which have different properties. For instance, a program can be asked to sum numbers together, but that operation is not possible with words. When the code is compiled, which means translated from something that humans can write and read to instructions that machines actually understand, a static language will check if each command is compatible with the type of data that it targets. On the other hand, a dynamic language will perform such checks while the program runs, which may lead to bugs and crashes. It implies that the developer must double-check beforehand and manually verify the types of data. A gradual set-theoretic type system deals with different types of data using operations coming from set theory, and checks the typing during compiling.
The gradual set-theoretic type system used in Elixir comes from Giuseppe Castagna and Guillaume Duboc’s research. ‘Our work was very theoretical, but José Valim read our papers and saw that they could be applied to Elixir, recalls the PhD student. People from WhatsApp and Roblox have also worked with some of our ideas.’ ‘Thanks to Giuseppe Castagna and his students, we don’t need to involve other people with our research, we already have the best!’, rejoices José Valim.
As Elixir is an expressive and flexible language, the gradual set-theoretic type system needs to assess all of its features. It achieves this mission by using mathematical proofs and concepts. Giuseppe Castagna’s team made it work based on several simple set operations that are more intuitive to use for developers. It allows a slow transition between a dynamic and a static language, taking into account existing codebases while at the same time it relieves developers from some of the mental burden. Things that are greatly appreciated by Guillaume Duboc, as his PhD happens to be under joint supervision of IRIF and Remote, a company which employs about fifty engineers specialized in Elixir.