Monadic effects and equational reasoning in Coq

This Coq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.

Meta

• Author(s):
  • Reynald Affeldt (initial)
  • David Nowak (initial)
  • Takafumi Saikawa (initial)
  • Jacques Garrigue
  • Ayumu Saito
  • Celestine Sauvage
  • Kazunari Tanaka
• License: LGPL-2.1-or-later
• Compatible Coq versions: Coq 8.15
• Additional dependencies:
  • MathComp ssreflect
  • MathComp fingroup
  • MathComp algebra
  • MathComp solvable
  • MathComp field
  • MathComp analysis
  • Infotheo
  • Paramcoq
  • Hierarchy Builder
  • Coq-Equations
• Coq namespace: monae
• Related publication(s):
  • A hierarchy of monadic effects for program verification using equational reasoning doi:10.1007/978-3-030-33636-3_9
  • A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism doi:10.1017/S0956796821000137
  • Extending Equational Monadic Reasoning with Monad Transformers doi:10.4230/LIPIcs.TYPES.2020.2
  • Towards a practical library for monadic equational reasoning in Coq doi:10.1007/978-3-031-16912-0_6

Building and installation instructions

The easiest way to install the latest released version of Monadic effects and equational reasoning in Coq is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-monae

It installs two directories in coq/user-contrib: monae and monaeImpredicativeSet.

To instead build and install manually (with GNU make), do:

git clone https://github.com/affeldt-aist/monae.git
cd monae
make -j 4
make install

Overview

This repository contains a formalization of monads including examples of monadic equational reasoning and several models (in particular, a model for a monad that mixes non-deterministic choice and probabilistic choice). This corresponds to the formalization of the following papers:

• [Gibbons and Hinze, Just do It: Simple Monadic Equational Reasoning, ICFP 2011] (except Sect. 10.2)
• [Gibbons, Unifying Theories of Programming with Monads, UTP 2012] (up to Sect. 7.2)
• [Mu, Equational Reasoning for Non-determinism Monad: A Case study of Spark Aggregation, TR-IIS-19-002, Academia Sinica]
• [Mu, Calculating a Backtracking Algorithm: An exercise in Monadic Program Derivation, TR-IIS-29-003, Academia Sinica]
• [Mu, Functional Pearls: Reasoning and Derivation of Monadic Programs, A case study of non-determinism and state, 2017]
  • This is a draft paper. In the first release, we formalized this draft up to Sect. 5. The contents have been since superseded by [mu2019tr2] and [mu2019tr3].
• [Mu and Chiang, Deriving Monadic Quicksort (Declarative Pearl), 2020]

This library has been applied to other formalizations:

• application to program semantics (see file smallstep.v)
• formalization of monad composition [Jones and Duponcheel, Composing Monads, Yale RR 1993] (Sections 2 and 3)
• formalization of monad transformers [Jaskelioff, Modular Monad Transformers, ESOP 2009] (up to Sect. 4)
  • completed with details from [Jaskelioff, Lifting of Operations in Modular Monadic Semantics, PhD 2009]
  • see directory impredicative_set for the formalization of [Jaskelioff, Modular Monad Transformers, ESOP 2009] (from Sect. 5)
• formalization of the geometrically convex monad (main reference: [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017])

Files

• monae_lib.v: simple additions to base libraries
• hierarchy.v: hierarchy of monadic effects
• monad_lib.v: basic lemmas about monads
• category.v: formalization of categories (generalization of hierarchy.v)
• fail_lib.v: lemmas about fail monad and related monads
• state_lib.v: lemmas about state-related monads
• array_lib.v: lemmas about the array monad
• trace_lib.v: lemmas about about the state-trace monad
• proba_lib.v: about the probability monad
• monad_composition.v: composing monads
• monad_transformer.v: monad transformers
  • completed by ifmt_lifting.v and iparametricty_codensity.v in the directory impredicative_set
    • the directory impredicative_set contains a lighter version of Monae where monads live in Set and that compiles with impredicative-set
• monad_model.v: concrete models of monads
• proba_monad_model.v: concrete model of the probability monad
• gcm_model.v: model of the geometrically convex monad
• altprob_model.v: model of a monad that mixes non-deterministic choice and probabilistic choice
• example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, quicksort, etc.)
• smallstep.v: semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs

About Installation with Windows 10 or 11

Installation of monae on Windows is less simple. First install infotheo following the instructions for Windows 10. Once infotheo is installed (with opam), do:

• opam install coq-monae or git clone [email protected]:affeldt-aist/monae.git; opam install .

Original License

Before version 0.2, monae was distributed under the terms of the GPL-3.0-or-later license