# 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 this^{1}, 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 are^{2}:

```
// 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 have^{4}. (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 an`Eq`

for`Authenticated[A]`

whenever`A`

itself has an`Eq`

- 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 an`Arbitrary`

for`Authenticated[A]`

whenever`A`

itself has an`Arbitrary`

- 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 a`Cogen`

for`Authenticated[A]`

whenever`A`

itself has a`Cogen`

- 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

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 produces^{5}.

### 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.