DP
D. Panis
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
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. ...
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.
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.