Last active
August 20, 2023 18:42
-
-
Save p-pavel/2fe96137dd8e8cf990098acd20873752 to your computer and use it in GitHub Desktop.
parametricity does not imply naturality in scala — beware implied equality
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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(龽,) | |
*/ |
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.