← All articles

In 1989, Philip Wadler wrote a paper, Theorems for Free!¹ In this article, we are going to explore what this means and some of the consequences. In previous articles, we looked at addition, multiplication and exponentiation with data types and we followed up with differentiating data types with respect to one type variable.

However, in producing these algebraic results, we were at all times discussing concrete data types with respect to exponentiation, such as Boolean and List. For example, we know that the Option[A] data type corresponds to the equation 1 + A and we know that a function of the type Option[Boolean] => Boolean corresponds to the equation BooleanOption[Boolean] or 23. We conclude, simply by counting, that there are 8 unique functions of the type Option[Boolean] => Boolean.

What about polymorphic functions?

Consider, for example, this function type:

def func[A, B](a: A, b: B): A

What does this function correspond to algebraically? The answer, in this case, is 1. There is only 1 possible function with this type (try it!). Calculating this result has a strong relationship to Theorems for Free, however we will defer the details of this calculation to a later post. In this post, we are going to look at general reasoning about code using Theorems for Free, or as the result is often called, Parametricity.

Wadler writes:

Write down the definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function's definition. I will tell you a theorem that the function satisfies. The purpose of this paper is to explain the trick.

An example is provided. Suppose any function with this type:

def func[A](a: List[A]): List[A]

We don't know what this function does; only its type. However, regardless of what this function does, we may freely conclude that this function, or theorem, is always true for all possible function arguments:

def theorem[A](x: List[A], f: A => A): Boolean =
  func(x.map(f)) == func(x).map(f)

An important requirement to draw this conclusion is the parametric polymorphism in the type of func. Specifically, func has the type [A]List[A] => List[A]. It is polymorphic in the list element types. It does not have a concrete type, such as List[Int] => List[Int], since if it did, our theorem would not hold true.

We can also intuit (or calculate, if preferred!) some other results. Given any function of the type [A]List[A] => List[A], we can conclude and with no further information, that the following statement is true about the function. It is a fun exercise to try to falsify this claim, and to gain insight into why it must be true.

Every list element in the list that is returned, appears in the list argument.

This statement would not hold true if the given function was not polymorphic. For example, if the given function had the type List[Int] => List[Int], we could easily falsify it:

def function(x: List[Int]): List[Int] =
  List(99)

// r = List(99)
// However, 99 does not appear in the argument
val r = function(List(12))

Fast and Loose Reasoning

It is also possible to falsify some of these theorems by taking into account bottom values. Bottom values generally denote non-termination of the function. Consider this simple example:

def two_exponent_two(b: Boolean): Boolean

We can reliably conclude that there are four possible values of this type i.e. we don't know what this function does, but we know that it is one of four possible values. However, suppose the following (fifth?) value:

// return null
def two_exponent_two(b: Boolean): Boolean = null

We can take this further (with other values?):

// never return
def two_exponent_two(b: Boolean): Boolean = two_exponent_two(b)

// throw an exception
def two_exponent_two(b: Boolean): Boolean = sys.error("bottom")

// perform a side-effect
def two_exponent_two(b: Boolean): Boolean = { deleteTheDatabase(); b }

So then, are all our theorems unreliable? Or even, completely false? Actually, the situation gets worse. Consider a polymorphic function type:

def function[A, B](a: A, b: B): A

We noted earlier that this function type has 1 possible solution. Here it is:

def function[A, B](a: A, b: B): A = a

But what about these code examples?

// type-casting
def function[A, B](a: A, b: B): A = b.asInstanceOf[A]

// type-casing (switching on type)
def function[A, B](a: A, b: B): A = a match {
  case _: String => 99.asInstanceOf[A]
  case _: Int    => b.asInstanceOf[A]
  case _: Char   => if(a.toString == 'x') a else b.asInstanceOf[A]
  case _         => a
}

// Any hashCode method
def function[A](a: A): Boolean =
  a.hashCode % 2 == 0
}

// Any toString method
def function[A](a: A): Boolean =
  a.toString.length % 2 == 0
}

It seems that reasoning about our code using free theorems cannot help us, since these possibilities must always be considered. However, we can handle each of these cases. Of our cases, we have the following:

• general recursion, leading to non-termination
• null
• exceptions
• side-effects
• type-casting
• type-casing
• Any methods

The first example, non-termination, is handled quite explicitly in a paper by Danielsson, Hughes, Jansson, Gibbons², Fast and Loose Reasoning is Morally Correct.

Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.

A total language is one where non-termination is eliminated as a possibility by the programming language — it's simply not possible. This, of course, has consequences for how we write programs. However, when we use non-total programming languages, such as Scala, can we simply ignore this possibility of non-termination when reasoning about our code? According to Fast and Loose Reasoning, yes we can and in fact, it is morally correct to do so.

The latter examples can be handled similarly, but with a little more nuance. For example, consider the following function type:

def cast[A, B](a: A): B

If you were to calculate this algebraically³, you'd have the value 0. That is to say, there exist zero programs with this type, therefore, it must fail to terminate. In fact, this specific type already handles one of our examples: type-casting. This is the type of type-casting itself, so can we simply ignore it when reasoning? Not so fast. Consider another example:

def function[A](a: A): Boolean

This type calculates to the value 2. We can reasonably conclude, by parametricity, that it returns either true or false and that it must ignore its argument. In fact, if you try to produce any other value for this type, you must use one of our unsafe examples so far given. This function has the same type as type-casing i.e. examining a value for its type and asking, "is it this type?", which clearly is not ignoring the argument. What can we do?

Recall: one of the most primary and immediate benefits of Functional Programming is local reasoning. That is to say, we can reason about code expressions independently of others are arrive at reliable results. Unfortunately, just a single use of any of the above unsafe examples breaks local reasoning and does so for our entire program. Suppose we have a 100KLOC program, with just one nasty piece of code hiding in a corner:

def function[A, B](a: A): B = a.asInstanceOf[B]

We might write this code one day and forget about it. However, its potential existence directly implies that we are no longer achieving any of the advantages of Functional Programming, and we have lost any ability for local reasoning. Functional Programming is not a particularly useful goal in itself, so losing any of its benefits would be quite pointless!

We might see some other code in our application:

def othercode[F[_]: Functor, A, B](k: B, x: F[A]): F[B]

We can reason algebraically about this code and conclude that there is only one possible outcome for this function. It maps across the value x, ignores the A and returns the B to return a F[B]. This is a reasonable result by looking at the type of this function. However, if we have introduced the potential for unsafe code, we must also consider this possibility:

def othercode[F[_]: Functor, A, B](k: B, x: F[A]): F[B] =
  function(List(1,2,3))

In fact, we must consider an open world of possibilities and we must do this for all of our 100KLOC application. We have lost all of local reasoning about our code. This can be quite devastating — is it possible read and comprehend our code at all!? What can we do about this?

Solution: use only the language subset that does not have these possibilities and never admit a single instance of unsafe code that breaks local reasoning

This may seem a little drastic, perhaps completely impractical. However, each of these specific examples of violating local reasoning has a safe solution and with not only little or no penalty, but often significant benefits. Consider an example of casing between two types, and an exception otherwise:

def swizzle[A](a: A): Boolean =
  a match {
    case x: Int    => x % 2 == 0
    case y: String => y.length % 3 == 0
    case _         => sys.error("never gets here, promise, trust me!")
  }

We can repair this function using a data type:

def swizzle(x: Either[Int, String]): Boolean =
  x match {
    Left(x)  => x % 2 == 0
    Right(y) => y.length % 3 == 0
  }

We would then have to update all the call sites to put either the Int or String into a constructor for Either[Int, String]. In doing so, we would also obtain the benefits of the data type itself e.g. having the ability to use the map function on the Either[Int, String] or the optics (prisms) that come about from each of the constructors of Either. In making the code easier to reason about, we have achieved ancillary benefits, such as composition with other functions. It seems then, there are only benefits to using a safe subset of the language.

However, this code refactoring is still not a free ride. Since local reasoning has already been broken, we may find instances of code where neither an Int nor a String is used, even though the code itself as a whole remains safe (we hope). We could continue updating call sites, repairing unsafe code, hoping that it is not too much work. However, since we have lost local reasoning, it is impossible to predict the amount of work we have ahead of ourselves! Not only must we use a safe language subset to avoid this scenario, but we also must do so from the start of application development. After all, that is an immediate consequence of losing local reasoning i.e. if this were not true, then by direct consequence, we would have preserved some amount of local reasoning!

Other examples of unsafe code are generally more immediately obvious. Many of us accept that instead of using null, we could choose to use an Option data type, and in doing so, achieve the same benefits; code that can be locally reasoned about, and composition of our code with other code — the benefits of Functional Programming. We can achieve similar goals for all of the examples above.

Assuming Safe Subset, Fast and Loose Reasoning

Let's assume a safe subset of our programming language along with Fast and Loose Reasoning to explore some more examples of parametricity. So far, we have seen rather trivial examples of reasoning about our code. We saw this type in an earlier example:

def function[F[_]: Functor, A, B](k: B, x: F[A]): F[B]

This type has one possible solution. Here it is:

def function[F[_]: Functor, A, B](k: B, x: F[A]): F[B] =
  x.map(_ => k)

However, if we strengthen the constraint on F, does this change?

def function[F[_]: Monad, A, B](k: B, x: F[A]): F[B]

We know this function could possibly be the same implementation as with the Functor constraint. Does changing the constraint to Monad change the guarantee that it is? Yes, it does. Consider this implementation:

def function[F[_]: Monad, A, B](k: B, x: F[A]): F[B] =
  x.flatMap(_ => x).map(_ => k)

By making the constraint stronger, we have introduced the potential for more candidate functions. This is why it is important to constrain type variables only as much as necessary. If we follow this principle, we can confidently assume that Monad is a necessary constraint and therefore, the implementation should behave in a way for which Functor (or even Applicative) is insufficient.

Here is another example presented as an exercise. Try it!

case class Store[A, B](put: A => B, A) {
  // there is only one possible solution here
  def map[C](f: B => C): Store[A, C] =
    ...

  // also here
  def copoint: B =
    ...

  // what about here?
  def coflatMap[C](f: Store[A, B] => C): Store[A, C] =
    ...
}

In the next article on parametricity, we will discuss the algebraic reasoning for polymorphic types. We will use the yoneda lemma to perform this calculation. For example, we can take the type [A]A => A and calculate its result to be 1 using the yoneda lemma. We will also discuss tools and solutions to reasoni about code where using parametricity does not give a complete picture of our code.

Footnotes

1. Theorems for free!, Philip Wadler, 1989 ↩

2. Fast and loose reasoning is morally correct, Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons, 2006 ↩

3. We will show how to do this in detail in a later post ↩