Prevajanje prestreznikov algebrajskih učinkov v jezik brez učinkov

magistrsko delo

Žiga Zupančič (Author), Matija Pretnar (Mentor)

Abstract

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.

Keywords

računski učinki;prestrezniki algebrajskih učinkov;eksplicitni tipi;jezik brez eksplicitnih učinkov;

Data

Language:	Slovenian
Year of publishing:	2020
Typology:	2.09 - Master's Thesis
Organization:	UL FMF - Faculty of Mathematics and Physics
Publisher:	[Ž. Zupančič]
UDC:	004.4
COBISS:	25937155
Views:	1614
Downloads:	207
Average score:	0 (0 votes)
Metadata:

Other data

Secondary language:	English
Secondary title:	Elaboration of algebraic effect handlers to a language without effects
Secondary abstract:	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.
Secondary keywords:	computational effects;algebraic effect handlers;explicit types;language without explicit effects;
Type (COBISS):	Master's thesis/paper
Study programme:	0
Embargo end date (OpenAIRE):	1970-01-01
Thesis comment:	Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Računalništvo in matematika - 2. stopnja
Pages:	IX, 59 str.
ID:	11555481