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.16-8.17
• 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
  • Extending Equational Monadic Reasoning with Monad Transformers doi:10.4230/LIPIcs.TYPES.2020.2
  • A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism doi:10.1017/S0956796821000137
  • Towards a practical library for monadic equational reasoning in Coq doi:10.1007/978-3-031-16912-0_6
  • Environment-friendly monadic equational reasoning for OCaml

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. This includes for example 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

• basics:
  • monae_lib.v: simple additions to base libraries
  • hierarchy.v: hierarchy of monadic effects
  • category.v: formalization of concrete categories (generalization of the bottom layers of hierarchy.v)
  • 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
• utility lemmas:
  • monad_lib.v: basic lemmas about monads
  • fail_lib.v: lemmas about the 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: lemmas about the probability monad
  • typed_store_lib.v: derived definitions and lemmas about about the typed store monad
• models of monads:
  • monad_model.v: concrete models of monads
  • proba_monad_model.v: 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
  • typed_store_model.v: alternative model of the typed store monad
• applications:
  • monad_composition.v: composing monads
  • smallstep.v: semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
  • example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling, Monty Hall problem, monad transformers, quicksort, OCaml programs, etc.)

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