Why regular programming languages are fraught with error

#blog

I learned a cool thing you might appreciate about why pure functions and data types are way less error-prone. It's because there are way less ways to write a parametrically polymorphic function (ie the type of polymorphism in haskell, elm, etc, where there is implicitly a forall a for each type param a).

If you're coming from imperative languages like C#, this is how you'd write a similar function in Haskell (or another functional language)

// C#
int add(int a, int b) {
	return a + b;
}

-- Haskell
add :: Int -> Int -> Int
add a b = a + b

For example, consider functions of type (Bool -> a) -> Maybe a. How many can you write?

one _ = Nothing
two f = Just (f False)
three f = Just (f True)

These are the only three.

Lets suppose we were writing a more specific type than we had to. For example, if we were using a language that doesn't support parametric polymorphism but instead has adhoc polymorphism (ie interfaces with concrete types, like length in java or c++). How many functions are there of type (Bool -> Bool) -> Maybe Bool?

We can do high school math (generalised via category theory) to figure it out. When we write |a| (with straight brackets) we mean "how many values of type a are there". There are some rules:

• For simple data constructors like Just, we have |Just a| = |a|
• For sum (either) types, we have: |a + b| = |a| + |b|
  • We can write Maybe a = Nothing + Just a (using the + in place of the usual "or" for data constructors |).
• For function types, we have: |a -> b| = |b|^|a|
  • To see why, try to write all the functions of type Bool -> Bool.
    1. id t = t (False to False, True to True)
    2. not t = if t == False then True else False (False to True, True to False)
    3. const False (everything to False)
    4. const True (everything to True)
    • There are 4, and we get this by taking one possible output (Bool) for each input (Bool), giving us |Output| ^ |Input| = |Bool| ^ |Bool| = 2 ^ 2 = 4

So with both these rules we have:

|(Bool -> Bool) -> Maybe Bool|
= |Maybe Bool| ^ |Bool -> Bool|
= |Nothing + Just Bool| ^ (|Bool| ^ |Bool|)
= (1 + 2) ^ (2 ^ 2)
= 3 ^ 4 = 81

Wow, 81 possible implementations! Of course, we can still write the three above functions one, two, three, but what might some of these other implementations look like?

four :: (Bool -> Bool) -> Maybe Bool
four f =
	-- if f == id
	if f True == True and f False == False
	then Just True
	else Just False

five :: (Bool -> Bool) -> Maybe Bool
five f =
	-- if f == not
	if f True == False and f False == True
	then Just True
	else Just False

By using a more specific type (Bool -> Bool) -> Maybe Bool instead of a more generic type (Bool -> a) -> Maybe a, the compiler accepts 27 times more possible implementations (or another 81-3=78 ways fuck up our implementation). This demonstrates why making our types as abstract as possible can save us a lot of headache (and a lot of tests).

For simple functions this might be fine to manage with our own thinking, but the number of possible (and therefore incorrect) implementations gets exponentially worse for every additional parameter we add to the function.

For multi-parameter functions in any language (even impure ones), they are one-to-one with their curried equivalents. Any three-parameter function f :: (a,b,c) -> d is the same as f_curry :: a -> b -> c -> d. We can then use our generalised high-school math from above to calculate the number of implementations for f:

|f|
= |a -> b -> c -> d|
= |d| ^ |c| ^ |b| ^ |a|

So for each additional parameter, we add exponentially more possible implementations for our function! And that's assuming they're pure, because each side effect adds new degrees of potentially infinite complexity, which we can only constrain by limiting the complexity (ie possible modifications) of our side effects on our other data structures.

You might be asking: "but types are often infinitely big! How can we count infinitely big things?" Indeed, we often deal with (countably) infinite types like Int and String. But some infinities are bigger (easier to get lost in) than others; we can easily "conceive of" (aka count) all the integers 0, 1, -1, 2, -2, ..., where we would need one hand with infinitely many fingers. However, it's much harder to conceive of all the strings (we need infinitely many ... and consequently infinitely many hands):

Hand 1: ø (empty string), a, aa, aaa, ...
Hand 2: b, bb, bbb, ...
...
Hand (infinitely big): ab, aba, abaa, ...

All of this is to say: the math is not on our side if we use functions that are impure or more specific than they have to be. If we don't take care to write code that is as generic as possible, sooner or later we're going to write something with a logically erroneous implementation. It becomes not a matter of if but when.

Of course, learning how to write code that is as generic as possible might requires some abstract math education. I'm currently trying to figure out how useful it is to learn about monoids, functors and monads, which seem to be the software patterns of the universe. I've just finished part one of Category theory for programmers, and I'll let you know how it goes.