/monae

Monadic effects and equational reasonig in Coq

Primary LanguageCoqGNU Lesser General Public License v2.1LGPL-2.1

Monadic equational reasoning in Coq

https://travis-ci.com/affeldt-aist/monae.svg?branch=master

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 roughly 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].

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] up to Sect. 5
  • formalization of the geometrically convex monad (main reference: [Cheung, Distributive Interaction of Algebraic Effects, PhD Thesis, U. Oxford, 2017])

Available monads

hier.png

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
  • 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 impredicate-set
  • monad_model.v: concrete models of monads (up to state and trace 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, etc.)
  • smallstep.v: semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs

Installation

The preferred way to install monae is with opam because it takes care of the dependencies with other libraries. If not already done, add the repository for Coq libraries to opam and update:

  1. opam repo add coq-released https://coq.inria.fr/opam/released
  2. opam update

Last stable version:

Version 0.2:

  1. opam install coq-monae

Requirements

All versions available from opam.

Development version (git master):

With Coq 8.11 or 8.12 and the last stable release of infotheo (the impredicative_set directory (as well as `make sect5`) require ParamCoq).

  1. git clone git@github.com:affeldt-aist/monae.git
  2. cd monae

If opam is installed, do:

  1. opam install .

opam takes care of the dependencies.

If opam is not installed but if the requirements are met, do:

  1. make
  2. make install

About Windows 10

Installation of monae on Windows is less simple. First install infotheo following the instructions for Windows 10. Once infotheo is installed:

  1. If opam is available, do
    • opam install coq-monae or git clone git@github.com:affeldt-aist/monae.git; opam install .
  2. If opam is not available (i.e., installation of MathComp using unzip, untar, cd, make, make install), do:
    • git clone git@github.com:affeldt-aist/monae.git
    • coq_makefile -o Makefile -f _CoqProject
    • make

License

LGPL-2.1-or-later

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

References