magistrsko delo
Povzetek
V delu je predstavljen funkcijski programski jezik Eff za delo z algebrajskimi učinki in njihovimi prestrezniki. Na primeru je prikazan prevod v OCaml in predstavljena učinkovitost izvajanja glede na ročno napisano kodo v OCaml-u. Opisana je optimizacija prevajanja in kakšne težave pri tem nastanejo. Kot rešitev je predstavljen eksplicitno tipiziran jezik ExEff z eksplicitnimi učinki in ciljni jezik tega jezika. Kot drug možen ciljni jezik je predstavljen eksplicitno tipiziran jezik NoEff, ki ne vsebuje eksplicitnih učinkov, sledi le njihovi uporabi. Dokazana sta izreka o ohranitvi ter delnem napredku za NoEff s spremljajočimi lemami. Opisana so pravila za prevajanje tipov, pretvorb, vrednosti in izračunov iz ExEff v NoEff. Podan je primer prevoda in dokazan je izrek o ohranitvi tipov. Na kratko je razložena tudi implementacija v jeziku OCaml, kjer predstavimo strukturo in nekatere dele kode.
Ključne besede
računski učinki;prestrezniki algebrajskih učinkov;eksplicitni tipi;jezik brez eksplicitnih učinkov;
Podatki
Jezik: |
Slovenski jezik |
Leto izida: |
2020 |
Tipologija: |
2.09 - Magistrsko delo |
Organizacija: |
UL FMF - Fakulteta za matematiko in fiziko |
Založnik: |
[Ž. Zupančič] |
UDK: |
004.4 |
COBISS: |
25937155
|
Št. ogledov: |
1614 |
Št. prenosov: |
207 |
Ocena: |
0 (0 glasov) |
Metapodatki: |
|
Ostali podatki
Sekundarni jezik: |
Angleški jezik |
Sekundarni naslov: |
Elaboration of algebraic effect handlers to a language without effects |
Sekundarni povzetek: |
In this work a functional programming language based on algebraic effect handlers, called Eff, is presented. It is shown on an example how it is translated to OCaml and how efficient its execution is in comparison to hand-written OCaml code. A compilation optimization is described and so are the difficulties of it. As a solution an explicitly typed language with explicit dirt, called ExEff, is presented and a backend for it. As another possible backend an explicitly typed language, called NoEff, is presented, which does not include explicit dirt but it tracks its use. Preservation and partial progress theorems are proved for NoEff with the corresponding lemmas. Rules for elaborating types, coercions, values and computations from ExEff to NoEff are described. An example of elaboration is given and the type preservation theorem is proved. Implementation to OCaml is briefly explained containing structure information and parts of the code. |
Sekundarne ključne besede: |
computational effects;algebraic effect handlers;explicit types;language without explicit effects; |
Vrsta dela (COBISS): |
Magistrsko 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, Računalništvo in matematika - 2. stopnja |
Strani: |
IX, 59 str. |
ID: |
11555481 |