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.
|
