Tag Archives: monads

The Maybe monad in Coq

The Maybe monad is pretty useful whenever you’re dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.

Posted in Coq, Haskell | Tagged | 8 Comments

Partiality is an effect

In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading

Posted in Coq | Tagged , , | Leave a comment

Definition of a monad

This rather rendundant post serves as a test case for the WP LaTeX plugin. A monad on a category is given by an endofunctor  and two natural transformations: such that the following two diagrams commute:

Posted in Mathematics | Tagged , | Leave a comment