Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

TL;DR

This paper presents Monae, a Coq-based framework for practical monadic equational reasoning in a dependent-type setting. It develops an extensible hierarchy of effect interfaces using Hierarchy-Builder, enabling modular definitions of functors, monads, and complex combinations such as nondeterminism, probability, and state, along with concrete models and monad transformers. The authors demonstrate the approach through applications to an in-place quicksort derivation and an ML-like typed-store monad for OCaml programs, illustrating how equational reasoning can be mechanized and reused to verify challenging, effectful programs. The work advances the practicality of formal monadic reasoning by separating laws from models, exploiting Coq's rewriting capabilities, and providing reusable libraries of lemmas that align pencil-and-paper proofs with machine-checked proofs. It also highlights how these techniques can inform the design of equational theories for languages with references, offering a path toward formally verified, effectful programming in realistic languages.

Abstract

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq's mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

TL;DR

This paper presents Monae, a Coq-based framework for practical monadic equational reasoning in a dependent-type setting. It develops an extensible hierarchy of effect interfaces using Hierarchy-Builder, enabling modular definitions of functors, monads, and complex combinations such as nondeterminism, probability, and state, along with concrete models and monad transformers. The authors demonstrate the approach through applications to an in-place quicksort derivation and an ML-like typed-store monad for OCaml programs, illustrating how equational reasoning can be mechanized and reused to verify challenging, effectful programs. The work advances the practicality of formal monadic reasoning by separating laws from models, exploiting Coq's rewriting capabilities, and providing reusable libraries of lemmas that align pencil-and-paper proofs with machine-checked proofs. It also highlights how these techniques can inform the design of equational theories for languages with references, offering a path toward formally verified, effectful programming in realistic languages.

Abstract

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq's mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.
Paper Structure (36 sections, 7 equations, 3 figures, 8 tables)

This paper contains 36 sections, 7 equations, 3 figures, 8 tables.

Table of Contents

  1. Introduction
  2. An extensible implementation of interfaces of effects
  3. Hierarchy-Builder in a nutshell
  4. Functors and natural transformations
  5. Formalization of monads
  6. Nondeterminism monad
  7. Assertions in monadic programs
  8. Exception monad
  9. State monad
  10. Array monad
  11. Probability monad
  12. Probability and nondeterminism
  13. Model of monads
  14. Monad transformers
  15. Example: The state monad transformer
  16. ...and 21 more sections

Figures (3)

  • Figure 1: Comparison between a paper proof and a proof using Monae
  • Figure 2: Hierarchy of effects for the nondeterminism monad
  • Figure 3: Hierarchy of effects for the plus monad