Haskell framework separates program effects from language meaning
A monadic interpreter and type-and-effect checker
Programming Languages
Summary
This work shows how to build a small computer program that can both run other programs and check what effects those programs might have, like throwing errors or making choices. The authors use a method that keeps the way programs are written separate from how their side effects work. They wrote this in a language called Haskell and showed their design works with examples involving errors and different possible outcomes. Their earlier work proved this approach is theoretically sound, and now they demonstrate it can be practically implemented.
monadinterpretertype-and-effect checkerHaskellsmall-step semanticslambda calculuscall-by-valuemonadic effectshandlersstatic analysis
Authors
Stefano Raviola, Paola Giannini, Francesco Dagnino
Abstract
We present a concrete implementation in Haskell of a monadic framework that includes both a small-step interpreter and a type-and-effect checker for the corresponding language. Our approach separates the language syntax from the semantics of its effects. This design allows the interpreter to remain parametric over the underlying monad, while the static checker approximates effects independently of their concrete implementation. The theoretical foundation of this framework-applied to a call-by-value lambda calculus with generic effects represented by operations that produce monadic values and are managed through handlers-was introduced in previous work, where the focus was on proving the soundness of the approach. In contrast, the present work leverages Haskell's support for modular programming and monads to demonstrate that the framework is practically implementable and usable. We illustrate the approach with examples using the monad of exceptions and the one of nondeterminism and expressions both with and without handlers.