gistfile1.txt

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
import Test.QuickCheck
import Control.Monad

{-
This defines a "continuous space" I and a continuous function from I to itself.
You can interpret this space as a really low resolution continuous line segment

It consists of 5 "open subspaces":
T = [------------]  (the whole space)
L = [--------)
R =     (--------]
M =     (----)
B =                 (nothing)

These five spaces come with a partial ordering <=, representing containment
   T
L     R  '<=' is pointing up
   M
   B

And two "complete lattice" operations called join and meet, which are just the
unions and intersections any collection of subspaces. Also theres an infinite
distributivity law which doesn't matter here.

A mapping of subspaces from B -> A is a homomorphism if it
"preserves meets and joins". You say that the corresponding abstract map from
A -> B is continuous.

This space automatically generates a topological space complete with points
in the following way. 

Let S be a functor from the category of locales to the category of topological
spaces. S sends each "open" in I to a set of points in S(I). These points are
the prime filters of I, and point p is in S(x) if x is in p. If f is a
continuous function between locales A and B, S(f) : S(A) -> S(B) is the
(topospace) continuous function that sends points in S(A) to points in S(B)
using the rule S(f)(p) = (f*)^-1(p). Where f* is the corresponding frame
homomorphism from B -> A, and ^-1 is inverse image of a function.

"it is easy to verfy that U is a frame homomorphism A -> P(S(A)), whose image
is therefore a topology on S(A)"
-}

data I = T | L | R | M | B deriving (Eq, Show, Enum, Bounded)

instance Arbitrary I where
  arbitrary = arbitraryBoundedEnum

class Eq t => Locale t where
  comp :: t -> t -> Maybe Ordering
  u :: [t] -> t
  n :: [t] -> t

instance Locale I where
  comp = table
    [[eq,gt,gt,gt,gt]
    ,[lt,eq,oo,gt,gt]
    ,[lt,oo,eq,gt,gt]
    ,[lt,lt,lt,eq,gt]
    ,[lt,lt,lt,lt,eq]]
  u xs = foldr f B xs where
    f = table
      [[T,T,T,T,T]
      ,[T,L,T,L,L]
      ,[T,T,R,R,R]
      ,[T,L,R,M,M]
      ,[T,L,R,M,B]]
  n xs = foldr f T xs where
    f = table
      [[T,L,R,M,B]
      ,[L,L,M,M,B]
      ,[R,M,R,M,B]
      ,[M,M,M,M,B]
      ,[B,B,B,B,B]]

gt = Just GT
lt = Just LT
eq = Just EQ
oo = Nothing

lte :: Locale t => t -> t -> Maybe Bool
lte x y = case comp x y of
  Just LT -> Just True
  Just EQ -> Just True
  Just GT -> Just False
  Nothing -> Nothing

table :: (Locale t, Enum t) => [[a]] -> t -> t -> a
table tab i j = (tab !! (fromEnum i)) !! fromEnum j

-- this thing is a poset
posetRefl :: Locale t => t -> Bool
posetRefl x = lte x x == Just True

posetEq :: Locale t => t -> t -> Bool
posetEq x y = case liftM2 (&&) (lte x y) (lte y x) of
  Just True -> x == y
  _         -> True

posetTrans :: Locale t => t -> t -> t -> Bool
posetTrans x y z = case liftM2 (&&) (lte x y) (lte y z) of
  Just True -> lte x z == Just True
  _         -> True

-- this thing is a locale
distrib :: Locale t => t -> [t] -> Bool
distrib x ys = n [x, (u ys)] == u (map (\y -> n [x, y]) ys)

homU :: (Locale a, Locale b) => (a -> b) -> [a] -> Bool
homU f xs = f (u xs) == u (map f xs)

homN :: (Locale a, Locale b) => (a -> b) -> [a] -> Bool
homN f xs = f (n xs) == n (map f xs)

checkLocale :: forall t . Locale t => t -> IO ()
checkLocale _ = do
  quickCheck (posetRefl :: Locale t => I -> Bool)
  quickCheck (posetEq :: Locale t => I -> I -> Bool)
  quickCheck (posetTrans :: Locale t => I -> I -> I -> Bool)
  quickCheck (distrib :: Locale t => I -> [I] -> Bool)

primeFilter :: Locale t => [t] -> [t] -> Bool
primeFilter p xs = if u xs `elem` p
  then any (`elem` p) xs
  else True

-- here is a frame homomorphism from I to I (also, its an isomorphism)
f :: I -> I
f T = T
f L = R
f R = L
f M = M
f B = B

-- here is a discontinuous function from I to I
g :: I -> I
g T = T
g L = L
g R = L
g M = M
g B = B

-- all 3 points of S(I), the prime filters of I.
points :: [[I]]
points = 
  [[T,L]     -- a
  ,[T,R]     -- b
  ,[T,L,R,M] -- c
  ]

{-- so the topological space S(I) is like
points a b c
with these subsets, one for each open subspace
S : I -> Set
T -> {a b c}
L -> {a c}
R -> {b c}
M -> {c}
B -> {}
(p is in S(x) if x is in p)

Which means we can tell what S(f) would concretely do in S(I):
a -> b
b -> a
c -> c
(S(f)(p) corresponds to (f*)^-1(p), which is guaranteed to be one of the points
because f* is a frame hom.
--}

run = do
  checkLocale (undefined :: I)
  putStrLn "f homU" >> quickCheck (homU f)
  putStrLn "f homN" >> quickCheck (homN f)
  putStrLn "g NOT homU" >> quickCheck (expectFailure (homU g))
  putStrLn "g NOT homN" >> quickCheck (expectFailure (homU g))
  forM_ points $ \p -> do
    quickCheck (primeFilter p)