Extending Equational Monadic Reasoning with Monad Transformers

TL;DR

This paper extends the Monae Coq library to support monad transformers, enabling modular and formal equational reasoning about monadic programs, and revisits lifting theorems with improved proofs.

Contribution

It introduces a formalization of monad transformers within Monae, enhancing reasoning capabilities and addressing previous proof limitations.

Findings

Simplified formalization of models in Monae

Supported reasoning with monad transformers

Provided corrected proofs for lifting theorems

Abstract

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.