A Gradual Type System for Elixir

TL;DR

This paper introduces a gradual type system for Elixir that enables type-checking without altering the language syntax, supporting untyped code and implemented via a prototype in Elixir.

Contribution

It presents a novel gradual type system for Elixir that integrates seamlessly without syntax changes and supports backward compatibility.

Findings

Type-checking is feasible on a significant language fragment.

The system supports untyped code fragments.

Prototype implementation demonstrates practicality.

Abstract

Elixir is a functional programming language with dynamic typing. We propose a gradual type system that makes it possible to perform type-checking on a significant fragment of the language. An important feature of the type system is that it does not require any syntactic change to Elixir. Type information is provided by means of function signatures which are declared in terms of Elixir typespec directives. The proposed type system is based on subtyping and is backward compatible, as it allows the presence of untyped code fragments. We have implemented a prototype of the type-checker in Elixir itself.