Matija Pretnar

Matija Pretnar

Fakulteta za matematiko in fiziko
Jadranska 21,
SI-1000 Ljubljana
tel: +386 1 4766 668
mail: matija.pretnar@fmf.uni-lj.si
GitHub: matijapretnar
ORCID iD: 0000-0001-7755-2303
Biblio: COBISS DBLP Scholar Scopus


Research

I study formalization, implementation, and semantics of programming languages. My current research is focused on algebraic effects and their handlers.

Poučevanje

Zaposlen sem na Fakulteti za matematiko in fiziko, kjer poučujem večinoma računalniške predmete.


Talks

Effect handlers and mathematically inspired language constructs

Structures de contrôle : de « goto » aux effets algébriques, 07 Mar 2024, Collège de France, Paris

Effect handlers are a programming language construct able to express and combine diverse computational features such as backtracking, stream redirection, multiple scheduling strategies, or continuations. This flexibility comes as no surprise since handlers are based on even more versatile homomorphisms of algebraic theories. Even though the design of handlers witnessed multiple iterations and extensions, their mathematical core remained unchanged.

In this seminar, I will discuss the discovery of effect handlers and initial considerations behind their design, in particular steps required when translating a mathematical concept into a useful programming tool. We shall also take a look at subsequent research on handlers, for example various effect systems or an efficient transpiler to OCaml, comparing features guided by mathematics and those with a more practical motivation.

The state of Eff

NII Shonan Meeting (No.203) – Effect Handlers and General-Purpose Languages, 26 Sep 2023, Shonan (remotely)

The talk describes the history and the current state of Eff, the first programming language with native support of algebraic effect handlers. The first version of Eff was developed by Andrej Bauer and myself and appeared in 2010. It was untyped and had a syntax similar to Python. In the next version in 2011, we introduced the more commonly known ML-like syntax and dynamic generation of effect instances that worked analogously to references in OCaml. After that, the versions are a bit harder to reconstruct, but the main improvement was a subtyping-based effect system.

Building on the effect system, the next goal for Eff was an optimizing compiler, on which I worked together with Tom Schrijvers and his students. The compiler would produce efficient code by inlining handlers as much as possible, and monadically embed the rest in OCaml. It soon became obvious that the effect system has to be more robust, which was achieved by using coercions as explicit witnesses of subtyping. Currently, Filip Koprivec, my PhD student, focuses on simplifying those witnesses in the polymorphic setting, as otherwise each coercion needs to be passed around as an additional parameter at runtime. In parallel to the optimizing compiler project, Žiga Lukšič developed EEff, a variant of Eff that tracks algebraic equations between operations that have to be respected by the handlers. Currently, EEff only prints out the obligations, though one could envision sending them to an SMT solver or producing specifications for a proof assistant.

Finally, the talk mentions Millet, a language one can use as a basis when developing a prototype language exploring an interesting novel idea. Millet implements all the boring and expected components of a programming language (parsing, algebraic datatypes, simple type-checking, interactive toplevel, compilation pipeline, …), and any fork just needs to extend all the components with the support for the additional features. Then, any later change to Millet (right now, a module system, a Wasm backend, and LSP support are in the works) should be orthogonal and can hopefully be merged into forks with not too much additional work.

Asynchronous Effects

Scottish Programming Languages Seminar, 07 Jun 2023, University of the West of Scotland, Paisley

In the standard algebraic approach to effects, once an operation is called, the evaluation of the continuation stalls until it gets a result (either from a built-in primitive effect or through a handler). But we often desire asynchronous behaviour, when the continuation may proceed with the evaluation and suitably incorporates the result once it arrives. I will describe a small calculus with primitives for sending such signals and receiving corresponding interrupts, and show a small prototype in which one can express promises, preemptive multi-threading and remote function calls.

Joint work with Danel Ahman.

Efficient compilation of algebraic effect handlers

Dagstuhl Seminar 21292, 21 Jul 2021, Dagstuhl (remotely)

The popularity of algebraic effect handlers as a programming language feature for user-defined computational effects is steadily growing. Yet, even though efficient runtime representations have already been studied, most handler-based programs are still much slower than hand-written code.

This paper shows that the performance gap can be drastically narrowed (in some cases even closed) by means of type-and-effect directed optimising compilation. Our approach consists of source-to-source transformations in two phases of the compilation pipeline. Firstly, elementary rewrites, aided by judicious function specialisation, exploit the explicit type and effect information of the compiler’s core language to aggressively reduce handler applications. Secondly, after erasing the effect information further rewrites in the backend of the compiler emit tight code.

This work comes with a practical implementation: an optimizing compiler from Eff, an ML style language with algebraic effect handlers, to OCaml. Experimental evaluation with this implementation demonstrates that in a number of benchmarks, our approach eliminates much of the overhead of handlers, outperforms capability-passing style compilation and yields competitive performance compared to hand-written OCaml code as well Multicore OCaml’s dedicated runtime support.

Introduction to Quantum Computing

Leamington Café Scientifique, 22 Jun 2021, Laemington Spa (remotely)

We often read in the media that quantum computers are fast because quantum superposition allows them to be in multiple states at once, enabling them to explore all the possible solutions in a single step.

As we shall see, things are not that simple because, in the end, we can observe only one randomly chosen result, which is likely not going to be the one we need. After all, with all the possible solutions out there, what’s the guarantee that the one we want is the one randomly chosen by the quantum computer? So we want to be able to increase the probability of getting the solution we want from among all the possible paths.

What can be done is to use interference to cancel out all the undesirable paths and unwanted solutions. Although we still end up with a randomly chosen path, it is a path chosen from among the ones we want.

Kvantno računalništvo

Gimnazija Bežigrad, 23 Jan 2020, Ljubljana

Asynchronous operations

IFIP WG2.1 meeting #79, 08 Jan 2020, Otterlo

In the standard algebraic approach to effects, once an operation is called, the evaluation of the continuation stalls until it gets a result (either from a built-in primitive effect or through a handler). But we often desire asynchronous behaviour, when the continuation may proceed with the evaluation and suitably incorporates the result once it arrives. I will describe a small calculus with primitives for sending and receiving such signals.

Joint work with Danel Ahman

Projekt Tomo

Maps ∩ Configurations ∩ Polytopes ∩ Molecules ⊆ Graphs: The mathematics of Tomaž Pisanski on the occasion of his 70th birthday, 23 May 2019, Ljubljana

Projekt Tomo is a web service for teaching programming that works by providing students immediate and low-overhead automated feedback on the correctness of the submitted solutions. In the talk, I will describe the basic principles of the service, its history and how its eponym helped shape it.

Putting reason back into handlers

IFIP WG2.1 meeting #77, 03 Jul 2018, Brandenburg

The main premise of algebraic effects is that effects can be described with an equational theory consisting of a set of operations and equations between them. However, many computationally interesting algebraic effect handlers do not respect these equations, which most approaches nowadays reconcile by assuming a trivial equational theory. I will present an approach in which the expected equations may be encoded in computation types.

Joint work with Žiga Lukšič

Bringing equations back to algebraic effect handlers

LFCS seminar, 02 Jul 2019, Edinburgh

Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. I will present an alternative approach where the effect system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.

Joint work with Žiga Lukšič

Local algebraic effect theories

Meet The Jury!, 23 Jan 2019, Leuven

Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety.

We present an alternative approach where the type system tracks equations thar are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.

Joint work with Žiga Lukšič

Explicit effects subtyping

IFIP WG2.1 meeting #76, 18 Oct 2017, Lesbos

To inform the programmer about the effects of a given program, a bottom up inference algorithm that Eff provides is sufficient. However, for an optimizing compiler, we need access to effects of all subterms. It turned out that adapting the current algorithm is overly error-prone as the core language is implicitly typed and subtyping-based.

In hope of remedying the situation, we present an explicitly-typed polymorphic core calculus, which reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof. We provide a constraint-based inference algorithm that turns an implicitly-typed term into our calculus, and effect erasure, which allows us to targets an ML-like language with or without support for algebraic effects.

The talk will include a brief introduction to algebraic effect handlers.

Joint work with Amr Hany Saleh, George Karachalias and Tom Schrijvers

Hekerski pristop k statistiki

FMF seminar za učitelje matematike, 01 Oct 2016, Ljubljana

Recimo, da so učenci 3. b razreda pri testu iz matematike dosegli povprečno 63%, učenci 3. c razreda pa 70%. Ali so učenci 3. c res bolj razumeli snov ali pa je razlika le posledica zunanjih dejavnikov in bi bil kakšen drug dan rezultat ravno obraten? Kaj pa, če se enaka razlika pojavi še pri naslednjem testu? S kakšno gotovostjo lahko rečemo, da ni šlo za naključje? Statistika nam na taka vprašanja zna odgovoriti, vendar so odgovori dostikrat precej zapleteni. Na seminarju si bomo zato ogledali alternativen pristop, pri katerem iskano gotovost ocenimo s pomočjo računalniških simulacij.

A low overhead automated service for teaching programming

Koli Calling 2015, 20 Nov 2015, Koli

Programming is a skill that often demands that students engage in a significantly high amount of individual practice and experimentation in order to acquire basic competence. Teachers are required to both encourage students by exposing them to numerous problems and supervise the students’ attempts to solve them.

To support this teaching approach we developed a web service called Projekt Tomo, presented in the article. The service is designed in such a way that it requires little or no additional work from students and teachers, enabling them to focus on the content. Furthermore, the service can be used in almost all teaching environments, as it can be adapted to most programming languages and has minor technical requirements.

Joint work with Matija Lokar

An Introduction to Algebraic Effects and Handlers

MFPS XXXI, 22 Jun 2015, Nijmegen