Writer comonad in Coq

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:

Variable s t : Type.
Variable Monoid_s : Monoid s.

Definition writer := writerT Monoid_s ident.
Definition runWriter x := 

   unIdent (@runWriterT s Monoid_s ident t x).
Definition execWriter x:= psnd (runWriter x).
Definition evalWriter x:= pfst (runWriter x).

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:

Class CoMonad (m : Type -> Type) : Type :=
{ coret : forall {A}, m A -> A
; cobind : forall {A B}, m A -> (m A -> B) -> m B
}.

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:

Variable w: Type.
Variable m: Monoid w.

Global Instance WriterCoMonad:  CoMonad (@writer w m) := {
  coret A x := evalWriter x ;
  cobind A B wa f := tell (execWriter wa) ;; ret (f wa)
}.

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:

Variable m : Type -> Type.
Variable C : CoMonad m.

Definition extract {A:Type}: (m A) -> A := @coret m C A.
Definition extend {A B:Type} (f: m A -> B): m A -> m B  :=
    fun x => @cobind m C A B x f.

Now we can define CoMonadLaws class which specifies the rules:

Class CoMonadLaws : Type := {
  extend_extract: forall (A B:Type),   extend (B:=A) extract = id ;
  extract_extend: forall (A B:Type) {f},   extract ∘ (@extend A B) f = f;
  extend_extend: forall (A B:Type) {f g}, (@extend B A) f ∘ (@extend A B) g = extend (f ∘ extend g)
}.

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.

Variable ml: MonoidLaws m.

Global Instance WriterCoMonadLaws:
    CoMonadLaws (@WriterCoMonad).
  Proof.
    split.
    -
      intros A B.
      unfold extract, extend.
      extensionality x.
      unfold coret, cobind, WriterCoMonad, id.
      unfold evalWriter, execWriter, runWriter.
      destruct x, runWriterT, unIdent.
      simpl.
      repeat f_equal.
      apply ml.
    -
      reflexivity.
    -
      intros A B f g.
      unfold extract, extend, compose.
      unfold coret, cobind, WriterCoMonad.
      extensionality x.
      repeat f_equal.
      apply ml.
  Qed.

For clarity in the code snippets above, I have omitted some auxiliary code. You can look at the full example at WriterComonad.v.