Filip Koprivec: Optimising subtyping coercions in a polymorphic calculus with effects, part 2

This is the continuation of last week's seminar.

Abstract: Algebraic effects and handlers are a popular way of structuring and reasoning about effectful computations. However, the performance of programs using these constructs is often a concern. Various optimization techniques having been proposed to migitage the problem.

This talk will focus on one such technique, a compilation scheme using type- and effect-system-directed optimizations that aim for efficient compilation directly to OCaml 4, which does not have native support for algebraic effects. The optimization scheme works well in monomorphic settings, but suffers from a blowup of explicit coercions when used in polymorphic scenarios. We will present a simple polymorphic calculus with effects, together with optimization primitives that signigicantly reduce the amount of additional coercions. We also provide an accompanying denotational semantics with respect to which our optimizations are sound.

Joint work with Matija Pretnar.