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

\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 non-strict ones:

\_ -> True
\_ -> False

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)“.

{-# 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:

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:

-- 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:

-- 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 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

-- U2 represents the unit type in a lazy language with no exceptions besides non-termination
-- T2 is termination with the unit value,
-- N2 is non-termination
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 non-termination
        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.

-- 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 non-termination
-- (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 non-termination:
        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.

-- 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 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.