Search code examples
scalafunctorscala-catscategory-theory

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

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.

Solution

  • 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.