Securing invariants through Parametricity
Or how parametric types entail theorems for free
Here’s a particular solution to 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 anrt
to produce aFizzBuzz pt rt
- A
pt
and anrf
to produce aFizz 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
:
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.
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 familiara -> Bool
. - Waddler P., Theorems For Free!
- Milewski B., Parametricity: Money for Nothing and Theorems for Free
- Runnable source for final version