Tag Archives: monads

The Maybe monad in Coq

Posted on 2011/01/25 by Thomas Strathmann

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

Posted on 2011/01/24 by Thomas Strathmann

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

Posted on 2011/01/24 by Thomas Strathmann

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