Algebraic effects and handlers are a new paradigm in functional programming. They aim at modularly handling side effects, by separating the declaration of those effects, from how they are handled. In this paper, we show how we can leverage their use to create an interface for concurrency using algebraic effects for which we can prove a list of concurrency laws, and also design handlers that allow us to run programs concurrently, thereby demonstrating the practical application of algebraic effects and handlers in managing concurrency.

When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.
This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into one.
This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda.

The first contribution replicates and extends Harper's (Co)Church encodings in Haskell, uncovering optimizer weaknesses and providing practical insights for achieving fusion within Haskell.
The second contribution formalizes these encodings in Agda, leveraging parametricity and the category theory described by Harper.
The formalization proves the equivalence of these encoded functions to the unencoded ones, showing that the encodings are in fact isomorphisms, as long as parametricity (Wadler, 1989) is assumed.

These findings highlight the effectiveness and correctness of shortcut fusion techniques and show the promise of shortcut fusion: Reduce the computational overhead associated with functional programming while retaining its nice, compositional properties.

When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.
This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into one.
This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda.

The first contribution replicates and extends Harper's (Co)Church encodings in Haskell, uncovering optimizer weaknesses and providing practical insights for achieving fusion within Haskell.
The second contribution formalizes these encodings in Agda, leveraging parametricity and the category theory described by Harper.
The formalization proves the equivalence of these encoded functions to the unencoded ones, showing that the encodings are in fact isomorphisms, as long as parametricity (Wadler, 1989) is assumed.

These findings highlight the effectiveness and correctness of shortcut fusion techniques and show the promise of shortcut fusion: Reduce the computational overhead associated with functional programming while retaining its nice, compositional properties.

Addressing the challenge of reasoning about programs across different evaluation strategies has long been a concern in functional programming. Levy's introduction of the call-by-push-value (CBPV) calculus represents a significant step forward in tackling this. His paradigm provided a more powerful approach that can encapsulate both call-by-value and call-by-name that was even later extended to include call-by-need. In this paper we present the development of an interface that integrates the theory of CBPV with algebraic effects and handlers. We demonstrate how this technique enables the definition and execution of programs, highlighting its capability to defer computations across different evaluation strategies and define operations in a modular fashion. We then define and prove a set of laws that can be used with our interface to reason about programs under varying evaluation regimes. This approach not only enhances the flexibility and modularity of language and library implementation but also allows for direct reasoning about these implementations, beyond the meta-level abstraction.

Algebraic effects and handlers has been a popular approach for modelling side-effects in functional programming languages. Focusing on composability and modularity, this approach separates the effectful syntax from its semantics, which helps programmers to create effect abstractions such that their implementation can be modified without changing the syntax. However, there exist mainstream functional programming languages, like Haskell, which lack built-in frameworks to accommodate specifying side-effects in this manner. In this paper, we provide an interface for Haskell's Software Transactional Memory (STM), a concurrency abstraction, in the framework of algebraic effects and handlers from prior literature. We embed our implementation into a simple concurrency model using higher-order effects, in order to demonstrate it is possible to define and execute effectful concurrent programs that obey the semantics of Haskell's STM. Furthermore, we prove that our implementation satisfies the necessary laws governing our interface, such that programmers can easily reason about programs using our STM model.

Errors from side-effecting operations, such as mutable state, error handling, and I/O operations, can be costly during software development. Haskell's monadic approach often obscures specific operations, limiting the ability to reason about them effectively. This paper explores implementing ML-style references in Haskell using algebraic effects separating the syntax and semantics of side-effecting operations.

ML-style references are mutable storage locations, similar to pointers that ensure type safety and allow imperative programming within a functional language. We address how to implement ML-style references in Haskell using algebraic effects while adhering to Staton's state laws. Our contributions include developing an algebraic effect for mutable references, creating a corresponding handler, and proving adherence to Staton’s state laws.

Additionally, we demonstrate the practical application of these principles by proving the correctness of an imperative-style factorial function. This work provides a flexible and predictable framework for using mutable references in Haskell, enhancing the ability to reason about program behaviour and correctness.

Errors from side-effecting operations, such as mutable state, error handling, and I/O operations, can be costly during software development. Haskell's monadic approach often obscures specific operations, limiting the ability to reason about them effectively. This paper explores implementing ML-style references in Haskell using algebraic effects separating the syntax and semantics of side-effecting operations.

ML-style references are mutable storage locations, similar to pointers that ensure type safety and allow imperative programming within a functional language. We address how to implement ML-style references in Haskell using algebraic effects while adhering to Staton's state laws. Our contributions include developing an algebraic effect for mutable references, creating a corresponding handler, and proving adherence to Staton’s state laws.

Additionally, we demonstrate the practical application of these principles by proving the correctness of an imperative-style factorial function. This work provides a flexible and predictable framework for using mutable references in Haskell, enhancing the ability to reason about program behaviour and correctness.

Algebraic effects and handlers are a new programming technique that allows for the definition of abstractions as interfaces, with handlers providing modular, concrete implementations of these interfaces. In this paper, we consider algebraic effects and handlers implemented in Haskell, and explore how they behave under fixed-point (value) recursion. We give different possible implementations of fixed-point combinators for effectful functions, and work out their evaluation processes. We find that these functions behave very predictably under normal fixed-point recursion, while value recursion seems to be a much harder problem. We discuss the difficulties of implementing value recursion, and several possibile solutions are explored, but the question of whether a fixed-point combinator with value recursion semantics can exist at all in the presence of algebraic effects remains unanswered.

Algebraic effects and handlers are a new programming technique that allows for the definition of abstractions as interfaces, with handlers providing modular, concrete implementations of these interfaces. In this paper, we consider algebraic effects and handlers implemented in Haskell, and explore how they behave under fixed-point (value) recursion. We give different possible implementations of fixed-point combinators for effectful functions, and work out their evaluation processes. We find that these functions behave very predictably under normal fixed-point recursion, while value recursion seems to be a much harder problem. We discuss the difficulties of implementing value recursion, and several possibile solutions are explored, but the question of whether a fixed-point combinator with value recursion semantics can exist at all in the presence of algebraic effects remains unanswered.

Algebraic effects and handlers are a new programming technique that allows for the definition of abstractions as interfaces, with handlers providing modular, concrete implementations of these interfaces. In this paper, we consider algebraic effects and handlers implemented in Haskell, and explore how they behave under fixed-point (value) recursion. We give different possible implementations of fixed-point combinators for effectful functions, and work out their evaluation processes. We find that these functions behave very predictably under normal fixed-point recursion, while value recursion seems to be a much harder problem. We discuss the difficulties of implementing value recursion, and several possibile solutions are explored, but the question of whether a fixed-point combinator with value recursion semantics can exist at all in the presence of algebraic effects remains unanswered.

For algebraic effects and handlers, we know both small-step and big-step operational semantics and we are familiar with denotational semantics. But, what is missing is a structured showing that one is equivalent to the other. On top of this, most efficient implementations of algebraic effects and handlers closely resemble their denotational semantics by encoding operations in what is called the free monad. In this work, we often refer to these implementations as freer monad-based embeddings of effects and handlers. These embeddings enable programmers to write effectful programs as though they are monadic programs. However, the derivation of such an embedding from an operational semantics remains thusfar unexplored. This work fills in the gap between a denotational interpreter derived by inverse closure conversion and the freer monad-based embedding of effects and handlers. We thus define and show program transformations that extend the steps needed to transform a denotational interpreter to a small-step interpreter and vice versa.

Effect handler orient programming (EHOP) is a recently proposed programming paradigm that aims to provide a high-level abstraction in code. Using this paradigm, programmers are able to define operations as an effect, which are implemented by an effect handler. Functions can then use effects, allowing the effect operations to be used in this function. Depending on the effect handler that handles the effect, an effect can have different functionality. In this research, EHOP is compared to the traditional functional programming paradigm on readability, maintainability, modularity and performance for IO intensive applications. The comparison is carried out by two programming experiments that each apply one of the programming paradigms to create an HTTP server. The comparison of these programs show that EHOP improves the readability, maintainability and modularity but decreases the performance in response time and memory. The conclusion of this case study is therefore that EHOP affects IO intensive applications in a negative manner due to its performance overhead.

Effect handler oriented programming or EHOP for short, is a new programming paradigm aiming to achieve separation of concerns in code which will lead to modular, readable and maintainable code. Since EHOP is significantly new, it is important to assess and compare it against traditional, commonly used paradigms in order to see if a wider adoption of EHOP would prove beneficial to computer science. In this research, EHOP was compared with traditional paradigms under the context of data processing applications. An Excel-like command line application called “MiniExcel” was implemented from scratch. Moreover, “Hierarchical EHOP”, a new structural pattern for EHOP was defined which enforces rules between concepts and produces a readable code structure. The main conclusions of this research can be summarized by the following statements. EHOP produces more modular, readable and maintainable code compared to traditional paradigms. Implementing additional concepts and updates to code is seamless using EHOP, yet the lack of development in EHOP’s ecosystem raises frustrating errors and requires the developer to implement libraries that are usually built-in for languages that support traditional paradigms. Functional programming produces faster running code, but EHOP is more memory efficient. Therefore, for applications that interact with users EHOP is the better choice and for applications that only execute code functional programming is more suitable.

Effect handler oriented programming (EHOP) is a recently proposed programming paradigm, which aims to provide a separation of concerns by isolating the handling of side-effects from the main application logic. Nowadays, as the core concepts behind EHOP are being added to more and more programming languages, it is evident that EHOP is slowly but steadily growing in popularity. Therefore, it is important to explore the applicability of EHOP for different areas of software development. However, so far, very little research has been conducted on this topic and, thus, barely any possible application domains of EHOP have been investigated. This study focuses on a potential field of application of EHOP, which has not been covered by previous research, namely - text-based game development, and aims to determine the extent to which the usage of EHOP for text-based game development affects the modularity, readability and maintainability of the source code. This goal will be achieved by performing both a qualitative as well as a quantitative analysis of the source code of a text-based game, written in Koka - a state-of-the-art programming language, which supports EHOP. The results show that there are substantial benefits to using EHOP for text-based game development. It significantly improves the modularity, readability and maintainability of the source code at the cost of very little to no performance.