Applications of algebraic effect theories
doctoral thesis
Povzetek
Algebrajski učinki so uveljavljena metoda za modeliranje računskih učinkov v funkcijskem programiranju. Učinke predstavimo z operacijami, pomen pa jim dodelimo s prestrezniki. Teorije algebrajskih učinkov so sestavljene iz signature, ki poda tipe operacij, in enačb, ki opisujejo njihovo obnašanje. Vsi prestrezniki morajo biti skladni s predpisano teorijo; prestreznik ne sme razlikovati med programi, ki jih v dani teoriji smatramo za enake. Teorije učinkov so običajno globalne, torej morajo vsi prestrezniki spoštovati isto množico enačb, kar omeji nabor možnih prestreznikov. Mnogo kasnejših pristopov zato enačbe odmisli, kar sicer olajša uporabo prestreznikov, vendar močno omeji možnosti dokazovanja lastnosti programov ob prisotnosti računskih učinkov, kjer enačbe igrajo ključno vlogo. V doktorskem delu predstavimo jezik ▫$EEFF$▫, ki z uporabo lokalnih teorij učinkov omili omejitve enotne teorije učinkov, saj omogoči uporabo različnih teorij v različnih delih programa. Za varnost poskrbi sistem tipov, nadgrajen z zmožnostjo sledenja teorijam učinkov, ki omogoča varno uporabo prestreznikov. Sistemu tipov je pridružena logika, v kateri preverjamo pravilnost prestreznikov. Za logiko imamo na voljo več možnosti, kar nam omogoča izbiro najprimernejše logike glede na problem. Zdravost logike določimo z uporabo denotacijske semantike, ki temelji na delnih ekvivalenčnih relacijah. Jezik ▫$EEFF$▫ je formaliziran v dokazovalnem pomočniku Coq in implementiran kot razširitev programskega jezika Eff. Formalizacija hkrati služi kot orodje za dokazovanje ekvivalence programov in vsebuje dve različni logiki, za kateri pokažemo zdravost. V doktorskem delu podamo več primerov, ki predstavijo prednosti uporabe lokalnih teorij algebrajskih učinkov.
Ključne besede
algebraic effects;effect handlers;functional programming;theory of programming languages;denotational semantics;
Podatki
| Jezik: | Angleški jezik |
|---|---|
| Leto izida: | 2020 |
| Tipologija: | 2.08 - Doktorska disertacija |
| Organizacija: | UL FMF - Fakulteta za matematiko in fiziko |
| Založnik: | [Ž. Lukšič] |
| UDK: | 510.6(043.3) |
| COBISS: |
43657475
|
| Št. ogledov: | 2019 |
| Št. prenosov: | 619 |
| Ocena: | 0 (0 glasov) |
| Metapodatki: |
|
Ostali podatki
| Sekundarni jezik: | Slovenski jezik |
|---|---|
| Sekundarni naslov: | Uporaba teorij algebrajskih učinkov |
| Sekundarni povzetek: | Algebraic effects are an established method of implementing effectful behaviour in functional programming languages. Computational effects are represented by operations and implemented through effect handlers. An effect theory consists of a type signature and a set of equations describing the behaviour of effect invocations. All effect handlers are required to adhere to the prescribed effect theory, meaning that they do not differentiate between two programs considered equal in the given theory. The standard approach to algebraic effects assumes a global effect theory, so all handlers need to respect the same set of equations. This often becomes very restricting in terms of suitable handlers and therefore most contemporary work focuses on theories that contain no equations. Discarding equations allows for a wider variety of viable handlers but drastically reduces the capabilities to reason about properties of effectful code. In the thesis we present the language ▫$EEFF$▫ that relaxes the single theory limitation by using local effect theories, allowing the use of different theories in different parts of the program, even when pertaining to effects with the same signature. This alleviates the issues of global effect theories while providing all benefits of equations. The type system is upgraded to track theory information, allowing for safe use of handlers and ensuring their correctness at the relevant theory. Proofs of handler correctness are done in a logic that is coupled with the type system. The type system can be coupled with different logics, granting the option to select a logic suitable for the problems at hand. The soundness of a logic is established with respect to a denotational semantics based on partial equivalence relations. The safety theorems of ▫$EEFF$▫ are formalised in the proof assistant Coq, and the implementation of ▫$EEFF$▫ is an extension of the language Eff. The formalisation also doubles as a reasoning tool for programs with algebraic effect theories and features two different logics to choose from, both of which are shown to be sound. Multiple examples throughout the thesis showcase the benefits of local algebraic theories. |
| Sekundarne ključne besede: | algebrajski učinki;prestrezniki algebrajskih učinkov;funkcijsko programiranje;teorija programskih jezikov;denotacijska semantika;disertacije; |
| Vrsta dela (COBISS): | Doktorsko delo/naloga |
| Študijski program: | 0 |
| Konec prepovedi (OpenAIRE): | 1970-01-01 |
| Komentar na gradivo: | Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Matematika - 3. stopnja |
| Strani: | XIII, 174 str. |
| ID: | 12158016 |
Priporočena dela: