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 Option
s, 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 Some
s. 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 Comonad
3. 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:
Eq
- we will need anEq
forAuthenticated[A]
wheneverA
itself has anEq
- We need this so we can explain how to show equality between two such
Authenticated[A]
values
- We need this so we can explain how to show equality between two such
Arbitrary
- we will need anArbitrary
forAuthenticated[A]
wheneverA
itself has anArbitrary
- We need this so we can explain how to generate non-uniformly random instances of
Authenticated[A]
- We need this so we can explain how to generate non-uniformly random instances of
Cogen
- we will need aCogen
forAuthenticated[A]
wheneverA
itself has aCogen
- We need this so we can explain how to generate non-uniformly random functions of type
Authenticated[A] => Authenticated[A]
(or nore general functions)
- We need this so we can explain how to generate non-uniformly random functions of type
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:
- It's inductive. We take as arguments implementations of the typeclass for our fields, and we use those.
- 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:
Eq
Arbitrary
Cogen
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!
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).
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.
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!)
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.
Check out https://begriffs.com/posts/2017-01-14-design-use-quickcheck.html for some more information.