There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
翻译:最近有人有兴趣用证据助理来核查monaddic程序。 这一研究线索提出了monad变压器的集成问题,这是将monad变压器结合在一起的一种标准技术。 在本文中,我们扩展了Monae,这是一个用monad变压器进行monadic等式推理的 Coq 图书馆,我们用monad变压器来解释这一扩展的好处。我们的出发点是模块monad变压器的现有理论,它提供了对操作的统一处理。我们利用这一理论,简化了Monae 模型的正规化,我们提出了一个方法,支持monad变压器出现时的monad 等式推理。我们还利用Monae 重新审视模块moad变压器的提法,提供方程式证据,并解释如何使用非标准使用的Coq来修补已知的虫,将不合理的多形态和对称性结合起来。