Opt-in Protocol Types for Effect Systems in Haskell

Abstract

Algebraic effect systems are a promising alternative to existing monad transformer approaches providing fine-grained tracking of side effects in the type signature of procedures. Even though existing algebraic effect systems allow describing a contract for tracking side effects, there is no way to capture more complex pre- and postconditions that can be verified by the compiler rather than the programmer. To address this shortcoming, we introduce preff, the first algebraic effect system library in Haskell that combines traditional algebraic effects and parameterised algebraic effects which enforce pre- and postconditions in the effectful code at compile-time. This allows developers to define and use algebraic effects, while also opting into parameterised effects to great effect. To demonstrate the expressiveness and real-world applicability, we use preff to implement session types in less than 120 lines of code and compare the run-time performance to state-of-the-art effect system libraries in a series of microbenchmarks. Our evaluation shows that preff is capable of expressing complex control-flow patterns comparable to related session type libraries and has competitive run-time performance showcasing its applicability in practice.

Algebraische Effektsysteme sind eine vielversprechende Alternative zu Monadentransformatoren, indem Effektsysteme die Seiteneffekte von Prozeduren in der Typensignatur feingranular dokumentieren. Obwohl existierende algebraische Effektsysteme es erlauben Seiteneffekte detailliert mitzuverfolgen, gibt es derzeit keine Möglichkeit, komplexe Vor- und Nachbedingungen automatisiert vom Übersetzer verifizieren zu lassen. Dieses Problem addressieren wir in dieser Arbeit und stellen preff vor, das erste in Haskell geschriebene algebraische Effektsystem, welches traditionelle algebraische Effekte mit parameterisierten, algebraischen Effektsystemen vereint. Parameterisierte algebraische Effektsysteme erlauben es zur Übersetzungszeit komplexe Vor- und Nachbedingungen im Ausführungskontext des Effekts zu verifizieren. Diese Kombination ermöglicht es, algebraische Effekte zu definieren und zu benutzen, aber auch die Mächtigkeit von parameterisierten Effekten zu nutzen, wenn es vorteilhaft ist. Um die Ausdrucksstärke und Anwendbarkeit von preff zu demonstrieren, implementieren wir Sitzungstypen in weniger als 120 Zeilen Quellcode und vergleichen in einer Reihe von Mikroexperimenten die Laufzeit mit fortgeschrittenen Effektsystemen in Haskell. Unsere Evaluation zeigt, dass preff ausgezeichnet geeignet ist, um komplexe Programmkontrollflüsse zu implementieren und die Laufzeit in der Praxis kompetitiv zu der aktueller Effektsysteme ist.