parametricity does not imply naturality in scala — beware implied equality

parametricityNotNaturality.scala

package com.perikov

import cats.*
import cats.implicits.*
import cats.laws.*
import org.scalacheck.Arbitrary
import org.scalacheck.Prop.forAll
import cats.laws.*
import cats.laws.discipline.*

trait NatLaws[F[_], G[_]](using F: Functor[F], G: Functor[G]):
  def natural[A, B](ff: F ~> G)(f: A => B, fa: F[A]): IsEq[G[B]] =
    ff(fa).map(f) <-> ff(fa.map(f))

object NatLaws:
  def apply[F[_], G[_]](using F: Functor[F], G: Functor[G]): NatLaws[F, G] =
    new NatLaws[F, G] {}

case class Dup[A](a: A, b: A)

given Functor[Dup] with
  def map[A, B](fa: Dup[A])(f: A => B): Dup[B] = Dup(f(fa.a), f(fa.b))

def nat: Dup ~> Option = new (Dup ~> Option):
  def apply[A](fa: Dup[A]): Option[A] =
    if fa.a != fa.b then Some(fa.a) else None // <- HERE'S A CATCH
    // In fact we should not have an ability to use != or ==. But in Scala all types are setoids

given [A: Eq]: Eq[Dup[A]] with
  def eqv(x: Dup[A], y: Dup[A]): Boolean = x.a === y.a && x.b === y.b

class Nat extends munit.DisciplineSuite:
  override val scalaCheckTestParameters =
    super.scalaCheckTestParameters.withMinSuccessfulTests(1000)

  given [A: Arbitrary]: Arbitrary[Dup[A]] = Arbitrary(
    for
      a <- Arbitrary.arbitrary[A]
      b <- Arbitrary.arbitrary[A]
    yield Dup(a, b)
  )


  property("natural")(
    forAll { (f: String => String, fa: Dup[String]) =>
      {
        NatLaws[Dup, Option].natural(nat)(f, fa)
      }
    }
  )
  
/*  
Failing seed: lTJj2E5eins1QOWgnjGGHvSnggfE-kzIZTI3p1PAaWG=
You can reproduce this failure by adding the following override to your suite:

  override val scalaCheckInitialSeed = "lTJj2E5eins1QOWgnjGGHvSnggfE-kzIZTI3p1PAaWG="

Falsified after 6 passed tests.
> Labels of failing property: 
Expected: None
Received: Some()
> ARG_0: org.scalacheck.GenArities$$Lambda$173/0x00000008001f6f18@10344365
> ARG_1: Dup(龽,)
*/

Of course I saw those lines. But note that the title of this gist says that "parametricity does not imply naturality". This title is misleading, as the gist actually gives an example where a function does not satisfy parametricity (and also fails to satisfy naturality).

frankly I can't remember why this gist was written in the first place, it was some discussion and the correct title probably should be something like "that is why you can't rely on parametricity to imply naturality in Scala" :) it was not intended to be treated as a publication of some result.

I'm very pleased to get your attention on this and I'm looking forward to read your curryhoward library and watching you series on parametricity.

I'll rename the gist to avoid ambiguity.

Thank you.
Please let me know if you have any questions. The parametricity videos are based on the material from my draft book "The Science of Functional Programming" that I'm still hoping to finish some time soon.

Thank you.
Please let me know if you have any questions. The parametricity videos are based on the material from my draft book "The Science of Functional Programming" that I'm still hoping to finish some time soon.

Based on you interests it would be great to get this book published. I think there's a lack of material on this level of functional programming beyond academic publications.