Scala comonads; Laws of the Komonada?

So, given this encoding of the comonad (see below), are the laws of the comonad over it correct? for some reason, I don’t think they are looking at them, and I know that this will not turn out a bad way, so I will be grateful for the push, hint, help, answer that you have.

/** * 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]] } 
+4
source share
1 answer

You are almost there. Both parameters (i) and (iii) are correct, but (ii) is incorrect. You may find a mistake because (ii) not well typed: for >>(counit(m) argument counit(m) is of type A , not M[A] .

The right 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) law is that applying either the counit or the "map" of counit to the result of a cojoin equivalent to an identical function.

+4
source

Source: https://habr.com/ru/post/1487590/


All Articles