Hey, it’s Haskell Hwednesday! For those learning Haskell who are already educated in mathematics, or vice versa, the experience can be a bit of a rollercoaster.

We first discover the category of Haskell types and functions, predictably called Hask. This is a very nice sort of category: it has a terminal object (the unit type), products (pair tuple types) and exponentiation (function types), indeed a well-known sort of category known as Cartesian closed. For good measure, it also has sums (Either types) and an initial object (any empty type). Fabulous! A programming language with the beauty and rigour of mathematics.

Then we discover that almost none of this is true. Hask is indeed a category, but it does not have products or sums, and the unit type is not a terminal object, and there is no initial object. It turns out we actually had a different category in mind, a kind of IdealHask. In our IdealHask, typically, all functions terminate. In the actual Hask, every object is a Haskell type, and every Haskell type includes “bottom values” representing non-termination and other awkward conditions. (There’s actually a faithful functor from IdealHask to Hask that allows us to write our programs.)

Oh dear. These “extra” values have ruined everything. Dan Piponi was right, you shouldn’t have even asked.

But wait! As it happens, simple non-termination can be represented by topologies, which are awesome. We associate a topology with every type, and the definable functions are exactly the continuous ones. For example, the type Bool nominally has two values, True and False. We add non-termination as a third value bottom. The topology we define on this has these open sets: {{}, {True}, {False}, {True, False}, {True, False, bottom}}. The eleven definable functions are the nine strict ones (i.e., where f bottom = bottom):

and the two non-strict ones:

These are precisely the continuous functions from our topological space to itself. And it seems perhaps straightforward to generalise this to any type?

Yay topology! We have some of our mathematicalliness back! We think.

Ah, but Haskell types are more complicated than this. There are many different bottom values, that are included in every type. Non-termination is one, but there are also exceptions. Plus, there’s a function called mapException that can inspect exception values and arbitrarily map them to bottom values. Can we create a topology for each Haskell type such that the definable functions are exactly the continuous ones?

Sadly, we cannot. To show this, let us consider different models of Haskell’s unit type (), and what can happen when we attempt to evaluate a term of that type, which we’ll collectively refer to as possibilities. We’ll define the models as types in Haskell, specifying exactly which functions are definable. Then we’ll search exhaustively for topologies that match. You’ll need to install the countable package, which among other things includes an extensional “instance Eq (a -> b)“.

First some set theory:

And this is how we do topology:

Now we need to model Haskell types in Haskell:

The simplest model of the unit type has only one possibility, termination with the unit value, in a language where all functions terminate. We’ll call that model U1, and its sole possibility T1. The only possible function there can be maps T1 to T1, and it is definable:

Our second model, U2, adds a non-termination possibility N2 (termination with the unit value is T2). A function is definable if either

• it ignores its input and behaves the same whatever it is passed
• it examines its input and therefore doesn’t terminate when the input doesn’t terminate

Our third model, U3, adds an “exception” possibility. An exception is a termination, but still considered by Haskell to be “bottom”. The previous rule applies, but in addition, Haskell ensures that if a function examines its input, it must yield a bottom when passed a bottom. However, it’s allowed to map exception to a different bottom using mapException.

Now we want to search for topologies. Thanks to the countable package, we can do this exhaustively.

And that’s it. This is what we get when we run our program:

U1 has the one-point topology. U2 has the Sierpiński topologies. But there is no matching topology for U3.

So what about the actual Haskell unit type? Consider the equivalence relation R with three equivalence classes: the unit value, non-termination, and all exceptions, corresponding to the possibilities of U3. For each “definable” function U3 -> U3, we can define a Haskell function () -> () that corresponds to it under R. For “disallowed” functions, we cannot.

So if there were a topology X on the Haskell unit type such that the continuous functions were the definable ones, then X/R would be a quotient topology on U3 where the continuous functions were the definable ones. But this doesn’t exist, so that doesn’t either.