CODEWITHSUNDEEP
scalafunctional-programmingcategory-theorycomonad
user1888498
user1888498

Reputation:

Scala comonads; Comonad laws?

So given this encoding of a comonad (see below) are the comonad laws above it correct? for some reason I don't think they are from looking at them, and I know that heading off wrong from there will yield only bad road, so I'd appreciate the nudge, hint, help, answer what have you.

      /**
       * note: I think these are right
       * Comonad Laws
       * 
       * (i)   counit(cojoin(m))      == m
       * 
       * (ii)  >>(counit(m))(cojoin)  == m
       * 
       * (iii) cojoin(cojoin(m))      == >>(cojoin(m))(cojoin)
       * 
       */

        trait Comonad[M[_]] {

           // map
           def >>[A,B](a: M[A])(f: A => B): B

          // extract | coeta 
          def counit[A](a:M[A]): A

          // cobind | =<< | extend
          def coflatMap[A,B](ma:M[A])(f: M[A] => B): M[B]

          // coflatten | comu
         def cojoin[A](a: M[A]): M[M[A]]
        }

Upvotes: 4

Views: 351

Answers (1)

dorchard
dorchard

Reputation: 1188

You are almost there. Both, (i) and (iii) are correct, but (ii) is wrong. You can spot the mistake because (ii) is not well typed: for >>(counit(m) the argument counit(m) has type A rather than M[A].

The correct laws for your operations are:

   * (i)   counit(cojoin(m))      == m
   * 
   * (ii)  >>(cojoin(m))(counit)  == m
   * 
   * (iii) cojoin(cojoin(m))      == >>(cojoin(m))(cojoin)

Thus, for both (i) and (ii), the law is that applying either counit or the "map" of counit to the result of a cojoin is equivalent to the identity function.

Upvotes: 4

Related Questions