babel
Project description
TITLE: Typing Behaviors for Elixir
This project is proposed in collaboration with Dashbit .

Context

Elixir is an open-source dynamic functional programming language that runs on the Erlang Virtual Machine [1], designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers. It is used by companies such as PagerDuty, Discord, PepsiCo, and Pinterest. Static typing seems nowadays to be the most important request coming from the Elixir community. IRIF has an ongoing collaboration with the Elixir development team to define and implement static type-checking for Elixir. The current type system we are implementing for Elixir is described in [2]. It is a type system based on the theory of semantics subtyping [3], thanks to which union, intersection, and negation types (a.k.a. set-theoretic types) can be added to existing languages [4]. It features cutting edge typing techniques: parametric polymorphism with local type inference, overloading, occurrence typing, gradual typing, and a sophisticated type analysis of patterns and guards [5,6,7,8,9]. It currently (and gradually) being integrated in Elixir.

Goals

The current type system does not cover yet Elixir module system. Elixir is a language with first-class modules: modules can be passed to functions and returned as results. The “types” for modules are called behaviors: when you declare a behavior in Elixir, you specify a list of function callbacks, alongside their domain and codomain. A module implements (i.e., it is typed by) a behavior if it defines for each callback in the behavior a function that accepts a superset of the callback domain and returns a subset of the callback codomain. Elixir uses behaviors to implement a naive static typing of modules: if a module adopting a behavior does not implement all the callbacks of the behavior or does not do it according to their specifications, then a warning is emitted. Currently, callbacks’ domains and codomains are specified in TypeSpec [12], but the goal of this project is to integrate behaviors in the Elixir type-system under development. This will require further research. Behaviors may specify the type of callbacks in terms of abstract types, that is, nominal types whose concrete implementation is provided only by each module. In Elixir this corresponds to use term() (Elixir top type) in the TypeSpec specification of a callback. We can already more advantageously replace term() by dynamic() (the dynamic type of our gradual type system), but to fully exploit the information provided by behaviors, we need a type system capable of distinguishing the different roles of each type introduced in a behaviour: the concrete types, shared by all implementations, must be exported transparently; the abstract types, that can be processed and known only by the callback functions, must be exported opaquely; some other types, that are specific to each implementation but must be publicly known, must be instead param- eters of the behaviours. This requires to extend the semantic subtyping framework, for instance to cope with existential types for packaged modules [10,11] or Bounded Existential Types as implemented in Julia [13,14]. A concrete example of this can be found in Appendix C of [2]. At the same time, even the simpler extension where abstract types are simulated by dynamic() will require careful consideration at the language design, especially in regard to backward compatibility.

The research will be carried out at the Research Institute on the Foundations of Computer Science (IRIF) in Paris under the supervision of Giuseppe Castagna (principal investigator for the Elixir Type System, directeur de recherche CNRS at IRIF) and collaboration with José Valim (creator and main developer of the Elixir programming language, at Dashbit). The project will explore both theoretical (e.g., existential types in semantic subtyping) and practical (e.g., languages design and implementation) aspects, in a proportion that will depend on the profile of the candidate. The perspective of this proposal is that the results of this project will be integrated in the compiler of Elixir.
References
[2,3,5,10,11,13] are mandatory reading
Contact
Giuseppe Castagna : IRIF, Research Institute on the Foundations of Computer Science, Université Paris Cité.

Powered by CDuce

XHTML Strict valid!

CSS valid!

Site map
This site was generated by two CDuce programs: the first transforms BibTeX files into an XML document while the second generates from this and few other XML documents a set of statically certified XHTML-strict pages with table of contents, list of references, non-dangling internal links, etc. More details can be found here.Français fr