Securing invariants through Parametricity

Or how parametric types entail theorems for free

Here’s a particular solution to FizzBuzz.

Simple, first attempt solution at FizzBuzz.

That’s fine! But what if we wanted to reflect some of our expectations from this program in our types? One example being that when you receive Val back from fizzbuzz, it contains the value you passed it.

Right now, we could always return Val 42 in that case, and it would still typecheck, that’s bad!

The answer lies in solving a more general problem. Let’s introduce a type parameter in our FizzResult case and factor out the general structure of the fizzbuzz function.

For this version, we see that the only sensible value we can return in the Val case is the same value we got as input, we have no other ways of getting our hands on an a!

With this, we can see how using type variables, solving in a way a more general problem, constrains the things we can do and leads us to correctness.

Can we actually do better, and make it so our mkFizzBuzz function only returns FizzBuzz when both predicates hold, Fizz when only the first predicate holds, Buzz when only the second one does, and finally, Val x only when both of them don’t hold?

The answer is a resounding Yes!
And we can use a very similar strategy to that above.

The idea is as follows: For each of the predicates, add two type parameters. These will correspond to the case when the predicate is true, and when it’s false. Naming the first predicate p, and the second one r, we get the following type:

And we modify our mkFizzBuzz accordingly:

If you stare at the code long enough (or better yet, try to come up with your own), you’ll see that this is the only possible function for this type signature.

The reason is that you need:

• A pt and an rt to produce a FizzBuzz pt rt
• A pt and an rf to produce a Fizz pt rf
• And so on

And the only way to get those is from the results of the predicates¹. In a way, these new predicates carry “witnesses” of their truth/falsity, namely the values of type pt and pf, respectively.

We can now, finally, implement our desired version of fizzbuzz :: Int -> FizzBuzz in terms of our type-correct mkFizzBuzz:

Complete source for this version here.

Hopefully, this illustrates the value of using higher-order, general combinators such as mkFizzBuzz here, to implement our particular functions. Given their very general nature, it’s much easier to write “obviously correct” programs with them.

Examples of these types of combinators, with uses in everyday life, include maps, folds, filters, and many more.

Medium likes pretty, high-res images

References and further reading:

• [1] I’m using the word predicate a bit liberally here in the sense that these are functions of the form a -> Either b c rather than the more familiar a -> Bool.
• Waddler P., Theorems For Free!
• Milewski B., Parametricity: Money for Nothing and Theorems for Free
• Runnable source for final version