
Recent Posts
Archives
Categories
January 2020 M T W T F S S « Nov 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 Meta
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.
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 nonterminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading
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: