An Algebraic Effect for ML-Style References in Haskell

Bachelor Thesis (2024)
Author(s)

D. Panis (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Contributor(s)

C.B. Poulsen – Mentor (TU Delft - Programming Languages)

Jaro Reinders – Graduation committee member (TU Delft - Programming Languages)

Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more
Publication Year
2024
Language
English
Graduation Date
23-06-2024
Awarding Institution
Delft University of Technology
Project
['CSE3000 Research Project', 'Programming with Effects and Algebras']
Programme
['Computer Science and Engineering']
Faculty
Electrical Engineering, Mathematics and Computer Science
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

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.

Files

Main.pdf
(pdf | 0.271 Mb)
License info not available