Note: writing in Agda is *very slow*.

— Ashley Yakeley

4 Replies

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.