I show some simple heuristic calculations to explain how monad rules stem from a functor adjunction.

Type logic is the logic directly associated to types. It turns out that one can go quite far with regards to proving statements with Haskell. I show how to do that, and even how to prove statements in classical logic with Haskell.

Another Haskell version of Peter Norvig's spelling corrector, illustrating list monads, type classes and polymorphic programming.

The Reader and Writer monad are well known, but I would like to present their comonadic counterpart.