Efficient multishot algebraic effect handlers : doctoral thesis

Koprivec, Filip (avtor), Vidali, Janoš (mentor)

Algebraic effects and handlers are a powerful abstraction for structuring effectful programs. Computational effects are represented by operations and the meaning of these operations is defined by handlers. This separation of concerns allows for a clear separation of the effectful code and the code that interprets these effects, allowing for a more modular and maintainable codebase. However, the performance of algebraic effects and handlers is still a concern. This thesis presents a compilation pipeline that compiles programs from Eff - a language with native support for algebraic effects and handlers - to Ocaml, which does not have native support for algebraic effects and handlers. The compilation pipeline performs several optimizations to improve the performance of the generated code. We first introduce an explicitly typed language CoreEff that serves as an intermediate language between Eff and Ocaml. We then introduce several optimizations that simplify coercions generated for polymorphic functions and optimize the code using source-to-source transformation and function specialization relying on the explicit type information available in the language. Furthermore, the optimization phases are designed to be modular, can be easily extended with new optimizations and are proven to preserve the denotational semantics of the program. Finally, we evaluate the performance of the generated code by implementing the compilation pipeline in Eff compiler and evaluation on several benchmarks. The results show that the optimizations significantly improve the performance of the generated code, making the overhead of using algebraic effects and handlers negligible in most cases.

• Jezik: Angleški jezik
• Ključne besede: Algebraic effects, effect handlers, functional programming, theory of programming languages, denotational semantics, optimizing compilation, polymorphic compilation, subtyping
• Vrsta gradiva: Doktorsko delo/naloga
• Tipologija: 2.08 - Doktorska disertacija
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2024
• PID: 20.500.12556/RUL-162658
• UDK: 004.43
• COBISS.SI-ID: 209434371
• Datum objave v RUL: 26.09.2024

Sekundarni jezik

• Jezik: Slovenski jezik
• Naslov: Učinkoviti večsmerni prestrezniki algebrajskih učinkov

Izvleček

Algebrajski učinki in njihovi prestrezniki ponujajo močno abstrakcijsko orodje za strukturiranje programov z računskimi učinki. Računske učinke predstavimo z operacijami, katerih pomen določajo prestrezniki. Ta ločitev omogoča jasno ločevanje kode, ki učinke lahko sproža, od tega, kako učinke interpretiramo, kar omogoča bolj modularno kodo, ki jo je lažje vzdrževati. Še vedno pa nas pestijo težave z učinkovitostjo programov, ki uporabljajo algebrajske učinke in prestreznike. V tem delu predstavimo prevajalnik, ki programe iz programskega jezika Eff - z vgrajeno podporo za algebrajske učinke in prestreznike - prevaja v jezik Ocaml, ki te podpore nima. Med prevajanjem izvedemo številne optimizacije za izboljšanje učinkovitosti končne kode. Najprej predstavimo eksplicitno tipiziran jezik CoreEff, ki služi kot vmesni jezik med prevajanjem iz Eff-a v Ocaml. Potem predstavimo optimizacije, ki poenostavijo pretvorbe med tipi za potrebe polimorfnih funkcij in dodatno optimizirajo kodo s pomočjo transformacijskih pravil in specializacije funkcij, ki temeljijo na eksplicitnih informacijah o tipih, ki so nam na voljo v samem jeziku. Optimizacije so zasnovane modularno in jih je mogoče enostavno razširiti z novimi, hkrati pa podamo tudi dokaze, ki zagotavljajo, da optimizacije ohranjajo denotacijsko semantiko programa. Nazadnje ovrednotimo učinkovitost prevedene kode z razširitvijo implementacije prevajalnika za jezik Eff in izmerimo hitrost izvajanja na več primerih. Rezultati pokažejo, da je optimizacija znatno izboljšala učinkovitost končne kode ter da ima uporaba algebrajskih učinkov in prestreznikov po optimizaciji v večini primerov zanemarljiv vpliv na hitrost izvajanja.

• Ključne besede: Algebrajski učinki, prestrezniki algebrajskih učinkov, funkcijsko programiranje, teorija programskih jezikov, denotacijska semantika, optimizirano prevajanje, polimorfno prevajanje, podtipi