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.

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.