发表机构
Università del Piemonte Orientale; Università di Genova（皮埃蒙特东方大学; 热那亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文用 Haskell 实现了单子框架，包含小步解释器和类型-效应检查器，通过分离语法与效应语义，并利用模块化编程验证其可实现性，以异常和非确定性单子示例展示。
AI 中文摘要
我们展示了在 Haskell 中对一个单子框架的具体实现，该框架包含一个小步解释器以及对应语言的类型-效应检查器。我们的方法将语言语法与其效应的语义分离。这种设计使得解释器能够保持对底层单子的参数化，而静态检查器则独立于效应的具体实现来近似效应。该框架的理论基础——应用于带有泛型效应的按值调用 lambda 演算，其中泛型效应由产生单子值并通过处理器管理的操作表示——已在先前的工作中引入，当时重点是证明该方法的可靠性。相比之下，本工作利用 Haskell 对模块化编程和单子的支持，以证明该框架在实践中是可实现和可用的。我们通过使用异常单子和非确定性单子以及带和不带处理器的表达式示例来说明该方法。
英文摘要
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.
