Is my Applicative for real?

The laws of Applicative

Posted by Niklas Leopold on August 14, 2020 · 29 mins read

About the post

In a previous post we created our own Validator Applicative, but is it for real? I.e. does it follow the rules of an Applicative. Let’s find out.

We will also attempt to create an Applicative that fails to conform to the rules and find out the implications of that.

What is an Applicative?

If you are uncertain, please read this post first.

Using the laws formulated by Scalaz to verify our Applicative

In a previous post we created our own Validator type, here you can also find examples of how the data type is used.

sealed trait Validator[+E, +T]

object Validator {
  type Validated[T] = Validator[String, T]
}

case class Valid[+T](t: T) extends Validator[Nothing, T]

case class Invalid[+E](es: Vector[E]) extends Validator[E, Nothing]

object Invalid {
  def apply[E](e: E): Invalid[E] = Invalid(Vector(e))
}

And we also defined it as an Applicative:

implicit val validationApplicative: Applicative[Validated] = new Applicative[Validated] {
    override def point[A](a: => A): Validated[A] = Valid(a)

    override def ap[A, B](fa: => Validated[A])(f: => Validated[A => B]): Validated[B] = (fa, f) match {
      case (Valid(a), Valid(fab)) => Valid(fab(a))
      case (Valid(a), Invalid(es)) => Invalid(es)
      case (Invalid(es), Valid(a)) => Invalid(es)
      case (Invalid(es1), Invalid(es2)) => Invalid(es1 ++ es2)
    }
}

What I failed to mention on that occasion is that it not enough to implement an instance of Applicative for you data type, it must also follow the laws of an Applicative.

For our convenience the people behind Scalaz has already written the laws in code for us and we will later use this in our tests:

trait ApplicativeLaw extends ApplyLaw {
    /** `point(identity)` is a no-op. */
    def identityAp[A](fa: F[A])(implicit FA: Equal[F[A]]): Boolean =
      FA.equal(ap(fa)(point((a: A) => a)), fa)

    /** `point` distributes over function applications. */
    def homomorphism[A, B](ab: A => B, a: A)(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(ap(point(a))(point(ab)), point(ab(a)))

    /** `point` is a left and right identity, F-wise. */
    def interchange[A, B](f: F[A => B], a: A)(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(ap(point(a))(f), ap(f)(point((f: A => B) => f(a))))
      
    // This law is inherited from "ApplyLaw" in Scalaz but I added it here with the other Laws  
    def composition[A, B, C](fbc: F[B => C], fab: F[A => B], fa: F[A])(implicit FC: Equal[F[C]]): Boolean =
          FC.equal(ap(ap(fa)(fab))(fbc),
                   ap(fa)(ap(fab)(map(fbc)((bc: B => C) => (ab: A => B) => bc compose ab))))    

    /** `map` is like the one derived from `point` and `ap`. */
    def mapLikeDerived[A, B](f: A => B, fa: F[A])(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(map(fa)(f), ap(fa)(point(f)))
}
  
def applicativeLaw: ApplicativeLaw = new ApplicativeLaw {}

Let’s walk through the laws one by one.

Identity

We start from the top with the identity law:

def identityAp[A](fa: F[A])(implicit FA: Equal[F[A]]): Boolean =
    FA.equal(ap(fa)(point((a: A) => a)), fa)

This law simply states that if we lift the identity function ((a: A) => a) and then applies it to the Applicative then the Applicative should be the same as before.

Can we test it? Of course we can!

private val applicative = Applicative[Validated]
private val laws = applicative.applicativeLaw

private def validatedGen[A](implicit a: Arbitrary[A]): Gen[Validated[A]] = for {
    isValid <- Arbitrary.arbitrary[Boolean]
    errors <- Gen.listOf[String](Arbitrary.arbitrary[String])
    a <- Arbitrary.arbitrary[A]
} yield (if (isValid) Valid(a) else Invalid(errors.toVector))

implicit def validatedArbitrary[A](implicit a: Arbitrary[A]): Arbitrary[Validated[A]] =
    Arbitrary(validatedGen)

property("identityAp Law") = forAll { fa: Validated[Int] =>
    laws.identityAp(fa)
}

In the code above we run the law specified by Scalaz on instances of our data type that was generated by ScalaCheck.

We can be reasonable sure that we follow the rule after the test above has passed, but let’s prove that we follow the rule as well:

There are two cases here, one is that the generated Validated[A] is valid:

def identityAp[A](fa: F[A])(implicit FA: Equal[F[A]]): Boolean =
    FA.equal(ap(fa)(point((a: A) => a)), fa)

// can be substituted to
FA.equal(ap(Valid(a))(Valid((a: A) => a)), Valid(a))

// can be simplified to
FA.equal(Valid(((a: A) => a)(a)), Valid(a))

// can be simplified to
FA.equal(Valid(a), Valid(a))

And then we have the case when Validated[A] is invalid:

def identityAp[A](fa: F[A])(implicit FA: Equal[F[A]]): Boolean =
    FA.equal(ap(fa)(point((a: A) => a)), fa)

// can be substituted to
FA.equal(ap(Invalid(m))(Valid((a: A) => a)), Invalid(m))

// can be simplified to
FA.equal(Invalid(m), Invalid(m))

Homomorphism

Let’s move on to the second law.

def homomorphism[A, B](ab: A => B, a: A)(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(ap(point(a))(point(ab)), point(ab(a)))

This law states that is should not matter if you:

  • lift a value and a function into the context of an Applicative and then applies the function to the value
  • or if you first a apply a function on a value and then lift’s the result of the invocation into the Applicative

I.e. it should not matter if you apply the function to the value inside or outside the context of an Applicative, the end result should be the same.

We can use ScalaCheck to test just as before:

property("homomorphism Law") = forAll { (aTob: String => Int, a: String) =>
    laws.homomorphism(aTob, a)
}

Can we prove it? Let’s try!

def homomorphism[A, B](ab: A => B, a: A)(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(ap(point(a))(point(ab)), point(ab(a)))
      
// can be substituted to      
FB.equal(ap(Valid(a))(Valid(ab)), Valid(ab(a)))

// can be simplified to  
FB.equal(Valid(ab(a)), Valid(ab(a)))

// can be simplified to  
FB.equal(Valid(b), Valid(b))

Interchange

And now the third law.

def interchange[A, B](f: F[A => B], a: A)(implicit FB: Equal[F[B]]): Boolean =
      FB.equal(ap(point(a))(f), ap(f)(point((f: A => B) => f(a))))

This law establishes that point is a left and right identity ref1.

And here’s a test for that:

property("interchange Law") = forAll { (a: String, faTob: Validated[String => Int]) =>
    laws.interchange(faTob, a)
}

And here’s the proof that we are following the Law. First we substitute with Valid

FB.equal(ap(point(a))(f), ap(f)(point((f: A => B) => f(a))))

// can be substituted to 
FB.equal(ap(Valid(a))(Valid(a: A => B)), ap(Valid(a: A => B))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(Valid((a: A => B)(a)), ap(Valid(a: A => B))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(Valid(b), ap(Valid(a: A => B))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(Valid(b), Valid(((f: A => B) => f(a))(a: A => B)))

// can be simplified to 
FB.equal(Valid(b), Valid((a: A => B)(a)))

// can be simplified to 
FB.equal(Valid(b), Valid(b))

And now we substitute with Invalid:

FB.equal(ap(Valid(a))(Invalid(m)), ap(Invalid(m))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(ap(Valid(a))(Invalid(m)), ap(Invalid(m))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(Invalid(m), ap(Invalid(m))(Valid((f: A => B) => f(a))))

// can be simplified to 
FB.equal(Invalid(m), Invalid(m))

MapLikeDerived

And now the fourth law:

def mapLikeDerived[A, B](f: A => B, fa: F[A])(implicit FB: Equal[F[B]]): Boolean =
    FB.equal(map(fa)(f), ap(fa)(point(f)))

Here we are proving that the Applicative supports the map operator.

The test:

property("mapLikeDerived Law") = forAll { (fa: Validated[String], aTob: String => Int) =>
    laws.mapLikeDerived(aTob, fa)
}

And the proof:

FB.equal(map(fa)(f), ap(fa)(point(f)))

// can be simplified to 
FB.equal(ap(fa)(point(f)), ap(fa)(point(f)))

Composition

In Scalaz the composition Law is defined for Apply which Applicative extends. However when reading about the Applicative in Haskell literature it is defined on Applicative. I guess Scalaz and Haskell has diverged a bit here.

def composition[A, B, C](fbc: F[B => C], fab: F[A => B], fa: F[A])(implicit FC: Equal[F[C]]): Boolean =
      FC.equal(
        ap(ap(fa)(fab))(fbc),
        ap(fa)(ap(fab)(map(fbc)((bc: B => C) => (ab: A => B) => bc compose ab)))
      )

This looks a bit intimidating but at least it’s easy to test:

property("composition Law") = forAll { (fbc: Validated[Int => String], fab: Validated[String => Int], fa: Validated[String]) =>
    laws.composition(fbc, fab, fa)
}

And here is a proof for our own Applicative if we substitute with Valid.

Bored!

Well actually, I think I leave it as an excercise for the reader since, well, I’m starting to get bored.

But why should we follow the rules?

Ok, so now we have proved that our Applicative follows the rules, but why should it? What are we loosing if we relax the rules?

So we are going to break the Laws and investigate the implications of that.

Alt Text

The data type we are using I have shamelessly stolen (or should I say borrowed?) from Learn You a Haskell for Great Good!, hopefully Miran doesn’t mind?

Fingers crossed!

The data type looks like this:

sealed trait CMaybe[+T]

object CMaybe {
  type MyMaybe[T] = CMaybe[T]
}

object CNothing extends CMaybe[Nothing]

case class CJust[+T](counter: Int, v: T) extends CMaybe[T]

The C here stands for counter. It’s a data type that looks much like Maybe a, only the Just part holds two fields instead of one. The first field in the CJust value constructor will always have a type of Int, and it will be some sort of counter and the second field is of type a, which comes from the type parameter and its type will, of course, depend on the concrete type that we choose for CMaybe a.

Our Applicative instance for the data type look like this:

implicit val cmaybeApplicative: Applicative[CMaybe] = new Applicative[CMaybe] {
    override def point[A](a: => A): CMaybe[A] = CJust(0, a)

    override def ap[A, B](fa: => CMaybe[A])(fab: => CMaybe[A => B]): CMaybe[B] = (fa, fab) match {
      case (CJust(i1, a), CJust(i2, fa)) => CJust((i1 max i2) + 1, fa(a))
      case (_, _) => CNothing
    }
}

We are running the same tests as before but for the new “Applicative”, now some of them fails!

NaughtyApplicative.identityAp Law: Falsified after 0 passed tests.
CJust(1,-104954648) ; CJust(0,-104954648)


NaughtyApplicative.homomorphism Law: Falsified after 0 passed tests.
CJust(1,1601982296) ; CJust(0,1601982296)


NaughtyApplicative.composition Law: Falsified after 6 passed tests.
CJust(2,ַ傆蹳䥐㟻硃⎆⟐) ; CJust(3,ַ傆蹳䥐㟻硃⎆⟐)

It’s easy to see that the offender in this case is the counter, and the reason that we fail the Laws is that we do things in the context that affects our data type. That’s exactly the thing that the Laws are supposed help us to prevent!

The fact that the end result differs depending on if a computation is done inside or outside the context will most likely lead to strange bugs!

When writing this section I tried to come up with a better example then the one above since it feels a little bit “artificial” but I discovered that it’s kind of hard (at least for me) to come up with a good example. The Scala type system does great work to prevent wrongdoings in this case. The fact that Scalaz makes you implement the Applicative as a type class makes it really obvious that you are doing something you shouldn’t if you start to manipulate the data type that it “contains”. I found it much easier to follow the rules then to break them, but that could be due to lack of imagination on my part.

Conclusion

I this post we have investigated the Laws for an Applicative. We found out that Scalaz provides us with test cases that we can use when testing our Applicative.

Provided that we are using immutable data types without side effects is’s also possible to prove that we are following the Laws.

We also tried to break the Laws but found it hard to do since that Scala type system and the Scalaz type class makes it obvious how things should be done in a safe way.

We stole (sorry, I mean borrowed) an example of a data type that doesn’t follow the rules and concluded that the result of some computations differed if they are executed inside or outside the context, it is not difficult to imagine that could lead to confusion and bugs.

Github

The code examples are available at github.

← Previous Post Next Post →