In the last post, we reviewed Writer comonad in Haskell. In this post we will implement it in Coq. Since monads are not the part of standard Coq library, and we will use ExtLib which provide basic monad definitions.
First, we need to define Writer monad. ExtLib only provides WriterT monad transformer, from which we can trivially create a Writer monad:
Here, we define `writer` type constructor and `runWriter` method. Additionally, we define a couple of convenience methods on top of `runWriter` to extract state and the value from the results of unwrapping the monad.
ExtLib has CoMonad class defined as:
The first thing you notice is that the names are different from the ones we've seen in Haskell. They reflect category theory duality between monads and comonads. Essentially 'coret' is 'extract,' and 'cobind' is 'extend' with slightly different argument order. For now, let us stick to these definitions. We define a Writer comonad as:
The definition is pretty much the same as we wrote in Haskell except for the adjustments for Coq/ExtLib monad syntax.
Since we are in Coq, in addition to defining the comonad we can formalize comonad laws and prove that our implementation complies with them. Unfortunately, `cobind` argument's order make the formulation of comonad rules little clumsy, so we will first define wrappers reverting it to familiar Haskell's name and argument order:
Now we can define CoMonadLaws class which specifies the rules:
Finally, we will prove that our WriterComonad satisfies these rules by instantiating this class and proving the rules. To do this, we need to assume that the proof is provided that underlying monid instance used in our Writer complies to MonoidLaws.
For clarity in the code snippets above, I have omitted some auxiliary code. You can look at the full example at WriterComonad.v.