A type system for dynamic instances

Abstract

Side-effect are ubiquitous in programming. Examples include mutable state, exceptions, non-determinism, and user input. Algebraic effects and handlers are an approach to programming that gives a structured way of programming with effects. Each effect in a system with algebraic effects is defined by a set of operations. These operations can then be called anywhere in a program. Using a handler we can give an interpretation for the operations used. Unfortunately we are unable to express dynamic effects using regular algebraic effects, such as the dynamic creation of mutable references. Extending algebraic effects with effect instances enables us to express dynamic effects. These effect instances can be dynamically created and operations called on them are distinct from the same operation called on a different instance. Without a type system effect instances may result in runtime errors, because operation calls may be left unhandled. Because of their dynamic nature it is hard to give a type system for effect instances. In this thesis we present a new language, Miro, which extends algebraic effects and handlers with a restricted form of effect instances. We introduce the notion of an effect scope which encapsulates the creation and usage of dynamically created effect instances. We give a formal description of the syntax and semantics of Miro. We also give a type system which ensures that all operation calls are handled, so that there will be no runtime errors because of unhandled operation calls. Because effect instances can still escape their effect scope, in computationally irrelevant parts, we encounter difficulties in proving type safety for Miro. We discuss these difficulties and give a possible approach to prove type safety in the future.