In Scala cats-laws, why is the functor composition law different from canonical definition?-CodePudding

The (covariant) functor definition in cats-laws looks like this:

  def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
    fa.map(f).map(g) <-> fa.map(f.andThen(g))

But if I translate the functor composition rule to Scala, it should be:

rule

  def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
    fa.map(f).andThen(fa.map(g)) <-> fa.map(f.andThen(g))

Why are they different? Which version is correct?

UPDATE 1 I'm aware of a similar implementation in Haskell, but I haven't had a chance to read it. I wonder if the Haskell version is more by the book.

CodePudding user response：

F(g ∘ f) = F(g) ∘ F(f) is the same as ∀fa, (F(g ∘ f))(fa) = (F(g) ∘ F(f))(fa) (equality of functions is equality of images for all arguments, this is extensionality in HoTT 1 2 3).

The latter is translated as

def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
  fa.map(f).map(g) <-> fa.map(f.andThen(g))

(actually, fa.map(f.andThen(g)) <-> fa.map(f).map(g)).

If you'd like to have "point-free" F(g ∘ f) = F(g) ∘ F(f) you could write _.map(f.andThen(g)) <-> _.map(f).map(g) or _.map(f.andThen(g)) <-> (_.map(f)).andThen(_.map(g)) (this is fmap (g . f) = fmap g . fmap f in Haskell, or more precisely, in some "meta-Haskell").

The 2nd code snippet in your question

def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
  fa.map(f).andThen(fa.map(g)) <-> fa.map(f.andThen(g))

is incorrect. fa.map(f).andThen... doesn't make sense as it was mentioned in comments. You seem to confuse F and F[A].

In category theory, in general categories, f: A -> B can be just arrows, not necessarily functions (e.g. related pairs in a pre-order if a category is this pre-order), so (F(g ∘ f))(fa) can make no sense. But the category of types in Scala (or Haskell) is a category where objects are types and morphisms are functions.

CodePudding user response：

I think your confusion comes from the different way functor map property can be represented.

trait Functor[F[_]] {
 
  def map1[A, B](f: A => B): F[A] => F[B]

  def map2[A, B](f: A => B)(fa: F[A]): F[B]

  def map3[A, B](fa: F[A])(f: A => B): F[B]

}

Here... map1 is the haskell aligned definition... and hence the functor law representation used by haskell also works with this one.

So, this haskell

fmap (g . f) = fmap g . fmap f

translates to following Scala

map1( g.compose(f) ) = map1(g).compose( map1(f) )

// or 
map1( f.andThen(g) ) <-> map1(f).andThen(map1(g))

But, the thing is that we have few more ways to represent the same map property as given by map2 and map3. The overall essens is still the same, we just switched the representation.

Now, when we add the full object oriented angle to it... the "object-oriented" Functor becomes something like following.

trait List[ A] {
  def map(f: A => B): List[B]
}

So... for the "object oriented functor" like List, the same law can be represented as following

listA.map(f).map(g) <-> listA.map(f.andThen(g))

And, you are seeing exactly this.