Computer Scientist Degree - Thesis Work
Coq
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

# Monads in functional programming: a formalized proof of their equivalence with Kleisli triples

“Being a language, mathematics may be used not only to inform but also, among other things, to seduce.”
─Benoît Mandelbrot

“There is no branch of mathematics, however abstract, which may not some day be applied to phenomena of the real world.”
─Nikolai Ivanovich Lobachevsky

“Category theory is a relatively young branch of pure mathematics that most computer scientists would consider esoteric”
─Benjamin C. Pierce

This repository contains my work for obtain my computer scientist degree. My thesis is here.

My work consisted in to formalize basic concepts of Category Theory in Coq, and realize a formal verification of a proof of equivalence between monads and Kleisli triples.

## A few history

The notion of monad was invented by Roger Godement in 1958 under the name "standard construction." In the 1960s and 1970s, many people used the name "triple." The now standard term "monad" is due to Saunders Mac Lane. (See Monad)

The more common definition for a monad in functional programming is actually based on a Kleisli triple rather than category-theory's standard definition. The two constructs turn out to be mathematically equivalent. (See Kleisli Triple)

In 1991, Moggi give us a small and informal proof of the mathematical equivalence between monads and Kleisli triples. (See Moggi, E. (1991). Notions of computation and monads). In 2007, Gammon shows a detailed and extended formal proof of the mathematical equivalence between monads and Kleisli triples. (See Gammon, S. C. (2007). Notions of category theory in functional programming (Doctoral dissertation, University of British Columbia).) Finally, in 2016, I formalized Gammon's proof in the proof assistant Coq.

## Coq

I used CoqIde 8.6 to run my script.

I use type classes to define category theory concepts (see A Gentle Introduction to Type Classes and Relations in Coq) and inspiration given from Matthieu Sozeau's work.

My script contains:

``````* Category definition
* Category examples
* Functor definition
* Identity functor definition
* Functors composition definition
* Natural Transformation definition