Generic Types are more Type Safe than Concrete Types

Insights from Advent of Code 2020 pt. 2

Posted on February 3, 2021

One interesting concept in type theory is the idea of “free theorems”. Sometimes we want to prove things about the programs we write, and the free theorems are the things we can prove about the program we write by just looking at its type, and not at any of the actual implementation. For example, if I write function :: a -> a, we are guaranteed that it returns exactly what was passed to it.

Of course, not all programming languages work this way. In Java, we could inspect the object’s class and call its constructor, or simply just return null always. Rust doesn’t quite have this property, even though you might assume it does based on the similarity of its type system to Haskell’s. For instance, let’s compare:

fn example<T>(x : T) -> u64 {
    ...
}

vs

example :: a -> Int
example = ...

In both of these cases, it might seem like we can be sure that the function always returns the same value. In Haskell, we simply can’t get any information out of an entirely generic type. But in Rust, T is not entirely generic. It has some information, specifically it knows how much memory it needs. All types implicitly implement the Sized trait. So the real equivalent in Rust is

fn example<T: ?Sized>(x : T) -> u64 {
    ...
}

which is actually parametric. (Until Rust adds another implicit trait that needs to be opted out of.)

However, it becomes clear rather quickly that parametricity doesn’t actually get us that much. For example, if I give you the function foo :: (a -> b) -> a -> b, then you can definitively know that the result (of type b) can only be constructed with the argument of type a and the argument of type a -> b. But if I give you the function foo :: [a] -> [a]… well, you know it gives you back a list. But it could be init, or tail, or reverse, or cycle . tail, or take only the even elements, or the Fibonacci elements, or any permutation, combinator, or subset of the elements of the input list.

So are the free theorems useless for real-world programming? Sort of. But that doesn’t mean that writing programs that are as parametric as possible isn’t a good thing.

In day 14 of Advent of Code, I wrote the following function:

import Data.Bits

maskBit2 :: Int -> (Int, Char) -> [Int]
maskBit2 x (i, 'X') = [setBit i x, clearBit i x]
maskBit2 x (_, '0') = [x]
maskBit2 x (i, '1') = [setBit i x]

This function takes a value, as well as a tuple containing an index and a character on which we branch. If the character is an X, we should return a list containing the value with that bit both set and unset. If the character is a '0', we should return a list containing the unchanged original value. If the character is an 'X', we return a list containing the value with that bit set. This code has a bug in it due to it being less parametric than it could be. Can you find it?

The order of the arguments to setBit and clearBit is wrong. In the above code, i is an index, so it has to be of type Int. x is the value we’re changing, and in the larger program, it is also of type Int. But this function doesn’t need to know that. It can be made more parametric by changing the type signature to

maskBit2 :: Bits a => a -> (Int, Char) -> [a]

If I do this for the original function, I now get a type error! setBit i x is not valid, because x is in the place where we need an index, an Int, but we don’t have an Int. x is only guaranteed to be something whose bits can be set and cleared.

I lost a decent chunk of time on this challenge debugging this issue, which I could have avoided by simply writing parametric code.