We often accept for granted that functional programming (FP) helps us reason about our programs more. This is often attributed to "referential transparency" or "equational reasoning" with only a cursory explanation.
With this post, I'd like to give a slightly more involved illustration for how the referential transparency of functional programming helps us reason equationally.
Because a few presentations have recently highlighted the utility of monoids, I thought I'd focus on monoids as an example. The main point, though, is more about reasoning, and less about monoids.
Since the parallels between programming, logic, and algebra run extremely deep, there's lots of concepts from abstract algebra that apply to programming. The monoid (and the popularly discussed monad, for that matter) is just one of these concepts. If you embrace the liberating view that programming is very much just mathematics, then many more concepts can reveal themselves in the programs we write. Once you see the mathematics clearly, it may not seem so far-fetched to reason about the correctness of your programs in the way a mathematician reasons about the correctness of a proof.
This post gives just a taste.
I'd like to target FP-curious readers working in languages with less FP-affinity, I've chosen to illustrate examples in Scala since Scala has a somewhat divided community with respect to FP. Knowledge of Scala will help you follow examples, but hopefully you can follow along either way. Examples in Haskell would have been notably more elegant, though.
I also assume some familiarity with algebra, but really not more than we learn in middle school. In those years we learned terms like "identity" and "associativity" with respect to addition and multiplication. It's not much to define a few more terms like "monoid."
To build a monoid, we need
-
a set of things
-
an operation
appendthat takes two of these things and yields another from the set things -
a special element of our set designated as
zero -
appendandzeroto satisfy some three laws (which we'll discuss in a moment).
In programming languages, we use types to describe our "set of things." We can encode the concept of a monoid generically for any type as follows:
trait Monoid[A] {
def zero: A
def append(a: A, b: A): A
}However, this is not enough. We also need to be clear about the laws that must
be satisfied. In the case of the monoid, we must assure that the following
laws alway hold for any a, b, and c:
- Associativity:
append(append(a, b), c) ≡ append(a, append(b, c)) - Left Identity:
append(zero, a) ≡ a - Right Identity:
append(a, zero) ≡ a
So now, let's look at an example of a monoid from our middle school algebra
classes -- the additive monoid for integers. Here zero is literally 0, and
append is +.
val additiveIntMonoid[Int]: Monoid[Int] =
new Monoid[Int] {
def zero: 0
def append(a: Int, b: Int) = a + b
}You may have a strong intuition that the definition above satisfies our three laws for monoids. But can we do better than just intuition?
One methodology we can follow is to write automated tests. Perhaps you can choose enough combinations of example integers to test all the laws.
Or perhaps you heard about "property-based" testing that will randomly generate instances of a required type so you can validate invariants more easily. This is certainly a great technique, and one that you'll find used broadly in the FP community.
But is there anything we can do to get back to the essense of the intuition we had originally? What can we do to formalize our intuition into a proof?
What if we just wrote our proof as small little expressions, using the referential transparency of functional programs to turn the left-hand side of our law into the right-hand side?
For instance, let's say we started with the left-hand side of the left identity law:
append(zero, f)We know that we've defined zero as 0 in our monoid instance:
append(0, f)And we know append is just + in our monoid instance:
0 + fAnd we know that 0 + does nothing for integers:
fHere's a full set of such proofs for the additive monoid for integers:
trait AdditiveIntegerMonoidProofs {
implicit val additiveIntMonoid[Int]: Monoid[Int] =
new Monoid[Int] {
def zero: 0
def append(a: Int, b: Int) = a + b
}
val f: Int
val g: Int
val h: Int
def leftIdentity {
val M = implicitly[Monoid[Int]]
import M.{zero, append}
val Step0: Int = append(zero, f) // LHS
val Step1: Int = append(0, f) // by definition of zero
val Step2: Int = 0 + f // by definition of append
val Step3: Int = f // RHS, by Int's additive identity
}
def rightIdentity {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: Int = append(f, zero) // LHS
val Step1: Int = append(f, 0) // by definition of zero
val Step2: Int = f + 0 // by definition of append
val Step3: Int = f // RHS, by Int's additive identity
}
def associativity {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: Int = append(append(f, g), h) // LHS
val Step1: Int = append(f + g, h) // by definition of append
val Step2: Int = (f + g) + h // by definition of append
val Step3: Int = f + (g + h) // by Int's additive associativity
val Step4: Int = f + append(g, h) // by definiton of append
val Step5: Int = append(f, append(g, h)) // RHS, by definition of append
}
}This program completely compiles. There's a little bit of encoding in a Scala
trait to allow us to talk about f, g, and h abstractly (irrespective of any
specific integer). Also, note that I've put my monoid in implicit scope, which
is then pulled in with the implicitly call. This is because I've encoded
Monoid as a type class (which comes from Haskell). Don't worry about
this just yet. We'll have more to say about it at the end of the post.
We're using definitions, known properties, and substitution to work our way through these proofs. FP gives us equations that have permanence, rather than just side-effecting assignment to variables for a fleeting scope of time. These equations are what we use for subtitution in our proofs.
Without FP, we can not do this kind of reasoning.
Unfortunately, the compiler isn't testing how we chain our steps together with substitution. This is why it's helpful to do each substitution one step at a time, so you can validate each step easily.
You may wonder if there's any programmers that actually do proofs like this. Probably most people just reason about their programs informally, perhaps just on a whiteboard or in their heads. Then, rather than work through proofs rigorously, they resort to tools like property-based testing frameworks, relying on the "small scope hypothesis" from model-checking communities to gain confidence from incomplete testing.
You may also have the idea that since our process is so systematic, computers can help out with more automation. This is very much true, and researchers are pursuing this automation with proof assistants and dependently typed languages. But for most languages used in industry, we have to work through our reasoning much more manually.
So how do you feel now? If you did the reasoning above, would you still feel like you need automated tests? We've taken informal reasoning, and translated it to a pretty good formalism. Also, we're getting a little bit of assistance from the compiler that we haven't made simple little errors.
When we test our monoid with automated testing frameworks (even property-based ones), though we have added confidence that our laws hold, we don't really know why our laws are holding. The only way to know is to run through a proof similar to what we've done above.
Even if we only informally reason about proofs, we still need a formal framework to transform them too. Otherwise we're really taking huge risks with correctness. Informal reaoning is just something we do as a shorthand once we've mastered a formal process.
Now that we've got the mechanics of these proofs, let's walk through a couple more interesting examples.
We can define a simple monoid for functions of type A => A. These types of
functions are sometimes called endomorphisms. The intuition is that
composition of these functions is associative and can be our append. And a
simple identity function will do nothing upon composition, so it can be our
zero.
The following is an implementation along with the necessary proofs.
object NaiveEndo {
def id[A]: A => A = a => a
implicit def monoid[A]: Monoid[A => A] =
new Monoid[A => A] {
def zero = id
def append(a: A => A, b: A => A) = a compose b
}
trait LawProofs[A] {
val f: A => A
val g: A => A
val h: A => A
def leftIdentity {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(zero, f)
val Step1: A => A = append(id, f)
val Step2: A => A = id compose f
val Step3: A => A = { a: A => id(f(a)) }
val Step4: A => A = { a: A => f(a) }
val Step5: A => A = f
}
def rightIdentity {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(f, zero)
val Step1: A => A = append(f, id)
val Step2: A => A = f compose id
val Step3: A => A = { a: A => f(id(a)) }
val Step4: A => A = { a: A => f(a) }
val Step5: A => A = f
}
def associativity {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(append(f, g), h)
val Step1: A => A = append(f compose g, h)
val Step2: A => A = append({ a: A => f(g(a))}, h)
val Step3: A => A = { a: A => f(g(a))} compose h
val Step4: A => A = { a: A => f(g(h(a)))}
val Step5: A => A = f compose { a: A => g(h(a))}
val Step6: A => A = f compose (g compose h)
val Step7: A => A = f compose append(g, h)
val Step8: A => A = append(f, append(g, h))
}
}
}There's another way we can have a monoid for endomorphisms A => A when we
have a monoid for A. It's a little less obvious than the endomorphism monoid
we just covered. For some it may not seem obvious that the monoid laws still
hold.
Fortunately, you can just work through the proof with basic substitution and using laws that we've already proven. This is illustrated in the following:
object VariantMonoid {
def id[A]: A => A = a => a
implicit def monoid[A: Monoid]: Monoid[A => A] =
new Monoid[A => A] {
def zero =
a => implicitly[Monoid[A]].zero
def append(f: A => A, g: A => A) =
a => implicitly[Monoid[A]].append(f(a), g(a))
}
trait LawProofs[A] {
val f: A => A
val g: A => A
val h: A => A
def leftIdentity(implicit A: Monoid[A]) {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(zero, f)
val Step1: A => A = append(a => A.zero, f)
val Step2: A => A = a => A.append({ a: A => A.zero } apply a, f(a))
val Step3: A => A = a => A.append(A.zero, f(a))
val Step4: A => A = a => f(a)
val Step5: A => A = f
}
def rightIdentity(implicit A: Monoid[A]) {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(f, zero)
val Step1: A => A = append(f, a => A.zero)
val Step2: A => A = a => A.append(f(a), { a: A => A.zero } apply a)
val Step3: A => A = a => A.append(f(a), A.zero)
val Step4: A => A = a => f(a)
val Step5: A => A = f
}
def associativity(implicit A: Monoid[A]) {
val M = implicitly[Monoid[A => A]]
import M.{zero, append}
val Step0: A => A = append(append(f, g), h)
val Step1: A => A = append(a => A.append(f(a), g(a)), h)
val Step2: A => A = a => A.append({ a: A => A.append(f(a), g(a)) } apply a, h(a))
val Step3: A => A = a => A.append(A.append(f(a), g(a)), h(a))
val Step4: A => A = a => A.append(f(a), A.append(g(a), h(a)))
val Step5: A => A = a => A.append(f(a), { a: A => A.append(g(a), h(a)) } apply a)
val Step6: A => A = append(f, a => A.append(g(a), h(a)))
val Step7: A => A = append(f, append(g, h))
}
}
}Notice how we use the known associativity of Monoid[A] to prove our
associativity for Monoid[A => A].
As mentioned earlier, I've put these monoid instances in implicit scope as a
way to encode Monoid as a type class. Type classes are parametrically
polymorphic interfaces that that compiler helps find concrete instances for.
It is very appropriate to regard type classes as logical proprositions, and the instances of these type classes as evidence that the logical proposition is true for a particular type.
But as we've encoded our monoid instances above, there's a problem with ambiguity. For instance, if I called
implicitly[Monoid[Int]]should we get the additive monoid for integers? What if we had also put a multiplicative monoid for integers in implicit scope? From the perspective of logic, both are valid monoids for integers.
Our second pair of monoids for endomorphisms exposes this problem as well. Which instance should we get for the following:
implicitly[Monoid[Int => Int]]Both of our monoids for endomorphisms apply (the simple one does not require
Monoid[Int], and the variant that does) since we have a Monoid[Int] in
implicit scope.
The commonly accepted solution to this problem is to wrap the type with another type that unambiguously helps us get the right type class instance from implicit scope. So for Int, we might have:
case class Additive[A](a: A) extends AnyValue
case class Multiplicative[A](a: A) extends AnyValueAnd then we could define unambiguously Monoid[Additive[Int]] and
Monoid[Multiplicative[Int]].
Similarly, when we can have a wrapper for our first endomorphism as follows:
case class Endo[A](run: A => A) extends AnyValueso we can define
implicit def endoMonoid[A]: Monoid[Endo[A]] =
new Monoid[Endo[A]] {
def mzero = Endo(identity[A])
def mappend(a: Endo[A], b: Endo[A]) = Endo(a.run compose b.run)
}and not have any ambiguity when we call implicitly[Monoid[Endo[A]]]. This is
precisely what's done in both Haskell and the Scalaz library for
Scala.