-
-
Save p-pavel/2fe96137dd8e8cf990098acd20873752 to your computer and use it in GitHub Desktop.
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(龽,) | |
*/ |
You are using the operator
!=
which explicitly breaks the assumptions behind the parametricity theorem. This operator does not work with all types in the same way, in other words, it is not a fully parametric operation.
Please note lines 26 and 27 :)
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).
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 thegist
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.
You are using the operator
!=
which explicitly breaks the assumptions behind the parametricity theorem. This operator does not work with all types in the same way, in other words, it is not a fully parametric operation.