../laws-law-tests-and-implementing-typeclasses

Laws, Law Tests, and Implementing Typeclasses


Table of contents

> wc -w ~ 2934
Reading time estimate ~ 15 minutes

Introduction

Something I have left purposefully under-specified in my previous posts is that most of those abstractions obey laws.

Those laws are important features of those abstractions — they specify the conditions for validity of an implementation.

In general, we would like to be able to test for any of our implementations that the laws do hold. Doing so would give us confidence in the validity and relaibility of our implementations.

In order to do so, we'll have to implement several typeclasses, and I'll show you how that can be done in detail. In that respect, you can also see this post as a sequel to my post on cats imports and typeclass structure.

Laws

What are laws? Why should we care about them?

Laws are rules that characterize the behavior of the component elements of a typeclass.

For example, the Order typeclass is meant to capture the concept of a total order. As such, it is characterized by one operation lte, short for less than or equal. You might model it like:

trait Order[A] {
  def lte(a: A, b: A): Boolean
}

This operation, in order to properly model a total order, has to obey the following three laws:

// transitivity
a.lte(b) && b.lte(c) -> a.lte(c)

// totality
a.lte(b) || b.lte(a)

// anti-symmetry
a.lte(b) && b.lte(a) <-> a == b

Transitivity says that if a is less than or equal to b, and b is less than or equal to c, then a is less than or equal to c. Clearly, we would want most implementations of a comparison operator to obey that rule!

Meanwhile, totality says that if we have two values, they are always comparable - one must be larger than the other. This essentially says that the function is total, everywhere defined, as a function from the product type (A, A) to Boolean.

Finally, anti-symmetry says that if two values are less than or equal to each other, then they are just equal straight out. There are cases where you wouldn't want this1, but in most cases you do!

For another, slightly more complicated example, let's look at the laws for Functor.

Recall that you can model Functor as:

trait Functor[F[_]] {
  def map[A, B](fa: F[A])(f: A => B): F[B]
}

In other words, a Functor implementation for a type explains how to lift a function into the context of the structured polymorphic type F.

What laws should such an operation obey to be reasonable? I imagine to most readers it is substantially less obvious than those for Order, which you might largely have guessed!

It turns out the appropriate laws are2:

// preserves identity
fa.map(identity) == fa

// preserves composition
fa.map(f.compose(g)) = fa.map(g).map(f)

Reasonable enough right? The Functor can't deform the operation of doing nothing into somehow doing something.

Similarly, the Functor is not allowed to disrespect the operation of function composition - it has to preserve the compositional structure of functions.

All of these are examples of laws attached to a typeclass to determine the behavior of the implementations of the components.

Now that we know what laws are and how they relate to typeclasses, we have to ask ourselves, why should we conform to them? What do we lose if our implementations are not lawful?

Why should we conform to laws?

While I'm sure Rousseau and Hobbes have opinions, that's not quite what I meant.

Fulfilling these laws lets us know that our implementations are sound.

Numerous benefits follow from ensuring that our implementations conform and are sound.

For example, some operations are only correct in all cases if all laws are fulfilled.

Consider taking the max element of a collection using an Order, say something like:

List(
  Some(5),
  None
  Some(6)
).maximumOption

Ideally, this should be order independent. The order of the elements in the List should not change the answer.

If we use the standard Order for Options, which is something like:

implicit def orderForOption[A: Order]: Order[Option[A]] =
  new Order[Option[A]] {
    def lte(a: Option[A], b: Option[B]): Boolean = (a, b) match {
      case (Some(l), Some(r)) => Order[A].lte(l, r)
      case (Some(_), None) => false
      case (None, Some(_)) => true
      case (None, None) => true
    }
  }

Then, it will be the case that there is an order independent maximum and this is because the implementation is lawful. Since the operation is anti-symmetric, the maximum is unique. If x is such that every other element y is y.lte(x) and x.lte(z) for some specific z, then it must be that x == z. In this way we know that the maximum for any set of values for that implementation is unique.

But consider this implementation:

implicit def preorderForOption[A: Order]: Order[Option[A]] =
  Order.by({
    case Some(_) => 1
    case None => 0
  })
}

This implementation fails anti-symmetry. As such, these two lists give different values!

// Returns Some(5)
List(
  Some(5),
  None
  Some(6)
).maximumOption(preorderForOption)

// Returns Some(6)!
List(
  Some(6),
  None
  Some(5)
).maximumOption(preorderForOption)

The reason that anti-symmetry fails is clear from the implementation - we threw away too much information in implementing it. It retains no information about the inner value of Somes. As such, it's not surprising that it can't track the contents of the Option. The failure of anti-symmetry follows from that.

However, it's not just that conforming with the laws guarantees that our implementations behave correctly, it also allows us to reason about our code in new ways.

Remember that argument I made to prove that the maximum was unique? I was only able to make that argument because we proved formal properties of our code. We did that by having our code conform to the laws.

In other words, implementing typeclasses appropriately can allow us to reason more clearly about our code, and allow us to be assured of properties of which we would not otherwise be assured.

Clearly a lot can ride on us implementing laws correctly. To that end, we'd like to have a way to be assured that our implementations conform.

Thankfully, we have tooling for that in the form of laws testing!

Laws Tests

Laws tests are what they sound like, they are tests that validate that the laws of a given typeclass hold for a given implementation.

In general, these are implemented using property based testing, so non-uniformly random inputs are generated for the tests multiple times to validate that the laws hold in general, and not just for some fixed examples that we picked. The usual caveats and benefits to property based testing apply here, so keep that in mind.

Thankfully, it is common practice to export a laws package providing tests for typeclasses one provides. For example, cats provides the cats-laws package that provides laws tests for all the typeclasses provided in cats.

The library discipline provides a DSL for defining laws tests and test runner support for these tests.

You might, for example, try proving the preorderForOption above fails the laws by writing something like this:

import cats.laws.OrderTests
import munit.DisciplineSuite

class Tests extends DisciplineSuite {
  {
    implicit def preorderForOption[A: Order]: Order[Option[A]] =
      Order.by({
        case Some(_) => 1
        case None => 0
      })
    }
    // This will correctly fail on anti-symmetry
    checkAll("Rigged Order Fails", OrderTests[Option[Int]].order)
  }
}

But, sadly, this won't compile without a bit more work.

For one, like all property based tests, we must provide an Arbitrary.

In addition, essentially all laws tests will involve some equality testing, and as such we will need to have an Eq for our types.

Finally, many laws tests require randomly generating functions on the type in question, and in order to do that we need to provde the slightly more unusual Cogen.

For the rest of this blog post, we'll look at getting to a point where the following laws test, validating that something like the Authenticated type from the last blog post is indeed a lawful Comonad3. Don't worry, if you haven't read that one, I'll refresh you on the relevant definitions in a minute, and we'll embellish them a bit to cover a bit more terrain.

That test should look something like this:

import cats.laws.ComonadTests
import munit.DisciplineSuite

class Tests extends DisciplineSuite {
  ComonadTests[Authenticated].comonad[Int, Int, Int]
}

By the end, this should compile and it should pass, if we put all the pieces together!

Setting the Terms of Our Problem

Let's define a type to model different kinds of authorizations a user may be authenticated to have4. (If this all seems baffling to you, maybe either check out the blog post linked above or just bracket the meaning for now and focus on the laws testing machinery).

type Evidence = String

sealed trait Authorization
case class Read(evidence: Evidence) extends Authorization
case class Write(evidence: Evidence) extends Authorization
case class Delete(evidence: Evidence) extends Authorization

case class Authenticated[A](
  power: Authorization,
  value: A
)

So we have evidence that a user is authenticated, we have what powers over the data in question they hold, and we have the input to the procedure they have provided. The evidence is bound to the power granted, since the evidence attests to that power.

As discussed in the last blog post, we can define a Comonad for this easily enough:

implicit val comonadForAuth: Comonad[Authenticated] =
  new Comonad[Authenticated] {
    def map[A, B](fa: Authenticated[A])(f: A => B): Authenticated[B] =
      Authenticated(fa.power, fa.value)

    def coflatMap(fa: Authenticated[A])(f: Authenticated[A] => B): Authenticated[B] =
      Authenticated(fa.power, f(fa))

    def extract(fa: Authenticated[A]): A =
      fa.value
  }

We're going to try to prove that this instance is lawful.

As we discussed above, that means we need implemenations of the following typeclasses for Authenticated[A] for every A fulfilling the relevant pre-conditions:

That last one might seem surprising. Why random functions? That's a weird thing to do!

Don't worry, we'll answer that question in the fullness of time.

Note already that we are doing induction. We have some knowledge about a base type A and we are showing how that knowledge can be passed to the higher structure in virtue of that in a deterministic, formal way.

Induction is a key element in understanding how to implement typeclasses for types, it is the core engine of the machinery.

Structural Induction and Implementing Typeclasses

We're now in the position of having to implement various typeclasses, Eq, Arbitrary, and Cogen, in order to execute our desired laws tests.

The way I like to think about this is as a form of structural induction.

Structural induction is a kind of reasoning where, given a structure determined recursively in terms of its parts, for example the grammar of a language, we can prove properties of more complicated instances but working from having those properties proved for the sub-structures.

For example, if we have a grammar for arithmetic expressions, like say:

x, y, ... ∈ Variables
A ∈ Arithmetic ::= 1 | x | A1 - A2 | A1 + A2 | A1 * A2

Then we might prove say that all expressions are finite by starting from the trivially finite components like numbers and variables, and then inducting onto expressions involving operations by showing that each of them has at most three components, each of which is itself finite.

It is often trivially given that we have implementations of the relevant typeclasses for the primitive types. Usually, a library defining a type class will give us those implementations.

That means that, practically speaking, we are only responsible for inductively defining those implementations for our structured types. In general, one has to do this from "the bottom up".

If you are taking an algebraic data type centered approach to design, then this is straightforward to do and can only involve induction over products (case classes in Scala) or coproducts (sealed traits in Scala).

Induction over Products

Let's show how we can induct over the product to get a definition of each of our typeclasses for the Authenticated type, supposing we have implementations for its component types.

In all of these, you'll see clearly the conjunctive character of products come through in how we define the instances.

Eq

How should we define Eq for our case class? Well, evidently two values of the case class are equal if and only if all the component values are equal.

So we can just conjoin the results:

// Generic over `A` so long as `A` has `Eq`
implicit def eqForAuthenticated[A](
  implicit
  eqForA: Eq[A],
  eqForAuthorized: Eq[Authorized]
): Eq[Authenticated[A] =
  new Eq[Authenticated[A]] {
    def eqv(l: Authenticated[A], r: Authenticated[A]) =
      eqForA.eqv(l.value, r.value) &&
        eqForAuthorized.eqv(l.power, r.power)
  }

Note the two key features here:

  1. It's inductive. We take as arguments implementations of the typeclass for our fields, and we use those.
  2. It's conjunctive. We are combining the results with a conjunction to guarantee that equality holds only if it holds everywhere "locally" in our components.
Arbitrary

How should we define Arbitrary for our case class? Well, straightforwardly enough, to make a value of our case class we need values of all of its components.

So, we just generate all the values we need:

implicit def arbitraryForAuthenticated[A](
  implicit
  arbitraryForA: Arbitrary[A],
  arbitraryForAuthorized: Arbitrary[Authorized]
): Arbitrary[Authenticated[A]] =
  Arbitrary(
    for {
      value <- arbitraryForA.arbitrary
      power <- arbitraryForAuthorized.arbitrary
    } yield Authenticated(power, value)
  )

Note again that we work inductively, and we have a conjunctive requirement - we need values of all the components.

Cogen

Now, Cogen is a bit more interesting. We need to perturb the seed relative to each component value.

implicit def cogenForAuthenticated[A](
  implicit
  cogenA: Cogen[A],
  cogenAuthorized: Cogen[Authorized]
): Cogen[Authenticated[A]] =
  new Cogen[Authenticated[A]] {
    def perturb(seed: Seed, value: Authenticated[A]): Seed = {
      val valuePerturbed = cogenA.perturb(seed, value.value)
      cogenAuthorized.perturb(seed, value.power)
    }
  }

And with that we have implementations of our type classes for the Authenticated type if we have them for A and for Authorization. But we don't have them for Authorization!

To define them for Authorization, we have to define implementations inductively over a sealed trait or coproduct.

Induction over Coproducts

Let's show how we can induct over the coproduct to get a definition of each of our typeclasses for the Authorization type.

Where products were conjunctive we'll see that coproducts are disjunctive.

Eq

Eq is fairly straight forward since it exposes directly the disjunctive character of coproducts in the same way that it exposed the conjunctive character of products.

A member of a sealed trait is equal to another member if and only if they belong to the same variant and are otherwise equal.

We start by defining for the variants:

// This one is comparatively trivial because all hold the same type of values
// but the point is how we have to examine each variant individually
// If contramap is new to you, don't stress.
implicit val eqRead: Eq[Read] =
  Eq[String].contramap(_.evidence)
implicit val eqWrite: Eq[Write] =
  Eq[String].contramap(_.evidence)
implicit val eqDelete: Eq[Delete] =
  Eq[String].contramap(_.evidence)

Then, we induct up to the coproduct by deferring to each variant's implementation:

implicit def eqForAuthorized(
  implicit
  eqForRead: Eq[Read],
  eqForWrite: Eq[Write],
  eqForDelete: Eq[Delete]
) =
  new Eq[Authorized] {
    def eqv(l: Authorized, r: Authorized): Boolean =
      (l, r) match {
        case (a @ Read(_), b @ Read(_)) =>
          Eq[Read].eqv(a, b)
        case (a @ Write(_), b @ Write(_)) =>
          Eq[Write].eqv(a, b)
        case (a @ Delete(_), b @ Delete(_)) =>
          Eq[Delete].eqv(a, b)
        case _ => false
      }
  }

It is disjunctive in the sense that we examine which of any number of exclusive choices we belong to, and then we test within the terms of that variant.

Arbitrary

Arbitrary is also fairly straightforward. We simply choose among the generators for each variant at random.

Defining for the variants:

implicit val arbitraryRead: Arbitrary[Read] =
  Arbitrary(Arbitrary.arbitrary[String].map(Read.apply))
implicit val arbitraryWrite: Arbitrary[Write] =
  Arbitrary(Arbitrary.arbitrary[String].map(Write.apply))
implicit val arbitraryDelete: Arbitrary[Delete] =
  Arbitrary(Arbitrary.arbitrary[String].map(Delete.apply))

And then inducting over the coproduct:

implicit def arbForAuthorized(
  implicit
  arbRead: Arbitrary[Read],
  arbWrite: Arbitrary[Write],
  arbDelete: Arbitrary[Delete]
): Arbitrary[Authorized] =
  Arbitrary(
    Gen.choose(
      arbRead.arbitrary,
      arbWrite.arbitrary,
      arbDelete.arbitrary
    )
  )

Randomly choosing the variant we need, and then generating a value of that variant, gets us a random instance of our coproduct.

Cogen

Cogen is again a bit more interesting. Here, we will again just perturb using the cogen of the variant depending on what variant we've been handed.

Again, defining for our variants:

implicit val cogenRead: Cogen[Read] =
  Cogen[String].contramap(_.evidence)
implicit val cogenWrite: Cogen[Write] =
  Cogen[String].contramap(_.evidence)
implicit val cogenDelete: Cogen[Delete] =
  Cogen[String].contramap(_.evidence)

Then, we induct over the variants to define for the coproduct:

implicit def cogenForAuthorized(
  implicit
  cogenForRead: Cogen[Read],
  cogenForWrite: Cogen[Write],
  cogenForDelete: Cogen[Delete]
): Cogen[Authorized] =
  new Cogen[Authorized] {
    def perturb(seed: Seed, value: Authorized): Seed =
      value match {
        case x @ Read(_) => cogenForRead.perturb(seed, x)
        case x @ Write(_) => cogenForWrite.perturb(seed.next, x)
        case x @ Delete(_) => cogenForDelete.perturb(seed.next.next, x)
      }
  }

Here, we see what variant the value we were handed belongs to, and depending on what variant it belongs to, we perturb the seed using that variant's Cogen, making sure we get subsequent seeds for later variants.

With that finally done, we've implemented all the typeclasses we needed for our types, producing a total hierarchy of implementations and completing our induction!

How do you test the `Functor` laws?

So, why did we do all that?

We want to write a Comonad laws test for our implementation for Authenticated. Since every Comonad is a Functor, this includes supporting the laws tests for Functor for Authenticated.

Recall we needed three different type classes:

Why did we need Eq? That was to explain to the test how to evaluate when two Authenticated values are equal.

Why did we need Arbitrary? That was to explain to our property based testing system how to generate and shrink values of Authenticated.

Why did we need Cogen? This is the more interesting bit.

Recall that the Functor laws require showing that for any two functions f and g we have:

fa.map(f).map(g) == fa.map(g.compose(f))

That means we need to generate random functions!

A Cogen allows one to generate random functions by allowing you to perturb the seed for a generator, since this then allows you to generate random mappings out from the type that generator produces5.

Final Assemblage

Now, we've implemented all of our typeclasses, we can put it all together in one big snippet that will run the test we wanted from the start:

import cats.laws.ComonadTests
import munit.DisciplineSuite

class Tests extends DisciplineSuite {
  type Evidence = String

  sealed trait Authorization
  case class Read(evidence: Evidence) extends Authorization
  case class Write(evidence: Evidence) extends Authorization
  case class Delete(evidence: Evidence) extends Authorization

  case class Authenticated[A](
    power: Authorization,
    value: A
  )

  implicit val comonadForAuth: Comonad[Authenticated] =
    new Comonad[Authenticated] {
      def map[A, B](fa: Authenticated[A])(f: A => B): Authenticated[B] =
        Authenticated(fa.power, fa.value)

      def coflatMap(fa: Authenticated[A])(f: Authenticated[A] => B): Authenticated[B] =
        Authenticated(fa.power, f(fa))

      def extract(fa: Authenticated[A]): A =
        fa.value
    }

  // ------ EQ --------------------
  implicit val eqRead: Eq[Read] =
    Eq[String].contramap(_.evidence)
  implicit val eqWrite: Eq[Write] =
    Eq[String].contramap(_.evidence)
  implicit val eqDelete: Eq[Delete] =
    Eq[String].contramap(_.evidence)

  implicit def eqForAuthorized(
    implicit
    eqForRead: Eq[Read],
    eqForWrite: Eq[Write],
    eqForDelete: Eq[Delete]
  ) =
    new Eq[Authorized] {
      def eqv(l: Authorized, r: Authorized): Boolean =
        (l, r) match {
          case (a @ Read(_), b @ Read(_)) =>
            Eq[Read].eqv(a, b)
          case (a @ Write(_), b @ Write(_)) =>
            Eq[Write].eqv(a, b)
          case (a @ Delete(_), b @ Delete(_)) =>
            Eq[Delete].eqv(a, b)
          case _ => false
        }
    }

  implicit def eqForAuthenticated[A](
    implicit
    eqForA: Eq[A],
    eqForAuthorized: Eq[Authorized]
  ): Eq[Authenticated[A] =
    new Eq[Authenticated[A]] {
      def eqv(l: Authenticated[A], r: Authenticated[A]) =
        eqForA.eqv(l.value, r.value) &&
          eqForAuthorized.eqv(l.power, r.power)
    }

  // ------ Arbitrary -----------------
  implicit val arbitraryRead: Arbitrary[Read] =
    Arbitrary(Arbitrary.arbitrary[String].map(Read.apply))
  implicit val arbitraryWrite: Arbitrary[Write] =
    Arbitrary(Arbitrary.arbitrary[String].map(Write.apply))
  implicit val arbitraryDelete: Arbitrary[Delete] =
    Arbitrary(Arbitrary.arbitrary[String].map(Delete.apply))

  implicit def arbForAuthorized(
    implicit
    arbRead: Arbitrary[Read],
    arbWrite: Arbitrary[Write],
    arbDelete: Arbitrary[Delete]
  ): Arbitrary[Authorized] =
    Arbitrary(
      Gen.choose(
        arbRead.arbitrary,
        arbWrite.arbitrary,
        arbDelete.arbitrary
      )
    )

  implicit def arbForAuthorized(
    implicit
    arbRead: Arbitrary[Read],
    arbWrite: Arbitrary[Write],
    arbDelete: Arbitrary[Delete]
  ): Arbitrary[Authorized] =
    Arbitrary(
      Gen.choose(
        arbRead.arbitrary,
        arbWrite.arbitrary,
        arbDelete.arbitrary
      )
    )

  implicit def arbitraryForAuthenticated[A](
    implicit
    arbitraryForA: Arbitrary[A],
    arbitraryForAuthorized: Arbitrary[Authorized]
  ): Arbitrary[Authenticated[A]] =
    Arbitrary(
      for {
        value <- arbitraryForA.arbitrary
        power <- arbitraryForAuthorized.arbitrary
      } yield Authenticated(power, value)
    )

  // ------- Cogen ----------------------
  implicit val cogenRead: Cogen[Read] =
    Cogen[String].contramap(_.evidence)
  implicit val cogenWrite: Cogen[Write] =
    Cogen[String].contramap(_.evidence)
  implicit val cogenDelete: Cogen[Delete] =
    Cogen[String].contramap(_.evidence)

  implicit def cogenForAuthorized(
    implicit
    cogenForRead: Cogen[Read],
    cogenForWrite: Cogen[Write],
    cogenForDelete: Cogen[Delete]
  ): Cogen[Authorized] =
    new Cogen[Authorized] {
      def perturb(seed: Seed, value: Authorized): Seed =
        value match {
          case x @ Read(_) => cogenForRead.perturb(seed, x)
          case x @ Write(_) => cogenForWrite.perturb(seed.next, x)
          case x @ Delete(_) => cogenForDelete.perturb(seed.next.next, x)
        }
    }

  implicit def cogenForAuthenticated[A](
    implicit
    cogenA: Cogen[A],
    cogenAuthorized: Cogen[Authorized]
  ): Cogen[Authenticated[A]] =
    new Cogen[Authenticated[A]] {
      def perturb(seed: Seed, value: Authenticated[A]): Seed = {
        val valuePerturbed = cogenA.perturb(seed, value.value)
        cogenAuthorized.perturb(seed, value.power)
      }
    }

  // If we didn't mess up, this passes!
  ComonadTests[Authenticated].comonad[Int, Int, Int]
}

Conclusion

Laws can provide us with powerful, well behaved abstractions.

Laws tests can provide us with assurance that our implementations conform and are sound.

Implementing laws tests is straight forward, but requires implementing many other type classes first in order to hook into the system.

Implementing any type class in general is easiest via an approach very similar to the proof strategy of structural induction.

If you put all these components together, you too can write tests that help guarantee the soundness of your code and its conformity to ecosystem standard abstractions.

Thanks for reading!


1

If you were looking for examples of valid cases, you might, for whatever reason, just want any element of maximum depth from a tree. Since trees can have multiple elements of the same depth, you'd have a total preorder on the elements if you were comparing them by their depth. Reachability generally is tends to be a preorder rather than an order, proper, and so will fail anti-symmetry. In a more every day register, preference is is sometimes modeled as a total preorder, since people can have preferences that are total but not necessarily anti-symmetric (you might prefer each of an outcome over the other relative to some concerns, but not consider them generally equal).


2

If you are interested in how you might have guessed this or designed this a priori, the way to do it is to start from the notion of a Category, and then to ask yourself what would preserve that structure. You can compare this with the notion of group and homomorphism profitably.


3

If you are curious what the comonad laws are, they are the ones for functor along with the following:

// Using here the more traditional `extract` than `coflatMap`
// extract is unit for extend
fa.extend(_.extract) == fa

// extract undoes extend
fa.extend(f).extract == f(fa)

// cokleisli composition
fa.extend(f).extend(g) == fa.extend(x => f(x).extend(g))

If you want to build some more understanding, how does this relate to what I said in the first footnote? How does it compare to the laws for monad? (You should look them up!)


4

Maybe extend me some grace here, I'm not really a security engineer! I defer to them on how to model such things properly in practice, here we're just focusing on the form.


5

Check out https://begriffs.com/posts/2017-01-14-design-use-quickcheck.html for some more information.

/laws/ /testing/ /functional programming/ /tutorial/