Eksplicitna izpeljava učinkov : magistrsko delo

Koprivec, Filip (author), Pretnar, Matija (mentor)

V delu je predstavljena avtomatska izpeljava in eksplicitna dopolnitev tipov programov z algebrajskimi učinki. Predstavljen je MiniEff, preprost funkcijski programski jezik s polimorfnimi shemami in podporo za algebrajske učinke, ki temelji na jeziku Eff. Za MiniEff sta podana in dokazana izrek o napredku in izrek o ohranitvi. Predstavljen in podan je jezik ImpEff, ki tipom v jeziku MiniEff doda informacije o sproženih učinkov, skupaj s pripadajočim sistemom tipov, ki uporablja podtipe. Izreka o napredku in ohranitvi sta posodobljena in dokazana tudi za ImpEff, kjer so pojasnjene ključne spremembe glede na jezik MiniEff. Podan je jezik ExEff, ki predstavlja eksplicitno obliko jezika ImpEff, osnovano na polimorfnem lambda računu. Podan je sistem tipov in izrekoma o napredku in ohranitvi in pripadajočima dokazoma. Podana so pravila za dopolnitev programov iz jezika ImpEff v jezik ExEff skupaj z dokazom, da dopolnitev ohranja tipe. Prikazana je variacija Hindley-Milnerjevega algoritma za izpeljavo tipov, ki programom iz jezika ImpEff določi tipe in jih dopolni v eksplicitno obliko v jeziku ExEff. Za prikazani algoritem sta podana izreka o zdravosti in polnosti. Prikazana je sprememba relacije izpeljave in dopolnitve z uporabo lenih substitucij, ki je trenutno uporabljana v prevajalniku za jezik Eff.

• Language: Slovenian
• Keywords: algebrajski učinki in njihovi prestrezniki, izpeljava tipov, eksplicitni tipi
• Work type: Master's thesis/paper
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2019
• PID: 20.500.12556/RUL-110366
• UDC: 004.42
• COBISS.SI-ID: 18718809
• Publication date in RUL: 14.09.2019

Secondary language

• Language: English
• Title: Explicit effect inference

Abstract

Automatic type inference and explicit elaboration of programs with support for algebraic effects is presented in this work. ImpEff, a simple polymorphic functional calculus with support for algebraic effects, based on the Eff language is presented. For the MiniEff language a corresponding progress and preservation theorems are presented and proved. The type system of the MiniEff language is enhanced with the ImpEff programing language, which adds an effect-type system with subtyping to existing MiniEff types. Progress and preservation theorems and their proofs are updated to coincide with effect based type system, where key changes to the MiniEff version are explained. The ExEff language is presented, which is an explicit version of ImpEff language based on the polymorphic lambda calculus. A type system along with the accompanying progress and preservation theorems and their proofs is presented. The rules for the elaboration of programs from ImpEff to ExEff are presented along with proof, that elaboration preserves types. A variation of the Hindley-Milner type derivation algorithm is presented, which infers types of ImpEff programs and elaborates them to explicit ExEff programs. For the given elaboration algorithm, the corresponding soundness, and completeness theorems are presented. Changed inference and elaboration relation with lazy substitutions, as currently used in Eff compiler is presented.

• Keywords: algebraic effects and their handlers, type inference, explicit types