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 wellknown 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 nontermination 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 nontermination 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 nontermination 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
):

\x > if x then True else True \x > if x then True else False \x > if x then True else bottom \x > if x then False else True \x > if x then False else False \x > if x then False else bottom \x > if x then bottom else True \x > if x then bottom else False \x > if x then bottom else bottom 
and the two nonstrict 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. Nontermination 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)
“.

{# LANGUAGE ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances, OverlappingInstances #} module Main where import Control.Applicative (liftA,liftA2,liftA3) import Data.List (intercalate) import Data.Countable import Data.Searchable 
First some set theory:
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

implies :: Bool > Bool > Bool implies False _ = True implies True x = x type Set x = x > Bool  is it a member? empty :: Set x empty _ = False full :: Set x full _ = True union :: Set x > Set x > Set x union p q a = p a  q a intersection :: Set x > Set x > Set x intersection p q a = p a && q a instance (Finite x,Show x) => Show (Set x) where show s = "{" ++ (intercalate "," (fmap show (filter s allValues))) ++ "}" 
And this is how we do topology:
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45

 Given a function, find the preimage of a set. preimage :: (x > y) > Set y > Set x preimage f s a = s (f a) type Topology x = Set (Set x)  set of open sets isTopology :: (Countable x) => Topology x > Bool isTopology top = hasEmpty && hasFull && hasIntersections && hasUnions where hasEmpty = top empty hasFull = top full hasIntersections = forevery ((p,q) > (top p && top q) `implies` top (intersection p q)) hasUnions = forevery ((p,q) > (top p && top q) `implies` top (union p q))  Given topologies on x and y, find the set of continuous functions continuous :: (Countable y) => Topology x > Topology y > Set (x > y) continuous topx topy f = forevery (set > implies (topy set) (topx (preimage f set))) 
Now we need to model Haskell types in Haskell:

class (Finite x) => Model x where  definable functions in this model definable :: Set (x > x) 
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:
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70

 U1 models the unit type in a strict language  T1 represents the only possibility, termination with the unit value data U1 = T1 deriving (Eq, Show) instance Countable U1 where countPrevious = finiteCountPrevious countMaybeNext = finiteCountMaybeNext instance Searchable U1 where search = finiteSearch instance Finite U1 where allValues = [T1] assemble afb = liftA (t a > case a of T1 > t ) (afb T1) instance Model U1 where definable f = af (f T1) where af T1 = True  there is only one possible function, which is definable 
Our second model, U2, adds a nontermination 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
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96

 U2 represents the unit type in a lazy language with no exceptions besides nontermination  T2 is termination with the unit value,  N2 is nontermination data U2 = T2  N2 deriving (Eq, Show) instance Countable U2 where countPrevious = finiteCountPrevious countMaybeNext = finiteCountMaybeNext instance Searchable U2 where search = finiteSearch instance Finite U2 where allValues = [T2,N2] assemble afb = liftA2 (t n a > case a of T2 > t N2 > n ) (afb T2) (afb N2) instance Model U2 where definable f = af (f T2) (f N2) where af T2 T2 = True  f _ = always termination af N2 N2 = True  f _ = always nontermination af T2 N2 = True  f x = x af N2 T2 = False  "inversion", not definable 
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
.
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130

 U3 represents the unit type in a lazy language with an additional "exception" possibility  T3 is termination with the unit value,  E3 is termination with the exception  N3 is nontermination  (E3 and N3 are both "bottoms") data U3 = T3  E3  N3 deriving (Eq, Show) instance Countable U3 where countPrevious = finiteCountPrevious countMaybeNext = finiteCountMaybeNext instance Searchable U3 where search = finiteSearch instance Finite U3 where allValues = [T3,E3,N3] assemble afb = liftA3 (t e n a > case a of T3 > t E3 > e N3 > n ) (afb T3) (afb E3) (afb N3) instance Model U3 where definable f = af (f T3) (f E3) (f N3) where  functions that ignore the argument are definable af t e n  n == e && n == t = True  otherwise, the function must not terminate when passed nontermination: af _ _ T3 = False af _ _ E3 = False  more generally, the function must return a bottom when passed a bottom: af _ T3 _ = False  all other functions are definable af _ _ _ = True 
Now we want to search for topologies. Thanks to the countable package, we can do this exhaustively.
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150

 this topology matches if its continous functions are exactly the definable functions matching :: (Model x) => Topology x > Bool matching top = (continuous top top) == definable  all matching topologies goodtops :: (Model x) => [Topology x] goodtops = filter (top > matching top && isTopology top) allValues printOnLines :: (Show s) => [s] > IO () printOnLines = mapM_ (putStrLn . show) main :: IO () main = do putStrLn "Topologies for U1:" printOnLines (goodtops :: [Topology U1]) putStrLn "Topologies for U2:" printOnLines (goodtops :: [Topology U2]) putStrLn "Topologies for U3:" printOnLines (goodtops :: [Topology U3]) 
And that’s it. This is what we get when we run our program:

Topologies for U1: {{},{T1}} Topologies for U2: {{},{T2},{T2,N2}} {{},{N2},{T2,N2}} Topologies for U3: 
U1 has the onepoint 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, nontermination, 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.