Menu
Effektsystemer er i øjeblikket et varmt forskningsområde inden for typeteori. Mange effektsystemer er dog meget komplicerede at bruge, selvom de er kraftfulde, især for programmører, der ikke er eksperter i typeteori. Effektsystemer med inferens kan give nyttige garantier til programmeringssprog, samtidig med at de er simple nok til at blive brugt i praksis af almindelige programmører.
Med udgangspunkt i det booleanske unifikationsbaserede polymorfe effektsystem i Flix programmeringssproget ønsker vi at forfølge to praktiske kortsigtede mål:
(a) forbedre kvaliteten af effekt-fejlmeddelelser, og
(b) udvikle teknikker til at forbedre ydeevnen af booleansk unifikation og effektinferens.
Dermed lægges grundlaget for et mere ambitiøst mål: Futhark programmeringssproget understøtter en form for referentielt transparente in-place opdateringer, kontrolleret af et system af unikhedstyper inspireret af Clean, men som er for begrænset i nærvær af polymorfe højere-ordens funktioner. En omformulering af typesystemet i forhold til effekter, baseret på det i Flix, kunne måske give et mere intuitivt system.
Et unikt aspekt af dette projekt er, at det samler to forskere inden for programmeringssprog, som begge arbejder på fuldgyldige programmeringssprogs-implementeringer.
Projektperiode: 2022-2023
Budget: 660.000 kr
Projektledere
og
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.
Projektet har til formål at forbedre tilgængeligheden og implementeringen af effektsystemer i virkelige programmeringssprog, ved at udnytte udviklingen af Flix og Futhark til at demonstrere deres praktiske anvendelse og påvirke integrationen af avancerede typestyrefunktioner i mainstream-programmeringssprog.
