Menu
Effect systems are currently a hot research subject in type theory. Yet many effect systems, whilst powerful, are very complicated to use, particularly by programmers who are not experts at type theory. Effect systems with inference can provide useful guarantees to programming languages while being simple enough to be used in practice by everyday programmers.
Building on the Boolean unification-based polymorphic effect system in the Flix programming language, we want to pursue two practical short-term objectives: to (a) improve the quality of effect error messages, and (b) develop techniques to improve the performance of Boolean unification and effect inference. Thus laying the foundation for a more ambitious objective: The Futhark programming language supports a form of referentially transparent in-place updates, controlled by a system of uniqueness types inspired by Clean, but which is too limited in the presence of polymorphic higher-order functions. Recasting the type system in terms of effects, based on the one in Flix, might provide a more intuitive system.
A unique aspect of this project is that it brings together two programming language researchers, who are both working on full-blown programming language implementations.
Project period: 2022-2023
Budget: DKK 660.000
The project addresses value creation following the three outlined categories:
Scientific Value
We see two clear publishable scientific contributions: (a) new techniques to improve the performance of Boolean unification and (b) new applications of type and effect systems based on Boolean unification.
Capacity Building
Flix and Futhark are the two major academic efforts toward building new programming languages in Denmark. Bringing the two research groups together will facilitate knowledge sharing and technology transfer; enabling both projects to thrive and grow even further. This unique opportunity exists because both languages are based on similar technology and because they do not compete in the same space. Success for one is not at the expense of the other, and they can rise together.
Business and Societal Value
A significant amount of research effort has been expended on designing effect systems. Despite widespread belief that such systems can lead to safer programs, few systems have been implemented in real-world programming languages. By focusing on improving ergonomics, we want to make these technologies more accessible. Being the designers of Flix and Futhark, we are in a great position to conduct such work. We can show the way for other mainstream programming languages by having real, full-blown implementations.
After decades of relative stagnation, programming languages are now rapidly absorbing features previously only seen in obscure or academic programming languages. Java and C# and prominent examples of originally very orthodox object-oriented languages that have been augmented with concepts from functional programming. We believe that effect systems and other fancy-type system features are a logical next step, but before they can be added to mainstream languages, it must be shown that they can be designed and implemented in a form that will be palatable to industrial users. Thus, while Flix and Futhark may or may not be the languages of the future, we believe that our research can help impact the direction of future programming languages by providing solid formal foundations and real-world implementations that others can build on directly or indirectly.
The project aims to enhance the accessibility and implementation of effect systems in real-world programming languages, leveraging the development of Flix and Futhark to demonstrate their practical application and influence the integration of advanced type system features in mainstream programming languages.
Aarhus University
Department of Computer Science
E: magnusm@cs.au.dk
University of Copenhagen
Department of Computer Science
